Back to Search
Start Over
Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem
- Source :
- Notre Dame J. Formal Logic 59, no. 1 (2018), 75-90
- Publication Year :
- 2018
- Publisher :
- Duke University Press, 2018.
-
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.
- Subjects :
- Logic
Cut-elimination theorem
Proof of impossibility
direct proof
Original proof of Gödel's completeness theorem
01 natural sciences
Combinatorics
Steiner–Lehmus theorem
absolute geometry
Computer Science::Logic in Computer Science
Direct proof
Structural proof theory
0101 mathematics
Mathematics
Discrete mathematics
Proof complexity
indirect proof
010102 general mathematics
03F07
010101 applied mathematics
Mathematics::Logic
sequent calculus
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
51F05
03B30
Analytic proof
Subjects
Details
- ISSN :
- 00294527
- Volume :
- 59
- Database :
- OpenAIRE
- Journal :
- Notre Dame Journal of Formal Logic
- Accession number :
- edsair.doi.dedup.....ff92e6e0516af72c4530d8054e0374a1