[FOM] Constructive Arithmetical Truth

[Dmytro Taranovsky]

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.

Questions:
* 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 
Pi-1-2 hard.
* 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 
for A.

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.

Other notes:
* 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.

Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm