I think its interesting to ask how far we can get without committing to any particular foundations, using just first-order logic.
For instance, we can prove theorems in this way about partially ordered sets, groups, fields etc. by just going straight from the axioms.
Okay, now suppose we have two partially ordered sets $P$ and $Q$ and an order-preserving function $f : P \rightarrow Q$. Even without any model theory, we can still reason about this configuration.
We do this by forming a new first-order theory, whose domain of discourse can be viewed as being $P \cup Q$ (or a superset thereof). Formally, our signature includes two unary predicates $P$ and $Q$, where $P(x)$ can be read '$x$ belongs to $P$' and $Q(x)$ can be read '$x$ belongs to $Q$.' More suggestively, lets write $x \in P$ and $x \in Q$ to mean $P(x)$ and $Q(x)$ respectively. We also need a unary function symbol $f$ together with the axiom
$$\forall x \in P : f(x) \in Q$$
Also, we need a relation symbol $\leq$. To express that $f$ is order-preserving, we assume:
$$\forall x,y \in P : x \leq y \Rightarrow f(x) \leq f(y)$$
Finally, we must assume that the axioms of a partially ordered set hold when relativized to $P$, and also to $Q$. This amounts to six different axioms.
- $\forall x \in P : x \leq x$
- $\forall x,y \in P : x \leq y, y \leq x \Rightarrow x=y$
- $\forall x,y,z \in P : x \leq y, y \leq z \Rightarrow x \leq z$
- $\forall x \in Q : x \leq x$
- $\forall x,y \in Q : x \leq y, y \leq x \Rightarrow x=y$
- $\forall x,y,z \in Q : x \leq y, y \leq z \Rightarrow x \leq z$
Okay, that's the setup. Using the formal system we just constructed, we can reason about the configuration $f : P \rightarrow Q,$ where $f$ is an order-preserving function and $P$ and $Q$ are partially ordered sets.
So my question is: how far can we get in this way, without committing to any particular foundations, and at what point do we hit a brick wall?