August 2014
Intermediate to advanced
386 pages
14h 39m
English
Content preview from Proof Theory
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
Start your free trial
62 Proof Theory: Sequent Calculi and Related Formalisms
A⊃B, Γ A B, A⊃B, Γ X
A⊃B, Γ X
⊃
A, Γ B
Γ A⊃B
⊃
A(y), ∀x A(x), Γ X
∀x A(x), Γ X
∀
Γ A(y)
Γ ∀x A(x)
∀
A(y), ∃x A(x), Γ X
∃x A(x), Γ X
∃
Γ A(y)
Γ ∃x A(x)
∃
X standsforeitherasingleformulaorfortheemptysequenceofformulas.
The variable restrictions, the notions of proof and theorem are as before.
Exercise
∗
3.1.9. Prove that if Γ Δ is provable in LK, then it is provable in
LK
3
, and vice versa. [Hint: Use inductions on the height of the proofs.]
Exercise
∗
3.1.10. Prove the equivalence of LJ and LJ
3
. [Hint: Prove similar
claims as in the previous exercise.]
3.2 Sequent calculi with multisets