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

On 2008-03-29, in sci.logic, Newberry wrote:
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.

Implies in what sense? Since P or not-P is a classical logical truth
for any P, it is materially implied by any statement. You have perhaps
in mind the following principle

if P is provable in first-order predicate logic then P

where P is a sentence in the relevant first-order language. This is a
mathematical result provable in some theories and unprovable in
some. It's provable in PA, for example, but not in ACA_0 -- or in
technicalese, PA is reflexive but ACA_0 is not.

--
Aatu Koskensilta (aatu.koskensilta@xxxxxxxxx)

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

Relevant Pages