Chapter 6: Structural proof analysis of axiomatic theories

In this chapter, we give a method of adding axioms to sequent calculus, in the form of nonlogical rules of inference. When formulated in a suitable way, cut elimination will not be lost by such addition. By converting axioms into rules, it becomes possible to prove properties of systems by induction on the height of derivations.

The method of extension by nonlogical rules works uniformly for systems based on classical logic. For constructive systems, there will be some special forms of axioms, notably (P ⊃ Q) ⊃ R, that cannot be treated through cut-free rules.

In the conversion of axiom systems into systems with nonlogical rules, the multisuccedent calculi G3im and G3c are most useful. All structural rules will be admissible in extensions of these calculi, which has profound consequences for the structure of derivations. The first application is a cut-free system of predicate logic with equality. In earlier systems, cut was reduced to cuts on atomic formulas in instances of the equality axioms, but by the method of this chapter, there will be no cuts anywhere. Other applications of the structural proof analysis of mathematical theories include elementary theories of equality and apartness, order and lattices, and elementary geometry.

6.1. From axioms to rules

When classical logic is used, all free-variable axioms (purely universal axioms) can be turned into rules of inference permitting cut elimination. The constructive case is more complicated, and we shall deal with it first.

(a) The representation of axioms as rules: We shall be using the intuitionistic multisuccedent sequent calculus G3ipm of Section 5.3. In adding nonlogical rules representing axioms, we follow

Principle 6.1.1. In nonlogical rules, the premisses and conclusion are sequents that have atoms as active and principal formulas in the antecedent, and an arbitrary context in the succedent.

The most general scheme corresponding to this principle, with shared contexts, is

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

where Γ, Δ are arbitrary multisets and P_{1}, …, P_{m}, Q_{1}, …, Q_{n} are fixed atoms, and the number of premisses n can be zero.

Once we have shown structural rules admissible, we can conclude that a rule admitting several atoms in the antecedents of the premisses reduces to as many rules with one atom, for example, the rule

\begin{matrix}Q_{1}, Q_{2}, Γ ⇒ Δ & R, Γ ⇒ Δ \\ P, Γ ⇒ Δ \end{matrix}

reduces to the two rules

\begin{matrix}Q_{1}, Γ ⇒ Δ & R, Γ ⇒ Δ \\ P, Γ ⇒ Δ \end{matrix}  \begin{matrix}Q_{2}, Γ ⇒ Δ & R, Γ ⇒ Δ \\ P, Γ ⇒ Δ \end{matrix}

The second and third rule follow from the first by weakening of the left premiss. In the other direction, weakening R, Γ ⇒ Δ to R, Q_{2}, Γ ⇒ Δ we obtain the conclusion P, Q_{2}, Γ ⇒ Δ from Q_{1}, Q_{2}, Γ ⇒ Δ by the second rule, and weakening again R, Γ ⇒ Δ to R, P, Γ ⇒ Δ, we obtain by the third rule P, P, Γ ⇒ Δ which contracts to P, Γ ⇒ Δ. This argument generalizes, so we do not need to consider premisses with several atoms.

The full rule-scheme corresponds to the formula P_{1}& … &P_{m} ⊃ Q_{1} ∨ … ∨ Q_{n}. In order to see better what forms of axioms the rule-scheme covers, we write out a few cases, together with their corresponding axiomatic statements in Hilbert-style calculus. Omitting the contexts, the rules for axioms of the forms Q&R, Q ∨ R and P ⊃ Q are

{Q ⇒ Δ \atop ⇒ Δ} , {R ⇒ Δ \atop ⇒ Δ}  \begin{matrix}Q ⇒ Δ & R ⇒ Δ \\ ⇒ Δ \end{matrix}  {Q ⇒ Δ \atop P ⇒ Δ}

The rules for axioms of the forms Q, ∼P and ∼(P_{1}&P_{2}) are:

{Q ⇒ Δ \atop ⇒ Δ}  P ⇒ Δ  P_{1}, P_{2} ⇒ Δ

We recall the definition of regular sequents and their trace formulas from Section 3.1: A sequent is regular if it is of the form

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

where the number of ⊥’s, m and n can be 0, and P_{i} ≠ Q_{j} for all i, j. Regular sequents are grouped into four types, each with a corresponding trace formula

1. P_{1}& … &P_{m} ⊃ Q_{1} ∨ … ∨ Q_{n} if m > 0, n > 0,

2. Q_{1} ∨ … ∨ Q_{n} if m = 0, n > 0,

3. ∼(P_{1}& … &P_{m}) if m > 0, n = 0,

4. ⊥ if m = 0, n = 0.

Regular sequents are precisely the sequents that correspond to rules (lat. “regulae”) following our rule-scheme. In terms of the rule-scheme, the formation of trace formulas corresponds to the deletion of all but one of several identical premisses in a rule when any of the Q_{j} are identical and contracting repetitions in the antecedent of the conclusion when any of the P_{i} are identical.

Given a sequent ⇒ A, we can perform a root-first decomposition by means of the rules of G3ipm. If the decomposition terminates, we reach leaves that are either axioms or conclusions of L⊥ or regular sequents. Among such leaves, we distinguish those that are reached from ⇒ A by “invertible paths,” ones that never pass via a noninvertible rule of G3ipm:

Definition 6.1.2: In a terminating decomposition of a sequent ⇒ A in G3ipm, if a topsequent is reached without passing through the left premiss of L⊃ or via an instance of R ⊃ with nonempty context Δ in its conclusion, it is an invertible leaf, and in the contrary case it is a noninvertible leaf.

We now define the class of regular formulas:

Definition 6.1.3. A formula A is regular if it has a decomposition that leads to invertible leaves that are either logical axioms or regular sequents and noninvertible leaves that are logical axioms.

We observe that the invertible leaves in a decomposition of ⇒ A are independent of the order of decomposition chosen, since any two rules among L&, R&, L∨, R∨, and R⊃ with empty right context Δ, commute with each other and each of them commutes with the right premiss of L⊃. This uniqueness justifies the following

Definition 6.1.4. For a regular formula A, its regular decomposition is the set {A_{1}, …, A_{k}}, where the A_{i} are the formula traces of the regular sequents among the invertible leaves of A. The regular normal form of a regular formula A is A_{1}& … &A_{k}.

Note that the regular decomposition of a regular formula A is unique, and A is equivalent to its regular normal form. Thus, regular formulas are those that permit a constructive version of a conjunctive normal form, one where each conjunct is an implication of form P_{1}& … &P_{m} ⊃ Q_{1} ∨…∨Q_{n}, instead of the classically equivalent disjunctive form ∼P_{1}∨… ∨ ∼P_{m}∨Q_{1}∨…∨Q_{n}. The class of formulas constructively equivalent to usual conjunctive normal form is strictly smaller than the class of formulas having regular normal form. The following proposition shows some closure properties of the latter class of formulas:

Proposition 6.1.5.

(i) If A has no ⊃, then A is regular,

(ii) If A, B are regular, then A&B is regular,

(iii) If A has no ⊃ and B is regular, then A ⊃ B is regular.

Proof: (i) By invertibility of the rules for & and ∨. (ii) Obvious. (iii) Starting with R⊃, a decomposition of ⇒ A ⊃ B has invertible leaves of the form P_{1}, …, P_{m}, Γ ⇒ Δ, where P_{1}, …, P_{m} are atoms (from the decomposition of A) and Γ ⇒ Δ is either a logical axiom or a regular sequent. Thus also P_{1}, …, P_{m}, Γ ⇒ Δ is either a logical axiom or a regular sequent. QED.

From the two cases of noninvertible rules we see that typical formulas that need not be regular are disjunctions that contain an implication, and implications that contain an implication in the antecedent. But sometimes even these are regular, such as the formula (P ⊃ Q) ⊃ (P ⊃ R).

In the next section we show that the class of regular formulas consists precisely of the formulas the corresponding rules of which commute with the cut rule. The reason for adopting principle 6.1.1 will then be clear.

