[FOM] Constructive Arithmetical Truth
dmytro at mit.edu
Sun Sep 30 15:18:21 EDT 2018
Constructive truth for arithmetic and analysis was defined and explored
in 2006 in my paper "Constructive Mathematical Truth"
https://arxiv.org/abs/math/0605138 . A statement is constructively true
iff it has a recursive realizer under Kleene's function realizability.
An explanation is below, but for visibility, I will put the questions first.
* Have there been progress in proving that the set of constructively
true statements in first order arithmetic is complete for second order
arithmetic? In my paper, I prove that it is both Sigma-1-2 hard and
* Have there been other reasonable formal notions of constructive
arithmetical truth such that constructively true statements (in first
order arithmetic) are classically true? While I argue that the
definition I give is the preferred one, that does not mean that other
notions are not useful.
Traditionally, intuitionistic and constructive mathematicians disfavored
platonic truth, and some semantics (such as Kripke models) explicitly
reject a single objective truth. But the difference in philosophy need
not stop a platonist from appreciating constructive mathematics, or from
finding a combination that combines constructiveness and objective
truth. And even to a nonplatonist, constructive truth can be viewed as
an idealization of constructive proof, a reasonable description of a
limit as one increases the strength of the constructive theory.
The basic framework should be a familiar one. In constructive
mathematics, logical connectives and statements indicate not only
ordinary truth values but also which constructions satisfy the
statement. A statement is constructively true iff it has a constructive
witness (or realizer) for existential aspects of the statement.
* There are no witnesses for false statements.
* True atomic statements have trivial witnesses (in our theories here).
* A witness for A or B gives a witness for A or a witness for B
(indicating which one is given, and similarly below).
* A witness for A and B gives a witness for A and a witness for B.
* A witness for thereis n A(n) gives n and a witness for A(n).
* A witness for forall n A(n) gives a transformation that maps n into a
witness for A(n).
* A witness for A ==> B gives a transformation that maps witnesses for A
into witnesses for B.
A constructive witness is recursive. However, to allow all
constructively true statements (in first order arithmetic) to be
classically true (which is not the case for number realizability), we
must allow nonrecursive witnesses. Thus, a constructive witness for A
==> B is recursive, but it must work even against nonrecursive witnesses
Now, a (possibly nonrecursive) witness is naturally presented as a real
number (or an infinite binary sequence), and a witness for A ==> B -- as
a real number coding a partial continuous function mapping witnesses for
A into witnesses for B; and the rest are routine formalization details.
The continuity stems from the interaction being finite at every stage.
A constructive witness for ((A ==> B) and A) ==> B must accept arbitrary
witnesses for the second A but since it gets only finite pieces at any
time (unless we use some kind of infinitary constructiveness), we need
the transformation for A ==> B to be continuous.
* Although the word 'constructive' has overtones of simplicity, a
constructive treatment adds structure, which often makes it more expressive.
* One can define other logical connectives, most notably nonconstructive
disjunction: A witness for the nonconstructive disjunction of A and B
gives a candidate witness for A and a candidate witness for B, at least
one of which is correct (without indicating which one).
* For second order arithmetic, constructive truth diverges from
classical truth, or rather it uses different quantifiers. An ordinary
forall X does not appear to work constructively because an arbitrary
(possibly random) infinite binary sequence X cannot be given in finite
time as a complete totality, so instead, constructively we use a
different quantifier, interpreting forall X phi(X) to mean for all X and
with the witness continuous in X. For first order arithmetic, the
classical and constructive quantifiers are compatible; we have no need
to define them incompatibly.
More information about the FOM