How far can we get without a foundation, using just first-order logic?

Question

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.

1. $\forall x \in P : x \leq x$
2. $\forall x,y \in P : x \leq y, y \leq x \Rightarrow x=y$
3. $\forall x,y,z \in P : x \leq y, y \leq z \Rightarrow x \leq z$
4. $\forall x \in Q : x \leq x$
5. $\forall x,y \in Q : x \leq y, y \leq x \Rightarrow x=y$
6. $\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?

Answer 1

The original question is perhaps not very clear, but the OP's responses to comments suggest the following two remarks could be relevant:

1. Suppose I specify a set of first-order sentences $\Sigma$. I can indeed explore what follows from $\Sigma$ by using first-order reasoning, without knowing in advance whether $\Sigma$ is a consistent set. (Of course, one thing that I can discover is that for some $\varphi$, we have both $\Sigma \vdash \varphi$ and $\Sigma \vdash \neg\varphi$, so that $\Sigma$ is actually, after all, inconsistent.) To this extent, we can indeed explore the theory whose axioms are $\Sigma$ without presupposing a "foundation" (i.e. without recourse to a background theory which we can use to model the axioms).

2. OK, suppose things have gone swimmingly so far: I've deduced lots of propositions from $\Sigma$. I conjecture that some $\sigma$ also follows. But try as I might, I can't get a proof. So I lose confidence. How can I show that indeed $\Sigma \nvdash \sigma$? Well, a standard method is to come up with a model with satisfies $\Sigma$ but not $\sigma$. But now I do need some background theory in which I can do some model-building. Maybe I can find a countermodel to $\Sigma \vdash \sigma$ in some relatively tame structure (the naturals or the reals). If I need something more exotic, ZFC gives me a sort of all-purpose Lego-kit for building mathematical structures. But we'll need some source of models.

In sum: while investigating what $\Sigma$ does entail "just" requires logic, to investigate what $\Sigma$ doesn't entail we will often need to appeal to some substantive background theory (if you like, a relatively "foundational" theory).