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

Research output: Contribution to journalArticle

2 Scopus citations

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

Keywords

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

ASJC Scopus subject areas

  • Logic

Fingerprint 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