Four approaches to extension by axioms

1. Addition of axioms A into sequent calculus in the form of sequents ⇒ A by which derivations can start. Leads to failure of cut elimination.

2. Gentzen (1938, sec. 1.4): add “mathematical basic sequents”

P_{1}, …, P_{m} ⇒ Q_{1}, …, Q_{n}.

By Gentzen’s “Hauptsatz,” the cut rule can be pushed into such basic sequents.

3. Gentzen’s consistency proof of elementary arithmetic (1934, sec. IV.3): treat axioms as a context Γ, and prove results of form Γ ⇒ C. Cut elimination applies.

4. Axioms as rules. All these approaches are equivalent, but the fourth is the best suited for proof analysis.

D finite set of regular formulas. Definition

(a) A-system for D: sequent system with axioms, G3ipm+LW+RW+ LC+RC+Cut+AD; AD set of sequents ⇒ D from D in D. Derivability of a sequent Γ ⇒ Δ in an A-system where sequents from AD may appear as premisses denoted by ⊢_{AD} Γ ⇒ Δ.

(b) B-system for D: sequent system with basic sequents, G3ipm+LW+ RW+LC+RC+Cut+BD, where BD is the set of regular sequents corresponding to elements of D. Derivability of a sequent Γ ⇒ Δ in a B-system, where sequents from BD may appear as premisses, denoted by ⊢_{BD} Γ ⇒ Δ.

(c) C-system for D: sequent system with a context. Derivability of a sequent Γ ⇒ Δ in a C-system, where instances of formulas in CD appear in the antecedent, denoted by ⊢_{CD} Γ ⇒ Δ.

(d) R-system for D: sequent system with rules, G3ipm+RD, where RD is the set of rules of inference given by the regular decomposition of the formulas in D. Derivability of a sequent Γ ⇒ Δ in an R-system, where rules from RD are permitted, denoted by ⊢_{RD} Γ ⇒ Δ.

Theorem ⊢_{AD} Γ ⇒ Δ iff ⊢_{BD} Γ ⇒ Δ iff ⊢_{CD} Γ ⇒ Δ iff ⊢_{RD} Γ ⇒ Δ.

Predicate logic with equality

Primitive relation a = b a = a (reflexivity) a = b &A(a/x) ⊃ A(b/x) (replacement scheme) In the usual treatment (B-system), add basic mathematical sequents

⇒ a = a

a = b, P (a/x) ⇒ P (b/x)

By Gentzen’s “extended Hauptsatz” cuts can be reduced to cuts on axioms, but cut elimination fails. For instance, there is no cut-free derivation of symmetry. (Weakening and) contraction must be assumed.

We restrict the replacement scheme to atomic predicates P, Q, R, … and convert the axioms into rules,

{a = a, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Ref}  {a = b, P (a/x), P (b/x), Γ ⇒ Δ \atop a = b, P (a/x), Γ ⇒ Δ}^{Repl}

G3im and G3c plus Ref and Repl give intuitionistic and classical predicate logic with equality. Theorem The rules of weakening, contraction and cut are admissible in predicate logic with equality.

Lemma The replacement axiom a = b, A(a/x) ⇒ A(b/x) is derivable for arbitrary A. Theorem The replacement rule

{a = b, A(a/x), A(b/x), Γ ⇒ Δ \atop a = b, A(a/x), Γ ⇒ Δ}^{Repl}

is admissible for arbitrary predicates A.

Our cut- and contraction-free calculus is equivalent to the usual calculi. But the formulation of equality axioms as rules permits proofs by induction on height of derivation. The conservativity of predicate logic with equality over predicate logic illustrates such proofs. To prove the conservativity, we show that Ref can be eliminated from the derivation. Rule of replacement has an instance with a duplication. Closure condition is satisfied: instance where both duplications are contracted is an instance of reflexivity. For the proof of conservativity, the closure condition satisfied by adding the contracted instance of Repl:

{a = b, b = b, Γ ⇒ Δ \atop a = b, Γ ⇒ Δ}^{Repl^{∗}}

