[FOM] Constructive Arithmetical Truth is Pi-1-1 Complete

[Dmytro Taranovsky]

Every Pi-1-1 statement phi can be transformed into an arithmetical
statement psi such that that phi is true if and only if psi is
constructively true, and vice versa.

This confirms that constructive arithmetical truth is richer than plain
truth.  It also shows existence of a 'universal' arithmetical formula
phi such that for every 'psi', phi('psi') is constructively true iff
'psi' is constructively true.  This is not a contradiction since the
universality is not constructively true.  For reference, constructive
arithmetical truth is defined in my FOM posting "On Constructive
Mathematical Truth" and its clarification.

To see that constructive arithmetical truth is Pi-1-1, a statement is
constructively true iff there is an integer (coding the constructive
witness) such that for every real number (trying to refute the alleged
constructive witness), the witness requirements are met.  The meeting of
requirements can be defined recursively on the complexity of the
formula.  For example, refutation of a putative witness to "A->B" fails
iff in every instance where a putative witness to A is given,
requirements for a witness to B are satisfied for as long as
requirements for being a witness to A are satisfied.

For converse, let P be such that "thereis n (forall m (m=n or P(m)) ->
P(n))" is not constructively true.   (Quantifiers have the least scope
permitted by parentheses and non-logical symbols; implication has lower
precedence than other logical operators.) For example, let P be "forall
i (x_n (i) or not x_n (i))" such that for every n, x_n is not recursive
in (x_0, x_1, x_2, ...) with x_n replaced by 0.  P is an approximation
to the idealized predicate T such that T(n) is true for every n, but for
every n, a witness for T(n) cannot be constructively obtained unless
previously given, and such that having a witness for T(n) does not give
any knowledge beyond the ability to give a witness to T(n).

Let '<<' be a recursive strict partial order given as such.  (Actually,
'<<' can be arbitrary arithmetical if given  such that "forall m forall
n (not not m<<n -> m<<n)" is arithmetical and constructively true.)
'<<' is well-founded iff
forall n (forall m<<n P(m) -> P(n)) -> forall n P(n)
is constructively true.

If '<<' is well-founded, then to get a witness for "forall n P(n)", you
request a witness for "forall m<<n P(m) -> P(n)" for every n.  Then you
fulfill all requests for witnesses for P(m) as witnesses become
available.

If '<<' is not well-founded, then a witness to the antecedent can act
arbitrarily provided that in the limit
(1) For some n, witness for P(n) is not given
(2) All possible requests are made
(3) For every n, if witness for P(n) is not given, then for some m<<n,
witness for P(m) is not given

(3) implies that witnesses for P(n) will eventually be given for every n
in the well-founded part of '<<'.  However, the behavior at any finite
stage is arbitrary, so no special information can be uniformly gathered
from witnesses for the antecedent.


Every arithmetical statement has an arithmetical witness, but the
property of being a witness is not arithmetical.  Had we required
witnesses to be arithmetical, constructive truth would be weakened yet
remain stronger than simply truth.  However, we cannot do that since we
may decide to extend the language of arithmetic, which would require
non-arithmetical witnesses.  (We cannot place different complexity
requirements on witnesses for P than for Q since we may discover P <-> Q
constructively, which can cause incompatibility.)

A richer language is obtained by using constructive truth as a modal
operator, where a witness for constructive truth is and given as a
(standard) code for a constructive witness for truth.  For every natural
number n, there is 'phi' in the language such that forall m (phi(m) <-->
m belongs to the nth hyperjump of 0).  Conversely, for every 'phi', {n:
phi(n)} is recursive in a finite hyperjump of zero.  Realizability
interpretation corresponds to inserting the constructive modal operator
at every relevant place.

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