Abstracts.2020.Sequent

Sequent Calculi

by Nachi

Exercises

1. Prove
   1. A → B → A
   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)