Lemma If Γ ⇒ Δ has no equalities and is derivable in G3c+Ref+ Repl+Repl^{∗}, no sequents in its derivation have equalities in the succedent. Lemma If Γ ⇒ Δ has no equalities and is derivable in G3c+Ref+ Repl+Repl^{∗} it is derivable in G3c+Repl+Repl^{∗}. Proof: We show that all instances of Ref can be eliminated from a given derivation, by induction on the height of derivation on a topmost instance

{a = a, Γ′ ⇒ Δ′ \atop Γ′ ⇒ Δ′} ^{Ref}

If the premiss is an axiom also the conclusion is, since by the above lemma Δ′ contains no equality, and the same if it is a conclusion of L⊥. If the premiss has been concluded by a logical rule, apply the inductive hypothesis to the premisses and then the rule. If the premiss has been concluded by Repl there are two cases, according to whether a = a is or is not principal. In the latter case the derivation is, with Γ′ = P (b/x), Γ′′,

{a = a, b = c, P (b/x), P (c/x), Γ′′ ⇒ Δ′ \atop a = a, b = c, P (b/x), Γ′′ ⇒ Δ′} ^{Repl}

b = c, P (b/x), Γ′′ ⇒ Δ′ Ref

By permuting the two rules, the inductive hypothesis can be applied. If a = a is principal, the derivation is, with Γ′ = P (a/x), Γ′′,

{a = a, P (a/x), P (a/x), Γ′′ ⇒ Δ′ \atop a = a, P (a/x), Γ′′ ⇒ Δ′} ^{Repl}

P (a/x), Γ′′ ⇒ Δ′ Ref

By height-preserving contraction, there is a derivation of a = a, P (a/x), Γ′′ ⇒ Δ′ to which the inductive hypothesis applies, giving a derivation of Γ′ ⇒ Δ′ without rule Ref.

If the premiss of Ref has been concluded by Repl^{∗} with a = a not principal the derivation is

{a = a, b = c, c = c, Γ′ ⇒ Δ′ \atop a = a, b = c, Γ′ ⇒ Δ′} ^{Repl^{∗}}

b = c, Γ′′ ⇒ Δ′ Ref

The rules are permuted and the inductive hypothesis applied. If a = a is principal the derivation is

{a = a, a = a, Γ′ ⇒ Δ′ \atop a = a, Γ′ ⇒ Δ′} ^{Repl^{∗}}

Γ′ ⇒ Δ′ Ref

and we apply height-preserving contraction and the inductive hypothesis. QED. Theorem If Γ ⇒ Δ is derivable in G3c+Ref+ Repl+Repl^{∗} and if Γ, Δ contain no equality, then Γ ⇒ Δ is derivable in G3c.

Herbrand’s theorem for universal theories T theory with a finite number of purely universal axioms and classical logic. Turn the theory T into a system of nonlogical rules: first remove the quantifiers from each axiom, then convert the remaining part into nonlogical rules. The resulting system will be denoted G3cT. Theorem: Herbrand’s theorem: If the sequent ⇒ ∀x∃y_{1} … ∃y_{k}A, with A quantifier-free, is derivable in G3cT, then there are terms t_{i_{j}} with i ⩽ n, j ⩽ k such that

⋁_{i=1}^{n} A(t_{i_{1}}/y_{1}, …, t_{i_{k}}/y_{k})

is derivable in G3cT.

Proof: Suppose that k = 1. The derivation of ⇒ ∀x∃yA ends with

\begin{matrix}{⇒ A(z/x, t_{1}/y), ∃yA(z/x) \atop ⇒ ∃yA(z/x)} & R∃ \\ ⇒ ∀x∃yA \end{matrix}_{R∀}

Every sequent in the derivation is of the form

Γ ⇒ Δ, A(z/x, t_{m}/y), …, A(z/x, t_{m+l}/y), ∃yA(z/x)

where Γ, Δ consist of subformulas of A(z/x, t_{i}/y), with i < m. Consider the topsequents of the derivation. If they are axioms or conclusions of L⊥ they remain so after deletion of the formula ∃yA(z/x). If they are conclusions of zero premiss nonlogical rules, they remain so after the deletion since the right context in these rules is arbitrary. After deletion, every topsequent in the derivation is of the form

Γ ⇒ Δ, A(z/x, t_{m}/y), …, A(z/x, t_{m+l}/y)

