Sequent calculus

base element, the sequent:

sequent: Γ ⊢ Δ

meaning: the conjunction of the formulae in Γ implies the disjunction of the formulae in Δ

proceed from simple sequents like x⊢x

rules combine them to form more complex ones

to prove that B follows from A₁,…,A_n
try to obtain the sequent A₁,…,A_n⊢B

axioms:

x⊢x

⊥⊢

⊢⊤

structural rule:

Γ₁⊢Δ₁		if Γ₁ ⊆ Γ₂ and Δ₁ ⊆ Δ₂
Γ₂⊢Δ₂		if Γ₁ ⊆ Γ₂ and Δ₁ ⊆ Δ₂

negation rules:

Γ⊢Δ,X

Γ,¬X⊢Δ

Γ,X⊢Δ

Γ⊢Δ,¬X

conjunction rules:

Γ,X,Y⊢Δ

Γ,X∧Y⊢Δ

Γ⊢Δ,X Γ⊢Δ,Y

Γ⊢Δ,X∧Y

disjunction rules:

Γ,X⊢Δ Γ,Y⊢Δ

Γ,X∨Y⊢Δ

Γ⊢Δ,X,Y

Γ⊢Δ,X∨Y

implication rules:

Γ⊢Δ,X Δ,Y⊢Δ

Γ,X→Y⊢Δ

Γ,X⊢Δ,Y

Γ⊢Δ,X→Y

parts of a rule:

premise premise premise …

consequent

proof=tree of sequents where:

each leaf is the consequent of an axiom
each internal node is the consequent of a rule and its children are the premises of the rule

obvious on an example (next)

prove that (A∧B)→(B∧A) is a valid formula