Axiom:Tarski's Axioms

Axioms

Tarski's Axioms are a series of axioms whose purpose is to provide a rigorous basis for the definition of Euclidean geometry entirely within the framework of first order logic.

In the following:

$\equiv$ denotes the relation of equidistance.

$\mathsf{B}$ denotes the relation of betweenness.

$=$ denotes the relation of equality.

The axioms are as follows:

Axiom $1$: Reflexivity Axiom for Equidistance

$\forall a,b: ab \equiv ba$

where $a$ and $b$ are points.

This article, or a section of it, needs explaining. In particular: Why is it referred to as reflexivity but defined as symmetry? You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. 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 {{Explain}} from the code.

Axiom $2$: Transitivity Axiom for Equidistance

$\forall a,b,p,q,r,s: \left({ab \equiv pq \land ab \equiv rs}\right) \implies pq \equiv rs$

where $a, b, p, q, r, s$ are points.

Axiom $3$: Identity Axiom for Equidistance

$\forall a, b, c: ab \equiv cc \implies a = b$

where $a, b, c$ are points.

Axiom $4$: Axiom of Segment Construction

$\forall a, b, c, q: \exists x: \mathsf{B} qax \land ax \equiv bc$

where $a, b, c, q, x$ are points.

Axiom $5$: Five-Segment Axiom

$\forall a, b, c, d, a', b', c', d':$

