Define a model for $\mathbb N$ without set theory

Question

I've been looking around for a long time about how to found mathematics on a solid base. This led me to a long and painful journey of avoiding circular loops.

It led me to do a bit of elementary logic and learning what are first-order formal systems, second-order logic, third-order logic, and so on. The notion of a predicate and so on. When that was done, I started having a look at ZF and ZFC, and realized that defining the set $\Bbb{N} $ correctly seemed highly non-trivial.

An issue that I have is that the axiom schemas of set theory (such as the axiom schema of Specification or Replacement) use natural numbers in them to admit an arbitrary number of finitely many logical variables in the formula defining the various sets involved. This pre-supposes that there should be a model where natural numbers are defined so that they can be used to construct this theory.

So for me, this meant that there should be a model of the natural numbers that doesn't use set theory, otherwise the axioms of set theory cannot be properly laid down.

Under what theory would such a model be built? The Peano axioms use strongly the notion of a "successor function", which seems to assume the notion of a set already.

Answer 1

The Question

Here is a rewriting of what I think your main question is, and it's what I'll try to address directly. If I've missed something, just let me know:

I would like to know how formal mathematics can be built-up from first principles without seeming circular. For example, Wikipedia's outline of the Peano axioms for the natural numbers mentions a successor "function", which would seem to require set theory (to define the meaning of "function"). But Wikipedia's statement of the axiom schema of specification involves notation like $\forall w_1,\ldots,w_n$, and the use of the index $n$ would seem to require already having the naturals.

Too-specific Answer

For the specific concerns you mentioned, I think the Wikipedia pages are just a little misleading because of their goal of being accessible, and the preferences of various authors.

It's true that the Peano page links the general function page, and functions are usually defined in terms of sets (at least having a set as a domain). But the word "function" is overloaded, and in Logic it has a meaning separate from set theory. The key phrase on the Peano page is "The non-logical symbols for the axioms consist of a constant symbol $0$ and a unary function symbol $S$.". Briefly, in logic, a function (symbol) is something that acts syntactically like a function; for more details, see the non-logical symbols section of the page on First-order logic(s).

In many books, the axiom/theorem schema of specification is not written with subscripts like on Wikipedia. For example,

• Introduction to Axiomatic Set Theory by Takeuti and Zaring has "$(\forall a)(\exists b)(\forall x)[x\in b\leftrightarrow x\in a\land\varphi(x)]$"
• Metamath Proof Explorer has (thanks to Norm Megill) "$\vdash\exists y\forall x(x\in y\leftrightarrow(x\in z\land \varphi)$"
• Set Theory: An Introduction to Independence Proofs by Kunen has "For each formula $\phi$ without $y$ free, the universal closure of the following is an axiom: $\exists y\,\forall x(x\in y\leftrightarrow(x\in z\land \phi)$.".

More-important General Answer

No matter how we set up formal mathematics, whether or not we use some form of bootstrapping, we'll have to rely on something informal at the bottom of things. For example, a standard logic treatment might take the concept of "strings of symbols" for granted. Or maybe we could define "strings of symbols" in terms of some formal construction of the natural numbers, but then we need some other informal concept to set up those natural numbers.

A key general idea is that of a "metalanguage" that we use to talk about some particular formal logic/language. I don't know the best source, but you can read about it at these philosophy notes and how it can be a formal language at this MSE question. For example, when we use a word like "finite" or "natural number", you could be using their everyday English sense ("'abc' has finite length" or "$w_1,\ldots,w_n$ is a finite bunch of variables"), or as shorthand for logical formulas (about sets, say). As long as we're clear when we do which, there's no real problem.

---

Side Comment

all those results in logic come from first using "meta-logic" to build set theory, use that to build formal logic and then deduce the logic results within set theory?

We don't need set theory to build a logical system (syntactically). We could just describe the axioms and the allowed rules for writing a proof to go from axioms/theorems to new theorems. (If you have questions about a particular source's treatment of how this is done, that could be a good separate question on MSE.)

But if you want to give semantics to a first-order logic system, the most common approach is to assume you have some version of set theory in your pocket (in the meta-language?), and then use a set as a model (this is described a bit here on the wikipedia page for model theory).

For example, if we say the axioms of the first-order theory of groups are something like:

• $\forall x, e*x=x\land x*e=x$
• $\forall x, x^{-1}*x=e\land x*x^{-1}=e$
• $\forall x, \forall y, \forall z, (x*y)*z=x*(y*z)$

Then a model could be some set $G$ with a distinguished element to take the role of $e$, a function (in the sense of sets) $G\to G$ to take the role of $\cdot^{-1}$, and a function $(G\times G)\to G$ to take the role of $*$.