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

Notre Dame Journal of Formal Logic 59 (1):75-90 (2018)
  Copy   BIBTEX

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.

Categories

Keywords

Reprint years

DOI

10.1215/00294527-2017-0019

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,075

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Proof nets sequentialisation in multiplicative linear logic.Paolo Di Giamberardino & Claudia Faggian - 2008 - Annals of Pure and Applied Logic 155 (3):173-182.
Proof-theoretical analysis of order relations.Sara Negri, Jan von Plato & Thierry Coquand - 2004 - Archive for Mathematical Logic 43 (3):297-309.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
A Negation-free Proof of Cantor's Theorem.N. Raja - 2005 - Notre Dame Journal of Formal Logic 46 (2):231-233.
LEt ® , LR °[^( ~ )], LK and cutfree proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
${LE}^{t}{{\rightarrow}}$ , ${LR}^{\circ}{\hat{\sim}}$, {LK} and Cutfree Proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
A formalization of Sambins's normalization for GL.Edward Hermann Haeusler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
Interpolants, cut elimination and flow graphs for the propositional calculus.Alessandra Carbone - 1997 - Annals of Pure and Applied Logic 83 (3):249-299.
2-Sequent calculus: a proof theory of modalities.Andrea Masini - 1992 - Annals of Pure and Applied Logic 58 (3):229-246.

Analytics

Added to PP
2017-09-01

Downloads
20 (#769,125)

6 months
7 (#433,721)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Cut Elimination in the Presence of Axioms.Sara Negri & Jan Von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
For Oiva Ketonen's 85th birthday.Sara Negri & Jan von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
Propositions in Prepositional Logic Provable Only by Indirect Proofs.Jan Ekman - 1998 - Mathematical Logic Quarterly 44 (1):69-91.

View all 7 references / Add more references