Abstracts.2020.Sequent

Sequent Calculi

by Nachi

Exercises

1. Prove
   1. 1. A → B → A
      2. A → B → A ∧ B
      3. A ∧ B → A
   2. 1. A → (A → B) → B
      2. (A → B → C) → (A → B) → A → C
   3. (A → B ∨ C) → (A → B) ∨ (A → C)
   4. ¬¬A → A
   5. (B → A) → ((A → B) → B) → A
   6. ((A → B) → A) → A
   7. (∀x. A → B(x)) → A → ∀x. B(x)
   8. ∃x. D(x) → ∀y. D(y)

Resources

• Logitext (web-based proof assistant for first-order classical logic using the sequent calculus without the rule Cut)

Bibliography

1. Gerhard Gentzen. 1969. The collected papers of Gerhard Gentzen. Edited by M. E. Szabo.
2. Stephen Cole Kleene. 1952. Introduction to metamathematics.
3. Jean-Yves Girard, Paul Taylor, Yves Lafont. 1989. Proofs and types.
4. Anne Sjerp Troelstra, Helmut Schwichtenberg. 1996. Basic proof theory.
5. Jan von Plato. 2008–2018. The Development of Proof Theory. In The Stanford Encyclopedia of Philosophy.
6. Frank Pfenning. 2017. Lecture notes on sequent calculus. For 15-317 Fall 2017: Constructive Logic.
7. Michael Rathjen, Wilfried Sieg. 2018–2020. Proof Theory. In The Stanford Encyclopedia of Philosophy.
8. Anupam Das. 2021. Gentzen’s sequent calculus and Hauptsatz: the cut-elimination theorem. For Midlands Graduate School 2021: Introduction to Proof Theory.