(b) Extension of classical systems with nonlogical rules: For the extension of classical systems, we use the classical multisuccedent sequent calculus G3c in which all structural rules are built in. All propositional rules of G3c are invertible, but instead of analysing regularity of formulas through decomposability as in Section 3.1, we can use the existence of conjunctive normal form in classical propositional logic: each formula is equivalent to a conjunction of disjunctions of atoms and negations of atoms. Each conjunct can be converted into the classically equivalent form P_{1}& … &P_{m} ⊃ Q_{1} ∨ …∨Q_{n} which is representable as a rule of inference. As special cases we can have m = 0 or n = 0 as in the four types of trace formulas. We therefore have

Proposition 6.1.6. All classical quantifier-free axioms can be represented by formulas in regular normal form.

Thus, to every classical quantifier-free theory, there is a corresponding sequent calculus with structural rules admissible.

(c) Conversion of axiom systems into systems with rules: Conversion of a Hilbert-style axiomatic system into a Gentzen-style sequent system proceeds, after quantifier-elimination, by first finding the regular decomposition of each axiom, and then converting each conjunct into a corresponding rule following principle 6.1.1. Right contraction is unproblematic due to the arbitrary context Δ in the succedents of the rule scheme. In order to handle left contraction, we have to augment this scheme. So assume we have a derivation of A, A, Γ ⇒ Δ, and assume the last rule is nonlogical. Then the derivation of A, A, Γ ⇒ Δ can be of three different forms. First, neither occurrence of A is principal in the rule; second, one is principal; third, both are principal. The first case is handled by a straightforward induction, and the second case by the method, familiar from the work of Kleene and exemplified by the L⊃ rule of G3ip, of repeating the principal formulas of the conclusion in the premisses. Thus, the general rule-scheme becomes

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

Here P_{1}, …, P_{m} in the conclusion are principal in the rule, and P_{1}, …, P_{m} and Q_{1}, …, Q_{n} in the premisses are active in the rule. Repetitions in the premisses will make left contractions commute with rules following the scheme. For the remaining case, with both occurrences of formula A principal in the last rule, consider the situation with a Hilbert-style axiomatization. We have some axiom, say ∼ (a < b & b < a) in the theory of strict linear order, and substitution of b with a produces ∼ (a < a & a < a) that we routinely abbreviate to ∼ a < a, irreflexivity of strict linear order. This is in fact a contraction. For systems with rules, the case where a substitution produces two identical formulas that are both principal in a nonlogical rule, is taken care of by the

Closure condition 6.1.7. Given a system with nonlogical rules, if it has a rule where a substitution instance in the atoms produces a rule of form

{Q_{1}, P_{1}, …, P_{m−2}, P, P, Γ ⇒ Δ … Q_{n}, P_{1}, …, P_{m−2}, P, P, Γ ⇒ Δ \atop P_{1}, …, P_{m−2}, P, P, Γ ⇒ Δ}^{Reg}

then it also has to contain the rule

{Q_{1}, P_{1}, …, P_{m−2}, P, Γ ⇒ Δ … Q_{n}, P_{1}, …, P_{m−2}, P, Γ ⇒ Δ \atop P_{1}, …, P_{m−2}, P, Γ ⇒ Δ}^{Reg}

The condition is unproblematic, since the number of rules to be added to a given system of nonlogical rules is bounded. Often the closure condition is superfluous; For example, the rule expressing irreflexivity in the constructive theory of strict linear order is derivable from the other rules, as will be shown in Section 6.6.

6.2. Admissibility of structural rules

In this section we shall prove the admissibility of the structural rules of weakening, contraction and cut for extensions of logical systems with nonlogical rules of inference. We shall deal in detail with constructive systems, and just note that the proofs go through for classical systems with inessential modifications.

We shall denote by G3im* any extension of the system G3im with rules following our general rule-scheme and satisfying the closure condition. Starting from the proof of admissibility of structural rules for G3im in Section 5.1, we then prove admissibility of the structural rules for G3im*.

Theorem 6.2.1. The rules of weakening

{Γ ⇒ Δ \atop A, Γ ⇒ Δ}^{LW}  {Γ ⇒ Δ \atop Γ ⇒ Δ, A}^{RW}

are admissible and height-preserving in G3im*.

Proof: For left weakening, since the two axioms and all rules have an arbitrary context in the antecedent, adding the weakening formula to the antecedent of each sequent will give a derivation of A, Γ ⇒ Δ. For right weakening, adding the weakening formula to the succedents of all sequents that are not followed by an instance of the R⊃ or R∀ rule will give a derivation of Γ ⇒ Δ, A. QED.

The proof of admissibility of the contraction rules and the cut rule for G3im requires the use of inversion lemmas. We observe that all the inversion lemmas of Section 5.1, holding for G3im, hold for G3im* as well. This is achieved by having only atomic formulas as principal in nonlogical rules, a property guaranteed by the restriction given in principle 6.1.1.

Theorem 6.2.2. The rules of contraction

{A, A, Γ ⇒ Δ \atop A, Γ ⇒ Δ}^{LC}  {Γ ⇒ Δ, A, A \atop Γ ⇒ Δ, A}^{RC}

are admissible and height-preserving in G3im*.

Proof: For left contraction, the proof is by induction on the height of the derivation of the premiss. If it is an axiom, the conclusion also is an axiom.

If A is not principal in the last rule (either logical or nonlogical), apply inductive hypothesis to the premisses and then the rule.

If A is principal and the last rule is logical, for L& and L∨ apply heightpreserving invertibility, inductive hypothesis and then the rule. For L⊃ apply inductive hypothesis to the left premiss, invertibility and inductive hypothesis to the right premiss, and then the rule. If the last rule is L∀, apply the inductive hypothesis to its premiss, and L∀. If the last rule is L∃, apply height preserving invertibility of L∃, the inductive hypothesis and L∃.

If the last rule is nonlogical, A is an atomic formula P and there are two cases. In the first case one occurrence of A belongs to the context, another is principal in the rule, say A = P_{m}(= P). The derivation ends with

{Q_{1}, P_{1}, …, P_{m−1}, P, P, Γ′ ⇒ Δ … Q_{n}, P_{1}, …, P_{m−1}, P, P, Γ′ ⇒ Δ \atop P_{1}, …, P_{m−1}, P, P, Γ′ ⇒ Δ}^{Reg}

and we obtain

{Q_{1}, P_{1}, …, P_{m−1}, P, P, Γ′ ⇒ Δ \atop Q_{1}, P_{1}, …, P_{m−1}, P, Γ′ ⇒ Δ}^{Ind} … {Q_{n}, P_{1}, …, P_{m−1}, P, P, Γ′ ⇒ Δ \atop Q_{n}, P_{1}, …, P_{m−1}, P, Γ′ ⇒ Δ}^{Ind}

P_{1}, …, P_{m−1}, P, Γ′ ⇒ Δ Reg

In the second case both occurrences of A are principal in the rule, say A = P_{m−1} = P_{m} = P, thus the derivation ends with

{Q_{1}, P_{1}, …, P_{m−2}, P, P, Γ′ ⇒ Δ … Q_{n}, P_{1}, …, P_{m−2}, P, P, Γ′ ⇒ Δ \atop P_{1}, …, P_{m−2}, P, P, Γ′ ⇒ Δ}^{Reg}

and we obtain

{Q_{1}, P_{1}, …, P_{m−2}, P, P, Γ′ ⇒ Δ \atop Q_{1}, P_{1}, …, P_{m−2}, P, Γ′ ⇒ Δ}^{Ind} … {Q_{n}, P_{1}, …, P_{m−2}, P, P, Γ′ ⇒ Δ \atop Q_{n}, P_{1}, …, P_{m−2}, P, Γ′ ⇒ Δ}^{Ind}

P_{1}, …, P_{m−2}, P, Γ′ ⇒ Δ Reg

with the last rule given by closure condition 6.1.7.

The proof of admissibility of right contraction in G3im* does not present any additional difficulty with respect to the proof of admissibility in G3im since in nonlogical rules the succedent in both the premisses and the conclusion is an arbitrary multiset Δ. So in case the last rule in a derivation of Γ ⇒ Δ, A, A is a nonlogical rule, one simply proceeds by applying the inductive hypothesis to the premisses, and then the rule. QED.

Theorem 6.2.3. The cut rule

Γ ⇒ Δ, A A, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ, Δ′ Cut

is admissible in G3im*.