Making the propositional and nonlogical inferences as before, but without the formula ∃yA(z/x) in the succedent, produces a derivation of

⇒ A(z/x, t_{1}/y), …, A(z/x, t_{m−1}/y),
A(z/x, t_{m}/y), …, A(z/x, t_{n}/y)

and conclusion by applications of rule R∨. QED.

If the theory T is empty we have Corollary If ⇒ ∃xA is derivable in G3c, there are terms t_{1}, …, t_{n} such that ⇒ A(t_{1}/x) ∨ … ∨ A(t_{n}/x) is derivable.

Theory of equality: Basic relation a = b with the axioms EQ1. a = a, EQ2. a = b & a = c ⊃ b = c. Symmetry of equality follows by substituting a for c in EQ2. Transitivity is directly an instance of the replacement axiom, with A equal to x = c. Addition of the rules

{a = a, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Ref}  {b = c, a = b, a = c, Γ ⇒ Δ \atop a = b, a = c, Γ ⇒ Δ}^{Trans}

gives a calculus G3im+Ref+Trans the rules of which follow the rule-scheme. A duplication in Trans is produced in case b is identical to c, but the corresponding contracted rule is an instance of rule Ref. The closure condition is satisfied and the structural rules admissible. Occurences of atoms of the form a = a disappear in Ref, however...

Theorem (subterm property) All terms in a minimum size derivation of Γ ⇒ Δ in G3EQ are terms in the conclusion. Proof: Consider an atom a = a active in Ref and trace it along the derivation. If it is never principal, it can be removed altogether, and Ref as well, with subsequent shortening of the derivation. If it is principal in an axiom, a is found in Δ. If if is principal in Trans, it has the form

{a = c, a = b, a = c, Γ ⇒ Δ \atop a = a, a = c, Γ ⇒ Δ}^{Trans}

Apply height-preserving contraction to the premiss and get a shorter derivation. QED Theory of apartness: Basic relation a ≠ b with the axioms

AP1. ∼a ≠ a, AP2. a ≠ b ⊃ a ≠ c ∨ b ≠ c.

The rules are

a ≠ a, Γ ⇒ Δ^{Irref}
\begin{matrix}a ≠ c, a ≠ b, Γ ⇒ Δ & b ≠ c, a ≠ b, Γ ⇒ Δ \\ a ≠ b, Γ ⇒ Δ \end{matrix}^{Split}

Both rules follow the rule-scheme, the closure condition does not arise because there is only one principal formula, and therefore structural rules are admissible in G3im+Irref+Split. Exercise: Prove the subterm property for the theory of apartness. Hint: Replace AP2 by

a ≠ b ⊃ b ≠ a

a ≠ b ⊃ a ≠ c ∨ c ≠ b and trace up in the derivation the term removed by Split.

The elementary theories of equality and apartness can also be given in a single succedent formulation based on extension of the calculus G3i, as in Negri (1999).

Corollary: Disjunction property for the theory of apartness. If ⇒ A ∨ B is derivable in the single succedent calculus for the theory of apartness, either ⇒ A or ⇒ B is derivable.

Proof: Consider the last rule in the derivation. The rules for apartness cannot conclude a sequent with an empty antecedent and therefore the last rule must be rule R∨ of G3i. QED.

Compare to the treatment of axiom systems as a context: Γ ⇒ A∨B is derivable in G3i. Whenever Γ contains an instance of the “split” axiom it has a formula with a disjunction in the consequent of an implication. Therefore, Γ does not consist of Harrop formulas only, so the above corollary gives a proper extension of the disjunction property under hypotheses that are Harrop formulas.

Harrop systems

Definition

1. Atoms P, Q, R, …, and ⊥ are Harrop formulas,

2. If A and B are Harrop formulas, then A&B is a Harrop formula,

3. If B is a Harrop formula, then A ⊃ B is a Harrop formula.

Harrop theory: axioms consist of Harrop formulas. Left Harrop system: system of mathematical rules obtained from the axioms of a Harrop theory by using the left rule-scheme.

The rules of a left Harrop system have at most one premiss, thus the derivations are linear, and therefore

