Re: Godel's comments about the "true reason" for incompleteness

On Mar 28, 8:49 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
On 2008-03-26, in sci.logic, R. Srinivasan wrote:

Which is what we have been arguing as not provable in PA without any
coding and which, in my view, means the *same* thing as:

PA proves "For each P, Pv~P".        (3)

It appears then, that by "PA proves 'For each P, P or not-P'" you mean
nothing more than that PA proves that for every formula P, there
exists a certain sequence of formulas that is a formal proof of 'P or
not-P' using no non-logical axioms. This is a rather curious
formulation since on ordinary usage "For each P, either P or not-P"
does not mean anything to do with sequences of formulas.

Not sure what you mean by "ordinary usage." But in ordinary usage
"there exists a certain sequence of formulas that is a formal proof of
'P or not-P' " implies P v ~P.


What syntactical fact does (3) express? In my view, it expresses
that PA proves itself free of any contradictions.

The existence of a formal derivation of "P or not-P" for every P is
not in any obvious sense equivalent to the non-existence of a formal
derivation of, say, "0=1" in PA, what we would ordinarily take to be
the content of the claim that PA is consistent.

--
Aatu Koskensilta (aatu.koskensi...@xxxxxxxxx)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

.

Relevant Pages