Dmytro Taranovsky
June 6, 2006
Abstract: We define constructive truth for arithmetic and for intuitionistic analysis, and investigate its properties. We also prove that the set of constructively true (first order) arithmetical statements is Π12 and Σ12 hard, and we conjecture it to be complete for second order arithmetic. A statement is constructively true iff it is realized by a constructive function under continuous function realizability.
List of Sections: Introduction, Definition of Constructive Truth, Basic Properties, Complexity of Constructive Truth, Narrow Constructive Truth, Constructive Truth for Analysis, Discussion.
Being able to construct a mathematical object is more satisfying than simply knowing it exists, and a branch of mathematics was developed with emphasis on construction. However, a satisfactory description of constructive truth has previously eluded mathematicians. Some like L.E.J. Brouwer thought that mathematics is a free activity of the mind, and hence subjective. Some others confined themselves to recursive functions and analysis. Still others emphasized constructive proof (as in Brouwer-Heyting-Kolmogorov semantics) over truth.
Constructive mathematics is as old as mathematics itself, and most mathematics before the 19th century was constructive. Constructive mathematics was considered just ordinary mathematics and was done in classical logic. In the early 20th century, Brouwer pioneered constructive mathematics, specifically intuitionism, as a distinct branch of mathematics with the rules of logic weakened to ensure that non-constructive results are not provable. Specifically, the law of the excluded middle A⋁¬A was omitted in favor of weaker statements. However, Brouwer adopted a polemic style and insisted on subjectivity of mathematics. As a consequence, his constructive analysis was imprecise and difficult to use. Only later was the intuitionistic logic formalized. Around 1950s and later, Russian mathematicians developed a different branch of constructive mathematics, namely constructive recursive analysis. In constructive recursive analysis, every real number is given by a recursive code and every answer must be a construction.
A major development was Bishop's Foundations of Constructive Analysis [Bishop 1967], where he showed that much of mathematics can be done constructively and without using controversial or classically incorrect principles. Bishop accomplished that by using mathematically relevant formalizations (among many classically but not constructively equivalent ones) and by using additional assumptions (like uniform continuity) for his theorems.
Still, semantics of constructive mathematics remained unsatisfactory. There is a qualitative leap from simply working in a constructive formal system to knowing what is constructive truth. Semantics gives meaning to symbol manipulations, explains why some rules are accepted while others are not, makes it much easier to have intuition about the subject, and provides a way resolve the incompleteness in the formal system. Historically, because of usability problems and unsatisfactory semantics, relatively few mathematicians actually worked in constructive formal systems. Some semantics was provided by Kripke models and related developments, but these do not provide a notion of constructive truth. Different statements are true at different nodes of a typical Kripke model.
For constructive recursive mathematics, semantics was provided through Kleene's recursive realizability (which is defined in this paper). However, recursive realizability essentially forbids non-recursive functions, which makes it too restrictive for ordinary mathematics. Later [Kleene 1965], Kleene defined function realizability, which comes close to constructive truth. Unfortunately, Kleene's function realizability became relatively obscure, and I did not know its definition until this paper was essentially complete.
My search for constructive truth started from the question, What do we know about a statement (beyond its truth) from having a constructive proof regardless of the constructive formal system used? The answer is that we know a constructive witness to the statement. A statement is constructively true iff it has a constructive witness.
Some constructivists may reject the notion that there is constructive arithmetical truth which can be formally defined. For them, our quest can be viewed in this way: If we have to formally define constructive truth, what would be the definition? Besides, the mathematical results can be enjoyed whether or not the reader accepts our philosophical claim.
Clearly, we cannot identify constructive truth with constructive proof since there is no single privileged formal notion of constructive proof. Our definition diverges from the thought of Brouwer and others, but only to the extent necessary for basic properties of truth. Constructive truth resembles recursive realizability, except that every constructively true arithmetical statement is true. In fact, our definition of witnessability (which we also call continuous function realizability) agrees with Kleene's function realizability but for notational differences (we use sets rather than functions, and our treatment of witnesses is more explicit).
In retrospect, defining the exact constructive content of implication is the technical impediment to the definition of constructive truth. We have to use real numbers to overcome the difficulty, which leads to the amazingly high complexity of constructive arithmetical truth. However, the technical difficulty was essentially overcome by Kleene, and the problem was more of a philosophical one. Intuitionism as a philosophy rejects objective mathematical truth, so constructive truth was not pursued. The result was a much less usable intuitionistic analysis than it could have been.
The paper is mostly self-contained. Background information can be found in articles "Intuitionistic Logic" and "Constructive Mathematics" in the Stanford Encyclopedia of Philosophy (online); in [Troelstra 1977]; and also in [Moschovakis 2005]. The latter defines function realizability.
The second section defines constructive arithmetical truth, and the third section describes its basic properties. In the fourth section, we prove that constructive arithmetical truth is Π12 and Σ12 hard. For ease of understanding, we build up to that result by presenting easier results first. We also prove that for a large class of statements, constructive truth is Π11. In fifth section, we consider a modification of constructive truth and prove that it is Π11 complete. In the sixth section, which is independent of the fourth and fifth sections, we define and analyze constructive truth for intuitionistic analysis. For brevity and smoothness of flow, in that section we omit formal proofs, but given enough details to make the proofs routine. That section also discusses constructive reverse mathematics and concludes with an independence result. The final section discusses correctness of the definition of constructive truth.
A 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 (in the classical sense) statements may have different designations, and thus different requirements on the witness, which can make the statements constructively inequivalent.
A witness must produce a certain output when given a certain input as described below. A witness is constructive if there is a constructive mechanism for its operation; the standard and default 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.
For readers who are familiar with Kleene's function realizability, we note that our definition of witnesses agrees up to recursive interconversion with function realizability; a statement is constructively true iff it is realized by a recursive function. The agreement extends to constructive analysis. However, here we present witnesses in a more explicit and readable syntactic form.
The language consists of the arithmetical symbols '0', '1', '+', '*', '<', '=', logical symbols of '¬', '⋀', '⋁', '→', '∃', '∀', and the modal operator '□' of constructive truth in the recursive sense. A formula is arithmetical if it does not use '□'. Quantifiers and '□' have the least possible scope. Implication has lower precedence than other logical operators.
Here A and B are formulas with an assignment of free variables. Technically, witnesses are real numbers (or arbitrary sets of integers) that specify which output to give for each possible input and satisfy the above requirements. The real number codes a sequence of input-output pairs in arbitrary order (and with arbitrary delay or whitespace), possibly omitting incorrect inputs. Having a witness refers to the ability to query the digits of the real number. W witnesses A → B iff for every X witnessing A, WX witnesses B. Here W is viewed as a continuous function, and WX is W applied to X (using whitespace in WX to make f: f(W, X)=WX total (and recursive); for inappropriate X, WX might consist of just whitespace). The rest is a formalization of the syntactic details (that should not affect constructive truth).
Input and output are given in the order of decreasing scope; '⋀' and '⋁' are treated like quantifiers. For example, for ∀x∃y (x=2*y ⋁ x=2*y+1), an input-output pair can be (25: 12, 1). 25 is the input x; the output provides 12 as y, and uses 1 to choose the second disjunct (0 would indicate the first disjunct; analogously with conjuncts). (25: 12) is also an input-output pair, but with insufficient output. (:) is the trivial pair (and is correct here); (: 12) gives too much output. A sample witness for ∀x∃y y=2*x is "(:) (0:0) (1:2) (2:4) …". Input does not affect output outside the scope. For example, for ∀x∃y∀z P(x, y, z), y is a part of output rather than input and may not depend on z.
For A → B, input consists of an initial segment of a witness for A and input for B. Arbitrary output (of the right syntactic form) for the consequent is permitted for false initial segments (including whenever A is false). Segments that are too short (or incorrect) can be rejected in that input-output pairs are omitted. However, for every witness for C, for every tuple of witnesses used as input into C, for every appropriate numerical input for C, some tuple of finite initial segments of the witnesses combined with the numerical input is accepted.
Output is uniquely determined by the input and is preserved if we extend the initial segments of the candidate witnesses for the antecedents (even for false candidate witnesses, where the output can otherwise be arbitrary; also, whitespace matters here for what constitutes an extension). (Alternatively, we could have allowed multiple outputs as long as the witness follows through and is accountable for each output. Any such witness can be converted into a witness with unique outputs.)
The semantic content of an input-output pair for a statement is the assertion (in classical logic) that the pair is correct. For example, for ∀x∃y y=x+1 → ∀x∃y y=x+2, the input-output pair ("(2:3) (3:4)", 2: 4) has semantic content ∀x∃y y=x+1 ⋀ 3=2+1 ⋀ 4=3+1 → 4=2+2.
Equivalently, witnesses can be described in computational terms. Witnesses are given as a blackbox or an oracle and need not be constructive. 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 can be run, and any instance can be copied. 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. A witness for a statement containing '→' can also be viewed as a functional of a higher type.
By running multiple instances of a witness W for A, we obtain the response tree for W, from which we can obtain W as a real number. Note that W has to meet the requirements for every path through the tree. (The response tree specifies the behavior for every possible input.) For a different notion, see Section 5 Narrow Constructive Truth.
Constructive truth for intuitionistic analysis is defined in Section 6. Recursive analysis can be interpreted in arithmetic and is not considered separately in this paper.
Some statements, such as ¬A, have no existential components (the witnesses have nothing non-trivial to do) and are thus treated classically: ¬A↔□¬A and ¬A↔¬¬¬A. ¬A may be viewed as an abbreviation of A → 0=1. A⋁B is constructively true iff A is constructively true or B is constructively true; analogously with A⋀B and (for integers) with ∃x A(x). ∀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.
The requirement on witnesses for implication is precisely such that key properties of implication are constructively true. A→B is constructively weaker than ¬A ⋁ B, which allows A→A to be constructively valid. If A ⋀ (A→B) is constructively true, then so is B. A↔B means (A→B)⋀(B→A), and '↔' has the same precedence as '→'. As required, constructive truth of A→B is preserved if the notion of constructiveness is broadened, which is why the witnesses for antecedents cannot be required to be constructive.
Because the whitespace in witnesses can absorb time complexity, every constructively true statement technically has a polynomial time computable witness. The transformations on witnesses corresponding to the connectives and quantifiers are also recursive (and hence polynomial-time computable). For example, to convert a witness for ∀x A(x) into a witness for A(n), pick all of the input-output pairs starting with n, and remove n from the inputs.
Like in the classical logic, every occurrence of a subformula is either positive or negative. If A→B is constructively valid, then any positive occurrence of A may be replaced B, and any negative occurrence of B may be replaced by A, and the above is constructively true.
Intuitionist predicate logic, Heyting arithmetic, and Markov's principle ∀x(A(x)⋁¬A(x)) ⋀ ¬∀x¬A(x) → ∃x A(x) are constructively true. ∀x(¬¬A(x)⋁¬A(x)) is constructively true iff A is decidable. Similarly, □(∀x(¬¬B(x)⋁¬B(x)) → ∀x(¬¬A(x)⋁¬A(x))) means A is recursive in B.
Every statement A has the associated set of witnesses S(A). A→B is constructively true iff there is a recursive mapping that is total on S(A) and maps S(A) into S(B).
Conjunction and disjunction are not strictly necessary since with some modifications to the formula, they may be replaced by the universal and existential quantifier, respectively.
The property of being a constructive witness is Π02 above the (constructive) complexity of blocks that start with negation or top-level implication. Thus, constructive truth is Σ03 above the complexity of such blocks. Moreover, □∀x∃y φ(x, y) ↔ □∃n∀x ({n}(x) exists ⋀ φ(x, {n}(x))) is constructively valid, and analogously with more quantifiers. Here {n}(x) is the output of the nth Turing machine with input x when that machine halts.
Also, a (constructively) Σ03 statement is true iff it is constructively true. In fact, φ↔□φ is constructively valid for (constructively) Σ03 φ.
Recursive realizability, or just realizability, is like constructive truth except that witnesses must be given as standard codes for partial recursive functions. A statement is realizable iff it has a witness in this sense. The realizability interpretation corresponds to inserting '□' at every relevant place, that is in front of the statement and antecedents and after '¬'. For every statement A, A or ¬A is realizable (as is A ⋁ ¬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. Intuitionistic predicate logic, Heyting arithmetic, and Markov's principle are realizable. Some realizable statements are false; an example is "not every partial recursive function is either defined or undefined at zero". Extended Church Thesis is the realizable assertion (actually, a schema) that truth equals realizability.
A constructive proof provides a number and demonstrates that the number codes a constructive witness. (However, even when the constructive proof is short, an actual computation of say which disjunct is true may be unfeasibly long.) 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. For example, constructive formal systems have applications in computer science since algorithms can be "read off" constructive proofs. 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".
Constructive truth acts as a necessity operator in intuitionistic modal logic. If the language is treated constructively, then A ⇒ □A is admissible as a rule of inference. We define the abstract theory of '□' to consist of intuitionistic predicate logic, rule A ⇒ □A, and axioms □(A→B)→(□A→□B), □A→A, □A→□□A, ¬A→□¬A, □(A⋁B) → □A⋁□B, and □∃x A(x) → ∃x □A(x). Constructive arithmetical truth satisfies the theory. In the above, we have assumed that every element is constructive (and given as a construction); see Section 6 for a treatment of non-constructive elements. The theory proves □(A⋀B) ↔ □A⋀□B, □(A⋁B) ↔ □A⋁□B, □∃x A(x) ↔ ∃x □A(x), and □∀x A(x) → ∀x □A(x); but ¬¬□A→A need not be constructively valid, that is the universal closure need not be constructively true.
However, intuitionistic logic has natural extensions. If the interpretation of '∀' is compatible with the classical one (as is the case here), then ∀x¬¬A(x) → ¬¬∀xA(x) can be added. If the domain is constructively enumerable and unbounded searches can be performed (as is also the case with constructive arithmetical truth), then ∀x(A(x) ⋁ B(x)) ⋀ ¬∀x B(x) → ∃x A(x) can be added. However, this principle can fail if the domain consists of say codes for total recursive functions or if we impose time limits on computations. Other principles can be added, but they should be constructive so that the rule A ⇒ □A can be retained.
An abstract theory of constructive knowledge consists of the abstract theory of '□' except for ¬A→□¬A but with additional axioms as appropriate. □A would stand for "A is constructively knowable". One notion of constructive knowledge is that a witness for □PA codes a witness for □A and a proof (in a sufficiently strong formal system) that the code witnesses □A. Another interesting notion of constructive knowledge includes ¬¬□A→A (and hence □∀x(¬¬□A(x)→□A(x))).
A Π11 formula is one that can be presented in the form ∀X φ where φ is arithmetical, allowing the use of the set of integers X as a predicate. Thus, a statement is Π11 if it is equivalent to a statement that a particular recursive (or arithmetical, or polynomial time computable) partial order (or total order) is well-founded.
Theorem 1: Constructive arithmetical truth is Π11 hard.
Proof:
Let x = (x0, x1, x2, …) be arithmetical and such that for every n, xn (which is a set of natural numbers) is not recursive in (x0, x1, x2, ...) with xn replaced by 0. Such x exists by standard results in recursion theory. For example, every real number Cohen generic over recursive sets can be split into infinitely many mutually generic predicates xn.
Let P be ∀i (¬¬xn(i) ⋁ ¬xn(i)). We have ¬□∃n (∀m≠n P(m) → P(n)).
Let T be a recursive tree of integer sequences under extension. We claim that T is well-founded iff □(∀n∃s (sequence s has length n ⋀ s∈T ⋀ P(s)) → ∃s∃t (s is incompatible with t ⋀ P(s) ⋀ P(t))). If T is well-founded, then we simply wait until incompatible s and t are given, and then copy the witnesses for P(s) and P(t). If T is not well-founded, then a "bad" witness for the antecedent will start to provide an infinite path through T and then once we commit to incompatible s and t, provide witnesses for every P except for P(s) or for P(t). Proof Complete
The proof shows that constructive truth for arithmetical statements of the form A→B where A and B are without '→' is Π11 complete. Also, by Proposition 3 (below), constructive truth for '∃'-free statements is Π11 hard.
Transfinite induction for P on '⊰', TI(P, ⊰) asserts ∀n(∀m⊰n P(m) → P(n)) → ∀n P(n).
Proposition 2: For every formula P and well-founded relation '⊰', □TI(P, ⊰).
Proof: To get a witness for ∀n P(n), request a witness for ∀m⊰n P(m) → P(n) for every n. Then, fulfill all requests for witnesses for P(m) as witnesses become available. By induction on the rank of n, for every n, a witness for P(n) will be provided. Witnesses for m⊰n are provided in ∀m (m⊰n → P(m)), so '⊰' need not be recursive.
Conversely, a form of constructive induction implies well-foundness.
Proposition 3: If '⊰' is a recursive strict partial-order given as such, and R is a universal Π01 predicate, then "⊰ is well-founded"↔□∀nTI(R(n)⋁ ¬R(n), ⊰).
Proof: An input-output pair for TI(R(n)⋁ ¬R(n), ⊰) can be converted into a finite boolean combination of {R(n, 0), R(n, 1), R(n, 2), …} asserting "input implies output". For a witness S, every such combination included must be true. We show that if '⊰' is ill-founded, then some combination included is not tautological. Let a0 ≻ a1 ≻ a2 ≻ … be infinite and consider the following witness T to the antecedent: For every i, require the correct truth-value of R(n, ai+1) before giving away R(n, ai); other than that, answer every R(n, m). Some (segment of T, (a0, truth value of ¬R(n, a0)) is included in S, but any such combination is non-tautological. Now, from any witness to ∀nTI(R(n)⋁ ¬R(n), ⊰), a non-tautological combination of (R(n, i))i can be extracted for every n, so by universality of R, the witness is non-recursive, which completes the proof.
In essence, the proof of Proposition 3 uses quantification over all Π01 predicates to approximate the idealized unknowable predicate G: A constructive witness for a statement using 'G' must work regardless of which set is {n: G(n)}. The same idea is used to prove the next theorem.
Theorem 4: Constructive arithmetical truth is Σ11 hard.
Proof: Let T be a recursive tree of integer sequences under extension. Let R be a universal Π01 predicate, and P(a, b) be R(a, b) ⋁ ¬R(a, b). We prove that T is ill-founded iff:
□∀n ((∀l∃s (sequence s has length l ⋀ s∈T ⋀ P(n, s)) → ∃s∃t (s is incompatible with t ⋀ P(n, s) ⋀ P(n, t)))→S(n)),
where S(n) asserts "there is a non-tautological finite boolean combination of {R(n, 0), R(n, 1), R(n, 2), …} that is not false." By universality of R, we have ¬□∀n S(n). If T is well-founded, then the antecedent has a recursive witness, and hence the full statement is not constructively true. On the other hand, if T is not well-founded, then any witness for the antecedent will have to respond to some branch s of the tree, and hence divulge a statement of the form ∀t (t is a subsequence of s) (¬)R(n, t) → (¬)R(n, u), where u is not a subsequence of s. Here '(¬)' means that '¬' can independently be either present or absent (but the statement must specify when '¬' is present). Now, that statement is not a tautology and hence witnesses S(n).
In contrast to theorems 1 and 4, we have the following theorem, which shows that in terms of the number of implications, the complexity of the formulas used in the proofs of the theorems above is optimal.
Theorem 5: Let φ be arithmetical and such that for every A→B in φ, A uses neither '→' nor '∃', except for bounded '∃'. (Negations do not count as implications.) Then, □φ is constructively equivalent to an arithmetical formula.
Proof Sketch: □φ ↔ ∃n "n is a witness to □φ". For statements without '→', strengthen the notion of witnesses by requiring that answers be given in order and without whitespace. Any witness can be so strengthened, so constructive truth is unaffected, and we show that under this change, being a witness to φ is arithmetical. W witnesses φ iff (W has the right syntactic form and) for every numerical input into φ for all witnesses input into φ, appropriate output is given. X witnesses A (in the strengthened sense) where A is an antecedent inside φ iff every initial segment of X is correct. By compactness, W witnesses φ iff for every numerical input into φ, there is a finite tree of (finite) witness inputs into φ such that W gives appropriate and complete numerical output for every witness input outside the finite tree (allowing false or incomplete output for false input). The above formula is arithmetical, which completes the proof.
Corollary to the Proof: Constructive truth for arithmetical statements for which every antecedent φ is as φ is in the theorem is Π11.
We conjecture constructive arithmetical truth to be complete for second order arithmetic and have the following partial results:
Proposition 6: The relation of being a witness is complete for second order arithmetic.
Proof: By inspection, for every φ, being a witness to φ is definable in second order arithmetic. Let A0 be ∀x∃y 0=0, and An+1 be An→(0=0 ⋁ 0=0). (By coding in whitespace, we could even have started with A-1 as 0=0 ⋁ 0=0, or without using whitespace, A-1 as ∀x(0=0 ⋁ 0=0).) We define a recursive function f such that for every infinite binary sequence X and every φ given as Π1n (n>0) but not as Π1n-1, φ(X) holds iff f("φ", X) is a witness to An. If φ is Π11, convert it to an assertion that a particular recursive-in-X relation is well-founded. Use the witness for the antecedent to guess an infinite descending path, and when that fails, give a witness to the consequent. Also, use additional delays to code X into f("φ", X). If φ is Π1n+1 (but not Π1n or Π11), then convert it to ∀Y ψ(X join Y) where ψ is Σ1n, and delay giving a witness to the consequent for as long as the candidate witness for the antecedent is f("¬ψ", X join Y).
Theorem 7: Constructive arithmetical truth is Π12 and Σ12 hard.
Proof: We build on the proofs of Theorem 4 and Proposition 6. As in Theorem 4, we quantify over all Π01 predicates. Let 'R' be a symbol for a Π01 predicate. For simplicity, we present our statements using R, and interpret □D as □∀n D(R'n) where R' is a universal Π01 predicate. Let P(n) be R(n) ⋁ ¬R(n). The Π12 hard formula □D will have D = A⋀B→C. A will assert ∀n∃s (sequence s has length n ⋀ s∈T ⋀ P(s)) → ∃s∃t (s is incompatible with t ⋀ P(s) ⋀ P(t)), where T is the tree of integer sequences that is effectively coded (say, as a primitive recursive predicate) by the free variable of A, and with sequences coded by odd natural numbers. B asserts ∀n(P(4n) ⋁ P(4n+2)). B is used as a second order universal quantifier; witnesses for B code real numbers through choices of 4n or 4n+2. C states ∃s∃u(∀n (n in sequence s) P(2n) ⋀ sequence u is not a subsequence of s ⋀ (∀t (t is a subsequence of s) (¬)R(t) → (¬)R(u))).
We claim that □D holds iff for every witness to B, there is an infinite path through T such that for every n in the path, P(2n) is given by the witness. To see that the claim implies the theorem, note that the statement is Π12 complete (as a function of the parameter of A). For Σ12 hardness, let E be D → "there is a true non-tautological finite boolean combination of {R(0), R(1), R(2), …}". Clearly, by universality of R, □E→¬□D, and in the proof of the claim, we will show ¬□D→□E.
Now, consider a witness X to B. Every witness to A will have to respond to every infinite path through T corresponding to X. If the Π12 statement is true, then such a path exists and hence (like in the proof of Theorem 4), by reading the witness for A, one can extract the information required for C. If the Π12 statement is false, let X be a counter-example witness for B. A "bad" witness Y for A will require correct answers to P and will delay giving away incompatible elements until the path used as input into A is past the point where some P(2n) is not given by X, and then give out P(s) and P(t) for incompatible s and t that are independent of the path. For every witness Z to D, the input-output pair corresponding to X and Y is not tautological. Thus, a non-tautological input-output pair can be extracted from Z through complete search, which completes the proof.
Question: What is the complexity of constructive arithmetical truth?
We expect that the proof of Theorem 7 can be generalized to prove that constructive arithmetical truth is complete for second order arithmetic. For Π1n hardness, let An+1 = (An ⋀ Bn → Cn) with A1 = A, Bn analogous to B (but using a different domain for each n), and Cn asserting existence of a true non-tautological combination of a certain type. However, there are combinatorial difficulties in actually stating a correct Cn, so we do not know how to prove the conjecture.
We note that An use the optimal number of implications since constructive truth for statements with implication nesting depth n>0 (or depth n+1 for statements corresponding to Theorem 5) is Π1n.
Question: Are there arithmetical statements not constructively equivalent to '∃'-free ones?
Note: Probably, the answer is yes and ∃n P(n) is such a statement where P is as in Theorem 1. On the other hand, we expect that every □φ is constructively equivalent to □ψ where ψ uses neither '∃' nor '□'. If □A(n) is equivalent to "n is a witness to φ", then □φ is equivalent to □∃n A(n) and may be equivalent to □(∀n(A(n)→B)→B) for appropriate B. A (and B) can likely be chosen without '□' and '∃'.
Narrow constructive truth is a particular modification of constructive truth in which witnesses are not completely given. A witness for narrow constructive truth provides a code for a recursive interactive function such that for every possible interaction, the witness requirements are met. The meeting of requirements is defined inductively on the complexity of the formula. If A is false, then the requirements for A are immediately violated. For A→B, multiple numbered instances can be launched, and different choices for the candidate witness for A require different instances. A new instance may copy the input and output (but not the internal state) from any point of an existing instance (it is unclear if omitting this provision would change which statements are narrow constructively true). Every instance for A→B must meet the requirements for B for as long as the requirements for A are met, including in the limit (that is at time infinity). If every instance meets the requirements, then the requirements for A→B are met even if answers are omitted along some path where the copying was done infinitely many times. For other connectives, the meeting of requirements is as usual. For example, in A⋁B, one must choose A or B, and then meet the requirements for the choice. Failure to choose violates the requirements at infinity but not at any finite time.
Narrow constructive truth is similar to constructive truth, with the difference limited to statements with implications inside antecedents. It satisfies all of the basic properties listed (except for the description of A→B in terms of mappings), and theorems 1, 2, 3, and 5. Narrow constructive truth implies constructive truth for statements without antecedents inside antecedents inside antecedents, and perhaps for all arithmetical statements. For this section only, '□' represents narrow constructive truth.
A key distinguishing feature of narrow constructive truth is that for A and C without '→', □((A→B)→C) ⋀¬□A⋀¬¬B → □C is narrow constructively valid (equivalently, constructively valid).
Theorem 8: Narrow constructive arithmetical truth is Π11 complete.
Proof:
By the proof of Theorem 1, narrow constructive truth is Π11 hard. To see that it (and the corresponding notion of witnesses) is Π11, a statement is narrow constructively true iff there is an integer (coding the narrow constructive witness) such that for every real number interacting with and trying to refute the alleged constructive witness, the witness requirements are met. The meeting of requirements is hyperarithmetically definable. Proof Complete
Thus, by using a universal Π11 formula, we can find a "universal" arithmetical formula φ such that for every arithmetical sentence ψ, □φ('ψ') iff □ψ. This does not contradict undefinability of truth since for some 'ψ', φ('ψ')→ψ is false.
The reasoning can be used to compute the expressive power of the full language, which allows nesting of the narrow constructive truth operator. A hyperjump of X is essentially the set of (standard codes for) well-founded relations that are recursive in X. For every natural number n, there is a formula φ that only uses '□' n times, such that □∀x(□φ('ψ(x)')↔□ψ(x)) (and hence □φ('ψ')↔□ψ if 'ψ' is a statement) whenever 'ψ' has at most n nested '□'; and {x:□φ(x)} has the same complexity (even under one-to-one polynomial time reducibility) as the (n+1)th hyperjump of 0. The proof is by induction on n, and is analogous to the proof of Theorem 8. The proof also shows that for expressible P and φ, "P is a witness to φ" is also expressible.
Before defining constructive analysis, we note that analysis can be interpreted in second order arithmetic. Analysis deals not with arbitrary functions but continuous and other reasonable functions, and these can be represented by real numbers. Under an appropriate representation, the theorems of analysis are almost all Π13, and are usually Π12. Moreover, most of the Π12 theorems have a natural Π11 strengthening by requiring that in ∀X∃Y φ(X, Y) Y is arithmetical in X. Similarly, most Π13 theorems ∀X∃Y∀Z φ(X, Y, Y) in analysis have a Π12 strengthening by requiring Y to be recursive in a finite hyperjump of X. Thus, analysis can essentially be interpreted through constructive truth in arithmetic. Philosophically, one can argue that natural numbers and constructive arithmetical truth are basic, so the high complexity of constructive arithmetical truth provides an (additional) ontological basis for analysis.
We use the language of second order arithmetic. Capital letters represent sets of natural numbers. Free variables need not be shown in schemas.
While there are different notions of constructive analysis, prominent among them is Brouwer's intuitionistic analysis. Under it, infinite binary sequences are given not as completed objects, but as a process that gives out zeroes and ones. Under the concept of choice sequences, we can make completely arbitrary choices as which natural numbers belong to a choice sequence X. We construe this to mean that any real number can be a choice sequence. Thus, the domain will include all sets of natural numbers (see Section 7 for discussion). Other approaches treat choice sequences either as a figure of speech or as a fundamentally non-classical construct. Also since the sets represent real numbers rather than being a shorthand for arbitrary properties, we will have ∀X∀n(X(n)⋁¬X(n)).
Answers must be given in finite time rather than after the process is completed. Therefore, we reinterpret ∀X to mean for all X and with answers given continuously in X. Under this view, every function is continuous on its domain, and ∀X(X=0 ⋁ ¬X=0) is false since one cannot always decide whether X=0 by looking at only a finite segment of X. Since the statements are not treated classically, this is not a contradiction. We use W(φ), φ is witnessable, for this interpretation of φ. We define "φ is continuous function realizable" to mean W(φ).
We formally define witnesses like in Section 2, except that being witnessable need not match classical truth. However, we do have W(¬φ)↔¬W(φ). Input in input-output pairs includes initial segments of the sequences for the second order universal quantifiers, and output includes initial segments of the sequences for the existential quantifiers. W witnesses ∀X φ(X) iff for all X, WX witnesses φ(X). As in Section 2, WX is obtained from W be selecting input-output pairs corresponding to X and and removing X from input. W witnesses ∃X φ(X) iff W provides arbitrarily long initial segments for a single X, and a witness for φ(X), but not initial segments incompatible with X. Treatment of other connectives (except '□') is unchanged.
Existence of non-constructive reals requires a change in the treatment of '□': Since ∃Y(Y=X) is valid, □∃Y(Y=X) should hold for all X, but ∃Y(Y=X) has a recursive witness only for recursive X.
A witness for □Sφ provides a standard code for a recursive in S witness to CLS(φ) where CLS is the universal closure except for first order variables and for variables in S. S is written as a list of second order variable symbols and is omitted when empty. S is treated as a set; for example, □X,Yφ ↔ □Y,Y,Xφ. Also, the semantics of '□' is definable in second order arithmetic, so we can treat '□' not as a primitive symbol but as a particular transformation of formulas.
To define an abstract theory of □Sφ, which should be valid in all domains, we can add '≤c' with S≤cT meaning S can be constructed from T. We allow ≤c to act on finite sets of elements, but with each element listed. We can axiomatize the theory by using the abstract theory of '□' for every □S (except that in ¬A→□S¬A, we require S to include all free second order variables of A, and analogously with the rules for '⋁', and '∃'), properties of ≤c (reflexivity, transitivity, S,T being the ≤c-least upper bound of S and T, and the empty set being the ≤c-least element (up to ≤c equivalence)), □Sφ → □S∀Xφ (X not in S), S≤cT → (□Sφ → □Tφ) (no element of S\T is free in φ), and □S∃Xφ(S, X) → ∃X≤cS □S,Xφ(S, X) (X not in S, and φ has no other free second order variables). Our constructive analysis satisfies additional properties including pairing and φ → ∃X□S,Xφ (completeness for witnessability; here S includes all free second order variables of φ), and in it, S≤cT means S is recursive in T.
Because of continuity (which is classically false) and compactness of 2N, we even have □( □S∀Xφ ↔ ∀X□S,Xφ ) (X not in S).
The entire discussion of Sections 3-5 generalizes to formulas with an arbitrary second order parameter X by replacing recursive with recursive in X and analogously replacing Π01 and other notions, and using □X in place of □.
We note that a witness for ∀X (φ(X)→ψ(X)) is simply a code for continuous function f such that if Y is a witness to φ(X), then f(X, Y) is a witness to ψ(X). (Because we allow whitespace in witnesses, we can require f to be total.)
Formulas without '∃' and '⋁' (and, but this is unnecessary here, with all atomic formulas negated) are called negative formulas and are treated classically. Every formula is classically equivalent to a negative one, so classical analysis can be interpreted in the constructive one. Conversely, the relation of being a witness is definable in analysis, so constructive analysis can be interpreted in the classical one.
Constructively, we define W(φ) as ∃X "X is a witness to φ", where the quoted statement is negative. We have □(φ↔W(φ)), so constructively, every formula is equivalent ∃X "a negative formula", and every negation equivalent to a negative formula. We expect that every □Sφ is constructively equivalent to □Sψ for an arithmetical ψ without '∃'.
Because the relation of being a witness is definable, we can define additional connectives by specifying witness requirements in terms of witnesses for the constituent formulas. We define a weak or non-constructive 'or' by: A witness for A⋁wB must provide X and Y such that X witnesses A or Y witnesses B. The following are constructively valid: A⋁wB ↔ B⋁wA, A⋁w(B⋁wC) ↔ (A⋁wB)⋁wC, ¬A⋁w¬¬A, A⋁B → A⋁wB, (A⋁wB) ⋀ ¬B → A, (B→C)→(A⋁wB→A⋁wC), □S(A⋁w B) → □S A ⋁w □S B, and (because of our particular treatment of witnesses) (A⋁wB → □S C)⋀¬¬(A⋀B) →□S C, but not □(A⋁wA) → A nor □A⋁w□A → □(A⋁wA). '⋁w' is the strongest (definable) connective satisfying □((¬A → B) ⋀ (¬¬A → C) → B⋁wC).
A generalization of the non-constructive 'or' is given by: A witness for ∃wn A(n) must provide X0, X1, X2, … such that for some n, Xn witnesses A(n). The quantifier ∃w satisfies the analogues of all of the above properties of '⋁w', and also □S ∃wn A ↔ ¬¬ □S A (n not free in A). For example, ∀n(A→B)→(∃wn A → ∃wn B) is constructively valid, which means that ∃w is non-modal and monotonic. A formula φ(..) is non-modal iff for all A and B, Clφ(A↔B)→(φ(A)↔φ(B)) is constructively valid, where Clφ(C) is the universal closure for variables free in C that are not free in φ(C).
We can also formalize the unknowable predicate G by treating ∀Gφ(G) as ∀Xφ(G) where G(m) is "{n: (m, n)∈X} is not finite" and X is not otherwise used in φ.
A constructive system for analysis can be defined as one in which proofs of φ can be constructively (and uniformly in φ) converted into (constructive) witnesses for the universal closure of φ. Continuous function realizability can also be treated classically, but then one would not have W(φ) to W(∀Xφ) as a rule of inference.
If φ is false, then W(φ) can only hold if φ has a negative occurrence of ∀X A(X) with A containing '∃' or '⋁' not in the scope of an antecedent (or negation) inside A (X can be any second order variable). Thus, we can form a classically correct subsystem by including all derivable (or witnessable) formulas not of this type, and using classically correct principles for other formulas. In constructivizing theorems of analysis, there is usually no problem in avoiding that type of formulas. Principles that are both classically and constructively correct include induction, transfinite induction, countable choice, and dependent choice. Apparently, even adding ¬¬∀X(A(X)⋁¬A(X)) will result (even in the presence of the above principles) in a system that is constructive with respect to formulas φ in which every positive (in φ) occurrence of ∀X that is inside an antecedent or negation is part of '∀X¬'.
A key constructively valid principle is countable choice ∀n∃X φ(X, n)→∃X∀nφ(Xn, n). Countable choice is a rather strong principle and implies constructivized comprehension: ∀n(φ(n)⋁¬φ(n)) ↔ ∃X ∀n (n∈X ↔ φ(n)) (X not free in φ). In combination with ¬¬∀n(φ(n)⋁¬φ(n)) (which is also constructively valid), constructivized comprehension is quite powerful and implies the negative form of full comprehension. Constructively, we also have transfinite induction ¬∃(an infinite ⊰-descending path) → TI(φ,⊰) for all formulas ⊰ and φ. We also have Markov's principle, which simplifies to ∀X(¬∀n¬X(n) → ∃nX(n)).
We quantify over real numbers, continuous functions, and infinite sequences of integers (points in the Baire space) by using their effective binary codes and writing for example ∀X("X codes an infinite sequence of integers" → φ(X)). A real number is coded by a nested sequence of intervals with rational endpoints. By using a conservative and essentially definitional extension, one can also quantify over real numbers (and open sets and continuous functions) directly rather than through coding.
Constructively, we have the continuity principle ∀X∃Y φ(X, Y) ↔ ∃(continuous f) ∀X φ(X, f(X)), and analogously with more quantifiers. This also holds for quantification over the Baire space NN. However, as stated the principle would fail for real numbers and should be modified to use ∃!Y (here, the uniqueness is for the real number coded by Y rather than the code Y). This is needed because different sequences can denote the same real number.
In contrast to arithmetic, many basic theorems of analysis are not constructively true (except in the negative form), and most of those that are true have to be stated carefully. Clearly, constructive analysis should be meant to complement rather than replace classical analysis. On the other hand, many non-constructive theorems have constructive versions. For example, the following is a constructive version of the intermediate value theorem: If f is a continuous function (on real numbers) that has both a positive and a negative value, and if, for no interval of positive length, f vanishes on every point of the interval, then f has a zero.
It is crucial that this theorem and other theorems in analysis are stated as implications rather than disjunctions. One generally cannot decide from the code whether the conditions of the theorem apply. However, given the conditions, the construction must succeed. A major reason to study constructive analysis is that it gives effective versions of theorems in analysis. The added condition for the constructive intermediate value theorem may sound strange, but the point is that under these conditions we can actually compute a zero of f and to do so uniformly in f.
Constructively, it is not the case the every bounded monotonic sequence of real numbers has a limit. To make the theorem constructively true we could include existence of the Turing jump of the sequence (or a certain much weaker property) as a condition. A crucial substitute that we do have is compactness of the unit interval: Every (countable) open cover has a finite subcover. Note that the compactness fails in recursive analysis, and the difference is that we require our continuous functions to be continuous even at non-recursive real numbers. The compactness is a consequence of the Fan Theorem, also called constructive Weak König's Lemma. An equivalent of the constructive Weak König's Lemma is: Every countable theory that does not have a model (with a complete diagram) has an inconsistency.
Most consequences of the Weak König's Lemma in analysis rely only on the constructively true form, so in terms of reverse mathematics, constructive analysis corresponds more closely to WKL than to RCA. For example, even constructively, continuity implies uniform continuity for functions from a complete totally bounded metric space.
Constructive reverse mathematics analyzes formal relationships between constructively true statements. Here, the emphasis is on deriving strong principles in weak theories.
Every constructive theory S has its classical counterpart T consisting of first order logic and negative theorems of S. Conversely, every theory S satisfying ED and containing intuitionistic RCA0 and φ↔W(φ) is determined by its classical counterpart T. RCA0 consists of basic arithmetic, Σ01 induction and recursive comprehension. ED stands for explicit definability, and this form of ED is sufficient: If S proves a sentence ∃Xφ(X), then for some n, S proves ∃X"the nth Turing machine outputs X and φ(X)". Because any constructive proof can be converted into such a recursive code, any reasonably closed constructive system satisfies ED. For any classical T containing RCA0, the (for sound T, constructive) counterpart S proves a sentence φ iff for some n, T proves "n witnesses □φ". S can be axiomatized by intuitionistic RCA0 + φ↔W(φ) + negative translation of T. S satisfies (the above form of) ED and is conservative over T for negative formulas. (ED is most often stated to imply Σ01 soundness for consistent S, but the above form of ED allows us to state the general correspondence between S and T.)
Constructive analysis can be done in a weak formal system. Classical mathematics in weak systems is developed in [Simpson 1999], and doing constructive mathematics is mostly analogous. Many results can be proved even in intuitionistic RCA0 + φ↔W(φ). The system is strong enough to prove the full continuity principle for Baire space, which implies countable choice and hence constructivized comprehension. On the other hand, the system is weak enough to be consistent with "every real number is not not recursive", an assertion that would turn our analysis into an analogue of constructive recursive analysis except that recursive codes cannot be extracted from real numbers.
Because of Σ01 induction, the continuity principle (for Baire space) also implies a form of dependent choice: ∀X∃Yφ(X,Y) → ∃X(X0=0 ⋀ ∀nφ(Xn, Xn+1)) where X and Y range of the Baire space (this implies countable choice and is classically correct). Over intuitionistic RCA0 + φ↔W(φ), the (constructively) stronger ∃Xφ(0,X)⋀∀X(∃Zφ(Z,X) → ∃Yφ(X,Y)) → ∃X(X0=0 ⋀ ∀nφ(Xn, Xn+1))is equivalent to full induction (equivalently, induction for negative formulas).
Analysis can be developed in intuitionistic RCA0 by using added assumptions about functions such as having a modulus of uniform continuity. Bishop's analysis can essentially be carried out in intuitionistic RCA0 + Countable Choice; and the use of countable choice can likely be eliminated by replacing it with recursive comprehension, and by using ∃X∀nφ(Xn, n) rather than ∀n∃X φ(X, n) in theorems and definitions (and when appropriate, analogously replacing ∀m∃n φ(m, n)).
The schema φ↔W(φ) is actually equivalent over intuitionistic RCA0 to Markov's Principle ∀X(¬∀n¬X(n) → ∃nX(n)) plus generalized continuity principle: ∀X(¬φ(X) → ∃Yψ(X,Y)) → ∃(continuous partial f) ∀X(¬φ(X) → "f(X) is defined" ⋀ ψ(X,f(X))). The proof of φ↔W(φ) is by induction on the complexity of φ. Markov's principle follows from φ↔W(φ) because of the way W(φ) is formulated.
A classically correct subsystem of intuitionistic RCA0 + φ↔W(φ) is intuitionistic RCA0 + Markov's Principle + Countable Choice. Intuitionistic RCA0+ φ↔W(φ) is conservative over the subsystem for formulas in which every negative occurrence of '∀X' classical (that is (provably) replaceable by '∀X¬¬'). (The proof is be showing W(φ)→φ for these formulas.) Moreover, countable choice is unneeded for formulas with every negative occurrence of '∀' classical. By extension, the conservation result also holds in the presence of additional negative axioms. This way constructive analysis can be effectively done even in a classically correct subsystem. Note that while countable choice is classically a rather strong principle, constructively it can be part of a weak formal system.
Most constructive results can actually be proved in just the constructive counterpart of WKL0, that is in intuitionistic RCA0 + φ↔W(φ) + constructive Weak König's Lemma. The system proves compactness of the unit interval and results that follow from the compactness, including for example, the constructive intermediate value theorem. (That theorem is equivalent over intuitionistic RCA0 to Markov's principle plus constructive Weak König's Lemma. In fact, most constructive theorems relying on compactness are equivalent over RCA0 + φ↔W(φ) to constructive Weak König's Lemma.) Still, the system is weak enough to be Π02 conservative over primitive recursive arithmetic and to be consistent with "not every Turing machine either halts or does does not halt on the empty tape".
The intuitionistic counterpart of ACA0 is (equivalent to) intuitionistic RCA0 + φ↔W(φ) + for arithmetical formulas φ, ¬¬∀n(φ(n)⋁¬φ(n)). Finally, over intuitionistic RCA0 + φ↔W(φ), the schema ¬¬∀n(φ(n)⋁¬φ(n)) is equivalent to the negative translation of the full second order arithmetic with countable choice. For an overview of the reverse mathematics of the law of the excluded middle, see for example [Ishihara 2004]; the base system there can likely be taken as intuitionistic RCA0 + Countable Choice.
We conclude with a principle of constructive reasoning whose (constructive) correctness is not provable in ZFC: ¬¬(∀X∃Y (φ(X)↔ψ(Y)) ⋁ ∀Y∃X (φ(X)↔¬ψ(Y))) where φ and ψ are negative (alternatively, negated) (φ and ψ may have additional parameters, but all occurrences of X and Y are shown). Because of the continuity principle, constructive correctness of the schema is equivalent to classical truth of projective Wadge determinacy, which is not provable in ZFC. Projective Wadge determinacy is implied by and probably equivalent to projective determinacy.
Since the law of excluded middle A ⋁ ¬A is a logical truth, one may wonder in what general sense can it fail. The answer is that constructively, 'A' is treated not just as a proposition to be true or false, but also as information or knowledge. Classically, for every formula and tuple of parameters, the formula either holds for the parameters or not, and no further structure is considered. Constructively, however, true statements are distinguished according to the information required of them. Logical connectives, beyond their effect on truth-values, also act on and help specify the information required. For example, in ∀n (A(n) ⋁¬A(n)), the information includes for every n whether A holds. Constructively, one uses ¬¬A to assert the truth of A without giving the information corresponding to A.
A witness for A consists of all information necessary for A; ¬A holds iff A has no witnesses. Note that the information contained in the witness does not include the reasons that the information is correct; for example, a witness for ¬A just asserts ¬A and need not explain why A fails. Constructively, a formula with an assignment of free variables is entirely determined by the requirements on witnesses. The general meaning of logical connectives is as listed in Section 2, and in a way consistent with intuitionistic logic, each framework specifies the details, including what it means to give a witness for the antecedent. A is constructively true iff a finite amount of knowledge can be transformed (in the required sense) into information sufficient for A; and a witness for □A supplies that finite information (which can be non-unique). A constructive justification of A is a classical justification that the integer specified witnesses □A.
Some constructive frameworks have ¬∀n (A(n) ⋁¬A(n)) for some A. The reason is that the universal quantifier acts not just on the truthfulness of the assertions, but also on the information required. In these frameworks, the information required for ∀n (A(n) ⋁¬A(n)) may (in a specific sense) be impossible, which falsifies ∀n (A(n) ⋁¬A(n)). The classical universal quantifier is '∀x¬¬', which ignores which information is required, and '∀x' is a strengthening of that quantifier. Intuitionistic logic proves ∀n¬¬(A(n) ⋁¬A(n)), so for formulas with the intensional aspects suppressed (including all negative formulas), intuitionistic logic is simply the full classical logic.
The high complexity of constructive truth reminds us of a key philosophical question: Are there other acceptable notions of constructive arithmetical truth? Our answer is no. Other notions such as recursive realizability and narrow constructive truth may be useful, but they do not meet all of the requirements. All of the conditions on the witnesses except the implication one are straightforward. The definition of constructive implication is fixed through a combination of several requirements. Key properties of implication must be true constructively, and constructively true statements must be true. These requirements force us to use non-recursive witnesses in defining constructive truth. This compels us to provide witnesses like real numbers, which essentially fixes how the witnesses are given.
Every true 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 for arithmetical statements would be (mostly) weakened yet remain much stronger than simply truth. However, we cannot do that since we have extended the language of arithmetic, which requires non-arithmetical witnesses. We cannot place different complexity requirements (in a truth-altering way) on witnesses for P than for Q since we may discover P↔Q constructively, which can cause inconsistency.
Intuitionistic logic is suitable for various things, and there are different notions of constructive, of which constructive truth is just the default notion. Another interesting approach to constructivity is to use the full theory of finite types, and treat witnesses for statements with implications as functionals of higher types. A statement would hold constructively iff it is witnessed by a constructive functional, and constructive functionals would be the recursive ones. By using ∀x(A(x)→∃yB(x,y)) ↔ ∃F∀x(A(x)→ B(x,F(x))) (A and B are negative), every formula would be equivalent to a list of existential quantifiers followed by a negative formula. This approach would allow making constructive sense of, for example, what is implied by ∀X(∃n X(n) ⋁ ∀n¬X(n)) (the ability to test whether any given real number is 0). However, for constructivity, we would have to allow functionals to be partial (in which case B(F(x)) implies F(x) exists) and either non-extensional or multi-valued, and the semantics is unclear. Also, in constructive arithmetic, computations should be based on numbers rather than on uncountable objects; so for constructive truth, we have to require that witnesses act based on finite segments rather than on the full witnesses, which leads to a kind of overspill exploited in Theorems 4 and 7.
We believe that the uniqueness extends to analysis. Our constructive analysis is more usable than any other previously proposed. (Compare it for example with Troelstra's syntactic treatment of choice sequences.) Our constructive treatment of implication allows all real numbers to be present in a negative form, yet maintain constructivity. The naturalness with which our framework extends to analysis confirms its correctness for arithmetic.
Some critics may question whether our analysis is really constructive. However, whether or not it represents an intuitionistic foundational stance, our analysis is constructive in that constructive truth of statements amounts to truth of the effective versions of those statements, and in that constructive proof of a statement specifies through a recursive procedure a way that the existential aspects of the statement are satisfied. For example, existence of a non-recursive real number is not claimed to be constructively true.
Our constructive analysis is derived from two choices, and a reasonable formalizations of the choices. First, we allow any real number in the domain. We have to allow every real number that might be generated by a physical or a mental process. However, our analysis is objective and mathematical (as opposed to being a physical theory), so it has to be independent of physical laws and of human mental capabilities. Moreover, even under physical laws as currently understood, many physical processes are random, so not every physical process is recursive. This compels us to include every real number.
Second, we reinterpret ∀X to mean for all X and with answers given continuously in X. Here, the key issue is how real numbers are given. One possibility is that they are given as complete infinite objects. In that case, computations will have to work with infinite objects directly rather than through finite codes and approximations. There are several inequivalent approaches to that, and infinite computation is a fruitful area of research. However, as far as it is known, humans and (physical) computers work only with finite objects, and generally, constructivists view real numbers as descriptions and as limits of finite approximations rather than as metaphysically existing infinite sets. Through finite approximations is also how real numbers are obtained from physical systems. Therefore, we require witnesses to provide answers based on finite segments to the sequences, which amounts to the continuity condition. The continuity also holds in Brouwer's intuitionism and (for extensional functions) in recursive analysis.
We hope our paper makes constructive analysis more appealing and its study more productive.
[Bishop 1967] Bishop, Errett. Foundations of Constructive Mathematics. McGraw-Hill, New York.
[Ishihara 2004] Ishihara, Hajime. "Informal Constructive Reverse Mathematics". Available: http://www.cs.auckland.ac.nz/CDMTCS/researchreports/229hajime.pdf
[Kleene 1965] Stephen Cole Kleene and Richard Eugene Vesley. The foundations of intuitionistic mathematics, especially in relation to recursive functions. Amsterdam, North-Holland Pub. Co.
[Moschovakis 2005] Moschovakis, Joan. Notes on the Foundations of Constructive Mathematics. Available: http://www.math.ucla.edu/~joan/newnotes.ps
[Simpson 1999] Simpson, Stephen. Subsystems of Second Order Arithmetic. Springer, Berlin.
[Troelstra 1977] "Aspects of Constructive Mathematics" in Handbook of Mathematical Logic, edited by Jon Barwise.