Theorem If a sequent Γ ⇒ Δ is derivable in a left Harrop system, then Γ ⇒ P is derivable for some atom P. If Δ contains atoms, the atom P can be chosen from Δ.

Proof: Consider a derivation D of Γ ⇒ Δ. If the topsequent is a logical axiom P, Γ′ ⇒ Δ′, P, with Δ = Δ′, P, the succedent can be changed into P. If the topsequent is a zero-premiss mathematical rule, any atom P can be put as the succedent and the derivation with the new succedent continued as with Δ. QED.

Partial order: The axioms of partial order are PO1. a ⩽ a, PO2. a ⩽ b & b ⩽ c ⊃ a ⩽ c. Equality is defined by a = b ≡ a ⩽ b & b ⩽ a. (Thus, we are working with what are sometimes called quasiorderings.) Equality is an equivalence relation and satisfies the principle of substitution of equals. As a system with rules GPO

{a ⩽ a, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Ref}  {a ⩽ c, a ⩽ b, b ⩽ c, Γ ⇒ Δ \atop a ⩽ b, b ⩽ c, Γ ⇒ Δ}^{Trans}

Closure condition arises when a ≡ b and b ≡ c when the premiss of rule Trans

a ⩽ a, a ⩽ a, a ⩽ a, Γ ⇒ Δ

Conclusion follows by rule Ref so that the closure condition is satisfied. Thus the rules of weakening, contraction, and cut are admissible in GPO. Weakening and contraction are admissible and height preserving.

Proof analysis GPO: There are exactly 2 kinds of derivation. To see what they are, assume that derivations contain no unnecessary detours: a derivation is of minimum size if no proper subtree of the given derivation is a derivation. If Γ ⇒ Δ is derivable, the topsequent has the form P, Γ′ ⇒ Δ′, P with Δ′, P = Δ, and we can delete Δ′ from the topsequent. The two kinds of derivations are:

1. Reflexivity derivations: P ≡ a ⩽ a. The conclusion Γ ⇒ a ⩽ a follows in one step from the logical axiom a ⩽ a, Γ ⇒ a ⩽ a with one application of rule Ref:

{a ⩽ a, Γ ⇒ a ⩽ a \atop Γ ⇒ a ⩽ a}^{Ref}

The context Γ is superfluous and can be deleted, thus, the conclusion becomes ⇒ a ⩽ a.

2. Transitivity derivations: The topsequent is a_{1} ⩽ a_{n}, Γ′ ⇒ a_{1} ⩽ a_{n}. The atom a_{1} ⩽ a_{n} must be the removed atom in a first step of transitivity or else the derivation can be shortened: If some other atom P were removed, with Γ′ ≡ P, Γ′′, the derivation could be shortened by starting with a_{1} ⩽ a_{n}, Γ′′ ⇒ a_{1} ⩽ a_{n} as topsequent. There cannot be steps of reflexivity in this derivation: The reflexivity atom would be principal in a step of transitivity, else it could be removed tout court from the derivation with a subsequent shortening, thus there would be a step of the form

{a ⩽ b, a ⩽ a, a ⩽ b, Γ ⇒ a_{1} ⩽ a_{n} \atop a ⩽ a, a ⩽ b, Γ ⇒ a_{1} ⩽ a_{n}} ^{Trans}

By height-preserving admissibility of contraction the conclusion of this step could be obtained already from the premiss, without using transitivity, in one step less.

Two atoms a_{1} ⩽ a_{2}, a_{2} ⩽ a_{n} are activated by the step of Trans removing a_{1} ⩽ a_{n} so that the topsequent is of the form

a_{1} ⩽ a_{n}, a_{1} ⩽ a_{2}, a_{2} ⩽ a_{n}, Γ′′ ⇒ a_{1} ⩽ a_{n}

In the second step, one of the activated atoms must become the removed atom, with two new activated atoms, say a_{2} ⩽ a_{3}, a_{3} ⩽ a_{n}, or else the derivation can be shortened. The closure of the principal atom a_{1} ⩽ a_{n} with respect to the activation relation gives us a chain a_{1} ⩽ a_{2}, a_{2} ⩽ a_{3}, … a_{n−1} ⩽ a_{n} in the topsequent. Deleting the atoms that have not been active in the derivation, we have a derivation of the form

