What are the features that make this proof constructive?

Question

Below is an inductive proof of an integer square root theorem from a previous posting.

$\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$

The proof was done using natural deduction in the Fitch system.

In the answer to my original posting it was mentioned that this proof is "constructive". My first question is what are the exact features that make this proof constructive?

Constructive Axioms My intuitive understanding is that a constructive axiom is one where certain given things uniquely determine the existence of another thing. Are there constructive axioms in the above proof? Where can I find an authoritative definition and example of the term constructive axiom?

Answer 1

Just addressing the first part of your question:

As already stated in the comments, the term constructive is usually used in the context of a proof of an existentially quantified statement (as in your proof of the statement "for all x exists y") and means that the proof provides a concrete example for an object that satisfies the formula, rather than just arguing that some element with the desired properties must exist without giving an actual instance of such an object.

While we're already at square roots, consider the following claim:

There exist irrational numbers $x$ and $y$ such that $x^y$ is rational.

We can show this in classical logic by employing the law of excluded middle ($\phi \lor \neg \phi$).

Clearly, $\sqrt{2}$ is irrational.
Now we do a proof by cases for the statement "$\sqrt{2}^\sqrt{2}$ is rational or $\sqrt{2}^\sqrt{2}$ is not rational":
Either $\sqrt{2}^\sqrt{2}$ is rational. Then with $x = y = \sqrt{2}$, the proposition holds.
Or $\sqrt{2}^\sqrt{2}$ is irrational. Then with $x = \sqrt{2}^\sqrt{2}$ and $y = \sqrt{2}$, the proposition follows from the fact that $x^y = {\sqrt{2}^\sqrt{2}}^\sqrt{2} \sqrt{2}^{\sqrt{2} \cdot \sqrt{2}} = \sqrt{2}^2 = 2$. $\quad \square$

So we proved an existentially quantified statement without having determined an actual value for $x$ and $y$, because the proof doesn't decide which of the cases is true. Therfore, the above proof is non-constructive.

If you presented the proof as a formal deduction, it would look something like this:

You see that the last rule application is a disjunction elimination for the LEM, rather than an $\exists Intro$, which occurs only in the subproofs of each of the disjunctive cases. So although the main/outermost operator of the formula is the existential quantifier, the main/outermost operation by which the formula is derived in the formal proof is not an introduction rule for the existential quantifier, which is the formal-proof-theoretic way of capturing the non-constructiveness of the proof.

Logics which allow for non-constructive proofs are also sometimes called non-constructive. Intuitionistic logic, in which the law of excluded middle doesn't hold, is a constructive logic.

Now to your example:

In each of the cases, existential introduction was used on a formula with a concrete term:

• In the base case, $\exists y$ is introduced from $0$;
• in the first inductive case, $\exists y$ is introduced from $b$;
• in the second inductive case, $\exists y$ is introduced from $s(b)$.

While these existential introductions only occur in subproofs for each of the steps in the induction, the remainder of the proof is just the generalization to all natural numbers because we need to handle the additional existential quantification that scopes over the existential one - as mentioned in the comments, the proof provides us with a means to construct a suitable $y$ for all $x$. The heart of the (universally quantified) existential proof lies at the $\exists I$ applications which are grounded on concrete instances of objects that satisfy the formula at any level of the induction/for any shape of the $x$'es. At no point did we need to employ the law of excluded middle or run into otherwise uncertainties about the exact nature of the existing object. This is why the proof is constructive.