Foundations Of Mathematics Absconditus

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

FOMA.  Note 1 : Bridges And Barriers

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Background --

AM = A Mani
HF = Harvey Friedman
NT = Neil Tennant
SS = Stephen G Simpson
TF = Torkel Franzen
VP = Vaughan Pratt

Feb 1998, Intuitionistic Mathematics and Building Bridges
http://www.cs.nyu.edu/pipermail/fom/1998-February/thread.html#1160
NT: http://www.cs.nyu.edu/pipermail/fom/1998-February/001160.html
TF: http://www.cs.nyu.edu/pipermail/fom/1998-February/001162.html
SS: http://www.cs.nyu.edu/pipermail/fom/1998-February/001246.html
VP: http://www.cs.nyu.edu/pipermail/fom/1998-February/001248.html

Oct 2008, Classical/Constructive Mathematics
http://www.cs.nyu.edu/pipermail/fom/2008-October/thread.html#13127
HF: http://www.cs.nyu.edu/pipermail/fom/2008-October/013127.html
AM: http://www.cs.nyu.edu/pipermail/fom/2008-October/013142.html

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Foreground --

Re: Classical/Constructive Mathematics
     Harvey Friedman (15 Oct 2008, 00:36:36 EDT)

HF: There seems to be a resurgence of interest in comparisons between
     classical and constructive (foundations of) mathematics.  This is
     a topic that has been discussed quite a lot previously on the FOM.
     I have been an active participant in prior discussions.

HF: There was a lot of basic information presented earlier, and I think
     that it would be best to restate some of this, so that the discussion
     can go forward with its benefit.

HF: In this message, I would like to focus on some important ways in which
     classical and constructive foundations are alike or closely related.

HF: For many formal systems for fragments of classical mathematics, T,
     there is a corresponding system T' obtained by merely restricting
     the classical logical axioms to constructive logical axioms - where
     the resulting system is readily acceptable as a formal system for
     a "corresponding" fragment of constructive mathematics. Of course,
     there may be good ways of restating the axioms in the classical system,
     which do NOT lead to any reasonable fragment of constructive mathematics
     in this way.

HF: The most well known example of this is PA = Peano Arithmetic.  Suppose
     we formalize PA in the most common way, with the axioms for successor,
     the defining axioms for addition and multiplication, and the axiom
     scheme of induction, with the usual axioms and rules of classical
     logic. Then HA = Heyting Arithmetic, is simply PA with the axioms
     and rules of classical logic weakened to the axioms and rules of
     constructive logic.

HF: Why do we consider HA as being a reasonable constructive system?
     A common answer is simply that a constructivist reads the axioms
     as "true" or "valid".

HF: An apparently closely related fact about HA is purely formal.
     HA possesses a great number of properties that are commonly
     associated with "constructivism".  The early pioneering work
     along these lines is, if I remember correctly, due to S.C. Kleene.
     Members of this list should be able to supply really good references
     for this work, better than I can.  PA possesses NONE of these properties.

HF: RESEARCH PROBLEM: Is there such a thing as a complete list of such
     formal properties? Is there a completeness theorem along these lines?
     I.e., can we state and prove that HA obeys all such (good from the
     constructive viewpoint) properties?

HF: On the other hand, we can formalize PA, equivalently, using the
     *least number principle scheme* instead of the induction scheme.
     If a property holds of n, then that property holds of a least n.
     Then, when we convert to constructive logic, we get a system PA#
     that is equivalent to PA - thus possessing none of these properties!

HF: For many of these T,T' pairs, some very interesting relationships
     obtain between the T and T'. Here are three important ones.

HF: 1.  It can be proved that T is consistent if and only if T'
         is consistent.

HF: 2.  Every A...A sentence, whose matrix has only bounded quantifiers,
         that is provable in T, is already provable in T'.

HF: 3.  More strongly, every A...AE...E sentence, whose matrix has only
         bounded quantifiers, that is provable in T, is already provable
         in T'.

HF: The issue arises as to just where these proofs are carried out - e.g.,
     constructively or classically. This is particularly critical in the
     case of 1. The situation is about as "convincing" as possible:

HF: Specifically, for each of these results, one can use weak quantifier
     free systems K of arithmetic, where constructive and classical amount
     to the same. E.g., for 1, there is a primitive operation in K which,
     provably in K, converts any inconsistency in T to a corresponding
     inconsistency in T'.

HF: Results like 1 point in the direction of there being no difference
     between the "safety" of classical and constructive mathematics.

HF: Results like 2,3 point in the direction of there being no difference
     between the "applicability" of classical and constructive mathematics,
     in many contexts.

HF: CAUTION:  For AEA sentences, PA and HA differ. There are some
     celebrated A...AE...EA...A theorems of PA which are not known
     to be provable in HA. Some examples were discussed previously
     on the FOM.

HF: RESEARCH PROBLEM: Determine, in some readily intelligible terms
     (perhaps classical), necessary and sufficient conditions for
     a sentence of a given form is provable in HA and PA.  Matters
     get delicate when there are several quantifiers and arrows (-->)
     present.

HF: I will continue with this if sufficient responses are generated.

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

I, too, find myself returning to questions about classical v. constructive logic
lately, partly in connection with Peirce's Law, the Propositions As Types (PAT)
analogy, the question of a PAT analogy for classical propositional calculus,
and the eternal project of integrating functional, relational, and logical
styles of programming as much as possible.

I am still in the phase of chasing down links between the various questions
and I don't have any news or conclusions to offer, but my web searches keep
bringing me back to this old discussion on the FOM list:

http://www.cs.nyu.edu/pipermail/fom/1998-February/thread.html#1160

I find one comment by Vaughan Pratt to be especially e-&/or-pro-vocative:

VP: It has been my impression from having dealt with a lot of lawyers over the
     last twenty years that the logic of the legal profession is rarely Boolean,
     with a few isolated exceptions such as jury verdicts which permit only
     guilty or not guilty, no middle verdict allowed.  Often legal logic
     is not even intuitionistic, with conjunction failing commutativity
     and sometimes even idempotence.  But that aside, excluded middle
     and double negation are the exception rather than the rule.

VP: Lawyers aren't alone in this.  The permitted rules of reasoning
     that go along with whichever scientific method is currently in
     vogue seem to have the same non-Boolean character in general.

VP: The very *thought* of a lawyer or scientist appealing to Peirce's law,
     ((P->Q)->P)->P, to prove a point boggles the mind.  And imagine them
     trying to defend their use of that law by actually proving it:  the
     audience would simply assume this was one of those bits of logical
     sleight-of-hand where the wool is pulled over one's eyes by some
     sophistry that goes against common sense.

Anyway, to make a long story elliptic, here is one of my current write-ups
on Peirce's Law that led me back into this old briar patch:

http://www.mywikibiz.com/Peirce's_law

More to say on this later, but I just wanted to get
a good chunk of the background set out in one place.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
knol: http://knol.google.com/k/-/-/3fkwvf69kridz/1
mathweb: http://www.mathweb.org/wiki/User:Jon_Awbrey
planet math: http://planetmath.org/?op=userobjs;id=15246
proof wiki: http://www.proofwiki.org/wiki/User:Jon_Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o