Γ′′′, a_{1} ⩽ a_{2}, a_{2} ⩽ a_{3}, … a_{n−1} ⩽ a_{n} ⇒ a_{1} ⩽ a_{n} _{Trans} ; ⋮ . a_{1} ⩽ a_{2}, a_{2} ⩽ a_{3}, … a_{n−1} ⩽ a_{n} ⇒ a_{1} ⩽ a_{n} Trans

in which Γ′′′ consists of the removed atoms a_{1} ⩽ a_{n}, . . .. Sequents Γ ⇒ Δ derivable in GPO are derivable as left and right weakenings of reflexivity and transitivity derivations.

Proof search for a sequent Γ ⇒ Δ is effected by two controls: Does Δ contain a reflexivity atom? Does Γ contain a chain from a_{1} to a_{n} with the atom a_{1} ⩽ a_{n} in Δ? If so, the sequent Γ ⇒ Δ is derivable, otherwise it is underivable.

Nondegenerate partial order is obtained by adding the axiom PO3. ∼1 ⩽ 0

to PO1 and PO2. The corresponding rule has zero premisses:

1 ⩽ 0, Γ ⇒ Δ^{Ndeg}

Derivations remain linear and the theorem on Harrop systems applies. If the topsequent is an instance of Ndeg, the atom 1 ⩽ 0 is removed by Trans (it cannot be removed by Ref). Steps of Trans hide the inconsistent assumption 1 ⩽ 0, with the general form of conclusion

1 ⩽ a_{1}, a_{1} ⩽ a_{2}, …, a_{n−1} ⩽ 0 ⇒ a ⩽ b

with the chain in the antecedent being the closure of formulas activated by 1 ⩽ 0 and a ⩽ b in the succedent an arbitrary atom.

Nontrivial partial order has in addition

PO4. 0 ⩽ 1. The corresponding rule is

{0 ⩽ 1, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Ntriv}

This rule commutes down with instances of Ref and Trans. The only interesting case is a transitivity derivation with a chain from which atoms 0 ⩽ 1 have been removed by Ntriv.

Linear order and Szpilrajn’s theorem

Theory of linear order: adding to partial order the linearity axiom LO. a ⩽ b ∨ b ⩽ a The corresponding rule is

\begin{matrix}a ⩽ b, Γ ⇒ Δ & b ⩽ a, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix}^{Lin}

The system of rules for linear order is designated GLO.

Conservativity theorem If Γ ⇒ P is derivable in GLO, it is derivable in GPO already.

Proof: Consider a derivation with just one instance of Lin, as the last rule, and assume the derivation to have minimum size. Thus, the premisses of Lin c ⩽ d, Γ ⇒ P and d ⩽ c, Γ ⇒ P are derivable in partial order. If P is a reflexivity atom in either topsequent, Γ ⇒ P is derivable in one step of Ref. Otherwise, with P ≡ a ⩽ b, there will be two transitive closures of the removed atom a ⩽ b in both derivations of the two premisses of Lin, and let them be a ⩽ a_{1}, … a_{m−1} ⩽ b and a ⩽ b_{1}, … b_{n−1} ⩽ b. If c ⩽ d is not an atom in the first chain, it can be deleted and a derivation of Γ ⇒ P in partial order obtained, and similarly for d ⩽ c in the second chain. Thus, we have the two chains a ⩽ a_{1}, …, a_{i} ⩽ c, c ⩽ d, d ⩽ a_{i+1}, … a_{m−1} ⩽ b a ⩽ b_{1}, …, b_{j} ⩽ d, d ⩽ c, c ⩽ b_{j+1}, … b_{n−1} ⩽ b

The chain a ⩽ a_{1}, …, a_{i} ⩽ c, c ⩽ b_{j+1}, … b_{n−1} ⩽ b appears in the antecedent of the topsequent, thus the sequent a ⩽ a_{1}, …, a_{i} ⩽ c, c ⩽ b_{j+1}, … b_{n−1} ⩽ b ⇒ a ⩽ b

is derivable in partial order. QED.