Proof: The proof is by induction on the length of A with subinduction on the sum of the heights of the derivations of Γ ⇒ Δ, A and A, Γ′ ⇒ Δ′. We consider here in detail only the cases arising from the addition of nonlogical rules. The other cases are treated in the corresponding proof for the intuitionistic multisuccedent calculus G3im, theorem 5.3.6.

1. If the left premiss is a nonlogical axiom, then also the conclusion is a nonlogical axiom, since nonlogical axioms have an arbitrary context as succedent.

2. If the right premiss is a nonlogical axiom with A not principal in it, the conclusion is a nonlogical axiom for the same reason as in 1.

3. If the right premiss is a nonlogical axiom with A principal in it, A is atomic and we consider the left premiss. The case that it is a nonlogical axiom is covered by 1. If it is a logical axiom with A not principal, the conclusion is a logical axiom; else Γ contains the atom A and the conclusion follows from the right premiss by weakening. In the remaining cases we consider the last rule in the derivation of Γ ⇒ Δ, A. Since A is atomic, A is not principal in the rule. Let us consider the case of a nonlogical rule (the others being dealt with similarly, except R⊃ and R∀ which are covered in 4). We transform the derivation, where P_{m} stands for P_{1}, …, P_{m},

Q_{1}, P_{m}, Γ′′ ⇒ Δ, A … Q_{n}, P_{m}, Γ′′ ⇒ Δ, A P_{m}, Γ′′ ⇒ Δ, A^{Reg} A, Γ′ ⇒ Δ′

P_{m}, Γ′, Γ′′ ⇒ Δ, Δ′ Cut

into

Q_{1}, P_{m}, Γ′′ ⇒ Δ, A A, Γ′ ⇒ Δ′ Q_{1}, P_{m}, Γ′, Γ′′ ⇒ Δ, Δ′^{Cut} … Q_{n}, P_{m}, Γ′′ ⇒ Δ, A A, Γ′ ⇒ Δ′ Q_{n}, P_{m}, Γ′, Γ′′ ⇒ Δ, Δ′^{Cut}

P_{m}, Γ′, Γ′′ ⇒ Δ, Δ′ Reg

where the cut has been replaced by n cuts with left premiss with derivation of lower height.

Let us now consider the cases in which neither premiss is an axiom.

4. A is not principal in the left premiss. These are dealt with as above, with cut permuted upwards to the premisses of the last rule used in the derivation of the left premiss (with suitable variable renaming in order to match the variable restrictions in the cases of quantifier rules), except for R⊃ and R∀. By the intuitionistic restriction in this rule, A does not appear in the premiss, and the conclusion is obtained without cut by R⊃ (R∀, resp.) and weakening.

5. A is principal in the left premiss only. Then A has to be a compound formula. Therefore, if the last rule of the right premiss is a nonlogical rule, A cannot be principal in the rule, because only atomic formulas are principal in nonlogical rules. In this case cut is permuted to the premisses of the right premiss. If the right rule is a logical one with A not principal in it, the usual reductions are applied.

6. A is principal in both premisses. This case can only involve logical rules, and is dealt with as in the usual proof for pure logic. QED.

The conversions used in the proof of admissibility of cut show why it is necessary to formulate the nonlogical rules so that they have an arbitrary context in the succedent, both in the premisses and in the conclusion. Besides, as already observed, active and principal formulas have to be atomic and appear in the antecedent. Thus nonlogical rules have the form of left rules.

Theorem 6.2.4. The rules of weakening, contraction and cut are admissible in G3c*.

Proof: The proof is an extension of the results for the purely logical calculus in Sections 3.2 and 4.2. The new cases are analogous to the intuitionistic case. QED.

6.3. Four approaches to extension by axioms

We found in Section 1.4 that the addition of axioms A into sequent calculus in the form of sequents ⇒ A by which derivations can start, will lead to failure of cut elimination. Another way of adding axioms, used by Gentzen (1938, sec. 1.4) already, is to add “mathematical basic sequents” which are (substitution instances of) sequents

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

Here P_{i}, Q_{j} are atomic formulas (typically containing free parameters) or ⊥. By Gentzen’s “Hauptsatz,” the use of the cut rule can be pushed into such basic sequents. A third way of adding axioms, first found in Gentzen’s consistency proof of elementary arithmetic in his (1934–35, sec. IV.3), is to treat axioms as a context Γ, and to relativize all theorems into Γ, thus proving results of form Γ ⇒ C. Now the sequent calculus derivations have no non-logical premisses, and cut elimination applies. A fourth way of adding axioms is the one of this chapter.

We shall specify formally the four different ways of extending logical sequent systems by axioms, and then establish their equivalence. Below, let D be a finite set of regular formulas. We define sequent systems of four kinds:

Definition 6.3.1:

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

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

(c) A C-system for D is a sequent system with a context. Derivability of a sequent Γ ⇒ Δ in a C-system, where instances of formulas in CD are always permitted in the antecedent, is denoted by ⊢_{CD} Γ ⇒ Δ. We can also write it as derivability in G3ipm, that is to say as ⊢_{G3} Γ, Θ ⇒ Δ, where Θ is the multiset of instances of formulas in D used in the derivation.

(d) An R-system for D is a 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, is denoted by ⊢_{RD} Γ ⇒ Δ.

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

Proof: Axioms and basic sequents are interderivable by cuts, so A- and Bsystems are equivalent. We show equivalence of R-systems with A-systems and C-systems. If a regular formula has to be considered, we take it to be the split formula P ⊃ Q ∨ R, as other formulas convertible to rules are special cases or inessential generalizations of it.

1. Equivalence of R- and A-systems: The rule

{Q, P ⇒ Δ R, P ⇒ Δ \atop P ⇒ Δ}^{Split}

can be derived in the A-system with axiom ⇒ P ⊃ Q ∨ R by means of cuts and contractions:

⇒ P ⊃ Q ∨ R\begin{matrix}\begin{matrix}P ⊃ Q ∨ R, P ⇒ P & Q ∨ R, P ⇒ Q ∨ R \\ P ⊃ Q ∨ R, P ⇒ Q ∨ R \end{matrix}^{L⊃} & \begin{matrix}Q, P ⇒ Δ & R, P ⇒ Δ \\ Q ∨ R, P ⇒ Δ \end{matrix}^{L∨} \\ P ⊃ Q ∨ R, P, P ⇒ Δ \end{matrix}_{Cut}

P, P ⇒ Δ Cut

P ⇒ Δ LC

In the other direction, ⇒ P ⊃ Q ∨ R is provable in the R-system with Split.

\begin{matrix}{Q, P ⇒ Q, R \atop Q, P ⇒ Q ∨ R}^{R∨} & {R, P ⇒ Q, R \atop R, P ⇒ Q ∨ R}^{R∨} \\ P ⇒ Q ∨ R \end{matrix}_{Split} ; ⇒ P ⊃ Q ∨ R_{R⊃}

2. Equivalence of C- and R-systems: Assume Γ ⇒ Δ was derived in the R-system with Split, and show Γ ⇒ Δ can be derived in the C-system with P ⊃ Q ∨ R. We assume that Split is the last rule in the derivation, and therefore Γ = P, Γ′. By induction, ⊢_{CD} Q, P, Γ′ ⇒ Δ and ⊢_{CD} R, P, Γ′ ⇒ Δ, thus there are instances A_{1}, …, A_{m} and A′_{1}, …, A′_{n} of the schemes in CD such that

⊢_{G3} Q, P, Γ′, A_{1}, …, A_{m} ⇒ Δ and ⊢_{G3} R, P, Γ′, A′_{1}, …, A′_{n} ⇒ Δ

Structural rules can be used, and we have, in G3ipm, a derivation starting with weakening of the A_{i} and A′_{j} into a common context A′′_{1}, …, A′′_{k} of instances from CD:

P ⊃ Q ∨ R, P, Γ′, A′′_{1}, …, A′′_{k} ⇒ P

{Q, P, Γ′, A_{1}, …, A_{m} ⇒ Δ \atop Q, P, Γ′, A′′_{1}, …, A′′_{k} ⇒ Δ} ^{LW} {R, P, Γ′, A′_{1}, …, A′_{n} ⇒ Δ \atop R, P, Γ′, A′′_{1}, …, A′′_{k} ⇒ Δ} ^{LW}

