Prev: Continuity and Uncountability
Next: instructor solution manual for Fundamentals of Corporate Finance 9th edition by Ross
From: David Libert on 8 Jul 2010 00:25
Nam Nguyen (namducnguyen(a)shaw.ca) writes:
> Aatu Koskensilta wrote:
>> Nam Nguyen <namducnguyen(a)shaw.ca> writes:
>>
>>> MoeBlee wrote:
>>>
>>>> And, in that regard, I have said all along that there is no
>>>> finitistic proof of the consistency of PA.
>>> So you've agreed that there's no formal proof for PA's consistency and that
>>> if you go by formal proof only then you don't have knowledge of PA's
>>> consistency.
>>
>> There are many formal proofs of the consistency of PA. None of them are
>> finitistic.
>
> So it doesn't seem you used the phrase "formal proof" in the standard
> way that textbook (e.g. Shoenfield's) would use. In that standard
> usage, a formal proof is a (finite) syntactical proof of a FOL formal
> system theorem.
>
> Given that standard definition of "formal proof", would you agree with
> my statement above that:
>
> >> there's no formal proof for PA's consistency and that if you go by
> >> formal proof only then you don't have knowledge of PA's consistency.
>
> ?


This discussion seems to me to be reducing to what people often call
(in common language, not the technical logical sense), semantics, ie
definitions of words. Namely what do we mean by "know" or
"really know" or "formal proof" .

My edition of Shoenfield is copyright 1967. All page numbers I reference
below are for that edition.

On page 4 Shoenfield defines the theorems of a formal system, namely
the usual involving axioms and rules and conclusion.

Earlier on this same page 4 he defines a formal system as havin axioms and
rules of inference. This simply says axioms, with no further specification.

On page 22 Shoenfield writes:

"We can now define the class of formal systems which we are going to study.
A first-order theory, or simply a thoery, is a formal stysten T such that

i) the language of T us a first order language;

ii) the axioms of T are the logical axioms of L(T) and certain further axioms,
called the nonlogical axioms;"


There is a iii) I omot about rules of inference.

An important part of logic is to be able to have applied theories.

If all we ever did with logic was pure logic, all we could talk avout is =
and substitution instances of propostional logic on other predicates.

And indeed, Shoenfield like any other logic book spends a lot of time discussing
applied theories.

So Shoenfield talked about theorems for formal theories, and later he spelled
out these formal theories include nonlogical axioms.

And this is what I have always understood to be the standard definition,
not just Shoenfield but every text and every course I have seen.

A formal proof is a sequence of statements with the conclusion at the end,
every statement following from previous statements by a rule of inference,
or being an axiom, an axiom being a logical axiom or a nonlogical axiom.

If you think that formal proofs must only be in pure logic, and all you are
telling us is pure logic does not prove Con(PA), all of us I am sure have
known that for years. I do know that I have.

For myself, and I think a reasonable reading of the pther people here,
we never meant to be claiming that pure logic has a formal proof of Con(PA).

Instead we regard Con(PA) as accepted by the normal canons of mathematics,
and many of us, including me, feel that ZFC or ZF or whatever is one reasonable
codification of that.

We say we consider that we know Con(PA) as a mathematical statement by the
normal standards of mathematical knowledge, and this fact itself can be
illuminated by ZF |- Con(PA).

And ZF provability is by a first order applied system, as Shoenfield
discusses. In fact on page 239 he evens begins a description of ZF.

So the technical work in logic defining what a proof is applies to this
case. And so we do apply it. As is justified by Shoenfield's own words
above. Anyway, if there is some problem with ZF being a formal system why
does Shoenfield have a chapter on it?

So you dispute our mathematical knowledge by saying know means really know,
and relaly know means having a formal proof, and formal proof means over
pure logic only with no nonlogical axioms.

But you are just changing our claims to something we never meant.


--
David Libert ah170(a)FreeNet.Carleton.CA
 | 
Pages: 1
Prev: Continuity and Uncountability
Next: instructor solution manual for Fundamentals of Corporate Finance 9th edition by Ross