Changes

: VP = Vaughan Pratt

: VP = Vaughan Pratt

====Feb 1998, Intuitionistic Mathematics and Building Bridges====

====Feb 1998 : Intuitionistic Mathematics and Building Bridges====

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

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

# VP: http://www.cs.nyu.edu/pipermail/fom/1998-February/001248.html

# VP: http://www.cs.nyu.edu/pipermail/fom/1998-February/001248.html

====Oct 2008, Classical/Constructive Mathematics====

====Oct 2008 : Classical/Constructive Mathematics====

* http://www.cs.nyu.edu/pipermail/fom/2008-October/thread.html#13127

* http://www.cs.nyu.edu/pipermail/fom/2008-October/thread.html#13127

===Foreground===

===Foreground===

Harvey Friedman (15 Oct 2008), "Classical/Constructive Mathematics", FOMA

    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

<p>There seems to be a resurgence of interest in comparisons betweenclassical 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.</p>

    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

<p>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.</p>

    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

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

    classical and constructive foundations are alike or closely related.

HF: For many formal systems for fragments of classical mathematics, T,

<p>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 &mdash; 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.</p>

    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

<p>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.</p>

    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?

<p>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".</p>

    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.

<p>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.</p>

    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

<p>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?</p>

    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

<p>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 &mdash; thus possessing none of these properties!</p>

    *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

<p>For many of these T,T' pairs, some very interesting relationships obtain between the T and T'. Here are three important ones.</p>

    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'

<p>1.  It can be proved that T is consistent if and only if T' is consistent.</p>

        is consistent.

HF: 2.  Every A...A sentence, whose matrix has only bounded quantifiers,

<p>2.  Every A&hellip;A sentence, whose matrix has only bounded quantifiers, that is provable in T, is already provable in T'.</p>

        that is provable in T, is already provable in T'.

HF: 3.  More strongly, every A...AE...E sentence, whose matrix has only

<p>3.  More strongly, every A&hellip;AE&hellip;E sentence, whose matrix has only bounded quantifiers, that is provable in T, is already provable in T'.</p>

        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.,

<p>The issue arises as to just where these proofs are carried out &mdash; e.g., constructively or classically. This is particularly critical in the case of 1. The situation is about as "convincing" as possible:</p>

    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

<p>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'.</p>

    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

<p>Results like 1 point in the direction of there being no difference between the "safety" of classical and constructive mathematics.</p>

    between the "safety" of classical and constructive mathematics.

HF: Results like 2,3 point in the direction of there being no difference

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

    between the "applicability" of classical and constructive mathematics,

    in many contexts.

HF: CAUTION:  For AEA sentences, PA and HA differ. There are some

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

    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

<p>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.</p>

    (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.

<p>I will continue with this if sufficient responses are generated.</p>

I, too, find myself returning to questions about classical v. constructive logic

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.

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

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:

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

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