Negation-free and contradiction-free proof of the Steiner-Lehmus theorem

DOI10.1215/00294527-2017-0019zbMath1455.03076OpenAlexW2752004485MaRDI QIDQ1704083

Victor V. Pambuccian

Publication date: 8 March 2018

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.ndjfl/1504252824

zbMATH Keywords

sequent calculusSteiner-Lehmus theoremabsolute geometrydirect proofindirect proof

Mathematics Subject Classification ID

Structure of proofs (03F07) Foundations of classical theories (including reverse mathematics) (03B30) Absolute planes in metric geometry (51F05)

Related Items (4)

A theory of duality in Euclidean geometry ⋮ A direct proof of the Steiner-Lehmus theorem ⋮ Is there a direct geometric proof of the Steiner-Lehmus theorem? ⋮ Prolegomena to any theory of proof simplicity

Uses Software

• Pesca

Cites Work

• The Steiner-Lehmus theorem and ``triangles with congruent medians are isosceles hold in weak geometries
• A constructive version of Tarski's geometry
• Ebenen mit Kongruenz
• A common axiom set for classical and intuitionistic plane geometry
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• Orthogonality as single primitive notion for metric planes
• Proof Analysis
• Cut Elimination in the Presence of Axioms
• Propositions in Prepositional Logic Provable Only by Indirect Proofs
• Other Versions of the Steiner-Lehmus Theorem
• An Intuitionistic Axiomatisation of Real Closed Fields
• Some topologic-geometrical properties of external bisectors of a triangle
• A further simplification of Tarski's axioms of geometry
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Negation-free and contradiction-free proof of the Steiner-Lehmus theorem