Q ∨ R, P, Γ′, A′′_{1}, …, A′′_{k} ⇒ Δ L∨

P ⊃ Q ∨ R, P, Γ′, A′′_{1}, …, A′′_{k} ⇒ Δ L⊃

Since the split formula and the A′′_{1}, …, A′′_{k} are in CD, we have shown ⊢_{CD} Γ ⇒ Δ.

In the other direction, assume ⊢_{CD} Γ ⇒ Δ. Suppose for simplicity that only one axiom occurs in the context, i.e., that ⊢_{G3} P ⊃ Q ∨ R, Γ ⇒ Δ. We have the derivation in G3ipm+RD+Cut,

\begin{matrix}{Q, P ⇒ Q, R \atop Q, P ⇒ Q ∨ R}^{R∨} & {R, P ⇒ Q, R \atop R, P ⇒ Q ∨ R}^{R∨} \\ P ⇒ Q ∨ R \end{matrix}_{Split} ; ⇒ P ⊃ Q ∨ R_{R⊃} P ⊃ Q ∨ R, Γ ⇒ Δ

Γ ⇒ Δ Cut

By admissibility of cut in G3ipm*, the conclusion follows QED.

Derivations in A- and B-systems can have premisses, and therefore cut must be assumed, whereas C- and R-systems are cut-free. The strength of Rsystems is that they permit proofs by induction on rules used in a derivation. This leads to some surprisingly simple, purely syntactic proofs of properties of elementary axiom systems.

6.4. Properties of cut-free derivations

The properties of sequent systems representing axiomatic systems are based on the subformula principle for systems with nonlogical rules:

Theorem 6.4.1. If Γ ⇒ Δ is derivable in G3im* or G3c*, then all formulas in the derivation are either subformulas of the endsequent or atomic formulas.

Proof: Only nonlogical rules can make formulas disappear in a derivation, and all such formulas are atomic. QED.

The subformula principle is weaker than that for purely logical systems, but sufficient for structural proof-analysis. Some general consequences are obtained: Consider a theory having as axioms a finite set D of regular formulas. Define D to be inconsistent if ⇒ ⊥ is derivable in the corresponding extension, and consistent if it is not inconsistent. For a theory D, inconsistency surfaces with the axioms through regular decomposition, with no consideration of the logical rules:

Theorem 6.4.2. Let D be inconsistent. Then

(i) All rules in the derivation of ⇒ ⊥ are nonlogical,

(ii) All sequents in the derivation have ⊥ as succedent,

(iii) Each branch in the derivation begins with a nonlogical rule of form

P_{1}, …, P_{m} ⇒ ⊥

(iv) The last step in the derivation is a rule of form

{Q_{1} ⇒ ⊥ … Q_{n} ⇒ ⊥ \atop ⇒ ⊥}

Proof: (i) By theorem 6.4.1, no logical constants except ⊥ can occur in the derivation. (ii) If the conclusion of a nonlogical rule has Δ as succedent, the premisses of the rule also have. Since the endsequent is ⇒ ⊥, (ii) follows. (iii) By (ii) and by ⊥ not being atomic, no derivation begins with P, Γ ⇒ P. Since only atoms can disappear from antecedents in a nonlogical rule, no derivation begins with ⊥, Γ ⇒ ⊥. This leaves only zero-premiss nonlogical rules. (iv) By observing that the endsequent has an empty antecedent. QED.

It follows that if an axiom system is inconsistent, its formula traces contain negations, and atoms or disjunctions. Therefore, if there are neither atoms nor disjunctions, the axiom system is consistent, and similarly if there are no negations.

By our method, the logical structure in axioms as they are usually expressed, is converted into combinatorial properties of derivation trees, and completely separated from steps of logical inference. This is especially clear in the classical quantifier-free case, where theorems to be proved can be converted into a finite number of regular sequents Γ ⇒ Δ. By the subformula principle, derivations of these sequents use only the nonlogical rules and axioms of the corresponding sequent calculus, with the succedent remaining the same throughout all derivations. It becomes possible to use proof theory for syntactic proofs of mutual independence of axiom systems, as follows. Let the axiom to be proved independent be expressed by the logic-free sequent Γ ⇒ Δ. When the rule corresponding to the axiom is left out from the system of nonlogical rules, underivability of Γ ⇒ Δ is usually very easily seen. Examples will be given in the last section of this chapter.

6.5. Predicate logic with equality

Axiomatic presentations of predicate logic with equality assume a primitive relation a = b with the axiom of reflexivity, a = a, and the replacement scheme, a = b &A(a/x) ⊃ A(b/x). In sequent calculus, the usual way of treating equality is to add regular sequents with which derivations can start (as in Troelstra and Schwichtenberg 1996, p. 98). These sequents are of form ⇒ a = a and a = b, P (a/x) ⇒ P (b/x), with P atomic, and Gentzen’s “extended Hauptsatz” says that cuts can be reduced to cuts on these equality axioms. For example, symmetry of equality is derived by letting P be x = a. Then the second axiom gives a = b, a = a ⇒ b = a, and a cut with the first axiom ⇒ a = a gives a = b ⇒ b = a. But there is no cut-free derivation of symmetry. Note also that in this approach, the rules of weakening and contraction must be assumed, and only then can cuts be reduced to cuts on axioms. (Weakening could be made admissible by letting arbitrary contexts appear on both sides of the regular sequents, but contraction not.)

By our method, cuts on equality axioms are avoided. We first restrict the replacement scheme to atomic predicates P, Q, R, … and then convert the axioms into rules,

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

There is a separate replacement rule for each predicate P, and a = b, P (a/x) are repeated in the premiss to obtain admissibility of contraction. By the restriction to atomic predicates, both forms of rules follow the rule-scheme. A case of duplication is produced in the conclusion of the replacement rule in case P is x = b. The replacement rule concludes a = b, a = b, Γ ⇒ Δ from the premiss b = b, a = b, a = b, Γ ⇒ Δ. We note that the rule where both duplications are contracted is an instance of the reflexivity rule so that the closure condition is satisfied. We therefore have, both for G3im and G3c, the

Theorem 6.5.1. The rules of weakening, contraction and cut are admissible in predicate logic with equality.

Next we have to show the replacement rule admissible for arbitrary predicates.

Lemma 6.5.2. The replacement axiom a = b, A(a/x) ⇒ A(b/x) is derivable for arbitrary A. Proof: The proof is by induction on length of A. If A = ⊥ the sequent is an axiom, and if A is an atom it follows from the replacement rule. If A = B&C or A = B ∨ C, we apply inductive hypothesis to B and C and then left and right rules. If A = B ⊃ C, we have the derivation

\begin{matrix}{b = a, B(b/x) ⇒ B(a/x) \atop b = a, a = b, a = a, B(b/x) ⇒ B(a/x)} & W,W \\ a = b, a = a, B(b/x) ⇒ B(a/x) \end{matrix}_{Repl} a = b, B(b/x) ⇒ B(a/x) Ref

a = b, B(a/x) ⊃ C(a/x), B(b/x) ⇒ B(a/x) W {a = b, C(a/x) ⇒ C(b/x) \atop a = b, C(a/x), B(b/x) ⇒ C(b/x)}^{W}

a = b, B(a/x) ⊃ C(a/x), B(b/x) ⇒ C(b/x) L⊃

a = b, B(a/x) ⊃ C(a/x) ⇒ B(b/x) ⊃ C(b/x) R⊃

If A = ∀yB, the sequent a = b, ∀yB(a/x) ⇒ ∀yB(b/x) is derived from a = b, B(a/x) ⇒ B(b/x) by applying first L∀ and then R∀. Finally, the sequent a = b, ∃yB(a/x) ⇒ ∃yB(b/x) is derived by applying first R∃ and then L∃. QED.

Theorem 6.5.3. The replacement rule

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

is admissible for arbitrary predicates A.

Proof: By the lemma, a = b, A(a/x) ⇒ A(b/x) is derivable. A cut with the premiss of the replacement rule and contractions lead to a = b, A(a/x), Γ ⇒ Δ. Therefore, by admissibility of contraction and cut in the calculus of predicate logic with equality, admissibility of the replacement rule follows. QED.

