First Order Logic of Relations "FOLR":
Language: first order logic with Equality "$=$"(and its axioms), and Membership "$ \in $", nLinks "$\overrightarrow {x_1,..,x_n.}$" Choice "$C$", "principal" and "linking"; for each natural $n \geq 2$ there is an nLink that is a partial $n$-ary function, Choice is a total unary function; principal and linking are unary predicates.
Define: $\operatorname {individual}(X) \iff \exists Y \, \forall Z \in X \,(Z=Y) $
Axioms:
Extensionality: $ A \subset B \land B \subset A \implies A=B$
Membership: $X \in Y \implies \operatorname {individual}(X)$
Atomhood $\forall X: \operatorname {individual}(X) \implies X \in X$
So we have: $\operatorname {individual}(X) \iff X=\{X\}$
Innocence: $\forall X \exists Y : \operatorname {individual}(Y) \land Y \in X$
Simplicity: $l=\overrightarrow {X1,..,Xn} \implies l,X_1,..,X_n \text { are individuals}$
Directionality: $\overrightarrow {x_1,..,x_n} = \overrightarrow {y_1,..,y_n} \implies x_1=y_1 \, \land \, .. \, \land \, x_n=y_n$
Existence: $\exists X: \operatorname {principal}(X)$
Links: $\forall \operatorname {principal} x_1,..,x_n \exists l: \overrightarrow {x_1,..,x_n}=l$
Linked: $ l=\overrightarrow {x_1,..,x_n} \implies x_1,..,x_n \text { are principal}$
Define: $_n \! \operatorname {linking} (l) \iff \exists x_1,..,x_n : l=\overrightarrow {x_1,..,x_n}$
Subspecies: $ _n \! \operatorname {linking}(l) \implies \operatorname {linking} (l)$
Dichotomy: $\operatorname {individual} (X) \iff \operatorname {principal} (X) \veebar \operatorname {linking}(X)$
Arity: $n=2,3,4,...; m=2,3,4,...; n \neq m \\ _n \! \operatorname {linking}(l) \land \, _m \! \operatorname {linking}(k) \implies l \neq k$
Comprehension: if $\phi$ is a formula in which $X$ is not free, then: $$\exists Y \, ( Y=\{Y\} \land \phi) \implies \\ \exists X \forall Y (Y \in X \iff Y=\{Y\} \land \phi)$$
The class of all principal individuals shall be denoted by $D$ (standing for Domain).
Choice: $C(X) \in X$
Linking ($\omega$-rule):
$\underline {[_{n=2,3,...} \forall l: \, _n \! \operatorname {linking}(l) \implies \phi(l)]} \\ \forall \operatorname { linking } l: \phi(l)$
The idea is for the above to be considered as background first order logic of relations, so the above primitives and axioms to be called as the logical axioms of relations, so any theory that extends it we take its domain to be $D$ and each of its primitives to be subsets of $D$ and subsets of $D^n$, and similarly defined predicates and functions to be coind as subsets of $D$ or $D^n$, the axioms stipulating totality x partiality of the n-ary relations and functions in their signature are to be considered as logical as well since its primarily connected to the language of the theory, those are generally considered to be total over $D$ for $n \geq 2$ for predicates, and $n \geq 1$ for functions, if not then they need to be explicitly specified as partial in the logical preample of the theory. Choice may be withdrawn if the exending theory is to violate Choice.
This shortens greatly the presentation of the axioms of an extending theory. For example a theory about arithmetic would be presented as:
Theory: Arithmetic
Logic: $\sf FOLR$
Signature: $\sigma = (S)$; $S$ is unary fuction.
Axioms:
- Succession: $ \forall n \in X \, (S(n) \in X) \implies \\\exists! m \in X: \not \exists n \in X (m=S(n))$
In English: every sucessor chain has a unique start.
So only one axiom is needed, since this is the only one that is not a part of the first order logic of relations or the totality stipulation of $S$. However, I think this theory is stronger than PA since it proves existence of sets of naturals, and so I think its equivalent to second order arithmetic.
- Had FOLR been pondered before? Reference?
- Is FOLR complete?