🚀 go-pugleaf

In article <9993@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes:
>In article <20010@netnews.upenn.edu> aaron@grad2.cis.upenn.edu.UUCP (Aaron Watters) writes:

>Look at "Bounded Arithmetic" by Sam Buss (Bibliopolis 1986)
>for an iteresting"real mathematic" use of proof theory.

I apologise for using bad terminology.  I suppose the proof of the
semidecidability of first order predicate calculus could be called
a `use' of proof theory -- and it's certainly good mathematics.
This is not the sense I meant when I said that proof theory was
seldom `used' by mathematicians.  I meant `use' in the sense of
`no sensible programmer uses turing machines.'  I.e, turing machines
are a theoretical object of study and not a practical way to implement
programs.

I should have said
that the original posting was misleading because it suggested that
mathematicians operate within the realm of formal proofs, which they
don't.  Proof theories are a theoretical object of study and not
a practical way to arrive and mathematical truth.

-aaron.