$\paren {\neg \paren {a = b} \land \paren {\mathsf B a b c \land \mathsf B a' b' c'} \land \paren {a b \equiv a' b' \land b c \equiv b' c' \land a d \equiv a' d' \land b d \equiv b' d'} }$

$\implies c d \equiv c' d'$

where $a, b, c, d, a', b', c', d'$ are points.

Axiom $6$: Identity Axiom for Betweenness

$\forall a,b: \mathsf{B}aba \implies a = b$

where $a$ and $b$ are points.

Axiom $7$: Pasch Axiom

$\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$

where $a, b, c, p, q, x$ are points.

Work In Progress In particular: Separate out Inner and Outer Forms of Pasch Axiom and link to them both You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. 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 {{WIP}} from the code.

Axioms $8^{(0)}, 8^{(1)}, \ldots, 8^{(n)}$: Lower $n$-Dimensional Axioms

$\exists a, b, c, p_1, \cdots, p_{n - 1}: \paren {\ds \bigwedge_{1 \mathop \le i \mathop < j \mathop < n} \map \neg {p_i = p_j} \land \bigwedge_{i \mathop = 2}^{n - 1} a p_1 \equiv a p_i \land \bigwedge_{i \mathop = 2}^{n - 1} b p_1 \equiv b p_i \land \bigwedge_{i \mathop = 2}^{n - 1} c p_1 \equiv c p_i}$

$\land \paren {\neg \mathsf B abc \land \neg \mathsf B bca \land \neg \mathsf B cab}$

where:

$a, b, c, p_i$ are points

$\ds \bigwedge$ denotes the general conjunction operator.

Axioms $9^{(0)}, 9^{(1)}, \ldots, 9^{(n)}$: Upper $n$-Dimensional Axioms

$\ds \forall a, b, c, p_1, \cdots, p_n: \paren {\bigwedge_{1 \mathop \le i \mathop < j \mathop \le n} \map \neg {p_i = p_j} \land \bigwedge_{i \mathop = 2}^n a p_1 \equiv a p_i \land \bigwedge_{i \mathop = 2}^n b p_1 \equiv b p_i \land \bigwedge_{i \mathop = 2}^n c p_1 \equiv cp_i}$

$\implies \paren {\mathsf B abc \lor \mathsf B bca \lor \mathsf B cab}$

where:

$a, b, c, p_i$ are points

$\ds \bigwedge$ denotes the general conjunction operator.

Axiom $10$: Euclid's Axiom

$\forall a, b, c, d, t: \exists x, y:$

$\left({\mathsf{B}adt \land \mathsf{B}bdc \land \neg (a = d)}\right) \implies \left({\mathsf{B}abx \land \mathsf{B}acy \land \mathsf{B}xty}\right)$

where $a, b, c, d, t, x, y$ are points.

Axiom $11$: Axiom of Continuity

$\left({\exists a : \forall x,y : \left({x \in X \land y \in Y}\right)\implies \mathsf{B}axy}\right) \implies \left({\exists b : \forall x,y : \left({x \in X \land y \in Y}\right)\implies \mathsf{B}xby}\right)$

where $a,b,x,y$ are points and $X, Y$ are point sets.

Axiom $12$: Reflexivity Axiom for Betweenness

$\forall a, b: \mathsf{B}abb$

where $a$ and $b$ are points.

Axiom $13$ (unnamed)

$\forall a,b: a = b \implies \mathsf{B}aba $

where $a$ and $b$ are points.

Axiom $14$: Symmetry Axiom for Betweenness

$\forall a, b, c: \mathsf{B}abc \implies \mathsf{B}cba$

where $a, b, c$ are points.

Axiom $15$: Inner Transitivity Axiom for Betweenness

$\forall a, b, c, d: \mathsf{B}abd \land \mathsf{B}bcd \implies \mathsf{B}abc$

where $a, b, c, d$ are points.

Axiom $16$: Outer Transitivity Axiom for Betweenness

$\forall a, b, c, d: \mathsf{B}abc \land \mathsf{B}bcd \land \neg \paren {b = c} \implies \mathsf{B}abd$

where $a, b, c, d$ are points.

Axiom $17$: Inner Connectivity Axiom for Betweenness

$\forall a,b,c,d: \left({\mathsf{B}abd \land \mathsf{B}acd}\right) \implies \left({\mathsf{B}abc \lor \mathsf{B}acb}\right)$

where $a, b, c, d$ are points.

Axiom $18$: Outer Connectivity Axiom for Betweenness

$\forall a, b, c, d: \left({\mathsf{B}abc \land \mathsf{B}abd \land \neg \left({a = b}\right) }\right) \implies \left({\mathsf{B}acd \lor \mathsf{B}adc}\right)$

where $a, b, c, d$ are points.

Axiom $19$ (unnamed)

$\forall a, b, c: a = b \implies ac \equiv bc$

where $a, b, c$ are points.

Axiom $20$: Uniqueness Axiom for Triangle Construction

$\forall a, b, c, c', d:$

$\paren {\neg \paren {a = b} \land ac \equiv ac' \land bc \equiv bc' \land \mathsf{B} bdc' \land \paren {\mathsf{B} adc \lor \mathsf{B} acd } }$

$\implies c = c'$

where $a, b, c, c', d$ are points.

Axiom $21$: Existence Axiom for Triangle Construction

$\forall a,a',b,b',c',p: ab \equiv a'b' \implies$

$\exists c,x: \left({ac \equiv a'c' \land bc \equiv b'c' \land \mathsf{B}cxp}\right) \land \left({\mathsf{B}abx \lor \mathsf{B}bxa \lor \mathsf{B}xab}\right)$

where $a, b, c, a', b', c', x, p$ are points.

Axiom $22$: Density Axiom for Betweenness

$\forall a, b: \exists c: \neg \left({a = b}\right) \implies \neg \left({c = a}\right)\land \neg \left({c = b}\right) \land \mathsf{B}acb$

where $a, b, c$ are points.

Axiom $23$ (unnamed)

$\forall x,y,z,x',y',z' : \left({\mathsf{B}xyz \land \mathsf{B}x'y'z' \land xy \equiv x'y' \land yz \equiv y'z'}\right) \implies xz \equiv x'z'$

where $x, y, z, x', y', z'$ are points.

This article is incomplete. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by expanding it. 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 {{Stub}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Source of Name

This entry was named for Alfred Tarski.

Sources

• June 1999: Alfred Tarski and Steven Givant: Tarski's System of Geometry (Bull. Symb. Log. Vol. 5, no. 2: pp. 175 – 214)