The conservativity theorem extends to nondegenerate nontrivial partial order: Theorem If Γ ⇒ P is derivable in nondegenerate GLO, it is derivable in nondegenerate nontrivial GPO already. (Note that a nondegenerate linear order is always nontrivial.)

Extension algorithm: Definition An ordering Σ is inconsistent if Γ ⇒ 1 ⩽ 0 is derivable for some finite subset Γ of Σ, otherwise it is consistent.

Corollary: Szpilrajn’s theorem. Given a set Σ of atoms in a consistent nondegenerate partial ordering, it can be extended to a consistent nondegenerate linear ordering.

Proof: Let a, b be any two elements in Σ not ordered in Σ. We claim that either Σ, a ⩽ b or Σ, b ⩽ a is consistent in GPO. Let us assume the contrary, i.e., that there exists a finite subset Γ of Σ such that both Γ, a ⩽ b ⇒ 1 ⩽ 0 and Γ, b ⩽ a ⇒ 1 ⩽ 0 are derivable in GPO. Application of rule Lin gives the conclusion Γ ⇒ 1 ⩽ 0 in GLO. By the conservativity theorem, Γ ⇒ 1 ⩽ 0 is already derivable in GPO, contrary to the consistency assumption. Iteration of the procedure gives the desired extension. QED.

Constructive conservativity vs nonconstructive extension Proof of the conservativity theorem is constructive, effectivity of the extension depends on how the set Σ is given. General phenomenon: Classical, nonconstructive set-theoretic extension results are reformulated as constructive proof-theoretical conservativity results. Examples: Pointfree constructive Hahn-Banach theorem (Cederquist, Coquand, and Negri (1998)) vs. classical nonconstructive Hahn-Banach theorem . Constructive conservativity of linar order over partial order vs classical Szpilrajn’s theorem. Classical proofs use non-constructive principles like Zorn’s lemma.

Decidability of order relation often assumed, either explicitly or through the application of the law of excluded middle. Our approach does not impose any such requirement and therefore does not rule out a computational approach to order relations in continuous sets. The law of excluded middle is avoided by considering extensions of the intuitionistic calculus G3im instead of the classical one. Proviso: The rules of implication do not permute down with mathematical rules if these latter have at least two premisses. In the case of Harrop theories, such as partial order or lattice theory, logical rules do permute down and derivations with mathematical rules can be considered in isolation.

The right rule scheme

The left rule-scheme for an axiom of the form

P_{1}& … &P_{m} ⊃ Q_{1} ∨ … ∨ Q_{n}

{Q_{1}, P_{1}, …, P_{m}, Γ ⇒ Δ … Q_{n}, P_{1}, …, P_{m}, Γ ⇒ Δ \atop P_{1}, …, P_{m}, Γ ⇒ Δ}

has a dual formulation as a right rule-scheme:

{Γ ⇒ Δ, Q_{1}, …, Q_{n}, P_{1} … Γ ⇒ Δ, Q_{1}, …, Q_{n}, P_{m} \atop Γ ⇒ Δ, Q_{1}, …, Q_{n}}

Repetition of the atoms Q_{i} in the premisses to obtain admissibility of right contraction. Closure condition: If the atoms in a rule have an instance that makes two atoms in the conclusion identical, contracted rule has to be added.

Theorem The structural rules of left and right weakening and contraction and the rule of cut are admissible in extensions of G3c and G3im with rules following the right rule-scheme and satisfying the closure condition. Right rules for linear order

Γ ⇒ Δ, a ⩽ b, b ⩽ a^{Lin}  Γ ⇒ Δ, a ⩽ a^{Ref}

\begin{matrix}Γ ⇒ Δ, a ⩽ c, a ⩽ b, & Γ ⇒ Δ, a ⩽ c, b ⩽ c \\ Γ ⇒ Δ, a ⩽ c \end{matrix}^{Trans}

Term b in rule Trans is called a middle term.

Theorem All terms in a minimum-size derivation of Γ ⇒ Δ in the right theory of linear order are terms in Γ, Δ.

Corollary The quantifier-free theory of linear order is decidable.

Proof: Application of rule Trans root first with middle terms chosen from the conclusion can produce only a bounded number of distinct atoms in the premisses. Whenever a duplication is produced, proof search fails by the admissibility of contraction. QED.