Definition:Tarski's Axioms

From ProofWiki
Jump to: navigation, search

Definition

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.


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':$
$\left({\neg \left({a = b}\right) \land \left({\mathsf B a b c \land \mathsf B a' b' c'}\right) \land \left({a b \equiv a' b' \land b c \equiv b' c' \land a d \equiv a' d' \land b d \equiv b' d'}\right)}\right)$
$\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.


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

$\exists a, b, c, p_1, \cdots, p_{n-1}: \left({\displaystyle \bigwedge_{1 \mathop \le i \mathop < j \mathop < n} \neg \left({p_i = p_j}\right) \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}\right)$
$\land \left({\neg \mathsf B abc \land \neg \mathsf B bca \land \neg \mathsf B cab}\right)$

where:

$a, b, c, p_i$ are points
$\displaystyle \bigwedge$ denotes the general conjunction operator.


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

$\forall a, b, c, p_1, \cdots, p_{n}: \left({\displaystyle \bigwedge_{1 \mathop \le i \mathop < j \mathop \le n} \neg \left({p_i = p_j}\right) \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}\right)$
$\implies \left({\mathsf B abc \lor \mathsf B bca \lor \mathsf B cab}\right)$

where:

$a, b, c, p_i$ are points
$\displaystyle \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 Schema $11$: Axiom Schema of Continuity

Axiom:Schema Axiom of Continuity

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 \left({b = c}\right) \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:$
$\left({\neg \left({a=b}\right) \land ac \equiv ac' \land bc \equiv bc' \land \mathsf{B} bdc' \land \left({\mathsf{B} adc \lor \mathsf{B} acd }\right)}\right)$
$\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.



Source of Name

This entry was named for Alfred Tarski.


Sources