Uniting Forces: Email to Prof. Norman J. Wildberger on Politics, Ineptitude and Fraud

[Charlie-Boo]

[ http://www.youtube.com/watch?v=JpEd1Mmgggc ]

Dear Prof. Wildberger,

I have seen your videos and read some of your papers concerning
problems in the development of Mathematics, especially in Foundations.
I share your sentiment greatly. I have been trying for over 30 years
to point out similar problems with little success. You are the only
person I have ever known who shares my concerns and is in a position
of prominence in Mathematics.

I do not have a PhD nor am I part of academia. I made a perfect score
(800) on my Mathematics College Board test, was # 1 in numerous math
competitions throughout primary school, and have a BS in Mathematics
and Computer Science. I did write a well received book on advanced
techniques of computer programming and am in fact prominent in the M
programming language world. But I have discovered that people who are
neither professors nor work as a researcher for a wealthy corporation
have little chance of publishing in the academic world, in particular,
in journals on Logic and Computer Science, my specialties. Simply
looking through the table of contents shows that. I have tried a few
times and received only what I consider absurd responses from the
editors.

I studied pure Mathematics for 20 years, and then Theoretical Computer
Science for 30 years. I applied Mathematics to Computer Science
problems, and axiomatized several branches of Computer Science,
including Program Synthesis, Theory of Computation (aka
Computability), Recursion Theory and Incompleteness in Logic. I also
developed a general system for formalizing any branch of Computer
Science, and have implemented some of this with software, i.e. written
theorem provers. I plan to write a retail book on my decades of study
as time permits.

The problems that I see in the Mathematical Logic / Theoretical
Computer Science world include:

1. Politics: Only papers of established acamadicians are accepted for
publication. My researcher friends tell me the same is true in their
fields of study e.g. Biology. These papers never give so much as a
hint that anything published before them has any imperfections. This
is in stark contrast to programming languages which are constantly
being revised and improved, with ANSI being the controlling
organization which enforces democracy and transparency. There is no
ANSI for Mathematics.

2. Ineptitude, especially in the area of formalizing: Nothing has
really been formalized to the point of automating the creation of
theorems outside of simple Logic (Propositional Calculus.) ZFC is a
real joke and is of no use. Most unfortunately, when I point out this
lack of formalizing in internet forums, the universal response is “ZFC
can do it.”, but of course ZFC has never produced anything. In fact,
much effort has been spent by great Mathematicians such as Godel and
Cohen showing that ZFC is useless for (independent of) all of the
important questions in Set Theory.

3. Fraud: The conventional wisdom is that the “Curry-Howard Protocol”
aka “Proofs-as-Programs” shows us how to create computer programs
automatically i.e. Program Synthesis. However, it has never been
demonstrated to do that. One of the most ambitious claims that it has
is the text Adapting Proofs as Programs The Curry-Howard Protocol. It
gives 4 examples of programs and claims they were created this way,
but there is no explanation as to how they were created nor even a
description of the general method of constructing programs.

I spent almost 2 years addressing the problem of Program Synthesis. I
took a dozen simple, well-understood programs and most of that time
was spent representing them in different ways. Finally I represented
them as trees of loops and tests, and discovered that there are 8
rules for combining programs with known functionality into new
programs with known functionality. The role of proof in program
construction is this:

We express the assertion that program M satisfies specification P in
programming language Q. I write M # P / Q. The 8 rules map one or two
of these expressions to another expression. The axioms are known
programs. To construct a program we prove M # P / Q (using the 8
rules) where P and Q (the specification and programming language) are
given, and M is anything - it is the program constructed. The
specification P is a function to calculate or a set to enumerate or
decide.

Every formalization (which always ends up in the form of an axiomatic
system) began with a collection of theorems (results in general) that
are to be included. But no published claim or discussion of a
formalization mentions which theorems are meant to be included.

In hindsight, it is easy to show that producing a program
automatically from specifications is equivalent to proving that some
particular program meets the specifications.

It is interesting that Program = Proof is contrary to Theoretical
Computer Science which recognizes that theorems are programs that halt
YES (and a refutation is a program that halts NO) and a proof is the
iteration at which a program halts YES (or NO.) Systems of Logic
represent, and computer programs enumerate, just the recursively
enumerable sets.

One of the most absurd authors is Gregory Chaitin, who claims that
there is incompleteness because Mathematics is random. Godel’s
sentence G is said to be randomly true and thus cannot be proven. Of
course, Godel’s sentence can be proven using metamathematics, it just
can’t be proven in the PA-like formal system of Logic that Godel uses,
as Godel himself points out. After all, Godel theorem wouldn’t be a
theorem if Godel had not proven that G is true (and unprovable in PA.)

Chaitin also ignores stronger theorems such as Rosser’s 1936
extension, and even the stronger version that Godel himself gives in
the same article based on omega-consistency.

Chaitin claims that he read Godel’s 1931 article as a child and later
talked to Godel himself to explain his “improvement”, but Godel
mistakenly rejected it. However, Chaitin never addresses the stronger,
more complex proof also given by Godel. In fact, there are simple
mistakes in Chaitin’s writings and he once had to revamp it because a
simple examination showed that it proves that the “probability that a
random Turing Machine halts” is greater than 1. In fact, it is easy to
show there is no such probability at all as that number does not
converge in general as we consider all Turing Machines.

Chaitin and his followers explain (informally, of course) how Godel’s
Incompleteness Theorem (in Logic) = Turing’s proof of the
unsolvability of the Halting Problem (in Computer Science.) It would
be a great coincidence if the first theorems of Incompleteness in
Logic and the Theory of Computation were equivalent. Turing’s result
actually translates into “The set of undecidable sentences is not
representable.” and Godel’s result translates into “There is a program
that does not halt i.e. does not halt YES or NO.”

I would say “Famous theorems are not always equivalent.” Another
example is that ZFC formalizes all of Mathematics. But what about all
of the variations to ZFC that have been proposed? Either they are all
equivalent or ZFC, the first Axiomatization of Set Theory, happens to
be the one that = all of Mathematics.

This also ignores Godel’s First Incompleteness Theorem. There are
always true but unprovable sentences, and we can always add any one of
them as an axiom. We are just not allowed to add more than a finite
number of axioms. There is no fixed “all of Mathematics”.

In reality, the first theorem becomes the most famous theorem in that
field, and authors (such as Chaitin) like to talk about the most
famous theorems and even claim to have an improvement. But it is
meaningless to improve something that has already been improved by
being generalized.

Whenever I have spent the time to walk through a massively complex
paper claiming to formalize a famous result in Mathematics, I have
always discovered that it does not prove anything.

The fact that no NEW theorems are ever generated alone indicates that
there is no theorem-proving.

Many professors have web sites that claim to have “formalized” various
famous theorems, giving only an expression with no explanation and
nothing about actually proving it formally. I am reminded of
Einstein’s famous quote:

“The skeptic will say: ‘It may well be true that this system of
equations is reasonable from a logical standpoint. But this does not
prove that it corresponds to nature.’ You are right, dear skeptic.
Experience alone can decide on truth. … Pure logical thinking cannot
yield us any knowledge of the empirical world: all knowledge of
reality starts from experience and ends in it.”

One of my greatest goals in life is to expose the fraud and ineptitude
in research and publishing in Mathematical Logic and Theoretical
Computer Science. I wish you success in your similar pursuit. If there
is anything that I could possibly do to help, I certainly would.

Warmest regards,

[C-B]

http://www.cs.nyu.edu/pipermail/fom/2010-July/014890.html

[MoeBlee]

On Oct 19, 1:40 pm, Charlie-Boo <shymath...@gmail.com> wrote:
> If there
> is anything that I could possibly do to help, I certainly would.

Answer phones, sweep up, make coffee ... That sort of thing.

MoeBlee

[Frederick Williams]

Charlie-Boo wrote:
>
> [...] After all, Godel theorem wouldn’t be a

> theorem if Godel had not proven that G is true (and unprovable in PA.)

