Upper-Dimension and Lower-Dimension Axioms

According to the Wikipedia article on Tarski's axioms for geometry, it can be easily extended to higher dimensions by changing the upper- and lower-dimension axioms. On the other hand, it didn't include examples of those and the papers that give examples appear to be hidden behind pay walls. So I'll have to devise my own…

Upper-Dimension Axioms

The axioms produced will be in first-order predicate logic in which β(abc) means “point b is between point a and point c” and δ(abcd) means “the distance between point a and point b is equal to the distance between point c and point d.”

The first button will produce a Π40 upper-dimension axiom whose length scales linearly with the number of dimensions:

Number of dimensions:

In English, it's supposed to mean that every sphere can be put inside a n-dimensional simplex.

The next button will produce a Π10 upper-dimension axiom whose length scales quadratically with the number of dimensions:

Number of dimensions:

In English, it's supposed to mean that there is no nontrivial n+1-dimensional simplex.

I'm not sure which style is simpler.

Lower-Dimension Axioms

The lower-dimension axioms for n dimensions is simply the negation of the upper-dimension axioms for n − 1 dimensions.

The first button will produce a Σ40 upper-dimension axiom whose length scales linearly with the number of dimensions:

Number of dimensions:

In English, it's supposed to mean that there is a sphere that cannot be put inside a n−1-dimensional simplex.

The next button will produce a Σ10 upper-dimension axiom whose length scales quadratically with the number of dimensions:

Number of dimensions:

In English, it's supposed to mean that there is a nontrivial n-dimensional simplex.

Main page