Formalism [Logic]

Prev: proof outline that Fibonacci primes are infinite set #685 Correcting Math
Next: instructor solution manual for Advanced Industrial Economics, 2nd ED Stephen Martin

From: Kester Tong on 16 Jul 2010 05:10

Hi,

I've been reading Edward Nelson's work, and it got me curious about
formalism.

From a modern point of view, formalism should be the belief that a
statement of the form
(I) "X is a valid proof of P in first order logic"
must be either true or false, but statements of the form
(II) "there are infinitely many primes"
are useful fictions which may help us in practical matters but have no
inherent meaning.

However, statements of the form (I) are also mathematical statements,
and in Peano Arithmetic, for example, we have an infinite set of
axioms (since the axiom schema of induction generates infinitely many
axioms). Therefore evaluating the truth of statements of the form (I)
seems to require as much mathematics as reasoning about the integers.
Therefore being a formalist seems to require either (A) considering
the notion of proof to be non-mathematical (which seems strange since
it is so easy to formalize), or (B) establishing that statements of
the form (I) can be verified using a weaker system than PA.

Anyway, if someone can point me towards work showing that the
mathematics required to verify the correctness of proofs in FOL is
weaker than PA (or the opposite result), that would be very
interesting.

Cheers,

Kester Tong

From: Sergei Tropanets on 16 Jul 2010 11:32

On Jul 16, 12:10 pm, Kester Tong <kester.t...(a)gmail.com> wrote:
> Hi,
>
> I've been reading Edward Nelson's work, and it got me curious about
> formalism.
>
> From a modern point of view, formalism should be the belief that a
> statement of the form
> (I) "X is a valid proof of P in first order logic"
> must be either true or false, but statements of the form
> (II) "there are infinitely many primes"
> are useful fictions which may help us in practical matters but have no
> inherent meaning.
>
> However, statements of the form (I) are also mathematical statements,
> and in Peano Arithmetic, for example, we have an infinite set of
> axioms (since the axiom schema of induction generates infinitely many
> axioms). Therefore evaluating the truth of statements of the form (I)
> seems to require as much mathematics as reasoning about the integers.
> Therefore being a formalist seems to require either (A) considering
> the notion of proof to be non-mathematical (which seems strange since
> it is so easy to formalize), or (B) establishing that statements of
> the form (I) can be verified using a weaker system than PA.
>
> Anyway, if someone can point me towards work showing that the
> mathematics required to verify the correctness of proofs in FOL is
> weaker than PA (or the opposite result), that would be very
> interesting.
>
> Cheers,
>
> Kester Tong

>Therefore evaluating the truth of statements of the form (I)
> seems to require as much mathematics as reasoning about the integers.

No. It require much less, namely, use of potential infinity (the
unbound ability to explicitly extend finite sets). The very purpose of
Hilbert's formalistic program was to reduce consistency of abstract
reasoning about the integers (involving actual infinity) to
consistency of finitist reasoning (restricted to potential infinity).
The later is taken for granted as a minimal methods for any reasonable
intellectual activity (see introduction to Hilbert, Bernays.
Foundations of mathematics, v.1).

According to official point of view, formal system PRA (primitive
recursive arithmetic) represents a formalist notions and proof
methods, i.e. everything that is definable/provable in PRA is also
definable/provable finitisticly and vice versa. The justification see
in Tait's famous paper "Finitism". This system can verify concrete
explicit properties like correctness of proof in FOL and so forth, as
well as prove both incompleteness theorems. However, Kreisel and
Parsons proposed other formalizations of finitism - PA and BPA (bound
recursive arithmetic). An interesting discussion of this controversy
you may find in Tait's "Remarks on finitism". See also chapter 2 from
the Stanford Encyclopedia of

Philosophy article: http://plato.stanford.edu/entries/hilbert-program/

and the works of mentioned logicians referenced there.

Sergei Tropanets

From: Sergei Tropanets on 16 Jul 2010 11:46

From: Kester Tong on 16 Jul 2010 14:10

On Jul 16, 8:32 am, Sergei Tropanets <trop.ser...(a)gmail.com> wrote:
> On Jul 16, 12:10 pm, Kester Tong <kester.t...(a)gmail.com> wrote:
>
>
>
>
>
> > Hi,
>
> > I've been reading Edward Nelson's work, and it got me curious about
> > formalism.
>
> > From a modern point of view, formalism should be the belief that a
> > statement of the form
> > (I) "X is a valid proof of P in first order logic"
> > must be either true or false, but statements of the form
> > (II) "there are infinitely many primes"
> > are useful fictions which may help us in practical matters but have no
> > inherent meaning.
>
> > However, statements of the form (I) are also mathematical statements,
> > and in Peano Arithmetic, for example, we have an infinite set of
> > axioms (since the axiom schema of induction generates infinitely many
> > axioms). Therefore evaluating the truth of statements of the form (I)
> > seems to require as much mathematics as reasoning about the integers.
> > Therefore being a formalist seems to require either (A) considering
> > the notion of proof to be non-mathematical (which seems strange since
> > it is so easy to formalize), or (B) establishing that statements of
> > the form (I) can be verified using a weaker system than PA.
>
> > Anyway, if someone can point me towards work showing that the
> > mathematics required to verify the correctness of proofs in FOL is
> > weaker than PA (or the opposite result), that would be very
> > interesting.
>
> > Cheers,
>
> > Kester Tong
> >Therefore evaluating the truth of statements of the form (I)
> > seems to require as much mathematics as reasoning about the integers.
>
> No. It require much less, namely, use of potential infinity (the
> unbound ability to explicitly extend finite sets). The very purpose of
> Hilbert's formalistic program was to reduce consistency of abstract
> reasoning about the integers (involving actual infinity) to
> consistency of finitist reasoning (restricted to potential infinity).
> The later is taken for granted as a minimal methods for any reasonable
> intellectual activity (see introduction to Hilbert, Bernays.
> Foundations of mathematics, v.1).
>
> According to official point of view, formal system PRA (primitive
> recursive arithmetic) represents a formalist notions and proof
> methods, i.e. everything that is definable/provable in PRA is also
> definable/provable finitisticly and vice versa. The justification see
> in Tait's famous paper "Finitism". This system can verify concrete
> explicit properties like correctness of proof in FOL and so forth, as
> well as prove both incompleteness theorems. However, Kreisel and
> Parsons proposed other formalizations of finitism - PA and BPA (bound
> recursive arithmetic). An interesting discussion of this controversy
> you may find in Tait's "Remarks on finitism". See also chapter 2 from
> the Stanford Encyclopedia of
>
> Philosophy article:http://plato.stanford.edu/entries/hilbert-program/
>
> and the works of mentioned logicians referenced there.
>
> Sergei Tropanets

Thanks, that's exactly what I was looking for,

Kester

From: Kester Tong on 17 Jul 2010 18:32

> What work of Edward Nelson do you mean?

His book "predicative arithmetic" and this article argueing that PA
may be inconsistent and how to demonstrate it.

http://www.math.princeton.edu/~nelson/papers/hm.pdf

|
Pages: 1
Prev: proof outline that Fibonacci primes are infinite set #685 Correcting Math
Next: instructor solution manual for Advanced Industrial Economics, 2nd ED Stephen Martin