[FOM] Complexity of Constructive Truth

[Dmytro Taranovsky]

Constructive arithmetic is about natural numbers and constructions, so
it should be clear and well-defined.  However, different constructivists
accepted different arithmetical principles, and there was no
satisfactory notion of constructive arithmetical truth that is
compatible with classical truth.

My paper "Constructive Mathematical Truth", available at
http://arxiv.org/abs/math.LO/0605138

defines constructive truth for arithmetic and (intuitionistic) analysis
and explores its properties.  A statement is constructively true iff it
is realized by a recursive function under Kleene's function
realizability.

I prove that the set of constructively true (first order) arithmetical
statements is Pi-1-2 and Sigma-1-2 hard, and conjecture it to be
complete for second order arithmetic.  

The high complexity stems from the precise meaning of constructive
implication.  I have previously written on FOM that constructive
arithmetical truth is Pi-1-1 complete; however, the definition given
there was imprecise; and a variation on constructive truth, called
narrow constructive truth, is Pi-1-1 complete.

Dmytro Taranovsky