Our cut- and contraction-free calculus is equivalent to the usual calculi: the sequents ⇒ a = a and a = b, P (a/x) ⇒ P (b/x) follow at once from the reflexivity rule and the replacement rule. In the other direction, the two rules are easily derived from ⇒ a = a and a = b, P (a/x) ⇒ P (b/x) using cut and contraction. 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. In a cut-free derivation of a sequent Γ ⇒ Δ that contains no equalities, the last nonlogical rule must be Ref. To prove the conservativity, we show that instances of this rule can be eliminated from the derivation. Above we noticed that the rule of replacement has an instance with a duplication, but that the closure condition is satisfied since the instance where both duplications are contracted is an instance of reflexivity. For the proof of conservativity, the closure condition will be satisfied by adding directly the contracted instance of Repl as a rule Repl^{∗}:

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

Lemma 6.5.4: If Γ ⇒ Δ has no equalities and is derivable in G3c+Ref+ Repl+Repl^{∗}, no sequents in its derivation have equalities in the succedent.

Proof: Assume there is an equality in a succedent. Only a logical rule can move it, but then it is a subformula of the endsequent. QED.

Lemma 6.5.5: If Γ ⇒ Δ has no equalities and is derivable in G3c+Ref+ Repl+Repl^{∗} it is derivable in G3c+Repl+Repl^{∗}.

Proof: It is enough to show that a topmost instance of Ref can be eliminated from a given derivation. The proof is by induction on the height of derivation of a topmost instance

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

If the premiss is an axiom also the conclusion is, since by lemma 6.5.4 the succedent Δ′ contains no equality, and the same if it is a conclusion of L⊥. If the premiss has been concluded by a one-premiss logical rule R we have

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

and this is transformed into

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

Γ′ ⇒ Δ′ R

There is by the inductive hypothesis a derivation of Γ′′ ⇒ Δ′′ without rule Ref. If a two-premiss logical rule has been applied, the case is similar.

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), Γ′′

{P (c/x), a = a, b = c, P (b/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), Γ′′

{P (a/x), a = a, 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), Γ′′ ⇒ Δ′ so that the premiss of Ref is obtained by a derivation with lower height. The inductive hypothesis applies, giving a derivation of Γ′ ⇒ Δ′ without rule Ref.

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

{c = c, a = a, b = 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 6.5.6: If Γ ⇒ Δ is derivable in G3c+Ref+Repl+Repl^{∗} and if Γ, Δ contain no equality, then Γ ⇒ Δ is derivable in G3c.

Proof: By lemma 6.5.5, there is a derivation without rule Ref. Since the endsequent has no equality, Repl and Repl^{∗} cannot have been used in this derivation. QED.

Note that if cuts on atoms had not been eliminated, the proof would not go through. Also, if the closure condition were satisfied by considering the contracted rule to be an instance of Ref, elimination of contraction could introduce new instances of Ref above the Ref to be eliminated in lemma 6.5.5.

6.6. Application to axiomatic systems

All classical systems permitting quantifier-elimination, and most intuitionistic ones, can be converted into systems of cut-free nonlogical rules of inference. In the previous section, we gave the first application, predicate logic with equality. In Section 5.4, we showed how to turn the logical axiom of excluded middle for atomic formulas into a sequent calculus rule. Also the calculus G3ip+Gem-at can be seen as an intuitionistic calculus to which a rule corresponding to the decidability of atomic formulas has been added, and from this point of view, it is more natural to consider the law of excluded middle a nonlogical rather than a logical axiom.

We shall first give as a general result for theories with purely universal axioms a version of Herbrand’s theorem. Then specific examples from elementary intuitionistic axiomatics are given: Theories of equality, apartness and order, as well as algebraic theories with operations, such as lattices and Heyting algebras, are representable as cut-free intuitionistic systems. On the other hand, the intuitionistic theory of negative equality does not admit of a good structural proof theory under the present approach: This theory has a primitive relation a ≠ b and the two axioms ∼ a ≠ a and ∼a ≠ c & ∼b ≠ c ⊃ ∼a ≠ b expressing reflexivity and transitivity of negative equality.

As a further application of the methods of this chapter, we give a structural proof theory of classical plane affine geometry, with a proof of the independence of Euclid’s fifth postulate obtained by proof-theoretical means. Another application of the fact that logical rules can be dispensed with is proof search. We can start root-first from a logic-free sequent Γ ⇒ Δ to be derived: The succedent will be the same throughout in derivations with nonlogical rules, and in typical cases very few nonlogical rules match the sequent to be derived.

(a) Herbrand’s theorem for universal theories: Let T be a theory with a finite number of purely universal axioms and classical logic. We turn the theory T into a system of nonlogical rules by first removing the quantifiers from each axiom, then converting the remaining part into nonlogical rules. The resulting system will be denoted G3cT.

Theorem 6.6.1: 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, to narrow things down, that k = 1. Then 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∀}

If the derivation continues, root first, with a propositional inference the next premiss is Γ_{1} ⇒ Δ_{1}, ∃yA(z/x) where Γ_{1}, Δ_{1} consist of subformulas of A(z/x, t_{1}/y). (For the sake of simplicity, only a one-premiss rule is considered.) Otherwise R∃ was applied and the premiss is

⇒ A(z/x, t_{1}/y), A(z/x, t_{2}/y), ∃yA(z/x)

The derivation can continue up from the second alternative in the same way, producing possible derivations where R∃ is applied and instances of the formula ∃yA(z/x) multiplied, but since the derivation cannot grow indefinitely at some stage a conclusion must come from an inference that is not 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. In particular, the formula ∃yA(z/x) can only occur in the succedent. 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 repeated application of rule R∨ now leads to the conclusion. QED.

In the end of Section 4.3(a) we anticipated a simple form of Herbrand’s theorem for classical predicate logic, as a result corresponding to the existence property of intuitionistic predicate logic: Dropping the universal theory from theorem 6.6.1, there are no nonlogical rules to consider and we obtain the Corollary 6.6.2: 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.

(b) Theories of equality and apartness: The axioms of an apartness relation were introduced in Section 2.1. We shall turn first the equality axioms and then the apartness axioms into systems of cut-free rules.

1. The theory of equality has one basic relation a = b obeying the axioms

EQ1. a = a,

EQ2. a = b & a = c ⊃ b = c.

Symmetry of equality follows by substituting a for c in EQ2. Note that the formulation is slightly different from the transitivity of equality as given in Section 2.1 where we had a = c & b = c ⊃ a = b. The change is dictated by the form of the replacement axiom of Section 6.5: Now 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}

where a = b, a = c are repeated in the premiss of rule Trans, gives a calculus G3im+Ref+Trans the rules of which follow the rule-scheme. As noted in Section 6.5, 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.

2. The theory of decidable equality is given by the above axioms EQ1 and EQ2 and

DEQ. a = b ∨ ∼a = b.

The corresponding rule is an instance of a multisuccedent version the scheme Gem-at:

\begin{matrix}a = b, Γ ⇒ Δ & ∼a = b, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix}^{Deq}

Admissibility of structural rules for this rule is proved similarly to the single succedent version in Section 5.4. For the language of equality, we have G3im+Gem-at = G3im+Deq, a cut-free calculus. Proof of admissibility of structural rules is modular for the rules Ref, Trans and Deq, and it follows that the intuitionistic theory of decidable equality, which is the same as the classical theory of equality, is cut-free.

3. The theory of apartness has the basic relation a ≠ b (a and b are apart, a and b are distinct), 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}

The first, premissless rule represents ∼a ≠ a by licensing any inference from a ≠ a, the second has repetition of a ≠ b in the premisses. 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.

4. Decidability of apartness is expressed by the axiom

DAP. a ≠ b ∨ ∼a ≠ b,

and the corresponding rule is

\begin{matrix}a ≠ b, Γ ⇒ Δ & ∼a ≠ b, Γ ⇒ Δ \\ Γ ⇒ Δ \end{matrix}^{Dap}

As before, it follows that the calculus G3im+Irref+Split+Dap is cut-free.

5. The intuitionistic theory of negative equality is obtained from the axioms of apartness, with the second axiom replaced by its constructively weaker contraposition:

