Equivalence of Formulations of Pasch's Axiom
Jump to navigation
Jump to search
Theorem
The two forms of Pasch's Axiom in Tarski's Geometry are consistent.
That is, the expressions:
- $(1): \quad \forall a, b, c, p, q: \exists x: \mathsf B a p c \land \mathsf B b q c \implies \mathsf B p x b \land \mathsf B q x a$
and:
- $(2): \quad \forall a, b, c, p, q: \exists x: \mathsf B a p c \land \mathsf B q c b \implies \mathsf B a x q \land \mathsf B b p x$
are logically equivalent.
Proof
This theorem requires a proof. In particular: It is important that we identify which other axioms this equivalence is based on for foundational purposes (and possible generalisations) You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
Sources
June 1999: Alfred Tarski and Steven Givant: Tarski's System of Geometry (Bull. Symb. Log. Vol. 5, no. 2: pp. 175 – 214) : p. $196$