From: Nam Nguyen on
Daryl McCullough wrote:
> Newberry says...
>
>> If it absolutely certain that PA is consistent why don't we formalize
>> the reasoning?
>
> It has been. It's easily formalized in ZFC.

But PA's consistency itself and the proof of PA's consistency in ZFC
are 2 different and independent issues. (There's a chance ZFC could be
syntactically inconsistent and in which case it'd prove anything).
From: Nam Nguyen on
Newberry wrote:
> On Apr 2, 7:00 am, Nam Nguyen <namducngu...(a)shaw.ca> wrote:
>> Daryl McCullough wrote:
>>> Newberry says...
>>>> On Apr 1, 5:59=A0am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>>>>> How do I know that Peano arithmetic is consistent? I know it the way I
>>>>> know any mathematical theorem I have personally proved.
>>>> You proved PA consistent?
>>> It's easy to prove in ZF.
>> Is ZF _syntactically_ consistent?
>
> Such a proof in ZF that PA is consistent is obviously wothless. We had
> a long discussion about this a while ago.

Ultimately inconsistency proof is just 1st order _syntactical & finite_
proof, while consistency is neither syntactical nor finite: it's a meta
proof requiring knowledge of FOL, subjective intuitions about "truth",
about the natural numbers, or all of those.

But in pursuing consistency proof in general, we tend not to realize a
*subtle* relationship between intuition, truth, and syntactical proof.
We often say a formula is a theorem iff there's a "finite" proof for it.
But that isn't quite precise; it should be:

"iff there's a _non-zero_ finite proof for it"!

The distinction is necessary because intuition would still accept the
following scenarios as valid:

1. - There's a proof which is of non-zero finite length. (This would be
a typical proof).
2. - All proofs are of the zero finite length. This would correspond to
to there's no proof!
3. - There's no proof of non-zero finite length length, but intuition
might perceive a proof of infinite length!

This is a enigma in reasoning: on the one hand intuition could have
reason to believe the underlying concept _might be_ sound, but on the
other hand neither the concept or its negation can be a syntactical
theorem of FOL!

So, if a "proof" falls into the 3rd category, the underlying formula
would be neither true nor false, model-theoretically speaking or otherwise!
And non-relative consistency "proofs" would fall into this 3rd category.
From: Newberry on
On Apr 2, 3:19 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote:
> Newberry says...
>
>
>
> >On Mar 31, 5:12=A0am, stevendaryl3...(a)yahoo.com (Daryl McCullough)
> >wrote:
> >> In general, any *procedure* used to evaluate the truth of sentences
> >> in a self-referential language is incomplete, in the sense that there
> >> are true sentences that are not evaluated as true by the procedure.
>
> >> This is easy to see: Let P be some procedure to evaluate the truth
> >> of sentences. Then consider the sentence
>
> >> "When procedure P is applied to this sentence, the result is not true"
>
> >And what procedure would it be?
>
> Well, for example, the search for a proof for the statement. Or
> Gaifman's procedure.
>
> >It cannot be Gaifman's procedure because the sentence above does
> >not have the form "The sentence written in/on ... is true"
>
> Then, as I said, it's a true sentence that Gaifman's procedure does
> not return true for.

Gaifman's procedure is not applicable. It cannot take your sentence as
an argument.

>
> --
> Daryl McCullough
> Ithaca, NY

From: Newberry on
On Apr 3, 6:54 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote:
> Newberry says...
>
> >If it absolutely certain that PA is consistent why don't we formalize
> >the reasoning?
>
> It has been. It's easily formalized in ZFC.

I do not know why we are going through this circle again.

Look it is very simple. All you have to do is to divorce

~(Ex)(Ey)(Pxy & Qy) (1)

from

~(Ex)Pxm (2)

[No need to repeat that m is the Goedel number of (1).] Then there is
no reason why (2) could not be proven.

> --
> Daryl McCullough
> Ithaca, NY

From: Daryl McCullough on
Newberry says...
>
>On Apr 3, 6:54=A0am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote:
>> Newberry says...
>>
>> >If it absolutely certain that PA is consistent why don't we formalize
>> >the reasoning?
>>
>> It has been. It's easily formalized in ZFC.
>
>I do not know why we are going through this circle again.
>
>Look it is very simple. All you have to do is to divorce
>
>~(Ex)(Ey)(Pxy & Qy) (1)
>
>from
>
>~(Ex)Pxm (2)
>
>[No need to repeat that m is the Goedel number of (1).] Then there is
>no reason why (2) could not be proven.

It can be proven. Just not in PA.

--
Daryl McCullough
Ithaca, NY