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

On Mar 29, 7:30 am, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:
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,

Is this really provable

(Ex)(Prov(x,#P) -> P ?

By "Prov" you mean first-order predicate logic as opposed to PA?

for example, but not in ACA_0 -- or in
technicalese, PA is reflexive but ACA_0 is not.

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

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

.

Relevant Pages
Loading