@article{bf76f22d0e4e4b43a6cbd4fcf08926f2,
title = "Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem",
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.",
keywords = "Absolute geometry, Direct proof, Indirect proof, Sequent calculus, Steiner–Lehmus theorem",
author = "Victor Pambuccian",
note = "Funding Information: This paper was written at the Centro di Ricerca Matematica Ennio De Giorgi, Collegio Puteano, Scuola Normale Superiore di Pisa, while the author was supported by an SRCA grant from ASU—West campus. The results were first presented at the PhilMath Inter-sem 4, on June 27, 2013. Its actual form has greatly benefited from the criticism of an anonymous referee, from the criticism and corrections of Michael Beeson, and from a suggestion of Thomas Strahm. Funding Information: This paper was written at the Centro di Ricerca Matematica Ennio De Giorgi, Collegio Puteano, Scuola Normale Superiore di Pisa, while the author was supported by an SRCA grant from ASU?West campus. The results were first presented at the PhilMath Inter-sem 4, on June 27, 2013. Its actual form has greatly benefited from the criticism of an anonymous referee, from the criticism and corrections of Michael Beeson, and from a suggestion of Thomas Strahm. Publisher Copyright: {\textcopyright} 2018 by University of Notre Dame.",
year = "2018",
doi = "10.1215/00294527-2017-0019",
language = "English (US)",
volume = "59",
pages = "75--90",
journal = "Notre Dame Journal of Formal Logic",
issn = "0029-4527",
publisher = "Duke University Press",
number = "1",
}