appendix sectionrules

Intuitionistic first-order natural deduction and LJ

Individual terms and formulas are generated by $\begin{aligned} t & ::= x ∣ f (t_{1}, \dots, t_{n}), \\ A & ::= P (t_{1}, \dots, t_{n}) ∣ ⊥ ∣ A \land A ∣ A \lor A \\ ∣ A \to A ∣ \forall x A ∣ \exists x A . \end{aligned}$ Substitution is capture avoiding. Contexts are finite multisets, and every eigenvariable side condition below is part of the rule.

The complete natural-deduction judgment $Γ ⊢_{N} A$ is generated by

A \in Γ

Γ ⊢_{N} A

Hyp

Γ ⊢_{N} ⊥

Γ ⊢_{N} A

Bot-E

Γ ⊢_{N} A

Γ ⊢_{N} B

Γ ⊢_{N} A \land B

And-I

Γ ⊢_{N} A_{1} \land A_{2}

Γ ⊢_{N} A_{i}

And-E_i

Γ ⊢_{N} A

Γ ⊢_{N} A \lor B

Or-I_1

Γ ⊢_{N} B

Γ ⊢_{N} A \lor B

Or-I_2

Γ ⊢_{N} A \lor B

Γ, A ⊢_{N} C

Γ, B ⊢_{N} C

Γ ⊢_{N} C

Or-E

Γ, A ⊢_{N} B

Γ ⊢_{N} A \to B

Imp-I

Γ ⊢_{N} A \to B

Γ ⊢_{N} A

Γ ⊢_{N} B

Imp-E

Γ ⊢_{N} A [a / x]

a \notin fv (Γ, \forall x A)

Γ ⊢_{N} \forall x A

All-I

Γ ⊢_{N} \forall x A

Γ ⊢_{N} A [t / x]

All-E

Γ ⊢_{N} A [t / x]

Γ ⊢_{N} \exists x A

Some-I

Γ ⊢_{N} \exists x A

Γ, A [a / x] ⊢_{N} C

a \notin fv (Γ, C, \exists x A)

Γ ⊢_{N} C

Some-E

LJ sequents have one conclusion. Its structural and logical rules are

Γ, A \Rightarrow A

Γ \Rightarrow A

Δ, A \Rightarrow C

Γ, Δ \Rightarrow C

Cut

Γ \Rightarrow C

Γ, A \Rightarrow C

W-L

Γ, A, A \Rightarrow C

Γ, A \Rightarrow C

C-L

Γ, ⊥ \Rightarrow C

Bot-L

Γ \Rightarrow A

Γ \Rightarrow B

Γ \Rightarrow A \land B

And-R

Γ, A_{i} \Rightarrow C

Γ, A_{1} \land A_{2} \Rightarrow C

And-L_i

Γ \Rightarrow A

Γ \Rightarrow A \lor B

Or-R_1

Γ \Rightarrow B

Γ \Rightarrow A \lor B

Or-R_2

Γ, A \Rightarrow C

Γ, B \Rightarrow C

Γ, A \lor B \Rightarrow C

Or-L

Γ, A \Rightarrow B

Γ \Rightarrow A \to B

Imp-R

Γ \Rightarrow A

Δ, B \Rightarrow C

Γ, Δ, A \to B \Rightarrow C

Imp-L

Γ \Rightarrow A [a / x]

a \notin fv (Γ, \forall x A)

Γ \Rightarrow \forall x A

All-R

Γ, A [t / x] \Rightarrow C

Γ, \forall x A \Rightarrow C

All-L

Γ \Rightarrow A [t / x]

Γ \Rightarrow \exists x A

Some-R

Γ, A [a / x] \Rightarrow C

a \notin fv (Γ, C, \exists x A)

Γ, \exists x A \Rightarrow C

Some-L

For labeled assumptions $Ξ = h_{1} : A_{1}, \dots, h_{k} : A_{k}$ , proof terms add $\begin{aligned} p ::= & h ∣ λ h . p ∣ p q ∣ ⟨ p, q ⟩ ∣ π_{i} p ∣ {in}_{i} p ∣ case (p; h . q; k . r) \\ ∣ Λ a . p ∣ p [t] ∣ pack (t, p) ∣ unpack (p; a, h . q) ∣ abort (p) . \end{aligned}$ The propositional constructors use the natural-deduction rules already listed, with proof labels attached. The quantifier and bottom rules are

Ξ ⊢ p : A [a / x]

a \notin fv (Ξ, \forall x A)

Ξ ⊢ Λ a . p : \forall x A

Ξ ⊢ p : \forall x A

Ξ ⊢ p [t] : A [t / x]

Ξ ⊢ p : A [t / x]

Ξ ⊢ pack (t, p) : \exists x A

Ξ ⊢ p : \exists x A

Ξ, h : A [a / x] ⊢ q : C

a \notin fv (Ξ, C, \exists x A)

Ξ ⊢ unpack (p; a, h . q) : C

Ξ ⊢ p : ⊥

Ξ ⊢ abort (p) : A

The proof-term roots corresponding to principal implication and quantifier cuts are $\begin{aligned} (λ h . q) p & ⇝_{p} q [p / h], \\ (Λ a . q) [t] & ⇝_{p} q [t / a], \\ unpack (pack (t, p); a, h . q) & ⇝_{p} q [t / a] [p / h] . \end{aligned}$ The first-order compatible-context additions are $K ::= Λ a . K ∣ K [t] ∣ pack (t, K) ∣ unpack (K; a, h . q) ∣ unpack (p; a, h . K) ∣ abort (K) .$ Together with the propositional contexts, they generate $i n f e r r u l e r ⇝_{p} r^{'} K [r] ⟶_{p} K [r^{'}]$ .