NEQ1. ∼a ≠ a,

NEQ2. ∼a ≠ c & ∼b ≠ c ⊃ ∼a ≠ b.

It is not possible to extend G3im into a cut-free theory of negative equality by the present methods. If a classical calculus such as G3c or G3i+Gem-at is used, a cut-free system is obtained since NEQ2 becomes equivalent to AP2.

The elementary theories in 1.–4. can also be given in a single succedent formulation based on extension of the calculus G3i, as in Negri (1999). As a consequence of the admissibility of structural rules in such extensions, we have the following result for the theory of apartness:

Corollary 6.6.3: 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.

Let us compare the result to the treatment of axiom systems as a context, the third of the approaches described in Section 6.3. Each derivation uses a finite number of instances of the universal closures of the two axioms of apartness, say Γ. The assumption becomes that Γ ⇒ 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 (definition 2.5.3), so that corollary 6.6.3 gives a proper extension of the disjunction property under hypotheses that are Harrop formulas, theorem 2.5.4.

(c) Theories of order: We first consider a constructive version of linear order, and next partial order. The latter is then extended in 6.6.(d) by the addition of lattice operations and their axioms.

1. Constructive linear order: We have a set with a strict order relation with the two axioms:

LO1. ∼(a < b & b < a),

LO2. a < b ⊃ a < c ∨ c < b.

Contraposition of the second axiom expresses transitivity of weak linear order. Two rules, denoted by Asym and Split, are uniquely determined from the axioms. Both rules follow the rule scheme, and the first one has an instance with a duplication, produced when a and b are identical:

a < a, a < a, Γ ⇒ Δ^{Asym}

The contracted sequent a < a, Γ ⇒ Δ is derived by

a < a, a < a, Γ ⇒ Δ^{Asym} a < a, a < a, Γ ⇒ Δ^{Asym}

a < a, Γ ⇒ Δ Split

We observe that the contracted rule is only admissible, rather than being a rule of the system. This makes no difference unless height-preserving admissibility of contraction is required. It is not needed for admissibility of cut.

2. Partial order: We have a set with an order relation satisfying the two axioms

PO1. a ⩽ a,

PO2. a ⩽ b & b ⩽ c ⊃ a ⩽ c.

Equality is defined by a = b ≡ a ⩽ b & b ⩽ a. It follows that equality is an equivalence relation. Further, since equality is defined in terms of partial order, the principle of substitution of equals for the latter is provable. The axioms of partial order determine by the rule-scheme two rules, the one corresponding to transitivity producing a duplication in case a = b and b = c. The rule where both the premiss and conclusion are contracted, is an instance of the rule corresponding to reflexivity, and therefore the structural rules are admissible. The rules corresponding to the two axioms are denoted by Ref and Trans:

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

Derivations of a regular sequent Γ ⇒ Δ in the theory of partial order begin with logical axioms, followed by applications of the above rules. As is seen from the rules, these derivations have the following peculiar form: They are all linear and each step consists in the deletion of one atom from the antecedent. If classical logic is used, by invertibility of all its rules, every derivation consists of derivations of regular sequents followed by application of logical rules only.

3. Nondegenerate partial order: We add to the axioms of partial order two constant 0, 1 satisfying the axiom of nondegeneracy ∼ 1 ⩽ 0. The corresponding rule has zero premisses:

1 ⩽ 0, Γ ⇒ Δ^{Nondeg}

Partial order is conservative over nondegenerate partial order:

Theorem 6.6.4: If Γ ⇒ Δ is derivable in the theory of nondegenerate partial order and Γ, Δ are quantifier-free and do not contain 0, 1, then Γ ⇒ Δ is derivable in the theory of partial order.

Proof: We prove that if a derivation of Γ ⇒ Δ contains atoms with 0 or 1 the atoms are instances of reflexivity, of the form 0 ⩽ 0 or 1 ⩽ 1. So suppose the derivation contains an atom with 0 or 1 and not of the above form. Its downmost occurrence can only disappear by an application of rule Trans

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

where a ⩽ c contains 0 or 1 and is not an instance of reflexivity. If a ≡ 0, i.e., a is syntactically equal to 0, then a ⩽ b in the conclusion must be an instance of reflexivity and we have b ≡ 0, therefore also c ≡ 0. But then a ⩽ c is an instance of reflexivity contrary to assumption. The same conclusion follows if a ≡ 1 or c ≡ 0 or c ≡ 1.

By the above, the derivation does not contain instances of 1 ⩽ 0 and therefore no instances of rule Nondeg. QED.

(d) Lattice theory: We add to partial order the two lattice constructions and their axioms:

Lattice operations and axioms:

a∧b the meet of a and b,  a∨b the join of a and b,
a∧b ⩽ a (Mtl),  a ⩽ a∨b (Jnl),
a∧b ⩽ b (Mtr),  b ⩽ a∨b (Jnr),
c ⩽ a & c ⩽ b ⊃ c ⩽ a∧b (Unimt), a ⩽ c & b ⩽ c ⊃ a∨b ⩽ c (Unijn).

All of the axioms follow the rule scheme, and we shall use the above identifiers as names of the nonlogical rules of lattice theory:

{a∧b ⩽ a, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Mtl}  {a ⩽ a∨b, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Jnl}
{a∧b ⩽ b, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Mtr}  {b ⩽ a∨b, Γ ⇒ Δ \atop Γ ⇒ Δ}^{Jnr}
{c ⩽ a∧b, c ⩽ a, c ⩽ b, Γ ⇒ Δ \atop c ⩽ a, c ⩽ b, Γ ⇒ Δ}^{Unimt} {a∨b ⩽ c, a ⩽ c, b ⩽ c, Γ ⇒ Δ \atop a ⩽ c, b ⩽ c, Γ ⇒ Δ}^{Unijn}

The uniqueness rules for the meet and join constructions can have instances with a duplication in the premiss and conclusion:

{c ⩽ a∧a, c ⩽ a, c ⩽ a, Γ ⇒ Δ \atop c ⩽ a, c ⩽ a, Γ ⇒ Δ}^{Unimt}

and similarly for join. The rule where c ⩽ a is contracted in both the premiss and conclusion can be added to the system to meet the closure condition. If height-preserving contraction is not required, the contracted rule can be proved admissible: Using admissibility of left weakening, admissibility of the rule obtained from Unimt is proved as follows, starting with the contracted premiss c ⩽ a∧a, c ⩽ a, Γ ⇒ Δ:

{c ⩽ a∧a, c ⩽ a, Γ ⇒ Δ \atop c ⩽ a∧a, c ⩽ a, a ⩽ a∧a, Γ ⇒ Δ}^{LW}

c ⩽ a, a ⩽ a∧a, Γ ⇒ Δ Trans

c ⩽ a, a ⩽ a∧a, a ⩽ a, a ⩽ a, Γ ⇒ Δ LW,LW

c ⩽ a, a ⩽ a, a ⩽ a, Γ ⇒ Δ Unimt

c ⩽ a, Γ ⇒ Δ

Ref,Ref

All structural rules are admissible in the proof-theoretical formulation of lattice theory.

As a consequence of having an equality relation defined through partial order, substitution of equals in the meet and join operations,

b = c ⊃ a∧b = a∧c b = c ⊃ a∨b = a∨c

need not be postulated but can instead be derived. For example, we have a∧b ⩽ a by Mtl and a∧b ⩽ c by Mtl, b ⩽ c and Trans, so a∧b ⩽ a∧c follows by Unimt.

Lattice theory is conservative over partial order:

Theorem 6.6.5: If Γ ⇒ Δ is derivable in lattice theory and Γ, Δ are quantifier-free and do not contain lattice operations, then Γ ⇒ Δ is derivable in the theory of partial order.

