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

Victor Pambuccian

Research output: Contribution to journal › Article

2 Citations (Scopus)

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

Fingerprint

Sequent Calculus
Classical Logic
Quantifiers
Axioms
Partial
Theorem

Keywords

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

ASJC Scopus subject areas

  • Logic

Cite this

Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem. / Pambuccian, Victor.

In: Notre Dame Journal of Formal Logic, Vol. 59, No. 1, 01.01.2018, p. 75-90.

Research output: Contribution to journal › Article

Pambuccian, V 2018, 'Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem', Notre Dame Journal of Formal Logic, vol. 59, no. 1, pp. 75-90. https://doi.org/10.1215/00294527-2017-0019
Pambuccian V. Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem. Notre Dame Journal of Formal Logic. 2018 Jan 1;59(1):75-90. https://doi.org/10.1215/00294527-2017-0019
Pambuccian, Victor. / Negation-Free and Contradiction-Free Proof of the Steiner–Lehmus Theorem. In: Notre Dame Journal of Formal Logic. 2018 ; Vol. 59, No. 1. pp. 75-90.
@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 = "1",
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 -

Access to Document