Subterm property via permutation of rules

Extension of the contraction-free sequent calculi G3c-G3i + height preserving invertibility of rules + height preserving admissibility of weak. and contr. + feasibility for proof search + subterm property enjoyed by minimum-size derivations − difficult proof analysis

Extension of natural deduction + more flexible proof analysis − limitation to Harrop theories

This second approach in the example of lattice theory

NDLT

Rules for lattice theory with meet and join

a ⩽ a^{Ref}  \begin{matrix}a ⩽ b & b ⩽ c \\ a ⩽ c \end{matrix}^{Trans}
a∧b ⩽ a^{L∧_{1}}  a∧b ⩽ b^{L∧_{2}}  \begin{matrix}c ⩽ a & c ⩽ b \\ c ⩽ a∧b \end{matrix}^{R∧}
a ⩽ a∨b^{R∨_{1}}  b ⩽ a∨b^{R∨_{2}}  \begin{matrix}a ⩽ c & b ⩽ c \\ a∨b ⩽ c \end{matrix}^{L∨}

Transitivity cannot be eliminated, but it can be reduced to instances where the middle term is a subterm of the conclusion Theorem. Subterm property for NDLT. If an atom is derivable from atomic assumptions in NDLT, it has a derivation with no new terms. Decidability of atoms from given assumptions follows.

Proof: consider topmost instance of Trans removing a new term b:

\begin{matrix}⋮ . ; a ⩽ b & ⋮ . ; b ⩽ c \\ a ⩽ c \end{matrix}^{Trans} (1)

1. First consider the derivation of the left premiss. If a ⩽ b concluded by Trans, permute up the Trans removing b:

\begin{matrix}\begin{matrix}a ⩽ d & d ⩽ b \\ a ⩽ b \end{matrix}^{Trans} & b ⩽ c \\ a ⩽ c \end{matrix}^{Trans} ⇝

\begin{aligned}a ⩽ d & \begin{matrix}d ⩽ b & b ⩽ c \\ d ⩽ c \end{matrix}^{Trans} \\ & a ⩽ c \end{aligned}_{Trans} (2)

Note that, by assumption, d is not a new term.

If a ⩽ b concluded by L∨, the term a has a form a ≡ d∨e and Trans is permuted up as follows:

\begin{matrix}\begin{matrix}d ⩽ b & e ⩽ b \\ d∨e ⩽ b \end{matrix}^{L∨} & b ⩽ c \\ d∨e ⩽ c \end{matrix}^{Trans} ⇝

\begin{matrix}d ⩽ b & b ⩽ c \\ d ⩽ c \end{matrix}^{Trans} \begin{matrix}e ⩽ b & b ⩽ c \\ e ⩽ c \end{matrix}^{Trans} d∨e ⩽ c_{L∨} (3)

Permutation of Trans removing b repeated until a left premiss d′ ⩽ b not derived by Trans or L∨. Can be: 1.1. Ref: Then d′ ≡ b, right premiss of Trans identical to the conclusion so b not a new term. L∧_{1}: Then d′ ≡ b∧e so b not a new term. L∧_{2}: Then d′ ≡ e∧b so b not a new term.

1.2. R∨_{1}, we have b ≡ d′∨b′ and the step

\begin{matrix}d′ ⩽ d′∨b′ ^{R∨_{1}} & d′∨b′ ⩽ c \\ d′ ⩽ c \end{matrix}^{Trans} ; ⋮ . ; a ⩽ c (4)

The case of R∨_{2} is similar. 1.3. R∧, we have some terms a′ and d, e such that b ≡ d∧e and

\begin{matrix}\begin{matrix}a′ ⩽ d & a′ ⩽ e \\ a′ ⩽ d∧e \end{matrix}^{R∧} & d∧e ⩽ c \\ a′ ⩽ c \end{matrix}^{Trans} ; ⋮ . ; a ⩽ c (5)

