[FOM] Re: On Constructive Mathematical Truth

[Dmytro Taranovsky]

In constructive mathematics, a witness for A->B must give a witness for
B when given a witness for A.  I would like to clarify and correct my
definition of what it means to give a witness.

Witnesses are real numbers that specify which output to give for each
possible input.  When given a witness, you may give it input and will
receive appropriate output; you will get no other information.  Multiple
instances of a witness may be run.  When requested a witness (as input
to a witness), you simply accept input and provide appropriate output;
you may give false output, but that may cause the instance of the
witness to enter an infinite loop or give arbitrary output.  A witness
may take arbitrarily long to give an answer and may call appropriate
witnesses (for example, a witness to A->B may call a witness to A) an
unlimited number of times.

Question:  What is the Turing degree of the set of constructively true
arithmetical statements?
The question is essentially whether the witnesses can be defined without
using real numbers.

The correction came from the following example.  The intended
constructive meaning of "((A->B)->C) and (A->C)" is that if you have a
witness to "A or (A->B)", you can get a witness to C.  As it stood,
however, if A->B is (classically) true and you have a witness to (A and
C)->B, you could merely state that you have a witness for A->B.  You
would then either obtain a witness to C or be given a witness to A (so
that a witness to B could be requested) which you could use to get a
witness to C (from A->C) and use the witness to C to get (as required) a
witness to B.

There is a qualitative leap from simply working in a constructive formal
system to knowing what is constructive truth.  Semantics gives
meaningfulness to symbol manipulations, explains why some rules are
accepted while others are not, makes it much easier to have intuition
about the subject, and gives a way resolve the incompleteness in the
formal system.  (Admittedly, however, some semantics was provided by
realizability and by Kripke models.)

Dmytro Taranovsky