Structural proof analysis for mathematical theories

Axiom-as-rules: Formulate axioms as inference rules extending G3 calculi .

Regular rule scheme: Only atomic formulas as active and principal. Logical content of the axiom embodied in the geometry of the rule. Arbitrary context in the succedent.

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

Classical logic: All quantifier-free axioms can be formulated as rules following the regular rulescheme.

Intuitionistic logic: All regular axioms can be formulated as rules following the regular rule-scheme.

Handling contraction

Principal formulas repeated in the premisses

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

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

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

then it also has to contain the rule

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

Results

Theorem: All the structural rules (weakening, contraction, and cut) are admissible in the extensions of the G3 calculi with rules following the regular rule scheme. Weakening and contraction are admissible and heightpreserving.

Geometric theories

Definition: A formula in the language of first-order logic is called geometric if it does not contain ⊃ or ∀. A geometric implication is a sentence of the form

∀\overline{x}(A ⊃ B)

where A and B are geometric formulas. A geometric theory is a theory axiomatized by geometric implications.

Canonical form for geometric implications: Any geometric implication can be reduced to a conjunction of formulas of the form

∀\overline{x}(P_{1}& … &P_{m} ⊃ ∃y_{1}M_{1}∨…∨∃y_{n}M_{n}) GA

where all the P_{i} are atomic formulas and all the M_{j} are conjunctions of atomic formulas and the variables y_{j} are not free in the P_{i}.

The geometric rule scheme

\frac{\overline{Q}_{1}(y_{1}/x_{1}), \overline{P} , Γ ⇒ Δ … \overline{Q}_{n}(y_{n}/x_{n}), \overline{P} , Γ ⇒ Δ}{\overline{P} , Γ ⇒ Δ} GRS

The variables x_{i} are called the replaced variables of the scheme, and the variables y_{i} the proper variables Condition: The proper variables are not free in \overline{P} , Γ, Δ.

Elimination of structural rules

Definition: Let T be a geometric theory and let G3cT (G3imT) be the Gentzen system obtained by adding to G3c(G3im) the geometric rule-schemes corresponding to the geometric axioms of T, together with the rules arising from the closure condition. Equivalence of axiomatic and rule system: A geometric axiom is derivable from the corresponding geometric rule-scheme. Conversely, a geometric rule is derivable from the corresponding geometric axiom in G3imT+contr+cut.

Inversion lemmas: All the inversion lemmas for the propositional rules that hold for G3c and G3im hold for their geometric extension as well.

Substitution lemma: Given a derivation of Γ ⇒ Δ in G3cT (G3imT, resp.), with x a free variable in Γ, Δ and a term t free for x in Γ, Δ not containing any of the variables of the geometric rules in the derivation, we can find a derivation of Γ(t/x) ⇒ Δ(t/x) in G3cT (G3imT, resp.) with the same height.

Inversion lemma for quantifier rules.

(i) If ⊢_{n} ∃xA, Γ ⇒ Δ and y is not among the variables of the geometric rules in the derivation, then ⊢_{n} A(y/x), Γ ⇒ Δ. (ii) If ⊢_{n} Γ ⇒ Δ, ∀xA and y is not among the variables of the geometric rules in the derivation, then ⊢_{n} Γ ⇒ Δ, A(y/x).

Disjointness condition. In a derivation in G3cT (G3imT) the sets of proper variables of the geometric rules are pairwise disjoint.

Theorem: The rules of weakening

\frac{Γ ⇒ Δ}{A, Γ ⇒ Δ}LW  \frac{Γ ⇒ Δ}{Γ ⇒ Δ, A}RW

are admissible and height preserving in G3cT and in G3imT.

Theorem: The rules of contraction

\frac{A, A, Γ ⇒ Δ}{A, Γ ⇒ Δ}LC  \frac{Γ ⇒ Δ, A, A}{Γ ⇒ Δ, A}RC

are admissible and height-preserving in G3cT and in G3imT. Theorem: The cut rule

\frac{Γ ⇒ Δ, A  A, Γ′ ⇒ Δ′}{Γ, Γ′ ⇒ Δ, Δ′} Cut

is admissible in G3cT and in G3imT.

Examples of geometric theories

• Robinson’s arithmetic

• Ordered fields, Real closed fields

• Constructive projective geometry

But... Classical projective geometry is not geometric a. Robinson arithmetic Language: constant 0, unary successor function s, binary functions + and ·, relation =. Atomic formulas of the form a = b, for arbitrary terms a and b.

1. ¬ s(x) = 0

2. s(x) = s(y) ⊃ x = y

3. x = 0 ∨ ∃y x = s(y)

4. x + 0 = x

5. x + s(y) = s(x + y)

6. x · 0 = 0

7. x · s(y) = x · y + x The classically equivalent axiomatization with 3. replaced by 3′. ¬ x = 0 ⊃ ∃y x = s(y) is not geometric because it has an implication (x = 0 ⊃⊥) in the antecedent of an implication. b. Ordered fields I. Axioms for nondegenerate linear order

1. x ⩽ x

2. x ⩽ y ∨ y ⩽ x