Proof: We can assume that Γ ⇒ Δ is a regular sequent. Its derivation is a linear sequence starting with a logical axiom, followed by applications of nonlogical rules of lattice theory. The succedent is always Δ, whereas each step of inference removes one atom from the antecedent. Let a ⩽ c be the atom active in the top sequent a ⩽ c, Γ′ ⇒ Δ′, a ⩽ c where Δ′, a ⩽ c = Δ. If in the derivation there is an instance of rule Ref with a ⩽ c principal in it, then a ≡ c and a ⩽ c, Γ ⇒ Δ is a logical axiom from which Γ ⇒ Δ follows by Ref. Since a ⩽ c has no lattice operations it can otherwise disappear only in an instance of rule Trans. We must thus have in the topsequent the atoms a ⩽ b, b ⩽ c, a ⩽ c, with a chain a ⩽ b, b ⩽ c of two atoms, and the atom a ⩽ c removed further down in an instance of Trans. If both a ⩽ b and b ⩽ c are in the endsequent of the whole derivation, then Γ = a ⩽ b, b ⩽ c, Γ′′ and Γ ⇒ Δ follows from the logical axiom a ⩽ c, a ⩽ b, b ⩽ c, Γ′′ ⇒ Δ by Trans. Else a ⩽ b or b ⩽ c is not in Γ. If, say, a ⩽ b diasappears by Trans, with active formulas a ⩽ d and d ⩽ b, then the topsequent contains the atoms a ⩽ d, d ⩽ b, b ⩽ c, a ⩽ c, a ⩽ b. Two applications of rule Trans leave the chain of three atoms a ⩽ d, d ⩽ b, b ⩽ c. Proceeding in this way we trace all the atoms that disappear through rule Trans and mark all the formulas in the topsequent that are active in the derivation up to that point. If some of them disappear through Ref they are simply removed from the derivation. We thus obtain a derivation containing a sequent with a chain a ⩽ b_{0}, b_{0} ⩽ b_{1}, …, b_{n} ⩽ c such that none of the atoms in the chain disappear through Ref or Trans. Therefore each b_{i} belongs to atoms that disappear because of lattice rules and each atom b_{i} ⩽ b_{i+1} must contain a lattice operation.

Next we give transformations of the given derivation of Γ ⇒ Δ that each reduce the number of atoms containing lattice operations in the antecedent of the topsequent and disappearing through lattice rules. Repeating the transformations we obtain a derivation where no atoms containing lattice operations and disappearing through lattice rules are present, thus a derivation where only rules of partial order are applied.

We claim that in the chain a ⩽ b_{0}, b_{0} ⩽ b_{1}, …, b_{n} ⩽ c there is a contiguous pair of atoms that disappear through rules Unimt, Mt or Jn, Unijn: Start with a ⩽ b_{0}. If the outermost lattice operation of b_{0} is ∧, the atom a ⩽ b_{0} has to disappear through Unimt (remember that a does not contain meet or join). Then b_{0} ⩽ b_{1} either disappears through Jn, Unimt or Mt. In the last case we are done, else we continue analyzing b_{1} ⩽ b_{2}. If the first case had occured, b_{1} ⩽ b_{2} can disappear through Unijn or Jn or Unimt, if the second, it can disappear through Jn or Unimt or Mt. In the last case we have the conclusion.

Let b_{k} be the first of the b_{i} that does not contain lattice operations. (If there are none, consider the last term c in the chain.) We continue until we have that b_{k−2} ⩽ b_{k−1} disappears through Jn or Unimt. But then b_{k−1} ⩽ b_{k} disappears throughUnijn or Mt respectively, since b_{k} does not contain lattice operations. We prove the result in a similar fashion if the outermost lattice operation of b_{0} is ∨.

Let two contiguous atoms b ⩽ d∧e and d∧e ⩽ d disappear through Unimt, Mt. Fot Unimt to be applicable, the topsequent has to contain the atoms b ⩽ d and b ⩽ e. Then replace the two atoms b ⩽ d∧e and d∧e ⩽ d with the single atom b ⩽ d, and continue the derivation as before except for removing the instances of Trans where the two atoms were active and the two steps Unimt, Mt. In this way the number of atoms containing lattice operations is decreased. If there are two contiguous atoms that diasppear through Jn, Unijn, let them to be b ⩽ b∨d, b∨d ⩽ e. Then replace them with the atom b ⩽ e that is found in the topsequent and remove the steps where the two atoms were active. Again, this proof transformation decreases the number of atoms containing lattice operations. QED.

(e) Affine geometry: We have two sets of basic objects, points denoted by a, b, c, … and lines denoted by l, m, n, …. In order to eliminate all logical structure from the nonlogical rules, we use a somewhat unusual set of basic concepts, written as follows:

a ≠ b, a and b are distinct points,

l ≠ m, l and m are distinct lines,

l ∦ m, l and m are convergent lines,

A(a, l), point a is outside line l.

The usual concepts of equal points, equal lines, parallel lines and incidence of a point with a line, are obtained as negations from the above. These are written as a = b, l = m, l ∥ m and I(a, l), respectively.

The axioms, with names added, are as follows:

I Axioms for apartness relations:

∼a ≠ a (Irref), a ≠ b ⊃ a ≠ c ∨ b ≠ c (Split),

∼l ≠ l (Irref), l ≠ m ⊃ l ≠ n ∨ m ≠ n (Split),

∼l ∦ l (Irref), l ∦ m ⊃ l ∦ n ∨ m ∦ n (Split).

These three basic relations are apartness relations and their negations equivalence relations.

Next we have three constructions, two of which have conditions: the connecting line ln(a, b) that can be formed if a ≠ b has been proved, the intersection point pt(l, m) where similarly l ∦ m is required to be proved, and the parallel line par(l, a) that can be applied without any conditions, uniformly in l and a.

Constructed objects obey incidence and parallelism properties expressed by the next group of axioms

II Axioms of incidence and parallelism:

a ≠ b ⊃ I(a, ln(a, b)) (Inc), a ≠ b ⊃ I(b, ln(a, b)) (Inc),

l ∦ m ⊃ I(pt(l, m), l) (Inc), l ∦ m ⊃ I(pt(l, m), m) (Inc),

I(a, par(l, a)) (Inc),

l ∥ par(l, a) (Par).

Uniqueness of connecting lines, intersection points and parallel lines is guaranteed by

III Uniqueness axioms:

a ≠ b & l ≠ m ⊃ A(a, l) ∨ A(b, l) ∨ A(a, m) ∨ A(b, m) (Uni),

l ≠ m ⊃ A(a, l) ∨ A(a, m) ∨ l ∦ m (Unipar).

The contrapositions of these two principles express usual uniqueness properties.

Last, we have

IV Substitution axioms:

A(a, l) ⊃ a ≠ b ∨ A(b, l) (Subst),

A(a, l) ⊃ l ≠ m ∨ A(a, m) (Subst),

l ∦ m ⊃ l ≠ n ∨ m ∦ n (Subst), Again, the contrapositions of these three axioms give the usual substitution principles.

The above axiom system is equivalent to standard systems, such as Artin’s (1957) axioms. These state the existence and uniqueness of connecting lines and parallel lines, and existence and properties of intersection points are obtained through a defined notion of parallels. As is typical in such an informal discourse, the principles corresponding to our groups I and IV are left implicit. There is a further axiom stating the existence of at least three noncollinear points, but as explained in von Plato (1995), we do not use such existential axioms, say (∃x : P t)(∃y : P t)x ≠ y and (∀x : Ln)(∃y : P t)A(y, x). The same effect is achieved by systematically considering only geometric situations containing the assumptions a : P t, b : P t, a ≠ b, c : P t, A(c, ln(a, b)).

An axiom such as a ≠ b ⊃ I(a, ln(a, b)) hides a structure going beyond first-order logic. Contrary to appearence, it does not consist of two independent formulas a ≠ b and I(a, ln(a, b)) and a connective, for the latter is a well-formed formula only if a ≠ b has been proved. (For a detailed explanation of this structure, dependent typing, see Section 3 of Appendix B.) As an example of conditions for well-formed formulas, from our axioms a “triangle axiom”

A(c, ln(a, b)) ⊃ A(b, ln(c, a))

can be derived, but the conditions a ≠ b and c ≠ a are required for this to be well-formed. Here we can actually prove more, the lemma

a ≠ b & A(c, ln(a, b)) ⊃ c ≠ a

