[FOM] On Constructive Mathematical Truth

[Dmytro Taranovsky]

While notions of constructive proofs are well-known, standard texts do
not adequately explain what it means for a statement to be
constructively true.  In this posting, I define (the canonical variety
of) constructive truth for arithmetic.  The notion of constructive truth
has a similarity with BHK notion of constructive proof.

An arithmetical statement is constructively true if it is true and there
is a constructive witness to existential aspects of its truthfulness.
Logical connectives are used to designate which aspects are existential.
Logically equivalent statements may have different designations, and
thus different requirements on the witness.  

A witness must produce a certain output when given a certain input as
described below.  A witness is constructive iff there is a constructive
mechanism for its operation;  the standard meaning of this is that the
witness is computable, but other notions are possible.  The stricter the
notion of being constructive, the more difficult it is for a statement
to be constructively true; the weakest possible notion is for
(classical) truth.

A witness for "A" only exists if "A" is true.
A witness for "not A" or (in standard arithmetic) for an atomic formula
is not required to do anything.
A witness for "A or B" must choose "A" or "B" and provide a witness for
it.
A witness for "A and B" must provide witnesses for both "A" and "B".
A witness for "thereis x A(x)" must provide n and a witness for A(n).
A witness for "forall x A(x)" must when given n as input, provide a
witness for A(n).
A witness for "A implies B" must provide a witness for "B" whenever
given a witness for "A".  (The witness for "A" is given as a black box
or an oracle and need not be constructive.  To "provide a witness" means
to act as a witness when requested.  A non-witness for "A" may not be
given as a witness for "A".)


Some statements, such as "not A", have no existential components and are
thus treated classically.  "not A" may be viewed as an abbreviation of
"A implies 0=1".  "A or B" is constructively true iff "A" is
constructively true or "B" is constructively true; analogously with "A
and B" and (for arithmetic) with "thereis x A".  "forall x A(x)" is
constructively true iff for every n, A(n) is constructively true and
uniformly so (that is the witnesses can be constructed uniformly in n).

"A implies B" is constructively weaker than "not A or B".  The
requirement on witnesses for implication is precisely such that key
properties of implication are constructively true.  If "A and (A implies
B)" is constructively true, then so is "B".  "A implies A" is
constructively true.  As required, constructive truth of "A implies B"
is preserved if the notion of constructiveness is broadened, which is
why the witnesses for antecedents are not required to be constructive.

For formulas without "implies", the property of being a constructive
witness is Pi-0-2 above the (unbounded quantifier) complexity of the
negated blocks.  Thus, in the absence of implications, constructive
truth is Sigma-0-3 above the complexity of the negated blocks. The most
immediate definition for witnesses of implication uses quantification
over reals ("for every real number coding a witness for A ...").  The
exact logical complexity is not clear to me.


Realizability in the sense of Kleene is like constructive truth (where
"constructive mechanism" is interpreted as recursive) except that
witnesses for antecedents must be given as codes for (partial) recursive
functions, and false statements with quantifiers may have witnesses, and
"not A" is interpreted as "A implies 0=1".  For every statement "A", "A"
or "not A" is realizable (as is "A or not A"). The set of realizable
sentences is a consistent completion of some constructive formal
systems; it has the same Turing degree as the truth predicate for
arithmetic.  Some realizable statements are false; an example is "not
every partial recursive function is either defined or undefined at
zero".

A constructive proof provides a number and demonstrates that the number
is a constructive witness.  A true constructive formal system is a
formal system in which only constructively true statements are
derivable, and in which derivations can be constructively converted into
witnesses for constructive truth.  When one is more interested in the
witnesses than in the truth, using a constructive formal system may be a
good way to manage complexity.  When one is more interested in
realizability than in truth, a constructive formal system that proves
false statements but does not prove unrealizable statements may be
useful.  However, the savings have to be balanced against the difficulty
of not using some logical truths; and to avoid contradiction, one must
always note when "A" is used as a shorthand for "A is realizable".

Dmytro Taranovsky