Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


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 languageEnglish (US)
Pages (from-to)75-90
Number of pages16
JournalNotre Dame Journal of Formal Logic
Issue number1
StatePublished - 2018


  • Absolute geometry
  • Direct proof
  • Indirect proof
  • Sequent calculus
  • Steiner–Lehmus theorem

ASJC Scopus subject areas

  • Logic


Dive into the research topics of 'Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem'. Together they form a unique fingerprint.

Cite this