We will prove a simple theorem (saying that if every element is minimum or maximum then there is a minimum) in four calculi. The first has free variables and is most flexible. Thus, it is best suited for search. We would not have been able to find the proof easily without it. The following calculi become more and more restrictive. Nevertheless, the whole transformation seems to be the only proper way to find proofs in natural deduction for classical logic.

Example 0.1 (Free Variable Liberalized Sequent Calculus)

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)} ⇒ ∃x. ∀y. Q(x, y)

An α- and two γ-steps yield:

∀y. Q(x^{∃}, y), ¬\binom{∀u. Q(u, v^{∃})}{∨ ∀w. Q(v^{∃}, w)}, ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

A β-step yields as first sequent, presented after a γ- and a liberalized δ-step generating the variable-condition \xymatrix{x^{∃} \ar[r]_{R} & y^{∀,s}} :

Q(x^{∃}, y^{∀,s}), ¬Q(u^{∃}, v^{∃}), ¬∀u. Q(u, v^{∃}), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

After closing this with σ := {u^{∃}↦x^{∃}, v^{∃}↦y^{∀,s}}, the variable-condition for the still present variables is still the same. The second sequent of the above β-step after applying σ is:

¬∀w. Q(y^{∀,s}, w), ∀y. Q(x^{∃}, y), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

Note that we cannot close this directly because {x^{∃}↦y^{∀,s}} is not an existential R-substitution. Instead, we need a second γ-step on the last formula with immediate instantiation to get

∀y. Q(y^{∀,s}, y), ¬∀w. Q(y^{∀,s}, w), ∀y. Q(x^{∃}, y), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

which is a tautology after λα-rewriting.

A version of the above proof without free existential variables (where all γ-steps instantiate immediately) is given in the example below. Note that, while the order of proof steps in the above example was chosen quite freely, we now have to do them in a precise order, changing from αγγβγδ … to αγδγβγ … because the δ-step must precede the second γ-step.

Example 0.2 (Ground sequent calculus)

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)} ⇒ ∃x. ∀y. Q(x, y)

An α-, a γ-step, and a δ-step yield:

Q(x^{∀}, y^{∀}), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

Just now it becomes possible to do the γ-step yielding

¬\binom{∀u. Q(u, y^{∀})}{∨ ∀w. Q(y^{∀}, w)}, Q(x^{∀}, y^{∀}), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

A β-step yields as first sequent with a subsequent γ-step the tautology

¬Q(x^{∀}, y^{∀}), ¬∀u. Q(u, y^{∀}), Q(x^{∀}, y^{∀}), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

The second sequent of the above β-step is also presented after a γ-step:

∀y. Q(y^{∀}, y), ¬∀w. Q(y^{∀}, w), Q(x^{∀}, y^{∀}), ¬∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ∃x. ∀y. Q(x, y)

which is a tautology after λα-rewriting.

Now, when we want to make an antecedent + succedent proof of this, where the succedent consists of at most one formula, it becomes clear that we have to add a non-intuitionistic step:

Example 0.3 (Quasi-Intuitionistic Calculus)

⟶ ∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)} ⇒ ∃x. ∀y. Q(x, y)

An α-step and a non-intuitionistic step yield:

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y) ⟶ ∃x. ∀y. Q(x, y)

A γ-step and and a δ-step yield:

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y) ⟶ Q(x^{∀}, y^{∀})

Just now it becomes possible to do the γ-step yielding

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y), \binom{∀u. Q(u, y^{∀})}{∨ ∀w. Q(y^{∀}, w)} ⟶ Q(x^{∀}, y^{∀})

A β-step yields as first sequent with a subsequent γ-step the tautology

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y), ∀u. Q(u, y^{∀}), Q(x^{∀}, y^{∀}) ⟶ Q(x^{∀}, y^{∀})

The second sequent of the above β-step is

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y), ∀w. Q(y^{∀}, w) ⟶ Q(x^{∀}, y^{∀})

Now, after removing the succedent formula, we have to activate the formula of the nonintuitionistic step

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y), ∀w. Q(y^{∀}, w) ⟶ ∃x. ∀y. Q(x, y)

After a γ-step we get

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}, ¬∃x. ∀y. Q(x, y), ∀w. Q(y^{∀}, w) ⟶ ∀y. Q(y^{∀}, y)

which is a tautology after λα-rewriting.

A translation into a natural deduction proof of this looks the following way.

Example 0.4 (Natural Deduction)

\begin{matrix}[∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)}] & 1 \\ ( & \begin{aligned}& ∀u. Q(u, y^{∀}) \\ ∨ & ∀w. Q(y^{∀}, w) \end{aligned} & ) \end{matrix}∀E \begin{matrix}[∀u. Q(u, y^{∀})] & 3 \\ Q(x^{∀}, y^{∀}) \end{matrix}∀E \begin{matrix}\begin{aligned}\begin{matrix}[∀y. Q(y^{∀}, y)] & 4 \\ ∃x. ∀y. Q(x, y) \end{matrix}∃I & [¬∃x. ∀y. Q(x, y)]^{2} \\ & ⊥ \end{aligned} & ⇒E \\ Q(x^{∀}, y^{∀}) \end{matrix} ; ⊥_{i}

Q(x^{∀}, y^{∀}) ∨E^{3,4}

∀y. Q(x^{∀}, y) ∀I

∃x. ∀y. Q(x, y) ∃I [¬∃x. ∀y. Q(x, y)]^{2}

⊥ ⇒E

∃x. ∀y. Q(x, y) ⊥2 c

∀v. \binom{∀u. Q(u, v)}{∨ ∀w. Q(v, w)} ⇒ ∃x. ∀y. Q(x, y) ⇒I^{1}