3. x ⩽ y & y ⩽ z ⊃ x ⩽ z

4. ¬ 1 ⩽ 0 II. Axioms for ordered additive group

5. (x + y) + z = x + (y + z)

6. x + y = y + x

7. x + 0 = x

8. ∃y x + y = 0

9. x ⩽ y ⊃ x + z ⩽ y + z III. Axioms for multiplication

10. (x · y) · z = x · (y · z)

11. x · y = y · y

12. x · 1 = x

13. x = 0 ∨ ∃y x · y = 1

14. x · (y + z) = x · y + x · z

15. x ⩽ y & 0 ⩽ z ⊃ x · z ⩽ y · z The classically equivalent axiomatization with

13′. ¬ x = 0 ⊃ ∃y x · y = 1 in place of 13. is not geometric.

Real closed fields: Add the axioms stating the existence of square roots and zeroes of polynomials of odd degree

16. 0 ⩽ x ⊃ ∃y x = y · y

17. a_{2n+1} = 0 ∨ ∃x a_{2n+1} · x^{2n+1} + a_{2n} · x^{2n} +

… a_{1} · x + a_{0} = 0

The classically equivalent axiomatization with 17 replaced by

17′. ¬ a_{2n+1} = 0 ⊃ ∃x a_{2n+1} · x^{2n+1} + a_{2n} ·

x^{2n} + … a_{1} · x + a_{0} = 0

is not geometric.

Classical projective geometry with constructions: Basic concepts equality and incidence: a = b, l = m, a ∈ l. Constructions: ln(a, b), pt(l, m).

I. Axioms for equivalence relations a = a, a = c & b = c ⊃ a = b l = l, l = n & m = n ⊃ l = m

II. Axioms of incidence:

a = b ∨ a ∈ ln(a, b), a = b ∨ b ∈ ln(a, b) l = m ∨ pt(l, m) ∈ l, l = m ∨ pt(l, m) ∈ m

III. Uniqueness axiom:

a ∈ l & b ∈ l & a ∈ m & b ∈ m ⊃ a = b ∨ l = m

IV. Substitution axioms:

a ∈ l & a = b ⊃ b ∈ l a ∈ l & l = m ⊃ a ∈ m

V. Existence of noncollinear points: ∃x∃y∃z(∼x = y & ∼z ∈ ln(x, y))

Not geometric.

Constructive projective geometry with constructions: Basic concepts: a ≠ b, l ≠ m, a ∉ l Constructions: ln(a, b), pt(l, m)

I. Axioms for apartness relations: a = a ⊃ ⊥, a ≠ b ⊃ a ≠ c ∨ b = c l = l ⊃ ⊥, l ≠ m ⊃ l ≠ n ∨ m = n

II.Axioms of incidence:

a ≠ b & a ∉ ln(a, b) ⊃ ⊥ a ≠ b & b ∉ ln(a, b) ⊃ ⊥ l ≠ m & pt(l, m) ∉ l ⊃ ⊥ l ≠ m & pt(l, m) ∉ m ⊃ ⊥

III. Uniqueness axiom:

a ≠ b & l ≠ m ⊃ a ∉ l ∨ b ∉ l ∨ a ∉ m ∨ b ∉ m

IV. Substitution axioms:

a ∉ l ⊃ a ≠ b ∨ b ∉ l a ∉ l ⊃ l ≠ m ∨ a ∉ m

V. Existence of noncollinear points: ∃x∃y∃z(x ≠ y & z ∉ ln(x, y))

Geometric.

Barr’s theorem

Topos Theory: For any Grothendieck topos E, there is a Boolean topos B and a geometric morphism γ : B → E such that γ^{∗} is faithful (cf. Johnstone (1977), Mac Lane and Moerdijk (1992)).

Logic: If a geometric implication is classically derivable in a geometric theory, then it is intuitionistically derivable. Palmgren (1998) proved the result using the Dragalin-Friedman translation.

Our statement: Let T be a geometric theory, and let A be a geometric implication. If G3cT ⊢ ⇒ A, then G3imT ⊢ ⇒ A.

Our proof: Nothing to prove!

References

Bell, J.L. (1988) Toposes and Local Set Theory, Clarendon Press, Oxford.

Coste, M., H. Lombardi, and M.-F. Roy (2001) Dynamical method in algebra: Effective Nullstellensätze, Annals of Pure and Applied Logic, in press.

Johnstone (1977) Topos Theory, Academic Press, London.

Mac Lane, S. and I. Moerdijk (1992) Sheaves in Geometry and Logic, Springer-Verlag.

Negri, S. (2001) A sequent calculus for constructive ordered fields. In U. Berger et al. (eds) Reuniting the Antipodes. Constructive and Nonstandard Views of the Continuum, Kluwer, Dordrecht, in press.

Negri, S. and J. von Plato (1998) Cut elimination in the presence of axioms, The Bulletin of Symbolic Logic, vol. 4, pp. 418–435.

Negri, S. and J. von Plato (2001) Structural Proof Theory, Cambridge University Press.

Palmgren, E. (1998) A note on constructive real closed fields, 3 pages. Available at

http://www.math.uu.se/ palmgren/publicat.html.