Assume for this a ≠ b and A(c, ln(a, b)). By the first substitution axiom, A(c, ln(a, b)) gives c ≠ a ∨ A(a, ln(a, b)). By incidence axioms, I(a, ln(a, b)), so that c ≠ a follows. By the second substitution axiom, A(c, ln(a, b)) gives ln(a, b) ≠ ln(c, a) ∨ A(c, ln(c, a)), so that ln(a, b) ≠ ln(c, a) follows. By the uniqueness axiom, a ≠ b and ln(a, b) ≠ ln(c, a)) give A(a, ln(a, b))∨A(b, ln(a, b))∨ A(a, ln(c, a)) ∨ A(b, ln(c, a)), so the incidence axioms lead to the conclusion A(b, ln(c, a)).

Examples of conditions can be found in mathematics whenever first-order logic is insufficient. A familiar case is field theory, where results involving inverses x^{−1}, y^{−1}, … can only be expressed after the conditions x ≠ 0, y ≠ 0, … have been established.

In a more formal treatment of conditions, they can be made into progressive contexts in the sense of type theory (see Martin-Löf 1984 and von Plato 1995). Such contexts can be arbitrarily complex, even if the formulas in them should all be atomic. For example, the formula ln(pt(l, m), a) ≠ l presupposes that pt(l, m) ≠ a which in turn presupposes that l ∦ m.

The reason for having basic concepts different from the traditional ones is not only that the “apartness” style concepts suit a constructive axiomatization. There is a reason for the choice of these concepts in classical theories also: Namely, if the conditions a ≠ b and l ∦ m were defined as a = b ⊃ ⊥ and l ∥ m ⊃ ⊥, the natural logic-free expression of the incidence axioms would be lost.

All of the axioms of plane affine geometry can be converted into nonlogical rules, moreover, closure condition 6.1.7 will not lead to any new rules. We conclude that the structural rules are admissible in the rule system for plane affine geometry.

We first derive a form of Euclid’s fifth postulate from the geometrical rules: Given a point a outside a line l, no point is incident with both l and the parallel to l through point a. Axiomatically, we may express this by the formula

A(a, l) ⊃ ∼(I(b, l)&I(b, par(l, a)))

The sequent

A(a, l) ⇒ A(b, l), A(b, par(l, a))

is classically equivalent to the previous one and expresses the same principle as a logic-free multisuccedent sequent. To derive this sequent, we note that by admissibility of structural rules, all rules in its derivation are nonlogical, and therefore the succedent is always the same, A(b, l), A(b, par(l, a)). Further, no conditions will appear. With these prescriptions, root-first proofsearch is very nearly deterministic. Inspecting the sequent to be derived, the last step has to be a substitution rule, where the second premiss is immediately derived. In order to fit the derivations in, the principal formulas are not repeated in the premisses, and the second formula in the succedent is abbreviated by A = A(b, par(l, a)).

l ≠ par(l, a) ⇒ A(b, l), A A(a, par(l, a)) ⇒ A(b, l), A^{Inc} A(a, l) ⇒ A(b, l), A Subst

The first premiss can be derived by the uniqueness of parallels, and now the rest is obvious:

A(b, l) ⇒ A(b, l), A A ⇒ A(b, l), A l ∦ par(l, a) ⇒ A(b, l), A^{Par} l ≠ par(l, a) ⇒ A(b, l), A Unipar

We shall show that when the rule of uniqueness of parallels is left out, the sequent

A(a, l) ⇒ A(b, l), A(b, par(l, a))

is not derivable by the rules of affine geometry. We know already that if there is such a derivation, it must end with one of the two first substitution rules. If it is the first rule, we have

\begin{matrix}a ≠ b ⇒ A(b, l), A & A(b, l) ⇒ A(b, l), A \\ A(a, l) ⇒ A(b, l), A \end{matrix}^{Subst}

Then the first premiss must be derivable. It is not an axiom, and unless a = b, it does not follow by Irref. Split only repeats the problem, leading to an infinite regress. This leaves only the second substitution rule, and we have

\begin{matrix}l ≠ m ⇒ A(b, l), A & A(a, m) ⇒ A(b, l), A \\ A(a, l) ⇒ A(b, l), A \end{matrix}^{Subst}

As in the first case, rules for apartness relations will not lead to the first premiss. Otherwise it could only be derived by uniqueness of parallels, but that is not available. By theorem 6.3.2, derivability in the system of rules is equivalent to derivability with axioms, and we conclude the

Theorem 6.6.6: The uniqueness axiom for parallel lines is independent of the other axioms of plane affine geometry.

In case of theorems with quantifiers, assuming classical logic, a theorem to be proved is first converted into prenex form, then the propositional matrix into the variant of conjunctive normal form used above. Each conjunct corresponds to a regular sequent, without logical structure, and the overall structure of the derivation is as follows: First the regular sequents are derived by nonlogical rules only, then the conjuncts by L&, R∨ and R⊃. Now R& collects all these into the propositional matrix, and right quantifier rules lead into the theorem. The nonlogical rules typically contain function constants resulting from quantifier elimination. In the constructive case, these methods apply to formulas in the prenex-fragment admitting a propositional part in regular normal form.

An example may illustrate the above structure of derivations: Consider the formula expressing that for any two points, if they are distinct, there is a line on which the points are incident,

∀x∀y(x ≠ y ⊃ ∃z(I(x, z)&I(y, z))).

In prenex normal form, with the propositional matrix in the implicational variant of conjunctive normal form, this is equivalent to

∀x∀y∃z((x ≠ y&A(x, z) ⊃ ⊥)&(x ≠ y&A(y, z) ⊃ ⊥)).

In a quantifier-free approach, we have instead the connecting line construction with incidence properties expressed by rules in a quantifier-free form:

a ≠ b, A(a, ln(a, b)), Γ ⇒ Δ^{Inc}  a ≠ b, A(b, ln(a, b)), Γ ⇒ Δ^{Inc}

We have the following derivation:

\begin{matrix}\begin{matrix}x ≠ y, A(x, ln(x, y)) ⇒ ⊥ & Inc \\ x ≠ y &A(x, ln(x, y)) ⇒ ⊥ \end{matrix}_{L&} ; ⇒ x ≠ y &A(x, ln(x, y)) ⊃ ⊥_{R⊃} & \begin{matrix}x ≠ y, A(y, ln(x, y)) ⇒ ⊥ & Inc \\ x ≠ y &A(y, ln(x, y)) ⇒ ⊥ \end{matrix}_{L&} ; ⇒ x ≠ y &A(y, ln(x, y)) ⊃ ⊥_{R⊃} \\ ⇒ (x ≠ y &A(x, ln(x, y)) ⊃ ⊥) &(x ≠ y &A(y, ln(x, y)) ⊃ ⊥) \end{matrix}_{R&} ; ⇒ ∃z((x ≠ y &A(x, z) ⊃ ⊥) &(x ≠ y &A(y, z) ⊃ ⊥))_{R∃} ; ⇒ ∀x∀y∃z((x ≠ y &A(x, z) ⊃ ⊥) &(x ≠ y &A(y, z) ⊃ ⊥))_{R∀,R∀}

Derivations with nonlogical rules and all but two of the logical rules of multisuccedent sequent calculi, R⊃ and R∀, do not show whether a system is classical or constructive. The difference only appears if classical logic is needed in the conversion of axioms into rules.

Notes to Chapter 6

Most of the materials of this chapter come from Negri (1999) and Negri and von Plato (1998). The former work contains a single succedent approach to extension of contraction- and cut-free calculi with nonlogical rules. These calculi are used for a proof-theoretical analysis of derivations in theories of apartness and order, leading to conservativity results which have not been treated here. The latter work uses a multisuccedent approach. The examples in subsections (b) and (c) of Section 6.6 are treated in detail in Negri (1999). The proof-theoretic treatment of constructive linear order in subsection (c) is extended in Negri (1999a) to a theory of constructive ordered fields and real closed fields. The geometrical example in subsection (e) comes from von Plato (1998b).

Our proof of theorem 6.6.1 was suggested by the proof in Buss (1998), section 2.5.1.

In Section 6.4, we mentioned some previous attempts at extending cut elimination to axiomatic systems. The work of Uesu (1984) contains the correct way of presenting atomic axioms as rules of inference. As to the use of conjunctive normal form in sequent calculus, we owe it to Ketonen’s thesis of 1944, in which the invertible sequent calculus for classical propositional logic was discovered.