Abstract
By rephrasing quantifier-free axioms as rules of derivation in sequent calculus, we show that the generalized Steiner–Lehmus theorem admits a direct proof in classical logic. This provides a partial answer to a question raised by Sylvester in 1852. We also present some comments on possible intuitionistic approaches.
Original language | English (US) |
---|---|
Pages (from-to) | 75-90 |
Number of pages | 16 |
Journal | Notre Dame Journal of Formal Logic |
Volume | 59 |
Issue number | 1 |
DOIs | |
State | Published - Jan 1 2018 |
Keywords
- Absolute geometry
- Direct proof
- Indirect proof
- Sequent calculus
- Steiner–Lehmus theorem
ASJC Scopus subject areas
- Logic