2. Consider the right premiss b ⩽ c of (4) and (5). If concluded by rules Trans or R∧, permute as in (2) and (3). Rules R∨_{1}, R∨_{2} are excluded dually to the excluded rules L∧_{1}, L∧_{2} in the left branch of (1). This leaves two cases for (4) and also for (5): 2.1. In (4), the right premiss after permutation becomes d′∨b′ ⩽ c′ for some term c′

\begin{matrix}d′ ⩽ d′∨b′ ^{R∨_{1}} & \begin{matrix}⋮ . ; d′ ⩽ c′ & b′ ⩽ c′ \\ d′∨b′ ⩽ c′ \end{matrix} ^{L∨} \\ d′ ⩽ c′ \end{matrix}_{Trans} ; ⋮ . ; a′ ⩽ c

is transformed into

⋮ . ; d′ ⩽ c′ ; ⋮ . ; a ⩽ c

with the transitivity step removed. 2.2

\begin{matrix}\begin{matrix}⋮ . ; a′ ⩽ d & a′ ⩽ e \\ a′ ⩽ d∧e \end{matrix}^{R∧} & d∧e ⩽ c′ ^{L∧_{1}} \\ a′ ⩽ c′ \end{matrix}_{Trans} ; ⋮ . ; a ⩽ c (6)

Now c′ ≡ d so the derivation is transformed into

⋮ . ; a′ ⩽ c ; ⋮ . ; a ⩽ c

with the transitivity step removed. Rule L∧_{2} is treated similarly. QED Corollary Lattice theory is conservative over partial order for universal formulas. Corollary 4. Decidability of universal formulas. The derivability of universal formulas in lattice theory is decidable.

Proof. Consider a universal formula in prenex form ∀x … ∀zA with A in conjunctive normal form. Each conjunct A_{k} is of the form P_{1}& … &P_{m} ⊃ Q_{1} ∨ … ∨ Q_{n}, with P_{i}, Q_{j} atoms. The lattice axioms have no disjunctions in positive parts and therefore (by Harrop’s theorem, see, e.g., Negri and von Plato 2001) A_{k} is derivable if and only if P_{1}& … &P_{m} ⊃ Q_{j} is derivable for some j. Apply theorem 2 to each of the Q_{j}. QED.

G0cp

Logical axiom: A ⇒ A Logical rules:

{A, B, Γ ⇒ Δ \atop A&B, Γ ⇒ Δ}^{L&}  Γ ⇒ Δ, A Γ′ ⇒ Δ′, B Γ, Γ′ ⇒ Δ, Δ′, A&B ^{R&}
A, Γ ⇒ Δ B, Γ′ ⇒ Δ′ A ∨ B, Γ, Γ′ ⇒ Δ, Δ′ ^{L∨}  {Γ ⇒ Δ, A, B \atop Γ ⇒ Δ, A ∨ B} ^{R∨}
Γ ⇒ Δ, A B, Γ′ ⇒ Δ′ A ⊃ B, Γ, Γ′ ⇒ Δ, Δ′ ^{L⊃}  {A, Γ ⇒ Δ, B \atop Γ ⇒ Δ, A ⊃ B} ^{R⊃}
⊥ ⇒ C ^{L⊥}

Rules of weakening:

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

Rules of contraction:

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

All the rules G0cp are invertible except L⊃ (only invertible with respect to its right premiss). The inversions of G0c are not height-preserving. The rule of cut,

Γ ⇒ Δ, D D, Γ′ ⇒ Δ′

Γ, Γ′ ⇒ Δ, Δ′ Cut

is admissible in G0c. Proof: Cf. NvP 2001, chapter 5.

G0c*

Extension of G0cp with rules following the right rule scheme

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

corresponding to axioms of the form

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

Results Admissibility of cut extends to G0c* In G0c* logical and structural rules permute down wrt the right rule scheme therefore in proof analysis suffices consider derivations of basic sequents. Weak subformula property holds. Sequent calculi with independent contexts are closer to natural deduction, but allow extension to non-Harrop theories. Example: Theory of linear lattices.