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

Victor Pambuccian

doi:10.1215/00294527-2017-0019

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

Victor Pambuccian

Research output: Contribution to journal › Article › peer-review

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 language	English (US)
Pages (from-to)	75-90
Number of pages	16
Journal	Notre Dame Journal of Formal Logic
Volume	59
Issue number	1
DOIs	https://doi.org/10.1215/00294527-2017-0019
State	Published - Jan 1 2018

Keywords

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

ASJC Scopus subject areas

Logic

Access to Document

10.1215/00294527-2017-0019

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

@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",

year = "2018",

month = jan,

day = "1",

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",

}

TY - JOUR

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

AU - Pambuccian, Victor

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

KW - Absolute geometry

KW - Direct proof

KW - Indirect proof

KW - Sequent calculus

KW - Steiner–Lehmus theorem

UR - http://www.scopus.com/inward/record.url?scp=85041095781&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85041095781&partnerID=8YFLogxK

U2 - 10.1215/00294527-2017-0019

DO - 10.1215/00294527-2017-0019

M3 - Article

AN - SCOPUS:85041095781

VL - 59

SP - 75

EP - 90

JO - Notre Dame Journal of Formal Logic

JF - Notre Dame Journal of Formal Logic

SN - 0029-4527

IS - 1

ER -