Not so, what G\"odel's theorem shows is that there is a G such that P
(G\"odel's name for his theory) does not prove G and also P does not
prove ~G. There is no need to establish that G is true.

--
Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.

[Charlie-Boo]

Gladly. On the occasions that I visited my friends Zohar Manna and
Richard Waldinger at SRI, all we did was to sit around and shoot the
breeze. Rich showed me his vast collection of family photos and Zo
was always that big jolly guy that he is.

C-B

[Charlie-Boo]

On Oct 19, 3:26 pm, Frederick Williams <freddywilli...@btinternet.com>
wrote:

same difference

(Actually, can you do that - not prove G is true first?)

C-B

[Frederick Williams]

Charlie-Boo wrote:
>
> On Oct 19, 3:26 pm, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
> > Charlie-Boo wrote:
> >
> > > [...] After all, Godel theorem wouldn t be a
> > > theorem if Godel had not proven that G is true (and unprovable in PA.)
> >
> > Not so, what G\"odel's theorem shows is that there is a G such that P
> > (G\"odel's name for his theory) does not prove G and also P does not
> > prove ~G. There is no need to establish that G is true.

> same difference
>
> (Actually, can you do that - not prove G is true first?)

The truth of G, or any other formula, needn't even be mentioned.

[Charlie-Boo]

On Oct 19, 4:29 pm, Frederick Williams <freddywilli...@btinternet.com>

wrote:
> Charlie-Boo wrote:
>
> > On Oct 19, 3:26 pm, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:
> > > Charlie-Boo wrote:
>
> > > > [...] After all, Godel theorem wouldn t be a
> > > > theorem if Godel had not proven that G is true (and unprovable in PA.)
>
> > > Not so, what G\"odel's theorem shows is that there is a G such that P
> > > (G\"odel's name for his theory) does not prove G and also P does not
> > > prove ~G.  There is no need to establish that G is true.
> > same difference
>
> > (Actually, can you do that - not prove G is true first?)
>
> The truth of G, or any other formula, needn't even be mentioned.

Although he does:

"From the remark that [R(q); q] asserts its own unprovability, it
follows at once that
[R(q); q] is correct, since [R(q); q] is certainly unprovable (because
undecidable). So the
proposition which is undecidable in the system PM yet turns out to be
decided by
metamathematical considerations."

http://jacqkrol.x10.mx/assets/articles/godel-1931.pdf

C-B

[Charlie-Boo]

On Oct 19, 4:29 pm, Frederick Williams <freddywilli...@btinternet.com>

wrote:
> Charlie-Boo wrote:
>
> > On Oct 19, 3:26 pm, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:
> > > Charlie-Boo wrote:
>
> > > > [...] After all, Godel theorem wouldn t be a
> > > > theorem if Godel had not proven that G is true (and unprovable in PA.)
>
> > > Not so, what G\"odel's theorem shows is that there is a G such that P
> > > (G\"odel's name for his theory) does not prove G and also P does not
> > > prove ~G.  There is no need to establish that G is true.

Here's what we're talking about:

Godel proves two theorems at that point (in this order):

1. There is a sentence S such that ~ |- S and ~ |- ~S.
2. There is a sentence S such that S and ~ |- S

You are saying "What Godel shows is (1)." I am saying "What Godel
shows is (2)."

We're both right! (And they're equivalent.) I just read more of the
article.

This is like the politician who recently referred to "legitiamate
rape" and his political opponents jumped all over it, saying there is
only one kind of rape (without saying what kind that is.)

He meant (and should have said) "legitimate accusaction of rape".

Such shifting of semantics is common in the Obama administration. He
himself recently referred to "a couple of agents" being involved in
the secret service agents' prostitution parties. At least 4 quit /
were fired. "couple" really means 2, but is commonly misused to mean
"a few". By the actual meaning of the word, Obama lied. By the
common meaning of the word, he can claim he told the truth.

C-B

[Nam Nguyen]

On 19/10/2012 1:26 PM, Frederick Williams wrote:
> Charlie-Boo wrote:
>>
>> [...] After all, Godel theorem wouldn’t be a
>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>
> Not so, what G\"odel's theorem shows is that there is a G such that P
> (G\"odel's name for his theory) does not prove G and also P does not
> prove ~G.

But how could Godel have possibly known that P be consistent?

> There is no need to establish that G is true.

Of course there is.

--
----------------------------------------------------
There is no remainder in the mathematics of infinity.

NYOGEN SENZAKI
----------------------------------------------------

[Rupert]

On Oct 20, 5:54 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>
> > Charlie-Boo wrote:
>
> >> [...] After all, Godel theorem wouldn t be a
> >> theorem if Godel had not proven that G is true (and unprovable in PA.)
>
> > Not so, what G\"odel's theorem shows is that there is a G such that P
> > (G\"odel's name for his theory) does not prove G and also P does not
> > prove ~G.
>
> But how could Godel have possibly known that P be consistent?
>

What he did was establish the result that P is incomplete on the
assumption that it is omega-consistent.

> > There is no need to establish that G is true.
>
> Of course there is.
>

Why?

[Frederick Williams]

Nam Nguyen wrote:
>
> On 19/10/2012 1:26 PM, Frederick Williams wrote:
> > Charlie-Boo wrote:
> >>
> >> [...] After all, Godel theorem wouldn�t be a
> >> theorem if Godel had not proven that G is true (and unprovable in PA.)
> >
> > Not so, what G\"odel's theorem shows is that there is a G such that P
> > (G\"odel's name for his theory) does not prove G and also P does not
> > prove ~G.
>
> But how could Godel have possibly known that P be consistent?

He assumed it to be omega consistent.

> > There is no need to establish that G is true.
>
> Of course there is.

--

[Colin]

On Oct 19, 1:40 pm, Charlie-Boo <shymath...@gmail.com> wrote:

> [http://www.youtube.com/watch?v=JpEd1Mmgggc]

Wow Charlie. After looking back over your previous posts and clicking
on some your links, etc., you still seem to be devoted to the false
idea that the set of true sentences in arithmetic (i.e., the set of
sentences satisfied by the standard model of arithmetic, i.e., the
natural numbers) is actually definable in arithmetic and, indeed, it's
a recursively enumerable set, Well, it's not: not only is the set of
true sentences not recusively enumerable, it's not even definable in
arithmetic (by which I mean not first-order definable). Haven't you
ever heard of Tarski's Theorem before?.

[Nam Nguyen]

On 20/10/2012 8:15 AM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>>> Charlie-Boo wrote:
>>>>

>>>> [...] After all, Godel theorem wouldnÂ’t be a

>>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>>>
>>> Not so, what G\"odel's theorem shows is that there is a G such that P
>>> (G\"odel's name for his theory) does not prove G and also P does not
>>> prove ~G.
>>
>> But how could Godel have possibly known that P be consistent?
>
> He assumed it to be omega consistent.

OK.

>
>>> There is no need to establish that G is true.
>>
>> Of course there is.

And G isn't true in one of the models of P, given the assumption
that P is (omega ) consistent above?

[Nam Nguyen]

On 20/10/2012 3:26 AM, Rupert wrote:
> On Oct 20, 5:54 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>>
>>> Charlie-Boo wrote:
>>
>>>> [...] After all, Godel theorem wouldn t be a
>>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>>
>>> Not so, what G\"odel's theorem shows is that there is a G such that P
>>> (G\"odel's name for his theory) does not prove G and also P does not
>>> prove ~G.
>>
>> But how could Godel have possibly known that P be consistent?
>>
>
> What he did was establish the result that P is incomplete on the
> assumption that it is omega-consistent.

OK.

>>> There is no need to establish that G is true.
>>
>> Of course there is.
>>
> Why?

And the assumed omega consistency of P would have nothing to do with
the natural numbers where G would be true?

[Frederick Williams]

Nam Nguyen wrote:
>
> On 20/10/2012 8:15 AM, Frederick Williams wrote:
> > Nam Nguyen wrote:
> >>
> >> On 19/10/2012 1:26 PM, Frederick Williams wrote:
> >>> Charlie-Boo wrote:
> >>>>
> >>>> [...] After all, Godel theorem wouldnÂ’t be a
> >>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
> >>>
> >>> Not so, what G\"odel's theorem shows is that there is a G such that P
> >>> (G\"odel's name for his theory) does not prove G and also P does not
> >>> prove ~G.
> >>
> >> But how could Godel have possibly known that P be consistent?
> >
> > He assumed it to be omega consistent.
>
> OK.
>
> >
> >>> There is no need to establish that G is true.
> >>
> >> Of course there is.
>
> And G isn't true in one of the models of P, given the assumption
> that P is (omega ) consistent above?

I didn't say that G wasn't true in a model, I said that there is no need
to establish that G is true. I'll expand on that:

To say of a theory T that it is incomplete means that there is a closed
formula phi such that neither T |- phi nor T |- ~phi. Truth isn't
mentioned in the result and it need not be mentioned in the proof. To
be sure, someone who proves of some particular T that there is a closed
formula phi such that neither T |- phi nor T |- ~phi, may, in the same
publication, say that phi (let's say) is true in the intended model of
T. My original reply was about G\"odel's theorem, not what else G\"odel
said in the paper where he first proved that theorem.

[Nam Nguyen]

On 20/10/2012 9:28 AM, Nam Nguyen wrote:
> On 20/10/2012 3:26 AM, Rupert wrote:
>> On Oct 20, 5:54 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>>>
>>>> Charlie-Boo wrote:
>>>
>>>>> [...] After all, Godel theorem wouldn t be a
>>>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>>>
>>>> Not so, what G\"odel's theorem shows is that there is a G such that P
>>>> (G\"odel's name for his theory) does not prove G and also P does not
>>>> prove ~G.
>>>
>>> But how could Godel have possibly known that P be consistent?
>>>
>>
>> What he did was establish the result that P is incomplete on the
>> assumption that it is omega-consistent.
>
> OK.
>
>>>> There is no need to establish that G is true.
>>>
>>> Of course there is.
>>>
>> Why?
>
> And the assumed omega consistency of P would have nothing to do with
> the natural numbers where G would be true?

I meant, by what Frederick said above, there seems to by a symmetry
between G, ~G, w.r.t. to P's incompleteness (or PA's; note his "and
unprovable in PA"), in the sense the syntactical incompleteness would
yield no information about the truths of G and ~G. So, would that mean
G could be _false_ in the naturals?

[Frederick Williams]

Nam Nguyen wrote:

>
> And the assumed omega consistency of P would have nothing to do with
> the natural numbers where G would be true?

Omega consistency has a purely syntactic matter and it makes no
reference to G.

[Nam Nguyen]

On 20/10/2012 9:44 AM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> On 20/10/2012 8:15 AM, Frederick Williams wrote:
>>> Nam Nguyen wrote:
>>>>
>>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>>>>> Charlie-Boo wrote:
>>>>>>

>>>>>> [...] After all, Godel theorem wouldn’t be a

>>>>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>>>>>
>>>>> Not so, what G\"odel's theorem shows is that there is a G such that P
>>>>> (G\"odel's name for his theory) does not prove G and also P does not
>>>>> prove ~G.
>>>>
>>>> But how could Godel have possibly known that P be consistent?
>>>
>>> He assumed it to be omega consistent.
>>
>> OK.
>>
>>>
>>>>> There is no need to establish that G is true.
>>>>
>>>> Of course there is.
>>
>> And G isn't true in one of the models of P, given the assumption
>> that P is (omega ) consistent above?
>
> I didn't say that G wasn't true in a model, I said that there is no need
> to establish that G is true. I'll expand on that:
>
> To say of a theory T that it is incomplete means that there is a closed
> formula phi such that neither T |- phi nor T |- ~phi.

Right. That's the _definition_ of T being incomplete. _NOT_ a proof.

> Truth isn't
> mentioned in the result and it need not be mentioned in the proof.

You seemed to be confused. What you had right above is just a definition
in which the word "result" is _not_ applicable.

> To
> be sure, someone who proves of some particular T that there is a closed
> formula phi such that neither T |- phi nor T |- ~phi, may, in the same
> publication, say that phi (let's say) is true in the intended model of
> T. My original reply was about G\"odel's theorem, not what else G\"odel
> said in the paper where he first proved that theorem.

So, could G be false then?

[Nam Nguyen]

On 20/10/2012 9:48 AM, Frederick Williams wrote:
> Nam Nguyen wrote:
>
>>
>> And the assumed omega consistency of P would have nothing to do with
>> the natural numbers where G would be true?
>
> Omega consistency has a purely syntactic matter and it makes no
> reference to G.

So, how many non-logical symbols would you need to have to express the
"purely syntactic matter" Omega consistency?

[Rupert]

On Oct 20, 5:28 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 20/10/2012 3:26 AM, Rupert wrote:
>
>
>
>
>
>
>
>
>
> > On Oct 20, 5:54 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>
> >>> Charlie-Boo wrote:
>
> >>>> [...] After all, Godel theorem wouldn t be a
> >>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>
> >>> Not so, what G\"odel's theorem shows is that there is a G such that P
> >>> (G\"odel's name for his theory) does not prove G and also P does not
> >>> prove ~G.
>
> >> But how could Godel have possibly known that P be consistent?
>
> > What he did was establish the result that P is incomplete on the
> > assumption that it is omega-consistent.
>
> OK.
>
> >>> There is no need to establish that G is true.
>
> >> Of course there is.
>
> > Why?
>
> And the assumed omega consistency of P would have nothing to do with
> the natural numbers where G would be true?
>

Why would you think that?

It can be shown that if P is consistent, then G is true. In fact it
can be proved in a very weak theory, such as EFA, that P is consistent
if and only if G is true.

[Rupert]

Only if P were inconsistent.

[Rupert]

On Oct 20, 6:00 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 20/10/2012 9:48 AM, Frederick Williams wrote:
>
> > Nam Nguyen wrote:
>
> >> And the assumed omega consistency of P would have nothing to do with
> >> the natural numbers where G would be true?
>
> > Omega consistency has a purely syntactic matter and it makes no
> > reference to G.
>
> So, how many non-logical symbols would you need to have to express the
> "purely syntactic matter" Omega consistency?
>

You can express the proposition in the first-order langauge of
arithmetic.

[Rupert]

On Oct 20, 5:56 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 20/10/2012 9:44 AM, Frederick Williams wrote:
>
>
>
>
>
>
>
>
>
> > Nam Nguyen wrote:
>
> >> On 20/10/2012 8:15 AM, Frederick Williams wrote:
> >>> Nam Nguyen wrote:
>
> >>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
> >>>>> Charlie-Boo wrote:
>

> >>>>>> [...] After all, Godel theorem wouldnÂ’t be a

G is equivalent in EFA to the assertion that P is consistent.

[George Greene]

On Oct 19, 3:26 pm, Frederick Williams <freddywilli...@btinternet.com>
wrote:

> Not so, what G\"odel's theorem shows is that there is a G such that P
> (G\"odel's name for his theory) does not prove G and also P does not
> prove ~G.  There is no need to establish that G is true.

G *is* true IN THE STANDARD model.
That IS IMPORTANT (AND "established").

[George Greene]

On Oct 20, 1:22 pm, Rupert <rupertmccal...@yahoo.com> wrote:
> It can be shown that if P is consistent, then G is true. In fact it
> can be proved in a very weak theory, such as EFA, that P is consistent
> if and only if G is true.

Well, sure, but that still leaves the question, is P (PA?) consistent?

[Rupert]

Yes, indeed.

[Charlie-Boo]

Including the link above?

> you still seem to be devoted to the false
> idea that the set of true sentences in arithmetic (i.e., the set of
> sentences satisfied by the standard model of arithmetic, i.e., the
> natural numbers) is actually definable in arithmetic and, indeed, it's
> a recursively enumerable set,

Where did I say that and what did I say?

C-B

[Charlie-Boo]

On Oct 20, 10:20 am, Colin <colinpoa...@hotmail.com> wrote:

Including the link above?

> you still seem to be devoted to the false
> idea that the set of true sentences in arithmetic (i.e., the set of
> sentences satisfied by the standard model of arithmetic, i.e., the
> natural numbers) is actually definable in arithmetic and, indeed, it's
> a recursively enumerable set,

Where did I say (or imply) that and what did I say?

C-B

[Nam Nguyen]

Let's be precise in the debate here.

Here's the conversation between Charlie and Frederick (above):

Charlie wrote:

> [...] After all, Godel theorem wouldn t be a theorem if Godel
> had not proven that G is true (and unprovable in PA.)

to which Frederick responded:

> Not so, what G\"odel's theorem shows is that there is a G such that P
> (G\"odel's name for his theory) does not prove G and also P does not
> prove ~G.

> [...]

> There is no need to establish that G is true.

What I'd like to emphasize (for clarity purposes) is that there are
_two_ formal theories involved:

- _P_ as the _proving theory_

- _PA_ as a _targeted theory_ whose G being true and being undecidable
are are what is being debated.

Here, without loss of generality, "PA" is synonymous with "T", a
formal system with:

(a) _an assumed consistency_
(b) _an assumption that one of its model is the natural numbers_ ;
(in English one could say we _assume_ T is strong enough to
carry out the concept of arithmetic of the natural numbers).

The point of my protesting Frederick's "There is no need to establish
that G is true" is twofold:

(1) Godel's proof stipulates (b) as a requirement; and given (a) is
also a requirement and that G(T) is logically equivalent to
CONT(T) (which would be interpreted by virtually everyone as
the consistency of T which is assumed to be true) then it's not
a coincidence that G(T) must be true in Godel's proof and that
(as George has alluded to) Godel's proof as we know can not be
established as a true meta theorem if G(T) isn't true.

So, Frederick was incorrect in saying "There is no need to establish
that G is true": there's a need, due to both requirements (a) and
(b).

(2) P is a proving system, using syntactical proofs, proving G(T) to be
undecidable (hence ~G(T) to be also undecidable).

But how do we know that P itself is consistent, without assuming
that it has the natural numbers [in which G(T) is assumed to be
true]?

Relative to what Frederick said above with 2 systems P and T=PA,
your explanation is a little off-track or circular: your EFA is really
his P and your P is really just his T (or PA as an example).

So, no: you haven't successfully defended his "There is no need to
establish that G is true", in proving in _the proving theory P_
that G(T) is undecidable in the _targeted theory_ T.

[Nam Nguyen]

Sure. For instance, by the formula Ax[(x >= 0)], you could express
the idea that " _All individual (numbers)_ are greater or equal
to zero. ".

But how would you express - in one formula written in L(PA) -
the idea " _All numerals_ are greater or equal to zero. "?

[Nam Nguyen]

On 20/10/2012 5:25 PM, Nam Nguyen wrote:
> On 20/10/2012 11:23 AM, Rupert wrote:
>> On Oct 20, 6:00 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>>> On 20/10/2012 9:48 AM, Frederick Williams wrote:
>>>
>>>> Nam Nguyen wrote:
>>>
>>>>> And the assumed omega consistency of P would have nothing to do with
>>>>> the natural numbers where G would be true?
>>>
>>>> Omega consistency has a purely syntactic matter and it makes no
>>>> reference to G.
>>>
>>> So, how many non-logical symbols would you need to have to express the
>>> "purely syntactic matter" Omega consistency?
>>>
>>
>> You can express the proposition in the first-order langauge of
>> arithmetic.
>
> Sure. For instance, by the formula Ax[(x >= 0)], you could express
> the idea that " _All individual (numbers)_ are greater or equal
> to zero. ".
>
> But how would you express - in one formula written in L(PA) -
> the idea " _All numerals_ are greater or equal to zero. "?

And "All numerals" would have to be expressed somehow to express
"Omega (in)consistency" of course.

[Nam Nguyen]

What did you mean by "Yes, indeed"?

The question of PA's consistency is still an open question?
Or, Yes in deed PA is consistent?

Assuming you meant the latter ....

So, in _what consistent theory_ T' would you prove PA is consistent?

And how would you _prove_ T' is consistent in the first place?

[Rupert]

On Oct 21, 1:28 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 20/10/2012 5:25 PM, Nam Nguyen wrote:
>
>
>
>
>
>
>
>
>
> > On 20/10/2012 11:23 AM, Rupert wrote:
> >> On Oct 20, 6:00 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >>> On 20/10/2012 9:48 AM, Frederick Williams wrote:
>
> >>>> Nam Nguyen wrote:
>
> >>>>> And the assumed omega consistency of P would have nothing to do with
> >>>>> the natural numbers where G would be true?
>
> >>>> Omega consistency has a purely syntactic matter and it makes no
> >>>> reference to G.
>
> >>> So, how many non-logical symbols would you need to have to express the
> >>> "purely syntactic matter" Omega consistency?
>
> >> You can express the proposition in the first-order langauge of
> >> arithmetic.
>
> > Sure. For instance, by the formula Ax[(x >= 0)], you could express
> > the idea that " _All individual (numbers)_ are greater or equal
> > to zero. ".
>
> > But how would you express - in one formula written in L(PA) -
> > the idea " _All numerals_ are greater or equal to zero. "?
>
> And "All numerals" would have to be expressed somehow to express
> "Omega (in)consistency" of course.
>

What you do is you make an assertion about the Gödel numbers of
numerals, and this stands as a surrogate for the assertion about the
numerals themselves.

[Rupert]

On Oct 21, 5:38 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 20/10/2012 12:17 PM, Rupert wrote:
>
> > On Oct 20, 8:04 pm, George Greene <gree...@email.unc.edu> wrote:
> >> On Oct 20, 1:22 pm, Rupert <rupertmccal...@yahoo.com> wrote:
>
> >>> It can be shown that if P is consistent, then G is true. In fact it
> >>> can be proved in a very weak theory, such as EFA, that P is consistent
> >>> if and only if G is true.
>
> >> Well, sure, but that still leaves the question, is P (PA?) consistent?
>
> > Yes, indeed.
>
> What did you mean by "Yes, indeed"?
>
> The question of PA's consistency is still an open question?
> Or, Yes in deed PA is consistent?
>

What I meant was: George is saying that you would need to know whether
PA is consistent in order to know whether or not G is true. I fully
agree on this point, hence my remark "Yes, indeed". I did not make any
comment about whether PA is consistent or whether its consistency is
an open question.

> Assuming you meant the latter ....
>
> So, in _what consistent theory_ T' would you prove PA is consistent?
>

You could do a model-theoretic proof in ATR_0, for example, and there
is also Gentzen's proof, which can be formalized in PRA together with
transfinite induction up to the ordinal epsilon-null.

> And how would you _prove_ T' is consistent in the first place?
>

I do not claim to be able to prove that these theories are consistent
in any interesting sense. I can, of course, prove their consistency in
theories which are stronger, but I make no claim that this fact should
have any epistemological force.

It's coherent to regard the consistency of PA as an open question.

You've said in the past that you regard the consistency of Q as an
open question. I think it is hard to make this coherent with your
other commitments.

[Rupert]

No, it doesn't. In his 1931 paper he assumed that the object theory T
is omega-consistent. He doesn't need to assume that the natural
numbers is one of the models of T.

> and given (a) is
>      also a requirement and that G(T) is logically equivalent to
>      CONT(T) (which would be interpreted by virtually everyone as
>      the consistency of T which is assumed to be true) then it's not
>      a coincidence that G(T) must be true in Godel's proof and that
>      (as George has alluded to) Godel's proof as we know can not be
>      established as a true meta theorem if G(T) isn't true.
>

If you had an object theory T for which the Gödel sentence wasn't
true, that that theory would be inconsistent. So the hypothesis of
omega-consistency would fail and the theorem would be true for this
object theory T vacuously.

The point, however, is that Gödel didn't set himself the task of
proving that the Gödel sentence was true. He could have done so on the
assumption that the object theory in question was consistent. But that
wasn't his goal; his goal was just to show that if the object theory
was omega-consistent then it would have to be incomplete. He succeeded
in doing this.

>     So, Frederick was incorrect in saying "There is no need to establish
>     that G is true": there's a need, due to both requirements (a) and
>     (b).
>

No, Frederick's remark was not incorrect.

> (2) P is a proving system, using syntactical proofs, proving G(T) to be
>      undecidable (hence ~G(T) to be also undecidable).
>
>      But how do we know that P itself is consistent, without assuming
>      that it has the natural numbers [in which G(T) is assumed to be
>      true]?
>

I don't really know exactly what you're referring to when you talk
about the assumption that P "has the natural numbers".

Also, you seem to be under the impression that P is the metatheory and
PA is the object theory. It would be possible to do things this way,
but actually in Gödel's 1931 paper P was the object theory.

> Relative to what Frederick said above with 2 systems P and T=PA,
> your explanation is a little off-track or circular: your EFA is really
> his P and your P is really just his T (or PA as an example).
>

I don't see what's "off-track" or "circular" about my remark. I
correctly observed that it can be proved in EFA that G (the Gödel
sentence for P) is equivalent to the assertion that P is consistent. I
could have made a different observation instead: namely, that it can
be proved in P that G (the Gödel sentence for PA) is equivalent to the
assertion that PA is consistent. Furthermore P can also prove the
consistency of PA, so that the Gödel sentence for PA can be proved to
be true in P. I don't really see what you're getting with all of this.

> So, no: you haven't successfully defended his "There is no need to
> establish that G is true", in proving in _the proving theory P_
> that G(T) is undecidable in  the _targeted theory_ T.
>

The goal is to prove (in whatever metatheory you wish to work with)
that if the object theory T is omega-consistent then the Gödel
sentence for T, G, is independent of T. That's the goal. If you happen
to end up proving along the way that also G is true, then that's fine,
but there's no need to do so. What you need to do is show that if T is
omega-consistent, then G is independent of T. Gödel succeeded in doing
this, so everything is fine.

[Rupert]

> as Godel himself points out. After all, Godel theorem wouldn’t be a

> theorem if Godel had not proven that G is true (and unprovable in PA.)
>

Professor Norman Wildberger teaches at my alma mater. I took a
combinatorics course of his once. He's a nice man.

[Frederick Williams]

I'll just remark that 'P' is G\"odel's name for his mash up (to use
young people's language) of PA and PM. He assumed the axioms of PA just
to save the bother of proving them as PM theorems and especially since,
as he remarks, in place of PM he could just as well have used ZF. It
was I who introduced 'P' into this thread and I hope I caused no
confusion.

[Frederick Williams]

Nam Nguyen wrote:
>
> On 20/10/2012 9:44 AM, Frederick Williams wrote:
> > Nam Nguyen wrote:
> >>
> >> On 20/10/2012 8:15 AM, Frederick Williams wrote:
> >>> Nam Nguyen wrote:
> >>>>
> >>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
> >>>>> Charlie-Boo wrote:
> >>>>>>

> >>>>>> [...] After all, Godel theorem wouldnÂ’t be a

> >>>>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
> >>>>>
> >>>>> Not so, what G\"odel's theorem shows is that there is a G such that P
> >>>>> (G\"odel's name for his theory) does not prove G and also P does not
> >>>>> prove ~G.
> >>>>
> >>>> But how could Godel have possibly known that P be consistent?
> >>>
> >>> He assumed it to be omega consistent.
> >>
> >> OK.
> >>
> >>>
> >>>>> There is no need to establish that G is true.
> >>>>
> >>>> Of course there is.
> >>
> >> And G isn't true in one of the models of P, given the assumption
> >> that P is (omega ) consistent above?
> >
> > I didn't say that G wasn't true in a model, I said that there is no need
> > to establish that G is true. I'll expand on that:
> >
> > To say of a theory T that it is incomplete means that there is a closed
> > formula phi such that neither T |- phi nor T |- ~phi.
>
> Right. That's the _definition_ of T being incomplete. _NOT_ a proof.
>
> > Truth isn't
> > mentioned in the result and it need not be mentioned in the proof.
>
> You seemed to be confused. What you had right above is just a definition
> in which the word "result" is _not_ applicable.

The result that P is incomplete as proved by G\"odel makes no reference
to truth. In (the English translation of) the paper were G\"odel proves
that result, the word 'true' is used. So what?

> > To
> > be sure, someone who proves of some particular T that there is a closed
> > formula phi such that neither T |- phi nor T |- ~phi, may, in the same
> > publication, say that phi (let's say) is true in the intended model of
> > T. My original reply was about G\"odel's theorem, not what else G\"odel
> > said in the paper where he first proved that theorem.
>
> So, could G be false then?

If P is inconsistent.

[Frederick Williams]

Rupert wrote:
>
> On Oct 19, 8:40 pm, Charlie-Boo <shymath...@gmail.com> wrote:
> > [http://www.youtube.com/watch?v=JpEd1Mmgggc]
> >
> > Dear Prof. Wildberger,
> >

> > I have seen your videos and read some of your papers [...]

>
> Professor Norman Wildberger teaches at my alma mater. I took a
> combinatorics course of his once. He's a nice man.

Perhaps he did some terrible wrong in a previous life and is now being
punished for it?

[Nam Nguyen]

On 21/10/2012 6:56 AM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> On 20/10/2012 9:44 AM, Frederick Williams wrote:
>>> Nam Nguyen wrote:
>>>>
>>>> On 20/10/2012 8:15 AM, Frederick Williams wrote:
>>>>> Nam Nguyen wrote:
>>>>>>
>>>>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>>>>>>> Charlie-Boo wrote:
>>>>>>>>

>>>>>>>> [...] After all, Godel theorem wouldn’t be a

>>>>>>>> theorem if Godel had not proven that G is true (and unprovable in PA.)
>>>>>>>
>>>>>>> Not so, what G\"odel's theorem shows is that there is a G such that P
>>>>>>> (G\"odel's name for his theory) does not prove G and also P does not
>>>>>>> prove ~G.
>>>>>>
>>>>>> But how could Godel have possibly known that P be consistent?
>>>>>
>>>>> He assumed it to be omega consistent.
>>>>
>>>> OK.
>>>>
>>>>>
>>>>>>> There is no need to establish that G is true.
>>>>>>
>>>>>> Of course there is.
>>>>
>>>> And G isn't true in one of the models of P, given the assumption
>>>> that P is (omega ) consistent above?
>>>
>>> I didn't say that G wasn't true in a model, I said that there is no need
>>> to establish that G is true. I'll expand on that:
>>>
>>> To say of a theory T that it is incomplete means that there is a closed
>>> formula phi such that neither T |- phi nor T |- ~phi.
>>
>> Right. That's the _definition_ of T being incomplete. _NOT_ a proof.
>>
>>> Truth isn't
>>> mentioned in the result and it need not be mentioned in the proof.
>>
>> You seemed to be confused. What you had right above is just a definition
>> in which the word "result" is _not_ applicable.
>
> The result that P is incomplete as proved by G\"odel makes no reference
> to truth. In (the English translation of) the paper were G\"odel proves
> that result, the word 'true' is used.

This is what Godel himself said (unless they translated incorrectly):

"This situation is not due in some way to the special nature of
the systems set up, but holds for a very extensive class of
formal systems, including, in particular, all those arising
from the addition of a finite number of axioms to the two systems
mentioned,[5] provided that thereby no false propositions of
the kind described in footnote 4 become provable."

[Where footnote 4 id where he stipulates the naturals as
what his "false propositions" would be about.]

Note his "thereby no _false_ propositions". (Emphasis is mine).

Sure, there he didn't the word "true" but we know false = not true,
naturally.

> So what?

So you're wrong in saying that arithmetic truths about the naturals
(G being true for instance) weren't used, stipulated, by Godel in his
Incompleteness Theorem.

>>> To
>>> be sure, someone who proves of some particular T that there is a closed
>>> formula phi such that neither T |- phi nor T |- ~phi, may, in the same
>>> publication, say that phi (let's say) is true in the intended model of
>>> T. My original reply was about G\"odel's theorem, not what else G\"odel
>>> said in the paper where he first proved that theorem.
>>
>> So, could G be false then?
>
> If P is inconsistent.

Why would that be if Godel's theorem doesn't have to depend on
the notion of truth or falsehood in the naturals?

[Frederick Williams]

Nam Nguyen wrote:
>
> On 21/10/2012 6:56 AM, Frederick Williams wrote:
> > Nam Nguyen wrote:
> >>
> >> On 20/10/2012 9:44 AM, Frederick Williams wrote:
> >>> Nam Nguyen wrote:
> >>>>
> >>>> On 20/10/2012 8:15 AM, Frederick Williams wrote:
> >>>>> Nam Nguyen wrote:
> >>>>>>
> >>>>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
> >>>>>>> Charlie-Boo wrote:
> >>>>>>>>

> >>>>>>>> [...] After all, Godel theorem wouldnÂ’t be a

I don't deny that G\"odel talks of things being true or false in his
paper, the point is this: neither in the statement of the theorem (P is
incomplete) nor in its proof, are the concepts of truth and falsity
used.

> >>> To
> >>> be sure, someone who proves of some particular T that there is a closed
> >>> formula phi such that neither T |- phi nor T |- ~phi, may, in the same
> >>> publication, say that phi (let's say) is true in the intended model of
> >>> T. My original reply was about G\"odel's theorem, not what else G\"odel
> >>> said in the paper where he first proved that theorem.
> >>
> >> So, could G be false then?
> >
> > If P is inconsistent.
>
> Why would that be if Godel's theorem doesn't have to depend on
> the notion of truth or falsehood in the naturals?

That seems to be a non sequitur. I don't see how

If P is inconsistent then G is false.

is relevant to either the statement or the proof of the incompleteness
theorem.

[Nam Nguyen]

On 21/10/2012 1:20 PM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> On 21/10/2012 6:56 AM, Frederick Williams wrote:
>>> Nam Nguyen wrote:
>>>>
>>>> On 20/10/2012 9:44 AM, Frederick Williams wrote:
>>>>> Nam Nguyen wrote:
>>>>>>
>>>>>> On 20/10/2012 8:15 AM, Frederick Williams wrote:
>>>>>>> Nam Nguyen wrote:
>>>>>>>>
>>>>>>>> On 19/10/2012 1:26 PM, Frederick Williams wrote:
>>>>>>>>> Charlie-Boo wrote:
>>>>>>>>>>

>>>>>>>>>> [...] After all, Godel theorem wouldn’t be a

You misunderstood his Incompleteness work.

Godel just didn't irreverently "talk" about truth/falsehood in the
naturals: it's a _requirement that an object theory T has to conform_ !

It's a simple fact in the foundation of FOL mathematics that it's
impossible to prove the undecidability of a formula F in a formal
system T, without using at least the notion of model-theoretical
truth and falsehood - at least. ("At least" because even then it's
very much questionable if the proof-method is logically valid).

Without the model-theoretical stipulation that G(T) is true, directly
or indirectly disguised as omega-consistency or what have you, Godel
could not have possibly made the meta inference that G(T) is
undecidable.

>
>>>>> To
>>>>> be sure, someone who proves of some particular T that there is a closed
>>>>> formula phi such that neither T |- phi nor T |- ~phi, may, in the same
>>>>> publication, say that phi (let's say) is true in the intended model of
>>>>> T. My original reply was about G\"odel's theorem, not what else G\"odel
>>>>> said in the paper where he first proved that theorem.
>>>>
>>>> So, could G be false then?
>>>
>>> If P is inconsistent.
>>
>> Why would that be if Godel's theorem doesn't have to depend on
>> the notion of truth or falsehood in the naturals?
>
> That seems to be a non sequitur. I don't see how
>
> If P is inconsistent then G is false.
>
> is relevant to either the statement or the proof of the incompleteness
> theorem.

As alluded to above, it's relevant to the method of meta-level proof
(even to the logical validity of the method) Godel used for his
Incompleteness.

[Nam Nguyen]

"irrelevantly" I meant.

[Frederick Williams]

Nam Nguyen wrote:

>
> You misunderstood his Incompleteness work.
>
> Godel just didn't irreverently "talk" about truth/falsehood in the

Noted from other post: > "irrelevantly" I meant.

> naturals: it's a _requirement that an object theory T has to conform_ !

If no one had ever heard of the natural numbers, it would still be that,
for some formula phi,

neither P |- phi nor P |- ~phi,

assuming that P is consistent.

> It's a simple fact in the foundation of FOL mathematics that it's
> impossible to prove the undecidability of a formula F in a formal
> system T, without using at least the notion of model-theoretical
> truth and falsehood - at least.

Curious, because Tarski didn't give the definition of truth and
falsehood in a model until after G\"odel had published.

> ("At least" because even then it's
> very much questionable if the proof-method is logically valid).
>
> Without the model-theoretical stipulation that G(T) is true, directly
> or indirectly disguised as omega-consistency or what have you, Godel
> could not have possibly made the meta inference that G(T) is
> undecidable.

Omega consistency is a syntactic matter not a model-theoretic one. P is
omega inconsistent iff for some formula phi(x) all the following hold:

P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ..., R |-
(Ex)~phi(x).

P is omega consistent iff it is not omega inconsistent. Rosser proved
that incompleteness still holds if consistency is assumed.

[Nam Nguyen]

I'm sorry Frederick, '...' isn't part of L(P). So I don't know what
you're talking about.

It looks like you're _trying_ to say the following formula F is true
in the naturals:

F <-> phi(0) /\ phi(S0) /\ phi(SS0) .... /\ (Ex)~phi(x)

but no one would have any idea at all what you'd mean by this formula
F!

>
> P is omega consistent iff it is not omega inconsistent. Rosser proved
> that incompleteness still holds if consistency is assumed.

OK. Given PA1 = PA + ~cGC.

Let's assume PA1 is consistent by assuming NEG( PA1 |- ~x=x), please
prove to the newsgroup that G(PA1) is undecidable in PA1, _without_
using omega consistency.

Also, Given PA2 = PA + cGC.

Let's assume PA2 is consistent by assuming NEG( PA2 |- ~x=x), please
prove to the newsgroup that G(PA2) is undecidable in PA2, _without_
using omega consistency.

[Frederick Williams]

So what? It doesn't need to be, and I don't claim that it is. The
things that lie between '|-' and ',' are formulae.

> So I don't know what
> you're talking about.

I know you don't, and it gracious of you to admit it. Read G\"odel's
paper and maybe you will.

> It looks like you're _trying_ to say the following formula F is true
> in the naturals:
>
> F <-> phi(0) /\ phi(S0) /\ phi(SS0) .... /\ (Ex)~phi(x)
>
> but no one would have any idea at all what you'd mean by this formula
> F!

Then it's just as well that that isn't what I was trying to say.

> > P is omega consistent iff it is not omega inconsistent. Rosser proved
> > that incompleteness still holds if consistency is assumed.
>
> OK. Given PA1 = PA + ~cGC.
>
> Let's assume PA1 is consistent by assuming NEG( PA1 |- ~x=x), please
> prove to the newsgroup that G(PA1) is undecidable in PA1, _without_
> using omega consistency.
>
> Also, Given PA2 = PA + cGC.
>
> Let's assume PA2 is consistent by assuming NEG( PA2 |- ~x=x), please
> prove to the newsgroup that G(PA2) is undecidable in PA2, _without_
> using omega consistency.

I don't know which of PA1 and PA2 is incomplete.

[Nam Nguyen]

Which formula?

That's why you've failed to understand Godel's proof. Your '...'
would start with 'P |- ...' which means '...' is a FOL proof and if
you don't even know which formula it should be then of course you'd
have no clue what Godel might have meant by "Omega consistency".

Not that after you could pin down what the formula be by Induction,
there's any guarantee that "Omega consistency" can even be assume-able,
given your phi(x)!

>
>> So I don't know what
>> you're talking about.
>
> I know you don't, and it gracious of you to admit it. Read G\"odel's
> paper and maybe you will.

It just means you don't know what you're talking about. And your just
citing Godel's paper would do any help.

>
>> It looks like you're _trying_ to say the following formula F is true
>> in the naturals:
>>
>> F <-> phi(0) /\ phi(S0) /\ phi(SS0) .... /\ (Ex)~phi(x)
>>
>> but no one would have any idea at all what you'd mean by this formula
>> F!
>
> Then it's just as well that that isn't what I was trying to say.
>
>>> P is omega consistent iff it is not omega inconsistent. Rosser proved
>>> that incompleteness still holds if consistency is assumed.
>>
>> OK. Given PA1 = PA + ~cGC.
>>
>> Let's assume PA1 is consistent by assuming NEG( PA1 |- ~x=x), please
>> prove to the newsgroup that G(PA1) is undecidable in PA1, _without_
>> using omega consistency.
>>
>> Also, Given PA2 = PA + cGC.
>>
>> Let's assume PA2 is consistent by assuming NEG( PA2 |- ~x=x), please
>> prove to the newsgroup that G(PA2) is undecidable in PA2, _without_
>> using omega consistency.
>
> I don't know which of PA1 and PA2 is incomplete.

Then you should review some basics of mathematical reasoning.

If you have a valid inference P => Q then it's still a valid inference
no matter if P is true or not.

It doesn't matter which of PA1, PA2 you'd choose; let it be T.
What you believe is if this T is consistent then this T can be
proven to be incomplete.

Now, you're given the assumption T (PA1 or Pa2) be consistent.
So prove that T _would be_ incomplete. If you know what you're
talking about.

For example, assuming ~GC is true we could prove that such a counter
example _would be_ greater than 10. See: we don't even know which of
GC or ~GC is true.

You just didn't know what you were talking about, about proving a T's
incompleteness through "omega consistency".

[Frederick Williams]

Nam Nguyen wrote:
>
> On 21/10/2012 5:01 PM, Frederick Williams wrote:
> > Nam Nguyen wrote:
> >>
> >> On 21/10/2012 3:35 PM, Frederick Williams wrote:

> >>>
> >>> Omega consistency is a syntactic matter not a model-theoretic one. P is
> >>> omega inconsistent iff for some formula phi(x) all the following hold:
> >>>
> >>> P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ..., R |-
> >>> (Ex)~phi(x).
> >>
> >> I'm sorry Frederick, '...' isn't part of L(P).
> >
> > So what? It doesn't need to be, and I don't claim that it is. The
> > things that lie between '|-' and ',' are formulae.
>
> Which formula?

phi(n) for each numeral n, and (Ex)~phi(x).

>
> You just didn't know what you were talking about, about proving a T's
> incompleteness through "omega consistency".

Have you ever read G\"odel's paper?

[Nam Nguyen]

On 21/10/2012 6:12 PM, Frederick Williams wrote:
> Nam Nguyen wrote:
>>
>> On 21/10/2012 5:01 PM, Frederick Williams wrote:
>>> Nam Nguyen wrote:
>>>>
>>>> On 21/10/2012 3:35 PM, Frederick Williams wrote:
>
>>>>>
>>>>> Omega consistency is a syntactic matter not a model-theoretic one. P is
>>>>> omega inconsistent iff for some formula phi(x) all the following hold:
>>>>>
>>>>> P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ..., R |-
>>>>> (Ex)~phi(x).
>>>>
>>>> I'm sorry Frederick, '...' isn't part of L(P).
>>>
>>> So what? It doesn't need to be, and I don't claim that it is. The
>>> things that lie between '|-' and ',' are formulae.
>>
>> Which formula?
>
> phi(n) for each numeral n, and (Ex)~phi(x).

But how would you know:

P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ...,

would _not_ lead to (Ex)~phi(x)?

[Frederick Williams]

Nam Nguyen wrote:
>
> On 21/10/2012 6:12 PM, Frederick Williams wrote:
> > Nam Nguyen wrote:
> >>
> >> On 21/10/2012 5:01 PM, Frederick Williams wrote:
> >>> Nam Nguyen wrote:
> >>>>
> >>>> On 21/10/2012 3:35 PM, Frederick Williams wrote:
> >
> >>>>>
> >>>>> Omega consistency is a syntactic matter not a model-theoretic one. P is
> >>>>> omega inconsistent iff for some formula phi(x) all the following hold:
> >>>>>
> >>>>> P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ..., R |-
> >>>>> (Ex)~phi(x).
> >>>>
> >>>> I'm sorry Frederick, '...' isn't part of L(P).
> >>>
> >>> So what? It doesn't need to be, and I don't claim that it is. The
> >>> things that lie between '|-' and ',' are formulae.
> >>
> >> Which formula?
> >
> > phi(n) for each numeral n, and (Ex)~phi(x).
>
> But how would you know:
>
> P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ...,
>
> would _not_ lead to (Ex)~phi(x)?

It's not a question of anything leading or not leading to anything;
still less is it a question of how I would know anything. That P is
omega consistent was an assumption made by G\"odel that he found
necessary to prove his incompleteness theorem. A few years later,
Rosser showed that an assumption of consistency (again a syntactic
matter) was sufficient.

Why don't you answer a question for a change? I asked "Have you ever
read G\"odel's paper?" Take that to mean in English translation, if you
wish. Well, have you?

[MoeBlee]

On Oct 21, 3:41 am, Rupert <rupertmccal...@yahoo.com> wrote:
> On Oct 21, 12:00 am, Nam Nguyen <namducngu...@shaw.ca> wrote:

> > (b) _an assumption that one of its model is the natural numbers [...] Godel's proof stipulates

> > (b) as a requirement;
>
> No, it doesn't. In his 1931 paper he assumed that the object theory T
> is omega-consistent. He doesn't need to assume that the natural
> numbers is one of the models of T.

> >     So, Frederick was incorrect in saying "There is no need to establish
> >     that G is true": there's a need, due to both requirements (a) and
> >     (b).
>
> No, Frederick's remark was not incorrect.

I mentioned in another thread that time after time Nguyen is in basic
disagreement with one or more informed posters. Here is yet another
example. I don't claim Nguyen is incorrect merely on the basis that
Rupert says he is, but I do wonder how Nguyen accounts for the fact
that in thread after thread after thread Nguyen is in basic
disagreement on simple matters with one or (usually) more well
informed posters.

If T is an omega-consistent (or even, per Rosser, consistent) formal
theory that can form a Godel sentence G for T, then T is incomplete.
This does not require referencing a notion of truth, models, or the
natual numbers as a model for T. And that is not contradicted by the
fact that we can also go on (as a bonus, so to speak) to show that G
is true in the naturals.

Williams and Ruperts are correct about this. A look at Godel's paper
or just about any textbook in mathematical logic would provide Nguyen
adequate explanation.

Why, in face of clear and correct explanation from a well informed
person such as Rupert, is Nguyen yet again stubbornly insisting on an
incorrect claim?

MoeBlee

[Nam Nguyen]

I'll respond more in some good details, but really no one has proven
that I'm wrong in my claim that Godel did use the truths of the naturals
numbers in his Incompleteness.

For the record, I did cite Godel's own stipulation, as his requirement,
that for an object formal system T, T should have no _false_
propositions as theorems, where false = not true. But so far no one
has adequately explained how that requirement vanished in the details
of his proof.

And no, simply saying that Godel just mentioned the word "true" or
"false" with no relevancy to the proof, as Frederick has implied,
is _NOT_ an adequate technical explanation. Far from it actually!

Any rate, I'll respond more, especially to address in some technical
details some of the points Rupert has raised.

But for the record, to say Godel didn't base his proof on the truths
of the naturals is incorrect. (Hint: why did Godel have to define
the prime numbers in his proof?).

[Nam Nguyen]

You just uttered an _extremely brief summary_ what you read in books,
sources, without adequate understanding the essence of Godel's proof
(paper).

>
> Why don't you answer a question for a change? I asked "Have you ever
> read G\"odel's paper?" Take that to mean in English translation, if you
> wish. Well, have you?
>

That's not a relevant technical question, in responding to my technical
question above which you've refused to adrress.

[Frederick Williams]

Nam Nguyen wrote:

> > Why don't you answer a question for a change? I asked "Have you ever
> > read G\"odel's paper?" Take that to mean in English translation, if you
> > wish. Well, have you?
> >
> That's not a relevant technical question, in responding to my technical
> question above which you've refused to adrress.

So the answer's no.

[Nam Nguyen]

On 21/10/2012 2:41 AM, Rupert wrote:
> On Oct 21, 12:00 am, Nam Nguyen <namducngu...@shaw.ca> wrote:

>> (2) P is a proving system, using syntactical proofs, proving G(T) to be
>> undecidable (hence ~G(T) to be also undecidable).
>>
>> But how do we know that P itself is consistent, without assuming
>> that it has the natural numbers [in which G(T) is assumed to be
>> true]?
>>
>
> I don't really know exactly what you're referring to when you talk
> about the assumption that P "has the natural numbers".

A little glossing here on my part: I meant part of a model of P
is interpretable as (isomorphic to) the natural numbers.

>
> Also, you seem to be under the impression that P is the metatheory and
> PA is the object theory. It would be possible to do things this way,
> but actually in Gödel's 1931 paper P was the object theory.

Right. His object theory P is my T. And below I'll mention the issue of
the meta theory that Godel used - if he indeed use any.

>
> The goal is to prove (in whatever metatheory you wish to work with)
> that if the object theory T is omega-consistent then the Gödel
> sentence for T, G, is independent of T. That's the goal.

Right. That's a _summary_ in English of what GIT is about.

The devil of course is in the details.

> If you happen
> to end up proving along the way that also G is true, then that's fine,
> but there's no need to do so. What you need to do is show that if T is
> omega-consistent, then G is independent of T. Gödel succeeded in doing
> this, so everything is fine.

No it's not fine. What exactly did you mean by "show"?

If by "show" you meant FOL "prove", can you express "omega-
consistency" as a _finite_ formula, since FOL proof involves
only finite formulas in finite number of steps?

As well, can you specify the FOL (meta) theory where this
"proving" would be in? Which FOL (meta) theory did Godel use
to "prove" the undecidability of G(P) in his object theory P?

If by "show" you didn't mean FOL "prove" as above, then
what did you mean by "show", or even "prove"?

These are important clarifications that I think we'd need
to have so as we'd understand each other positions well
enough to continue the argument.

[Rupert]

On Oct 23, 8:29 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 21/10/2012 2:41 AM, Rupert wrote:
>
> > On Oct 21, 12:00 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> (2) P is a proving system, using syntactical proofs, proving G(T) to be
> >>       undecidable (hence ~G(T) to be also undecidable).
>
> >>       But how do we know that P itself is consistent, without assuming
> >>       that it has the natural numbers [in which G(T) is assumed to be
> >>       true]?
>
> > I don't really know exactly what you're referring to when you talk
> > about the assumption that P "has the natural numbers".
>
> A little glossing here on my part: I meant part of a model of P
> is interpretable as (isomorphic to) the natural numbers.
>

Well, it could be that P is consistent and only has nonstandard
models.

>
>
> > Also, you seem to be under the impression that P is the metatheory and
> > PA is the object theory. It would be possible to do things this way,

> > but actually in G del's 1931 paper P was the object theory.

>
> Right. His object theory P is my T. And below I'll mention the issue of
> the meta theory that Godel used - if he indeed use any.
>
>
>
> > The goal is to prove (in whatever metatheory you wish to work with)

> > that if the object theory T is omega-consistent then the G del

> > sentence for T, G, is independent of T. That's the goal.
>
> Right. That's a _summary_ in English of what GIT is about.
>
> The devil of course is in the details.
>
> > If you happen
> > to end up proving along the way that also G is true, then that's fine,
> > but there's no need to do so. What you need to do is show that if T is

> > omega-consistent, then G is independent of T. G del succeeded in doing

> > this, so everything is fine.
>
> No it's not fine. What exactly did you mean by "show"?
>
> If by "show" you meant FOL "prove", can you express "omega-
> consistency" as a _finite_ formula, since FOL proof involves
> only finite formulas in finite number of steps?
>

Yes.

> As well, can you specify the FOL (meta) theory where this
> "proving" would be in?

PRA would work fine.

> Which FOL (meta) theory did Godel use
> to "prove" the undecidability of G(P) in his object theory P?
>

He used informal reasoning which was obviously finitistically
acceptable. I think the definition of PRA came later; it would have
then been obvious that the proof could be formalized in PRA.

> If by "show" you didn't mean FOL "prove" as above, then
> what did you mean by "show", or even "prove"?
>

When discussing mathematics, it's usually taken as a given that we
know what "prove" means. That's what you're supposed to learn when you
do a mathematics degree.

> These are important clarifications that I think we'd need
> to have so as we'd understand each other positions well
> enough to continue the argument.
>

Gödel gave an informal proof which is finitistically acceptable and
can be formalized in PRA.

[MoeBlee]

On Oct 22, 6:57 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>
simply saying that Godel just mentioned the word "true" or
> "false" with no relevancy to the proof, as Frederick has implied,

Williams's correct observation is that it is not necessary to prove
that G is true just to prove that the omega-consistent (even
consistent, we can say) theory P proves neither G nor ~G.

Further, since either G or ~G is true, we have that there is true
sentence the theory does not prove, still without having determined
whether G is true.

And, as far as I recall, Williams did not contradict that G happens to
be true (given that the theory is omega-consistent, or even just
consistent) since: (1) G is not provable and (2) G is true iff G is
not provable.

> But for the record, to say Godel didn't base his proof on the truths
> of the naturals is incorrect. (Hint: why did Godel have to define
> the prime numbers in his proof?).

Godel used the primes and such things as the fundamental theorem of
arithmetic for his Godelization of the syntax. Still this does not
require proving that the formula G is true.

MoeBlee

[Aatu Koskensilta]

MoeBlee <mode...@gmail.com> writes:

> Williams's correct observation is that it is not necessary to prove
> that G is true just to prove that the omega-consistent (even
> consistent, we can say) theory P proves neither G nor ~G.

Sure, provided (for mere consistency) that by G we mean the Rosser
sentence for P.

> Further, since either G or ~G is true, we have that there is true
> sentence the theory does not prove, still without having determined
> whether G is true.

This is, logically speaking, an entirely unnecessary invocation of
excluded middle, since we can constructively prove that if a theory T
(satisfying the usual conditions) is consistent the Gödel sentence for T
is true but unprovable in T.

--
Aatu Koskensilta (aatu.kos...@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

[MoeBlee]

On Oct 23, 1:29 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> can you express "omega-
> consistency" as a _finite_ formula

Of course. 'omega-consistent' has a finite definition. Look it up.

> As well, can you specify the FOL (meta) theory where this
> "proving" would be in?

Godel does not refer to a particular theory in which he's doing his
proving about the theory P. Rather Godel is working in informal
mathematics. However, Z\R set theory is more than adequate to use for
a formal proof, as the proof can be formalized even in a theory as
restrictive as PRA.

If I recall, such matters are mentiond in Franzen's book, which you've
read.

MoeBlee

[MoeBlee]

On Oct 23, 11:29 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote:

> MoeBlee <modem...@gmail.com> writes:
> > Williams's correct observation is that it is not necessary to prove
> > that G is true just to prove that the omega-consistent (even
> > consistent, we can say) theory P proves neither G nor ~G.
>
>   Sure, provided (for mere consistency) that by G we mean the Rosser
> sentence for P.

Yes.

> > Further, since either G or ~G is true, we have that there is true
> > sentence the theory does not prove, still without having determined
> > whether G is true.
>
>   This is, logically speaking, an entirely unnecessary invocation of
> excluded middle, since we can constructively prove that if a theory T

> (satisfying the usual conditions) is consistent the G del sentence for T

> is true but unprovable in T.

I mentioned it only in the context of defending that we don't need to
establish that "G is true" merely to infer that there is a true and
unprovable sentence.

MoeBlee

[MoeBlee]

On Oct 22, 7:04 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 22/10/2012 8:58 AM, Frederick Williams wrote:

> > That P is
> > omega consistent was an assumption made by G\"odel that he found
> > necessary to prove his incompleteness theorem.  A few years later,
> > Rosser showed that an assumption of consistency (again a syntactic
> > matter) was sufficient.
>
> You just uttered an _extremely brief summary_ what you read in books,
> sources, without adequate understanding the essence of Godel's proof
> (paper).

It's a reasonable summary. So what that it's brief? And you've not
shown that Williams does not understand the essence of Godel's proof.

> > Why don't you answer a question for a change?  I asked "Have you ever
> > read G\"odel's paper?"  Take that to mean in English translation, if you
> > wish.  Well, have you?
>
> That's not a relevant technical question, in responding to my technical
> question above which you've refused to adrress.

It's not a technical question, but it is a relevant question in this
discussion.

My own question is also non-technical: Why are continually take the
wrong side in technical arguments with people who are vastly more
informed on the subject than you are?

MoeBlee

[Nam Nguyen]

Can you give a brief description of such (finite) _formula_ ?

>
>> As well, can you specify the FOL (meta) theory where this
>> "proving" would be in?
>
> PRA would work fine.

But how would anyone know that PRA is consistent in the first place?

>
>> Which FOL (meta) theory did Godel use
>> to "prove" the undecidability of G(P) in his object theory P?
>>
>
> He used informal reasoning which was obviously finitistically
> acceptable. I think the definition of PRA came later; it would have
> then been obvious that the proof could be formalized in PRA.

So, "informal reasoning" here is the same as "informal proof".

Wouldn't you think it very much borderlines (at best) inconsistency
in argument, to attribute above that his proof is of _formal proof_
viz-a-viz PRA while here it's of the status of an _informal proof_ ?

I mean you do agree that _formal proof is not informal proof_ right?

>
>> If by "show" you didn't mean FOL "prove" as above, then
>> what did you mean by "show", or even "prove"?
>>
>
> When discussing mathematics, it's usually taken as a given that we
> know what "prove" means. That's what you're supposed to learn when you
> do a mathematics degree.

Agree. So, to you, is Godel's proof an informal proof or a formal proof?
Please clarify for 100% certainty, since above you seem to have given 2
contradictory accounts.

>
>> These are important clarifications that I think we'd need
>> to have so as we'd understand each other positions well
>> enough to continue the argument.
>>
>
> Gödel gave an informal proof which is finitistically acceptable and
> can be formalized in PRA.

So in mathematical logic the phrases "formalized proof" and
"informalized proof" would mean the same?

In any rate how do we know that PRA is consistent in the first place,
_without_ using any notion that would depend on the notion of the
natural number which you, MoeBlee, and Frederick (incorrectly) have
insisted Godel didn't use in his proof, despite Godel's own words
of requirement?

[Isn't it true that the 'R' in "PRA" would have a lot to do with
recursions in the natural numbers, and that the naturals collectively
is an _assumed_ model of PRA?]

[Nam Nguyen]

So what does it mean to you to prove F is undecidable in T, _without_
mentioning the notion of model-theoretical truth or falsehood?

For instance, how would you prove, as a _pure_ FOL theorem, that the
commutativity of a group is undecidable in the FOL simple-group theory?

[Nam Nguyen]

On 23/10/2012 10:49 AM, MoeBlee wrote:
> On Oct 22, 7:04 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> On 22/10/2012 8:58 AM, Frederick Williams wrote:
>
>>> That P is
>>> omega consistent was an assumption made by G\"odel that he found
>>> necessary to prove his incompleteness theorem. A few years later,
>>> Rosser showed that an assumption of consistency (again a syntactic
>>> matter) was sufficient.
>>
>> You just uttered an _extremely brief summary_ what you read in books,
>> sources, without adequate understanding the essence of Godel's proof
>> (paper).
>
> It's a reasonable summary. So what that it's brief?

It's brief because it's like explaining that PA has these specific
axioms plus an axiom schema! Which axiom schema?

What specific formula(s) did Godel use the omega consistency stipulation
for?

> And you've not
> shown that Williams does not understand the essence of Godel's proof.

I did ask him how

> P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ...,
> would _not_ lead to (Ex)~phi(x)?

and he didn't answer the question.

>
> My own question is also non-technical: Why are continually take the
> wrong side in technical arguments with people who are vastly more
> informed on the subject than you are?

I have my own non-technical question: why does MoeBlee have a habit
of acting and sounding like a member of a modern time Inquisition
cult?

If you could answer this non-technical question that's fine. Otherwise
you could perhaps help Frederick to answer the question I had asked
him (above). (And that's just 1 technical question he didn't answer).

[Nam Nguyen]

On 23/10/2012 10:09 PM, Nam Nguyen wrote:
> On 23/10/2012 10:42 AM, MoeBlee wrote:
>> On Oct 23, 11:29 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote:
>>> MoeBlee <modem...@gmail.com> writes:
>>>> Williams's correct observation is that it is not necessary to prove
>>>> that G is true just to prove that the omega-consistent (even
>>>> consistent, we can say) theory P proves neither G nor ~G.
>>>
>>> Sure, provided (for mere consistency) that by G we mean the Rosser
>>> sentence for P.
>>
>> Yes.
>>
>>>> Further, since either G or ~G is true, we have that there is true
>>>> sentence the theory does not prove, still without having determined
>>>> whether G is true.
>>>
>>> This is, logically speaking, an entirely unnecessary invocation of
>>> excluded middle, since we can constructively prove that if a theory T
>>> (satisfying the usual conditions) is consistent the G del sentence for T
>>> is true but unprovable in T.
>>
>> I mentioned it only in the context of defending that we don't need to
>> establish that "G is true" merely to infer that there is a true and
>> unprovable sentence.
>
> So what does it mean to you to prove F is undecidable in T, _without_
> mentioning the notion of model-theoretical truth or falsehood?
>
> For instance, how would you prove, as a _pure_ FOL theorem, that the
> commutativity of a group is undecidable in the FOL simple-group theory?

Of course you and Frederick would know what it means to prove, as a
_pure_ FOL theorem, F is decidable in T.

It's the undecidability of F here, and G(T) there in Godel's proof,
that would "do it in" (so to speak) your understanding of Incompleteness
proof.

[Rupert]

I suggest you read Gödel's paper; then you should be able to figure
out how to construct it yourself.

>
>
> >> As well, can you specify the FOL (meta) theory where this
> >> "proving" would be in?
>
> > PRA would work fine.
>
> But how would anyone know that PRA is consistent in the first place?
>

It is almost universally accepted that the consistency of PRA is
obvious. Furthermore a theory considerably weaker than PRA will do,
namely quantifier-free polynomial-time computable arithmetic. I don't
think that even Edward Nelson has doubts about the consistency of this
theory.

>
>
> >> Which FOL (meta) theory did Godel use
> >> to "prove" the undecidability of G(P) in his object theory P?
>
> > He used informal reasoning which was obviously finitistically
> > acceptable. I think the definition of PRA came later; it would have
> > then been obvious that the proof could be formalized in PRA.
>
> So, "informal reasoning" here is the same as "informal proof".
>
> Wouldn't you think it very much borderlines (at best) inconsistency
> in argument, to attribute above that his proof is of _formal proof_
> viz-a-viz PRA while here it's of the status of an _informal proof_ ?
>
> I mean you do agree that _formal proof is not informal proof_ right?
>

Yes, I do. I correctly stated that Gödel gives an informal argument in
his paper which can be formalized in PRA (and also in quantifier-free
polynomial-time computable arithmetic, which not even Nelson doubts to
be consistent).

>
>
> >> If by "show" you didn't mean FOL "prove" as above, then
> >> what did you mean by "show", or even "prove"?
>
> > When discussing mathematics, it's usually taken as a given that we
> > know what "prove" means. That's what you're supposed to learn when you
> > do a mathematics degree.
>
> Agree. So, to you, is Godel's proof an informal proof or a formal proof?
> Please clarify for 100% certainty, since above you seem to have given 2
> contradictory accounts.
>

The argument given in the paper is an informal argument, but it can be
formalized. It would be in principle possible to convert it into a
formal argument and check it by computer, and I believe that project
is already underway.

I did not give two contradictory accounts at all. What I said was
perfectly consistent.

>
>
> >> These are important clarifications that I think we'd need
> >> to have so as we'd understand each other positions well
> >> enough to continue the argument.
>

> > G�del gave an informal proof which is finitistically acceptable and

> > can be formalized in PRA.
>
> So in mathematical logic the phrases "formalized proof" and
> "informalized proof" would mean the same?
>

Of course not.

> In any rate how do we know that PRA is consistent in the first place,
> _without_ using any notion that would depend on the notion of the
> natural number which you, MoeBlee, and Frederick (incorrectly) have
> insisted Godel didn't use in his proof, despite Godel's own words
> of requirement?
>

Hardly anyone has serious doubts about the consistency of PRA, and, as
I observed, the argument will go through in quantifier-free polynomial-
time computable arithmetic. Not even Nelson doubts the consistency of
that theory. If you doubt the consistency of that theory, then of
course you will regard all nontrivial mathematics as doubtful,
including Gödel's argument.

I never said that Gödel didn't use the notion of natural number in his
proof, and I doubt anyone else did either.

[MoeBlee]

On Oct 23, 11:09 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

> what does it mean to you to prove F is undecidable in T, _without_
> mentioning the notion of model-theoretical truth or falsehood?

There are two senses of 'undecidable' and we need to be clear which
one we mean in a given context. But, still, the definition of neither
requires referencing model-theoretic truth.

(1) A relation R is undecidable iff there is no algorithm to determine
for membership in R. So, using Church's thesis, R is undecidable iff R
is not recursive.

(2) A formula F is undecidable from a set of formulas T iff neither T
|- F nor T |- ~F. Another way of saying this is that "F is independent
of T".

I surmise it's sense (2) you have in mind now. And the definition does
not reference a notion of models or truth.

But you asked, how do we PROVE that F is independent of T. Well, we
prove by whatever formal or informal principles we have accepted as
basis for proof. In many cases, we do use the method of models to
prove independence results. This is allowed by the soundness and
completeness theorem for first order so that:

T |- F iff T |= F.

But using model theoretic methods is not the ONLY way to prove certain
results in context of the first incompleteness theorem.

In particular, Godel does NOT use model theoretic methods to prove:

(*) If P is omega-consistent, then there is a sentence G such that
neither P |- G nor P |- ~G.

or, as strenghtened by Rosser:

(**) If P is consistent, then there is a sentence G such that neither
P |- G nor P |- ~G.

If you claim that the notion of model theoreretic truth was used for
those proofs, then it's up to you to show exactly where in the proofs
this occurs.

MoeBlee

[MoeBlee]

(1) What F is decidable in what T?

What I've said is that the Godel proof of

If P is omega-consistent then there is a G such that neither P |- G
nor P |- ~G

does not use model theoretic arguments.

Also that (as I have read in the literature, and can fathom from
Godel's paper itself) the theorem just mentioned can be proven in PRA.

But I never claimed that the incompleteness theorem makes no use of
any non-logical axioms or principles. PRA is finitistic, but it does
have non-logical axioms.

MoeBlee

[MoeBlee]

On Oct 24, 4:13 am, Rupert <rupertmccal...@yahoo.com> wrote:

> the argument will go through in quantifier-free polynomial-
> time computable arithmetic.

Cool.

MoeBlee

[MoeBlee]

On Oct 23, 10:42 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

> _without_ using any notion that would depend on the notion of the
> natural number which you, MoeBlee, and Frederick (incorrectly) have
> insisted Godel didn't use in his proof, despite Godel's own words
> of requirement?

I never said that natural numbers aren't used in the proof. Please
don't put words in my mouth.

> [Isn't it true that the 'R' in "PRA" would have a lot to do with
> recursions in the natural numbers, and that the naturals collectively
> is an _assumed_ model of PRA?]

The naturals and the recursive functions on naturals are a model of
PRA.

But IN a PRA proof itself we don't mention such considerations as
models of PRA.

MoeBlee

[MoeBlee]

On Oct 23, 10:42 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 23/10/2012 2:03 AM, Rupert wrote:

> But how would anyone know that PRA is consistent in the first place?

You're free to doubt the consistency of PRA. I have my own reasons for
taking PRA to be consistent, but no matter my own views on the
consistency of PRA, the incompleteness theorem is provable in PRA.

> is Godel's proof an informal proof or a formal proof?

Godel's own paper is itself an informal presentation of a proof that,
with a bit of study, one can see how to formalize it.

> > Godel gave an informal proof which is finitistically acceptable and

> > can be formalized in PRA.
>
> So in mathematical logic the phrases "formalized proof" and
> "informalized proof" would mean the same?

No, of course not. Rupert didn't suggest anything of the kind.

MoeBlee

[Frederick Williams]

Nam Nguyen wrote:

>
> In any rate how do we know that PRA is consistent in the first place,
> _without_ using any notion that would depend on the notion of the
> natural number which you, MoeBlee, and Frederick (incorrectly) have
> insisted Godel didn't use in his proof, despite Godel's own words
> of requirement?

I was arguing that G\"odel never used the notions of truth or falsity in
his proof of his theorem. Have I ever said he didn't use the notion of
the natural number?

[MoeBlee]

On Oct 23, 11:42 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 23/10/2012 10:49 AM, MoeBlee wrote:

> > It's a reasonable summary. So what that it's brief?
>
> It's brief because it's like explaining that PA has these specific
> axioms plus an axiom schema! Which axiom schema?

Of course, any brief summary is going to omit many details. That
doesn't entail that one does not undertstand the essence of a matter
merely because one has given a brief summary of it.

> What specific formula(s) did Godel use the omega consistency stipulation
> for?

You can ask question after question after question about the proof.
But instead, why don't you start by reading it?

> > And you've not
> > shown that Williams does not understand the essence of Godel's proof.
>
> I did ask him how
>
> > P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ...,
> > would _not_ lead to (Ex)~phi(x)?

Unless there's context that needs to be reiterated for the above, my
answer to the above is "Why should it?" and "What's the relevance or
your question?"

Let '0n' stand for n number of 'S's' in front of '0'. An omega-
consistent theory T is one such that there is no phi such that we have
both (1) and (2): (1) for every n, we have T |- phi(0n) and (2) T |-
Ex~phi(x).

> and he didn't answer the question.

> > My own question is also non-technical: Why are continually take the
> > wrong side in technical arguments with people who are vastly more
> > informed on the subject than you are?
>
> I have my own non-technical question: why does MoeBlee have a habit
> of acting and sounding like a member of a modern time Inquisition
> cult?

Your question begs the question that I do act like a member of a
modern time Inquistion cult. On the other hand, my question to you is
based on the fact that you continually take the wrong side in

technical arguments with people who are vastly more informed on the

subject than you are. But even dropping the matter of whether you're
on the wrong side in such arguments, still, do you ask yourself why
you are continually, for years, in thread after thread after thread,
in such long drawn out disagreements with well informed posters?

MoeBlee

[Aatu Koskensilta]

Nam Nguyen <namduc...@shaw.ca> writes:

> I mean you do agree that _formal proof is not informal proof_ right?

Let me put it this way:

(Ex)(p)(p[x] --> 34{32x} / fnoffle).

> Agree. So, to you, is Godel's proof an informal proof or a formal proof?

Didn't I already explain all this to you, once upon the time?

--
Aatu Koskensilta (aatu.kos...@uta.fi)

"Wovon man nicht sprechen kann, dar�ber muss man schweigen"

[Frederick Williams]

Nam Nguyen wrote:
>
> On 23/10/2012 10:49 AM, MoeBlee wrote:
> > On Oct 22, 7:04 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> On 22/10/2012 8:58 AM, Frederick Williams wrote:
> >
> >>> That P is
> >>> omega consistent was an assumption made by G\"odel that he found
> >>> necessary to prove his incompleteness theorem. A few years later,
> >>> Rosser showed that an assumption of consistency (again a syntactic
> >>> matter) was sufficient.
> >>
> >> You just uttered an _extremely brief summary_ what you read in books,
> >> sources, without adequate understanding the essence of Godel's proof
> >> (paper).
> >
> > It's a reasonable summary. So what that it's brief?
>
> It's brief because it's like explaining that PA has these specific
> axioms plus an axiom schema! Which axiom schema?
>
> What specific formula(s) did Godel use the omega consistency stipulation
> for?
>
> > And you've not
> > shown that Williams does not understand the essence of Godel's proof.
>
> I did ask him how
>
> > P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ...,
> > would _not_ lead to (Ex)~phi(x)?
>
> and he didn't answer the question.

Just a reminder that this question of yours rose when I defined omega
consistency thus:

P is omega inconsistent iff for some formula phi(x)

all the following hold: P |- phi(0), P |- phi(0'),
P |- phi(0''), P |- phi(0'''), ..., R |- (Ex)~phi(x).

P is omega consistent if it is not omega inconsistent.

You then asked:

But how would you know:

P |- phi(0), P |- phi(0'), P |- phi(0''), P |- phi(0'''), ...,

would _not_ lead to (Ex)~phi(x)?

And I replied:

It's not a question of anything leading or not leading to anything;

still less is it a question of how I would know anything. That P is

omega consistent was an assumption made by G\"odel that he found
necessary to prove his incompleteness theorem.

So I did answer.

> >
> > My own question is also non-technical: Why are continually take the
> > wrong side in technical arguments with people who are vastly more
> > informed on the subject than you are?
>
> I have my own non-technical question: why does MoeBlee have a habit
> of acting and sounding like a member of a modern time Inquisition
> cult?

And I have one too:

Have you ever read G\"odel's paper?" Take that to mean in English
translation, if you wish. Well, have you?

> If you could answer this non-technical question that's fine. Otherwise
> you could perhaps help Frederick to answer the question I had asked
> him (above). (And that's just 1 technical question he didn't answer).

I answer all your questions if I understand them and know the answer.
You are the one who doesn't answer questions. Don't think I've
forgotten your "first things first" in another thread. I have a
terrible memory, but I can remember being wronged as well as a woman
can.

[Frederick Williams]

Nam Nguyen wrote:

>
> So what does it mean to you to prove F is undecidable in T, _without_
> mentioning the notion of model-theoretical truth or falsehood?

The you isn't me, but never mind.

It means proving that neither T |- F nor T |- ~F without mentioning
truth or falsehood.

> For instance, how would you prove, as a _pure_ FOL theorem, that the
> commutativity of a group is undecidable in the FOL simple-group theory?

Do you mean, how would you prove that neither

First order theory of groups |- all groups are commutative

nor

First order theory of groups |- there exists a non commutative group

? Because I suspect that neither 'all groups are commutative' nor
'there exists a non commutative group' are expressible in the language
of the first order theory of groups.

[MoeBlee]

On Oct 24, 4:44 pm, Frederick Williams <freddywilli...@btinternet.com>
wrote:

> Nam Nguyen wrote:

> > For instance, how would you prove, as a _pure_ FOL theorem, that the
> > commutativity of a group is undecidable in the FOL simple-group theory?
>
> Do you mean, how would you prove that neither
>
>    First order theory of groups |- all groups are commutative
>
> nor
>
>    First order theory of groups |- there exists a non commutative group

Though what he posted came out differently, maybe what he has in mind
is this:

Prove (where 'S' stands for the axioms of the first order theory of
groups):

It's not the case that S |- Axy x*y = y*x
and
it's not the case that S |- ~Axy x*y = y*x

However, it's still not clear what non-logical axioms he allows to be
used in making such a proof.

Anyway, I would GUESS his point is that it's with models that we would
make the proof. That is, show a group (a model of S) that is
commuative and show a group (a model of S) that is not commutative,
and we're done.

My reply earlier was that the fact that certain independence proofs
use models doesn't entail that Godel's proof of the indepencdence of
the sentence G from the axioms of P uses models. If Nguyen wants to
claim that Godel's proof does use models then it's up to Nguyen to
show where models are used in the proof. He just doesn't seem to get
(or want to find out for himself) that Godel's proof is syntactic, not
model theoretic.

MoeBlee

[Frederick Williams]

Nam Nguyen wrote:

>
> OK. Given PA1 = PA + ~cGC.
>
> Let's assume PA1 is consistent by assuming NEG( PA1 |- ~x=x), please
> prove to the newsgroup that G(PA1) is undecidable in PA1, _without_
> using omega consistency.

If PA1 is consistent then the Rosser version would be used. If your
notation G(PA1) indicates that you have in mind the G\"odel sentence for
PA1, then it's irrelevant.

> Also, Given PA2 = PA + cGC.
>
> Let's assume PA2 is consistent by assuming NEG( PA2 |- ~x=x), please
> prove to the newsgroup that G(PA2) is undecidable in PA2, _without_
> using omega consistency.

If PA2 is consistent then the Rosser version would be used. If your
notation G(PA2) indicates that you have in mind the G\"odel sentence for
PA1, then it's irrelevant.

I'll tell you why I'm not going to provide the proofs you want.
(i) I'm not a circus animal that jumps through hoops at your command.
(ii) The proofs are long and not suitable for expressing in Ascii.
(iii) They have no bearing on your claim that when G\"odel proved
G\"odel's first incompleteness theorem, he used the notions of truth or
falsity.

See Rosser, Extensions of some theorems of G\"odel and Church, JSL vol
1, 1936.

[Frederick Williams]

Indeed so, I had supposed we were heading for 'Since models are used in
the group case, G\"odel must have used models in his case.'

[Nam Nguyen]

On 24/10/2012 4:07 PM, MoeBlee wrote:
> On Oct 24, 4:44 pm, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
>> Nam Nguyen wrote:
>
>>> For instance, how would you prove, as a _pure_ FOL theorem, that the
>>> commutativity of a group is undecidable in the FOL simple-group theory?
>>
>> Do you mean, how would you prove that neither
>>
>> First order theory of groups |- all groups are commutative
>>
>> nor
>>
>> First order theory of groups |- there exists a non commutative group
>
> Though what he posted came out differently, maybe what he has in mind
> is this:
>
> Prove (where 'S' stands for the axioms of the first order theory of
> groups):
>
> It's not the case that S |- Axy x*y = y*x
> and
> it's not the case that S |- ~Axy x*y = y*x
>
> However, it's still not clear what non-logical axioms he allows to be
> used in making such a proof.

As you've mentioned above, it's the first order finitely axiomatizable
theory of group, which Shoefield axiomatized with 2 axioms G1, G2 on
page 22. (Let's denote this theory as G).

>
> Anyway, I would GUESS his point is that it's with models that we would
> make the proof. That is, show a group (a model of S) that is
> commuative and show a group (a model of S) that is not commutative,
> and we're done.

Exactly.

Now .... we're not there yet here with Godel's proof you mentioned
below.

>
> My reply earlier was that the fact that certain independence proofs
> use models doesn't entail that Godel's proof of the indepencdence of
> the sentence G from the axioms of P uses models.

Before we go further on the above, please do confirm if it's your
understanding that in the case of G, _the only possible way to prove_
_the undecidability_ of Axy[x*y = y*x] in this case of G is through
_model-theoretical proofs_ (using truth, falsehood).

<Note>

Please bear in mind that here:

(a) bt decidability of F in T I do mean:

(T |- F) or (T |- ~F)

(b) by undecidability of F in T I do mean:

NEG(T |- F) and NEG(T |- ~F)

</Note>

> If Nguyen wants to
> claim that Godel's proof does use models then it's up to Nguyen to
> show where models are used in the proof. He just doesn't seem to get
> (or want to find out for himself) that Godel's proof is syntactic, not
> model theoretic.

[Nam Nguyen]

On 24/10/2012 12:09 PM, Aatu Koskensilta wrote:
> Nam Nguyen <namduc...@shaw.ca> writes:
>
>> I mean you do agree that _formal proof is not informal proof_ right?
>
> Let me put it this way:
>
> (Ex)(p)(p[x] --> 34{32x} / fnoffle).

Sure. Whatever that is! :-)

>
>> Agree. So, to you, is Godel's proof an informal proof or a formal proof?
>
> Didn't I already explain all this to you, once upon the time?

Yes. A long ... long time ago in a galaxy far ... far away, so to speak,
where Torkel Franzen used to help people with a lot of _good details_
in explaining difficult, subtle, technical issues.

In any rate, could you please help refreshing my memory if you agreed
or said sometimes before that - up to a limit - it's really up to each
individual to _know_ what the natural numbers be, especially w.r.t.
the truth value of the formula cGC.

I thought you did say something to that effect but my conversation
with you is _too few_ to let me remember. (Thanks.)

[Nam Nguyen]

Right. We're _heading_ that way.

But first I'm waiting for Moeblee to confirm if indeed in the case
of the theory S above (Shoenfield called it G), language-structure
theoretical means (truth/falsehood) would be _the only available mean_
to "prove" the undecidability of Axy[x*y = y*x].

Of course, you, Rupert, Aatu, or anyone else, could confirm or deny
that too. [With _technical reasons_ please.]

[Nam Nguyen]

I take your refusal to mean that you couldn't articulate what you'd
mean by the technically vague term "show" here.

>>>> As well, can you specify the FOL (meta) theory where this
>>>> "proving" would be in?
>>
>>> PRA would work fine.
>>
>> But how would anyone know that PRA is consistent in the first place?
>>
>
> It is almost universally accepted that the consistency of PRA is
> obvious.

I'm sorry. Being a guy who has been "grilled" with question such as
what is your definition of 'it's impossible to prove'" [and I did give
technical definition on that], you should explain the technical
definitions of "almost universally accepted" and "obvious", knowing
that inconsistency and consistency of formal systems has strictly
technical definitions, using formulas and rules of inference on them.

Fairness is fairness. I can't be the only person in a technical debate
who has to supply technical definitions of difficult terms such as "it's
impossible", while "orthodox" people like you, Aatu, MoeBlee, Federick,
use terms like "almost universally accepted", "obvious", "ordinary
mathematics", "informal reasoning", as if mathematical _logic_ is a
no man land (so to speak).

> Furthermore a theory considerably weaker than PRA will do,
> namely quantifier-free polynomial-time computable arithmetic. I don't
> think that even Edward Nelson has doubts about the consistency of this
> theory.

For the record, this is _NOT_ about doubting the consistency of PRA or
the like. It's about accepting the fact that we're _ASSUMING_ PRA or the
like _be_ consistent.

You would agree that _assumption is NOT proof_ would you not?

>>>> Which FOL (meta) theory did Godel use
>>>> to "prove" the undecidability of G(P) in his object theory P?
>>
>>> He used informal reasoning which was obviously finitistically
>>> acceptable. I think the definition of PRA came later; it would have
>>> then been obvious that the proof could be formalized in PRA.
>>
>> So, "informal reasoning" here is the same as "informal proof".
>>
>> Wouldn't you think it very much borderlines (at best) inconsistency
>> in argument, to attribute above that his proof is of _formal proof_
>> viz-a-viz PRA while here it's of the status of an _informal proof_ ?
>>
>> I mean you do agree that _formal proof is not informal proof_ right?
>>
>
> Yes, I do. I correctly stated that Gödel gives an informal argument in
> his paper which can be formalized in PRA (and also in quantifier-free
> polynomial-time computable arithmetic, which not even Nelson doubts to
> be consistent).

So, in the end and in essence Godel's proof is a formalized FOL proof,
in your opinion it seems. It's the _essence_ that we should care, imho.

>>>> If by "show" you didn't mean FOL "prove" as above, then
>>>> what did you mean by "show", or even "prove"?
>>
>>> When discussing mathematics, it's usually taken as a given that we
>>> know what "prove" means. That's what you're supposed to learn when you
>>> do a mathematics degree.
>>
>> Agree. So, to you, is Godel's proof an informal proof or a formal proof?
>> Please clarify for 100% certainty, since above you seem to have given 2
>> contradictory accounts.
>>
>
> The argument given in the paper is an informal argument, but it can be
> formalized. It would be in principle possible to convert it into a
> formal argument and check it by computer, and I believe that project
> is already underway.
>
> I did not give two contradictory accounts at all. What I said was
> perfectly consistent.

Let me put it in a succinct way: _the knowledge of the consistency_
of a formal system _is always an _informal knowledge_ . Period.

If you understand that point then you'd understand my point.

If you can't refute that point then you can't say I'm incorrect
in my analysis here.

There's no alternative, we having come this far.

So please acknowledge or refute this point here.

>>>> These are important clarifications that I think we'd need
>>>> to have so as we'd understand each other positions well
>>>> enough to continue the argument.
>>
>>> G�del gave an informal proof which is finitistically acceptable and
>>> can be formalized in PRA.
>>
>> So in mathematical logic the phrases "formalized proof" and
>> "informalized proof" would mean the same?
>>
>
> Of course not.

Right. So what are your definition of "formalized proof", and
"informalized proof"?

>
>> In any rate how do we know that PRA is consistent in the first place,
>> _without_ using any notion that would depend on the notion of the
>> natural number which you, MoeBlee, and Frederick (incorrectly) have
>> insisted Godel didn't use in his proof, despite Godel's own words
>> of requirement?
>>
>
> Hardly anyone has serious doubts about the consistency of PRA, and, as
> I observed, the argument will go through in quantifier-free polynomial-
> time computable arithmetic. Not even Nelson doubts the consistency of
> that theory. If you doubt the consistency of that theory, then of
> course you will regard all nontrivial mathematics as doubtful,
> including Gödel's argument.

Would you be able to give an example of an _invalid argument_ ?

(I'm claiming Godel's proof is an invalid argument).

>
> I never said that Gödel didn't use the notion of natural number in his
> proof, and I doubt anyone else did either.

Iirc, Frederick and MoeBlee believed truth and falshood of the naturals
weren't used by Godel, despite my giving the reference to where Godel
wrote it.

How could Godel possibly have _used_ "the notion of natural number"
_without_ truth or falsehood in (of) the naturals?

[Rupert]

> > I suggest you read G�del's paper; then you should be able to figure

> > out how to construct it yourself.
>
> I take your refusal to mean that you couldn't articulate what you'd
> mean by the technically vague term "show" here.
>

Where did I use the term "show"?

Given a specification of Turing machine which will accept precisely
the axioms of a given theory in the first-order language of
arithmetic, I do know how to construct a sentence in the first-order
language of arithmetic which expresses the assertion that the theory
is omega-consistent. I will do this for you if you specify such a
Turing machine and if you are willing to pay me for my valuable time
and effort. I suggest the best approach is for you to read Gödel's
paper. It contains the proof that it is always possible.

> >>>> As well, can you specify the FOL (meta) theory where this
> >>>> "proving" would be in?
>
> >>> PRA would work fine.
>
> >> But how would anyone know that PRA is consistent in the first place?
>
> > It is almost universally accepted that the consistency of PRA is
> > obvious.
>
> I'm sorry. Being a guy who has been "grilled" with question such as
> what is your definition of 'it's impossible to prove'" [and I did give
> technical definition on that], you should explain the technical
> definitions of "almost universally accepted" and "obvious", knowing
> that inconsistency and consistency of formal systems has strictly
> technical definitions, using formulas and rules of inference on them.
>
> Fairness is fairness. I can't be the only person in a technical debate
> who has to supply technical definitions of difficult terms such as "it's
> impossible", while "orthodox" people like you, Aatu, MoeBlee, Federick,
> use terms like "almost universally accepted", "obvious", "ordinary
> mathematics", "informal reasoning", as if mathematical _logic_ is a
> no man land (so to speak).
>

It's not a term with a technical definition. I'm just referring to the
fact that most people who know what is meant by the assertion "PRA is
consistent" would also regard it as an obvious truth. If you don't
regard it as obvious, that's fine. That means that just because an
assertion can be proved in PRA doesn't necessarily settle the question
of whether the assertion is true, for you. But you should at least
accept that it can indeed be proved in PRA.

> > Furthermore a theory considerably weaker than PRA will do,
> > namely quantifier-free polynomial-time computable arithmetic. I don't
> > think that even Edward Nelson has doubts about the consistency of this
> > theory.
>
> For the record, this is _NOT_ about doubting the consistency of PRA or
> the like. It's about accepting the fact that we're _ASSUMING_ PRA or the
> like _be_ consistent.
>

No, we're not. We're just showing that the argument Gödel gave can be
formalized in various formal theories. There is no need to assume that
these formal theories are consistent.

> You would agree that _assumption is NOT proof_ would you not?
>

If you prove a certain assertion in PRA, then that's a proof. If
someone later showed that PRA was inconsistent then you would probably
revise your view about the epistemological significance of the proof,
but it's still a proof.

>
>
>
>
>
>
>
>
> >>>> Which FOL (meta) theory did Godel use
> >>>> to "prove" the undecidability of G(P) in his object theory P?
>
> >>> He used informal reasoning which was obviously finitistically
> >>> acceptable. I think the definition of PRA came later; it would have
> >>> then been obvious that the proof could be formalized in PRA.
>
> >> So, "informal reasoning" here is the same as "informal proof".
>
> >> Wouldn't you think it very much borderlines (at best) inconsistency
> >> in argument, to attribute above that his proof is of _formal proof_
> >> viz-a-viz PRA while here it's of the status of an _informal proof_ ?
>
> >> I mean you do agree that _formal proof is not informal proof_ right?
>

> > Yes, I do. I correctly stated that G�del gives an informal argument in

> > his paper which can be formalized in PRA (and also in quantifier-free
> > polynomial-time computable arithmetic, which not even Nelson doubts to
> > be consistent).
>
> So, in the end and in essence Godel's proof is a formalized FOL proof,
> in your opinion it seems. It's the _essence_ that we should care, imho.
>

It can be formalized, yes.

>
>
>
>
>
>
>
>
> >>>> If by "show" you didn't mean FOL "prove" as above, then
> >>>> what did you mean by "show", or even "prove"?
>
> >>> When discussing mathematics, it's usually taken as a given that we
> >>> know what "prove" means. That's what you're supposed to learn when you
> >>> do a mathematics degree.
>
> >> Agree. So, to you, is Godel's proof an informal proof or a formal proof?
> >> Please clarify for 100% certainty, since above you seem to have given 2
> >> contradictory accounts.
>
> > The argument given in the paper is an informal argument, but it can be
> > formalized. It would be in principle possible to convert it into a
> > formal argument and check it by computer, and I believe that project
> > is already underway.
>
> > I did not give two contradictory accounts at all. What I said was
> > perfectly consistent.
>
> Let me put it in a succinct way: _the knowledge of the consistency_
> of a formal system _is always an _informal knowledge_ . Period.
>
> If you understand that point then you'd understand my point.
>

I don't understand was is meant by "informal knowledge".

> If you can't refute that point then you can't say I'm incorrect
> in my analysis here.
>

Remind me what your analysis is, and I'll let you know whether I think
I'm in a position to say it's incorrect.

> There's no alternative, we having come this far.
>
> So please acknowledge or refute this point here.
>

I don't know what "informal knowledge" means.

> >>>> These are important clarifications that I think we'd need
> >>>> to have so as we'd understand each other positions well
> >>>> enough to continue the argument.
>
> >>> G�del gave an informal proof which is finitistically acceptable and
> >>> can be formalized in PRA.
>
> >> So in mathematical logic the phrases "formalized proof" and
> >> "informalized proof" would mean the same?
>
> > Of course not.
>
> Right. So what are your definition of "formalized proof", and
> "informalized proof"?
>

For the definition of "formalized proof", see a textbook in
mathematical logic. "Informal proof" is a concept which we learn by
acquaintance with various specific examples, when we undergo
mathematical training.

>
>
> >> In any rate how do we know that PRA is consistent in the first place,
> >> _without_ using any notion that would depend on the notion of the
> >> natural number which you, MoeBlee, and Frederick (incorrectly) have
> >> insisted Godel didn't use in his proof, despite Godel's own words
> >> of requirement?
>
> > Hardly anyone has serious doubts about the consistency of PRA, and, as
> > I observed, the argument will go through in quantifier-free polynomial-
> > time computable arithmetic. Not even Nelson doubts the consistency of
> > that theory. If you doubt the consistency of that theory, then of
> > course you will regard all nontrivial mathematics as doubtful,

> > including G�del's argument.

>
> Would you be able to give an example of an _invalid argument_ ?
>

All great apes evolved from the lower life forms.
Homo sapiens evolved from the lower life forms.
Therefore homo sapiens is a great ape.

> (I'm claiming Godel's proof is an invalid argument).
>

Perhaps you should provide some evidence for your contention.

>
>
> > I never said that G�del didn't use the notion of natural number in his

> > proof, and I doubt anyone else did either.
>
> Iirc, Frederick and MoeBlee believed truth and falshood of  the naturals
> weren't used by Godel, despite my giving the reference to where Godel
> wrote it.
>

They correctly observed that Gödel makes no use of semantic notions in
the main part of his argument.

> How could Godel possibly have _used_ "the notion of natural number"
> _without_ truth or falsehood in (of) the naturals?
>

I don't see the problem.

[LudovicoVan]

"Rupert" <rupertm...@yahoo.com> wrote in message
news:1a22a307-17c8-4159...@m4g2000yqb.googlegroups.com...

> On Oct 25, 6:35 am, Nam Nguyen <namducngu...@shaw.ca> wrote:

<snip>

>> How could Godel possibly have _used_ "the notion of natural number"
>> _without_ truth or falsehood in (of) the naturals?
>
> I don't see the problem.

Not that I claim to understand what point is made (my bad), but it is true
that we need a *notion* of the counting numbers before we can even begin the
whole adventure.

-LV

[Frederick Williams]

Nam Nguyen wrote:
>
> On 24/10/2012 4:44 PM, Frederick Williams wrote:

> >
> > Indeed so, I had supposed we were heading for 'Since models are used in
> > the group case, G\"odel must have used models in his case.'
>
> Right. We're _heading_ that way.
>
> But first I'm waiting for Moeblee to confirm if indeed in the case
> of the theory S above (Shoenfield called it G), language-structure
> theoretical means (truth/falsehood) would be _the only available mean_
> to "prove" the undecidability of Axy[x*y = y*x].

I will respond to your reply to Moe Blee.

[Frederick Williams]

Nam Nguyen wrote:
>
> On 24/10/2012 4:07 PM, MoeBlee wrote:
> > On Oct 24, 4:44 pm, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:
> >> Nam Nguyen wrote:
> >
> >>> For instance, how would you prove, as a _pure_ FOL theorem, that the
> >>> commutativity of a group is undecidable in the FOL simple-group theory?
> >>
> >> Do you mean, how would you prove that neither
> >>
> >> First order theory of groups |- all groups are commutative
> >>
> >> nor
> >>
> >> First order theory of groups |- there exists a non commutative group
> >
> > Though what he posted came out differently, maybe what he has in mind
> > is this:
> >
> > Prove (where 'S' stands for the axioms of the first order theory of
> > groups):
> >
> > It's not the case that S |- Axy x*y = y*x
> > and
> > it's not the case that S |- ~Axy x*y = y*x
> >
> > However, it's still not clear what non-logical axioms he allows to be
> > used in making such a proof.
>
> As you've mentioned above, it's the first order finitely axiomatizable
> theory of group, which Shoefield axiomatized with 2 axioms G1, G2 on
> page 22. (Let's denote this theory as G).

The question is not how does Nam prove things in first order group
theory (G), but rather how does he prove things about G? Specifically,
how does he prove

It's not the case that G |- Axy x*y = y*x

and

it's not the case that G |- ~Axy x*y = y*x ?

> >
> > Anyway, I would GUESS his point is that it's with models that we would
> > make the proof. That is, show a group (a model of S) that is
> > commuative and show a group (a model of S) that is not commutative,
> > and we're done.
>
> Exactly.
>
> Now .... we're not there yet here with Godel's proof you mentioned
> below.
> >
> > My reply earlier was that the fact that certain independence proofs
> > use models doesn't entail that Godel's proof of the indepencdence of
> > the sentence G from the axioms of P uses models.
>
> Before we go further on the above, please do confirm if it's your
> understanding that in the case of G, _the only possible way to prove_
> _the undecidability_ of Axy[x*y = y*x] in this case of G is through
> _model-theoretical proofs_ (using truth, falsehood).

How would one know that the only possible way to prove something is by
some particular means? Just because the incompleteness of G is proved
by exhibiting models and showing that Axy[x*y = y*x] is true in one
model and false in another, does not mean that there is no other way.

> <Note>
>
> Please bear in mind that here:
>
> (a) bt decidability of F in T I do mean:
>
> (T |- F) or (T |- ~F)
>
> (b) by undecidability of F in T I do mean:
>
> NEG(T |- F) and NEG(T |- ~F)
>
> </Note>
>
> > If Nguyen wants to
> > claim that Godel's proof does use models then it's up to Nguyen to
> > show where models are used in the proof. He just doesn't seem to get
> > (or want to find out for himself) that Godel's proof is syntactic, not
> > model theoretic.

--

[Frederick Williams]

Here they are, Ludo:

0, f0, ff0, fff0, and so on.

No mention of truth or falsity. f is G\"odel's name for the successor
function.

[Frederick Williams]

Nam Nguyen wrote:

> In any rate, could you [Aatu Koskensilta] please help refreshing my memory if you agreed

> or said sometimes before that - up to a limit - it's really up to each
> individual to _know_ what the natural numbers be, especially w.r.t.
> the truth value of the formula cGC.

Here's a question for you:

Have you ever read G\"odel's paper?" Take that to mean in English
translation, if you wish. Well, have you?

[LudovicoVan]

"Frederick Williams" <freddyw...@btinternet.com> wrote in message
news:50893362...@btinternet.com...

> LudovicoVan wrote:
>> "Rupert" <rupertm...@yahoo.com> wrote in message
>> news:1a22a307-17c8-4159...@m4g2000yqb.googlegroups.com...
>> > On Oct 25, 6:35 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> <snip>
>>
>> >> How could Godel possibly have _used_ "the notion of natural number"
>> >> _without_ truth or falsehood in (of) the naturals?
>> >
>> > I don't see the problem.
>>
>> Not that I claim to understand what point is made (my bad), but it is
>> true
>> that we need a *notion* of the counting numbers before we can even begin
>> the
>> whole adventure.
>
> Here they are, Ludo:
>
> 0, f0, ff0, fff0, and so on.
>
> No mention of truth or falsity. f is G\"odel's name for the successor
> function.

Yes my friend, but that is already formal. It remains true that a notion of
counting is a pre-requisite to any mathematical adventure, formal or
informal: to even *think* structures or constructions or processes, etc. In
fact, for all I can understand of Nam's point, my reply would be that those
counting numbers are in fact not the same as the natural numbers in Goedel's
formalization: but then the technical details of where to locate the truths
of what quite escape me.

-LV

[MoeBlee]

On Oct 24, 10:09 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> On 24/10/2012 4:07 PM, MoeBlee wrote:

> > My reply earlier was that the fact that certain independence proofs
> > use models doesn't entail that Godel's proof of the indepencdence of
> > the sentence G from the axioms of P uses models.

Instead of addressing that point, you prolong by asking me yet another
question:

> Before we go further on the above, please do confirm if it's your
> understanding that in the case of G, _the only possible way to prove_
> _the undecidability_ of Axy[x*y = y*x] in this case of G is through
> _model-theoretical proofs_ (using truth, falsehood).

Before we go further on the above, please tell me why I need to answer
this question. Whatever my answer, how will it bear on the fact that
Godel did not use model theoretic methods to prove that if P is omega-
consistent then P is incomplete?

I've answered probably literally hundreds of questions for you over
the years. I don't see the sense of it. If you have some point you
want to make, then go ahead and make it; you don't need me first to
confrim this or that.

Meanwhile, questions for you that you've not answered:

1. Why do you think you're continually in protracted arguments about
basic technical matters with people who are well informed in the
subject?

2. Why won't you read Godel's incompleteness proof so that you can see
that he doesn't use model-theoretic methods to prove that if P is
omega-consistent then P is incomplete?

But wait, I'll answer your question anyway, though I should say I
should resist letting you make this into a continual quiz - one
question after another - while instead it is up to YOU to point out
where exactly in Godel's proof of "P is omega consistent then P is
incomplete" there is use of model theoretic methods.

As to your question:

First, by "prove", what axioms and rules (or principles, if informal
proof) do you have in mind? Obviously, trivially, I can make a proof
by adopting "commutativity is independent of group theory" as an
axiom. But that's not satifsfying, so you need to say what system I am
allowed for making such a proof.

Second, if we mean formal proof, there's even a question of how to
formalize "without model-theoretic methods".

Third, supposing we have setttled on what axioms and rules are
allowed, I still might not know whether or not it is possible to prove
the independence of commutativity from the first order group axioms by
means other than model-theoretically. I can't at the moment think of a
"reasonable" system that proves the independence of commutativity from
the first order group axoms, but my inability to think of a system or
proof does not entail they don't exist.

Fourth, suppose, for purpose of discussion, we assume that there is no
"reasonable" (e.g., not just adopting what is to be proven as itself
an axiom) proof of the independence of commutativity, then so what? It
would still not entail that it's not possible to prove "if P omega
consistent then P incomplete" without model theoretic methods.

So answer my question please:

Given what I've said about this, what is the point of your question?

And, again, why do you think you're continually in protracted
arguments about basic technical matters with well informed posters?

And why won't you read Godel's proof?

Like I said:

> > If Nguyen wants to
> > claim that Godel's proof does use models then it's up to Nguyen to
> > show where models are used in the proof. He just doesn't seem to get
> > (or want to find out for himself) that Godel's proof is syntactic, not
> > model theoretic.

Please respond to that.

MoeBlee

[MoeBlee]

> > I suggest you read G�del's paper; then you should be able to figure

> > out how to construct it yourself.
>
> I take your refusal to mean that you couldn't articulate what you'd
> mean by the technically vague term "show" here.
>
> >>>> As well, can you specify the FOL (meta) theory where this
> >>>> "proving" would be in?
>
> >>> PRA would work fine.
>
> >> But how would anyone know that PRA is consistent in the first place?
>
> > It is almost universally accepted that the consistency of PRA is
> > obvious.
>

> Being a guy who has been "grilled" with question such as
> what is your definition of 'it's impossible to prove'"

The matter I recall was your claim to have a technical definition of
"impossible to KNOW". YOU kept referring to an impossibility of
KNOWING. Meanwhile, as to "impossible to prove", as long as you have a
certatin system of proof in mind, then I would take "impossible to
prove" as merely "there does not exist a proof" and I would not have
hassled you for a definition. But "impossible to KNOW", yes, if you
claim to have a technical definition, then I will ask you for it.

> you should explain the technical
> definitions of "almost universally accepted" and "obvious",

He's not claiming that they're technical.

> Fairness is fairness.

YOU claimed to have a technical definition "impossible to know" so
it's fair to ask you for your technical defintion. Rupert does NOT
claim that "almost universally accepted" and "obvious" are technical.

>"orthodox" people like you, Aatu, MoeBlee, Federick,
> use terms like "almost universally accepted", "obvious", "ordinary
> mathematics", "informal reasoning", as if mathematical _logic_ is a
> no man land (so to speak).

I never claimed they're technical terms.

And what do you mean by "orthodox"?

> > Furthermore a theory considerably weaker than PRA will do,
> > namely quantifier-free polynomial-time computable arithmetic. I don't
> > think that even Edward Nelson has doubts about the consistency of this
> > theory.
>
> For the record, this is _NOT_ about doubting the consistency of PRA or
> the like. It's about accepting the fact that we're _ASSUMING_ PRA or the
> like _be_ consistent.

We don't have to assume it's consistent. Rather, the main point is
that these systems do prove incompleteness. If you doubt the
consistency of these systems then no one is saying you must assume
them consistent.

But, if you materially doubt the consistency of PRA or even the system
Rupert mentioned, then what system do you NOT materially doubt?

> > Yes, I do. I correctly stated that G�del gives an informal argument in

> > his paper which can be formalized in PRA (and also in quantifier-free
> > polynomial-time computable arithmetic, which not even Nelson doubts to
> > be consistent).
>
> So, in the end and in essence Godel's proof is a formalized FOL proof,
> in your opinion it seems. It's the _essence_ that we should care, imho.

Why are you not understanding this? Godel's own presentation is
informal, but it can be formalized, and, by reading a book in
mathematical logic, you could see for yourself how one would formalize
it

>
> >> Agree. So, to you, is Godel's proof an informal proof or a formal proof?
> >> Please clarify for 100% certainty, since above you seem to have given 2
> >> contradictory accounts.
>
> > The argument given in the paper is an informal argument, but it can be
> > formalized. It would be in principle possible to convert it into a
> > formal argument and check it by computer, and I believe that project
> > is already underway.
>
> > I did not give two contradictory accounts at all. What I said was
> > perfectly consistent.
>
> Let me put it in a succinct way: _the knowledge of the consistency_
> of a formal system _is always an _informal knowledge_ . Period.

Putting aside what you mean by "informal knowledge", you asked Rupert
a question, and he answered it, and you've not shown anything wrong
with his answer.

> If you understand that point then you'd understand my point.
>
> If you can't refute that point then you can't say I'm incorrect
> in my analysis here.

Whatever your "analysis" is here, you've not shown anything wrong with
Rupert's reply.

> There's no alternative, we having come this far.
>
> So please acknowledge or refute this point here.

Please acknowledge Rupert's reply to your question. Please acknowledge
that you've not read Godel's paper, and say why you won't read it.
Please acknowledge that, along the lines I mentioned in another
thread, here you are yet again in a protracted disagreement about a
basic technical question (Godel's proof this time) with a well
informed poster (Rupert this time), and please say why you think that
is continually the case.

> So what are your definition of "formalized proof", and
> "informalized proof"?

Oh come on. This has been gone over and over and over in sci.logic for
years. Pick up a book in mathematical logic and read it.

>

> >> In any rate how do we know that PRA is consistent in the first place,
> >> _without_ using any notion that would depend on the notion of the
> >> natural number which you, MoeBlee, and Frederick (incorrectly) have
> >> insisted Godel didn't use in his proof, despite Godel's own words
> >> of requirement?
>
> > Hardly anyone has serious doubts about the consistency of PRA, and, as
> > I observed, the argument will go through in quantifier-free polynomial-
> > time computable arithmetic. Not even Nelson doubts the consistency of
> > that theory. If you doubt the consistency of that theory, then of
> > course you will regard all nontrivial mathematics as doubtful,

> > including G�del's argument.

>
> Would you be able to give an example of an _invalid argument_ ?

Would you please stop popping irrelevant quiz questions for people
when you're not able to adequately respond to their quite reasonable
points?

> (I'm claiming Godel's proof is an invalid argument).

Really? Oh, please DO tell... Suggestion though: First actually READ
the proof.

> Iirc, Frederick and MoeBlee believed truth and falshood of  the naturals
> weren't used by Godel, despite my giving the reference to where Godel
> wrote it.

No, I never said such a thing. I never said it because I don't even
know what one would mean by "truth and falsehood of the naturals".

MoeBlee

[Frederick Williams]

Charlie-Boo wrote:
>
> On Oct 19, 4:29 pm, Frederick Williams <freddywilli...@btinternet.com>
> wrote:
> > Charlie-Boo wrote:
> >
> > > On Oct 19, 3:26 pm, Frederick Williams <freddywilli...@btinternet.com>
> > > wrote:
> > > > Charlie-Boo wrote:
> >
> > > > > [...] After all, Godel theorem wouldn t be a
> > > > > theorem if Godel had not proven that G is true (and unprovable in PA.)
> >
> > > > Not so, what G\"odel's theorem shows is that there is a G such that P
> > > > (G\"odel's name for his theory) does not prove G and also P does not
> > > > prove ~G. There is no need to establish that G is true.
> > > same difference
> >
> > > (Actually, can you do that - not prove G is true first?)
> >
> > The truth of G, or any other formula, needn't even be mentioned.
>
> Although he does:
>
> "From the remark that [R(q); q] asserts its own unprovability, it
> follows at once that
> [R(q); q] is correct, since [R(q); q] is certainly unprovable (because
> undecidable). So the
> proposition which is undecidable in the system PM yet turns out to be
> decided by
> metamathematical considerations."

Yes, G\"odel showed that G (if that's what we're calling it) is true.
But in his ***proof*** that

Neither P |- G nor P |- ~G.

G\"odel didn't mention the truth or falsity of G or ~G. His proof was
entirely syntactic.

I'm wondering: just suppose that someone has drawn Professor
Wildberger's attention to the Usenet post that mentions him, and just
suppose he's working his way through the thread, and just suppose he's
reading Nam's contributions. The poor man's head must be spinning.

[Frederick Williams]

Nam Nguyen wrote:

>
> So what does it mean to you to prove F is undecidable in T, _without_
> mentioning the notion of model-theoretical truth or falsehood?
>

> For instance, how would you prove, as a _pure_ FOL theorem, that the
> commutativity of a group is undecidable in the FOL simple-group theory?

So what you mean is

The first order theory of groups is incomplete, in particular
(forall x, y)(x*y = y*x) is not a theorem of it. How would
you [Moe Blee] prove that?

If I were answering, I'd say:

By the completeness of first order logic, and since the first order
theory of groups is finitely axiomatized,

G |- phi iff G |= phi

where G is the conjunction of the axioms of the first order theory of
groups. So

not-(G |- phi) iff not-(G |= phi).

To prove not-(G |= phi) we need a model of G that is not a model of
phi. If phi is

(forall x,y)(x*y = y*x)

then the dihedral group D_3 will do.

But I haven't proved

not-(G |- (forall x,y)(x*y = y*x))

"as a _pure_ FOL theorem" to use your words. To prove

not-(G |- (forall x,y)(x*y = y*x))

would one need at least a rudimentary theory of sets (which could be
coded in a simple arithmetic)? Clearly (for |-) a notion of sequence of
arbitrary finite length is needed. G\"odel's beta function could be
used, but there is no point in considering the details because pure FOL
won't do.

[Frederick Williams]

Nam Nguyen wrote:

>
> Iirc, Frederick and MoeBlee believed truth and falshood of the naturals
> weren't used by Godel, despite my giving the reference to where Godel
> wrote it.

I don't know what 'truth of the naturals' means, ditto 'fals[e]hood of
the naturals'. I do know what 'truth in the structure with universe the
naturals and ...' means; and if G\"odel used such a concept *in his
proof*, please give a reference. I don't doubt that G\"odel mentioned
truth/falsehood *in his paper*.

> How could Godel possibly have _used_ "the notion of natural number"
> _without_ truth or falsehood in (of) the naturals?

Easily, had he wanted to, he might have written:

The natural numbers are the denotations of 0, f0, ff0, ...

He might even have written

The natural numbers are 0, f0, ff0, ...

using the same thing both as a symbol and as the thing symbolized.

[Nam Nguyen]

On 25/10/2012 12:27 PM, Frederick Williams wrote:
> Nam Nguyen wrote:
>
>>
>> Iirc, Frederick and MoeBlee believed truth and falshood of the naturals
>> weren't used by Godel, despite my giving the reference to where Godel
>> wrote it.
>
> I don't know what 'truth of the naturals' means, ditto 'fals[e]hood of
> the naturals'. I do know what 'truth in the structure with universe the
> naturals and ...' means; and if G\"odel used such a concept *in his
> proof*, please give a reference. I don't doubt that G\"odel mentioned
> truth/falsehood *in his paper*.

What do you think Godel meant by his "false propositions"?
And you don't understand that if a statement (proposition) P
is false then ~P is true?

I got it: you (and MoeBlee) were ignorant of the fact that P is true
or false here when Godel wrote it means true or false in the natural
numbers. Please see the quoted below.

>
>> How could Godel possibly have _used_ "the notion of natural number"
>> _without_ truth or falsehood in (of) the naturals?
>
> Easily, had he wanted to, he might have written:
>
> The natural numbers are the denotations of 0, f0, ff0, ...
>
> He might even have written
>
> The natural numbers are 0, f0, ff0, ...
>
> using the same thing both as a symbol and as the thing symbolized.

You have no idea what you're talking about.

Godel required that his object formal system T be such that its
arithmetical ( _theorem_ ) statements must be _true_ :

"provided that thereby no false propositions of the kind described
in footnote 4 become provable".

Note, again, the phrases: "no false propositions", "footnote 4",
and "become provable".

Please go and read that portion of his paper carefully because it'd
give you some clue how he'd use the Omega Consistency stipulation.

Without the above requirement that I quoted from his writing, the Omega
Consistency stipulation, in fact the assumed consistency of T, would be
useless; and we would have never heard of the word "Incompleteness"!

[LudovicoVan]

"Frederick Williams" <freddyw...@btinternet.com> wrote in message

news:50897532...@btinternet.com...

<http://jacqkrol.x10.mx/assets/articles/godel-1931.pdf>

<< For the proof of Gödel's 'Unprovability' Theorem the importance of
recursiveness lies in the fact (Proposition V, p. 55) that every statement
of a recursive relationship holding between given numbers x1, x2, . . . xn
is expressible by a formula f of the formal system P which is 'provable'
within P if the statement is true and 'disprovable' within P (i.e. the
'negation' of f, written as Neg f, is 'provable' within P) if the statement
is false. [...] Consequently any proposition about them is expressible in
P by a formula which is 'provable' or 'disprovable' according as the
proposition is true or false. >>

<< This formula [Goedel's sentence], and of course each of the abbreviations
of it, may be regarded as expressing the proposition that the formula itself
is 'unprovable', i.e. the formula expresses its own 'unprovability'. >>

In fact, how do we know that Goedel's sentence _expresses_ its own
unprovability? Isn't that (our interpretation?) crucial to the conclusion.

-LV

[Frederick Williams]

LudovicoVan wrote:

>
> In fact, how do we know that Goedel's sentence _expresses_ its own
> unprovability?

It doesn't. That is only an informal way of putting it. The G\"odel
sentence is a sentence of number theory and can say nothing about
anything except numbers, addition and multiplication.

[Frederick Williams]

Nam Nguyen wrote:

>
> I got it: you (and MoeBlee) were ignorant of the fact that P is true
> or false here when Godel wrote it means true or false in the natural
> numbers. Please see the quoted below.

I do not deny that G\"odel used the words true and false in his paper,
but they have no relevance to the proof of the incompleteness theorem.
There is more in that paper than the proof. The proof is in section 2.

> Godel required that his object formal system T be such that its
> arithmetical ( _theorem_ ) statements must be _true_ :
>
> "provided that thereby no false propositions of the kind described
> in footnote 4 become provable".
>
> Note, again, the phrases: "no false propositions", "footnote 4",
> and "become provable".
>

> Please go and read that portion of his paper carefully [...]

I suggest you read the whole of his paper carefully. Have you read it?
No.

[MoeBlee]

On Oct 25, 6:04 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:

> I got it: you (and MoeBlee) were ignorant of the fact that P is true
> or false here when Godel wrote it means true or false in the natural
> numbers.

No, it's been explained to you over and over and over that I know that
Godel that mentions that G is true, but that mention is not itself
part of the proof that if P is omega-consistent then P is incomplete.

> Godel required that his object formal system T be such that its
> arithmetical ( _theorem_ ) statements must be _true_ :

No, the particular system he discusses is P and for proving P
incomplete he requires that P is omega-consistent. He does not require
that the thoerems of P be true.

>    "provided that thereby no false propositions of the kind described
>     in footnote 4 become provable".

You left off what goes before this so that it makes sense. Here's more
of the quote:

"These two systems [PM and ZF] are so extensive that all methods of
proof used in mathematics today have been formalized in them, i.e.
reduced to a few axioms and rules of inference. It may therefore be
surmised that these axioms and rules of inference are also sufficient
to decide all mathematical questions which can in any way at all be
expressed formally in the systems concerned. It is shown below that
this is not the case, and that in both the systems mentioned there are
in fact relatively simple problems in the theory of ordinary whole
numbers which cannot be decided from the axioms. This situation is not
due in some way to the special nature of the systems set up, but holds
for a very extensive class of formal systems, including, in
particular, all those arising from the addition of a finite number of
axioms to the two systems mentioned, provided that thereby no false

propositions of the kind described in footnote 4 become provable."

There is nothing in that quote that contradicts that in the proof
Godel actually makes, he does not use model-theoretic methods or
require of system P that its theorems are true rather than merely that
system P is omega-consistent.

All he says there is that if no false theorems (of a certain kind)
result from an extension of PM or ZF then the extended theory also is
incomplete. He does NOT say that to prove the incompleteness of P he
must assume that all theorems of P are true.

If you claim that Godel does use model theoretic methods to show that
if P is omega-consisent then P is incomplete, then show the exact
steps in the proof where you claim model theoretic methods are used.

MoeBlee