Pete Olcott

2017-06-08 15:45:01 UTC

When you used a technique that had zero chance of

working, _listing the true sentences_ , you might as

well have admitted that you had no idea how MTT was

going to do these things you say.

I just have to complete more of my formal specificationworking, _listing the true sentences_ , you might as

well have admitted that you had no idea how MTT was

going to do these things you say.

so that you can directly see how MTT works.

would have been that you didn't know -- yet.

It's really more pleasant all around when you just say

that you don't know the things you don't know.

dishonest thing to say, because _it is not possible_

for you to adopt truths as axioms as a general rule

for incorporating truths into MTT. There are too many.

Of course that could not work. I am explicitly defining

the small set of the constituent parts from which all

truth is comprised.

tell us how MTT was going to get from that small set of

truths to the rest of the truths.

Making 7 > 3 an axiom was a dodge.

Instead of showing how MTT was going to get from the small

set of truths to his example, 7 > 3, you just put 7 > 3

in the set. As you say, _of course that could not work_ .

Nonetheless, that's what you did for 7 > 3.

----

I looked through what you've described below, and it

looks nicely capable. I'm looking especially at the control

structures that you plan to have.

However, that is beside the point if you can't formalize

your Big Claim: All sentences will be either provable

or refutable. How do you plan to implement that?

It is not (at least initially) as big as that. Initially it is simply (~Provable(X) & ~Refutable(X)) -> Incorrect(X).set of truths to his example, 7 > 3, you just put 7 > 3

in the set. As you say, _of course that could not work_ .

Nonetheless, that's what you did for 7 > 3.

----

I looked through what you've described below, and it

looks nicely capable. I'm looking especially at the control

structures that you plan to have.

However, that is beside the point if you can't formalize

your Big Claim: All sentences will be either provable

or refutable. How do you plan to implement that?

----

Suppose this is a theorem of your formal system

(Ey)( ~Prov(y) & sub(b,[z],b) = y ) <-> ~Prov(sub(b,[z],b))

I will have to put the concept (besides finite string rewrite rules specified by axioms) substitution on a back burner for now. I am still striving diligently to specify the YACC BNF syntax for MTT.Suppose this is a theorem of your formal system

(Ey)( ~Prov(y) & sub(b,[z],b) = y ) <-> ~Prov(sub(b,[z],b))

for b = 287411460918262346019384610938410936864016324\

47287740229742074027478734924802984y20984208479872749\

20847080249827474878092748787294874774872734872399472,

as it may well be a theorem.

Does your system check to see

whether 287411460918262346019384610938410936864016324\

47287740229742074027478734924802984y20984208479872749\

20847080249827474878092748787294874774872734872399472

represents

(Ey)( ~Prov(y) & sub(x,[z],x) = y )

or not? (x is a free variable, b is a constant. This

is close to but not exactly the LHS above.)

If MTT checks, where does it do that?

If MTT does not check, how else is this apparent

true-iff-not-provable sentence of MTT formally excluded?

Will the formal system implemented by your software

be consistent when you're finished? Just _claiming_

it will be consistent is not enough.

----

I see below that you've stripped the numbers off of Kurt

Goedel's proof again. How is it that you get to use numbers,

but he doesn't?

He is only using numbers to make the pretense that he is actually talking about arithmetic seem more credible.47287740229742074027478734924802984y20984208479872749\

20847080249827474878092748787294874774872734872399472,

as it may well be a theorem.

Does your system check to see

whether 287411460918262346019384610938410936864016324\

47287740229742074027478734924802984y20984208479872749\

20847080249827474878092748787294874774872734872399472

represents

(Ey)( ~Prov(y) & sub(x,[z],x) = y )

or not? (x is a free variable, b is a constant. This

is close to but not exactly the LHS above.)

If MTT checks, where does it do that?

If MTT does not check, how else is this apparent

true-iff-not-provable sentence of MTT formally excluded?

Will the formal system implemented by your software

be consistent when you're finished? Just _claiming_

it will be consistent is not enough.

----

I see below that you've stripped the numbers off of Kurt

Goedel's proof again. How is it that you get to use numbers,

but he doesn't?

When this extraneous (Fred Brooks, inessential) complexity is stripped away understanding what is really going on is enormously simpler.

----

It might interest you to know that there are much simpler

formal systems with true-iff-not-provable sentences.

A very simple one (the simplest I know of) has three

axioms in addition to the logical axioms.

1. There is an _empty set_ .

2. Two sets are _equal_ iff they have the same elements.

3. If x and y are sets, then there exists a set w, the

_adjunction_ of x and y, whose members are just y and

the members of x. ( w = (x U {y}) )

John Burgess calls that theory ST.

-- Burgess, John, 2005. Fixing Frege. Princeton Univ. Press.

Set theory has too much incoherence. I will probably use proper classes or something similar instead.It might interest you to know that there are much simpler

formal systems with true-iff-not-provable sentences.

A very simple one (the simplest I know of) has three

axioms in addition to the logical axioms.

1. There is an _empty set_ .

2. Two sets are _equal_ iff they have the same elements.

3. If x and y are sets, then there exists a set w, the

_adjunction_ of x and y, whose members are just y and

the members of x. ( w = (x U {y}) )

John Burgess calls that theory ST.

-- Burgess, John, 2005. Fixing Frege. Princeton Univ. Press.

<snip>

--

(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)

(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)