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

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?

-
Very few of the standard important results about groups, fields can be expressed, let alone proved, in the usual first-order axiomatizations of group theory/field theory. (The situation with number theory is different.) – André Nicolas Jul 18 '13 at 23:11
How can you define (order-preserving) function without any set theory (foundation)?? – Berci Jul 19 '13 at 0:18
How do you know that you are reasoning about anything without a foundation? E.g. how do you know that there exist things called partially ordered sets, groups, fields, etc. without constructing some? – Qiaochu Yuan Jul 19 '13 at 0:48
@Berci, I have edited the question to try to make it clearer. Hopefully, its better now. – goblin Jul 19 '13 at 6:01
@user: we have a different problem. With a foundations, we know that we're okay if our foundations are consistent. Without a foundations, we need to ask the question separately, for each kind of thing we want to reason about, whether the axioms describing those things are consistent. – Qiaochu Yuan Jul 19 '13 at 7:11

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).

-
Great example! How do you prove that group theory neither proves nor disproves $\forall x\forall y(x\cdot y=y\cdot x)$, without some model theoretical foundations? – Asaf Karagila Jul 19 '13 at 9:24
All purpose Lego-kit? +1. – goblin Jul 19 '13 at 9:53
Peter Smith and @AsafKaragila, out of curiosity, how strong of a foundations do we need to carry out the argument that, okay, we can write down the multiplication table for the group $S_3,$ which is a group that is not Abelian, so therefore we cannot deduce $\forall x\forall y(xy=yx)$ from the group axioms? – goblin Jul 21 '13 at 20:24
@user18921: How do you prove that group theory is consistent? If you can't prove that, how can you prove that you can't prove something from those axioms? – Asaf Karagila Jul 21 '13 at 21:36
@AsafKaragila, yes good point. Okay, but we can write out the multiplication table for the trivial group. So, we'd like to conclude the consistency of group theory. In general, if we can describe a finite model of a system of first-order axioms over a finite signature, we'd like to be able to conclude that the system of axioms is consistent. So, out of curiosity, how powerful of a foundations do we to do this? – goblin Jul 21 '13 at 23:36