[FOM] Complexity of Constructive Truth

Dmytro Taranovsky dmytro at MIT.EDU
Sun Jun 4 12:45:42 EDT 2006

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

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

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

More information about the FOM mailing list