At the moment the page is very much under construction. I have just thrown together some axioms which I have been using recently with Otter. I hope this page will gradually become more comprehensive and more systematic.

I give all axioms in syntax accaptable to the Otter theorem prover. The meanings of the logical symbols should be clear. Note however that the `|' sympol is used for disjunction.

These definitions make use of an 'iota' operator. A term (iota x
Psi(x)) is read as '*the* x such that Psi(x)'.

The KR-92 paper tells us that in the context of definitions such as
that given for sum etc. the iota can be eliminated by replacing

f(x...) = (iota y (Psi(f(x...)))) with (all x... (Psi(f(x...))))

where x... stands for the sequence of variables which are the arguments
of f.

In fact this translation is too weak. One should replace the iota as
follows:

(all x... ( (y = f(x...)) <-> (Psi(y)))).

after applying this transform the Quasi-Boolean definitions become:

The following axiom links the Quasi-Boolean functions to the sort
structure of the theory:

Finally the NTPP axiom ensures that every region has an NTPP:

(all x all y (C(x,y) -> C(y,x))).

(all x C(x,x)).

(all x all y (O(x,y) <-> (exists z (P(z,x) & P(z,y))))).

**sum existence**

(all x y (exists z (all w (C(w,z) <-> (C(w,x) | C(w,y)))))).

*complement existence*

(all x ( (exists y -C(x,y)) -> (exists z ( (all w (C(w,z) <-> -NTPP(w,x))
&(all w (O(w,z) <-> -P(w,x)) ) ) )).

*product existence*

(all x y ( O(x,y) <-> (exists z (all w (P(w,z) <-> (P(w,x) &
P(w,y))))) )).

*universe existence*

(exists x (all y C(x,y)))

Replacement for NTPP axiom

(exists x exists y -(x = y)).

It can be shown that the NTPP axiom must hold unless there is only
a single region in the universe. Thus, by requiring that there are at least
two distinct regions in the universe, one ought to be able to prove the
NTPP axiom.

Another axiom which may be helpful although not officially an axiom
is the following
*non-descreteness*

(all x ( (exists y -C(x,y)) -> (exists z (C(z,x) & -O(z,x))))).

Probably this can be proved by making use of the compl definition.

A final axiom, which is almost certainly independent of the others and
encodes a basic property of infinitely divisible space is the following:
*dense nesting*

(all x y (NTPP(x,y) -> (exists z (NTPP(x,z) & NTPP(z,y))).

2) all x all y [PP(x,y) -> exists z[P(z,y) & -0(z,x)]]

3) all x all y all z [P(z,prod(x,y)) <-> [P(z,x) & P(z,y)]]

4) all x all y all z [C(z,diff(x,y)) <-> exists v [P(v,x) & -O(v,y) & C(z,v)]]

5) all x EC(x,compl(x))

6) all x compl(compl(x)) = x

7) all x all y [P(x,y) <-> all z[O(z,x) -> O(z,y)]]

8) all x all y [[PP(x,y) & Con(y)] -> EC(diff(y,x),x)]

9) all x all y all z [[C(z,y) & -C(z,x)] -> exists w [Pwy & -O(w,x) & C(z,w)]]

10) all x all y [PP(x,y) & Con(y) -> exists z [P(z,y) & EC(z,x)]]

11) all x all y all z [C(z,diff(Y,x)) <-> exists v [P(v,y) & -O(v,x) & C(z,v)]]

12) all x sum(x,compl(x)) = us

13) all x all y O(y,x) or O(x,compl(y))

14) all x all y [P(x,y) -> C(y,compl(x))]

15) all x all y [NTPP(x,y) -> O(y,compl(x))]

16) all x all y DR(x,y) <-> P(y,compl(x))]

17) all x all y [PO(x,y) -> exists z [P(z,x) & -O(z,y)]]

18) all x all y [-P(y,x) -> exists w [P(w,y) & -O(w,x)]]

18) all x all y [O(z,compl(x)) -> -P(z,x)]

- from C(z,compl(x)) <-> -NTPP(z,x) part of compl(x) defn only

- no proof the other way though