Two types of axiomatic theories in mathematics

Question

Apart from the notion of formal theory, which formalises the idea of axiomatic system in first order logic, in mathematics people also consider another type of axiomatic systems, which can be described as extensions by definitions of the axiomatic set theory that a mathematician uses in his work. The examples of such systems are

• axioms of general topology,

• axioms of probability theory,

• Hilbert's axioms of geometry,

etc. As far as I know these are not formal theories in first order logic, although, of course they can be presented as such theories, since they are extensions by definitions of ZFC; I think however that this will be too bulky, so I believe, there must be another notion of axiomatic theory in mathematics, which covers the theories from my list.

Is that true? Can anybody enlighten me if the second kind of axiomatic systems has a formal definition (different from the phrase "extension by definitions of ZFC", so that this indeed clarifies the picture)? Or, in other words,

is there a common scheme that describes the axiomatic systems of second type and explains the differences between them and the formal theories in first order logic?

For some time I thought that these are just axiomatic theories in second order logic, but now I got some doubts, and I would prefer to use first order language for describing the differences (I believe, this is possible).

Answer 1

Generally mathematicians when doing mathematics (like topology, probability or geometry) do that in the framework of set theory.

This means that they introduce some definitions (topology, $\sigma$-algebras, points etc) in terms of sets and provide proofs of facts about these objects using properties of sets.

Formally what mathematicians do is take ZFC theory add new symbols to the language (for instance predicates like "is a topology", "is a topological space", "is a continuous function" and so on) and then axiomatically define these predicates in terms of formulas in the language of ZFC, that is they add some axioms of the form $$x \text{ is a topology} \iff \varphi(x)$$ $$x \text{ is a topological space} \iff \varphi'(x)$$ $$\dots$$ where the formulas $\varphi(x)$, $\varphi'(x)$ etc are ZFC formulas.

In this way they can reduce any proof about the new introduced objects (toplogical spaces, geometric figures etc) to a proof about sets, that is a proof that ultimately relies on the axioms of ZFC+the definitional axioms for the new predicates.

On the other hand in principle one could try to look at the formal systems you listed as some logical systems on their own.

For instance Hilber's system for euclidean geometry can be easily seen as a first-order theory, as it is basically shown in the wikipedia link you gave.

The other systems you listed could be seen as formal systems for an higher-order logic, but you have to go at least third order because in these systems you would need to quantify over families of subsets (that is over families of predicates, or predicates of predicates).

If you like I could add the details, at least for one of the systems. Let me know if you need any additional clarification.

Hope this helps.

Answer 2

EDIT: Based on the comments, I think this more accurately answers the OP's question:

The axioms for rings are actually first-order - and we say they constitute a first-order theory! Basically, I can write down the ring axioms as first-order sentences in the language $\{+, \times,0, 1\}$, and then rings are the same as models of this set of axioms. These models, of course, are sets, and so we can only talk about them directly in general inside a theory of sets; but the set of axioms itself is first-order. (And note that we can still talk about the theory of rings, and deductions from that theory, in a theory without sets like PA.)

The same is true for groups, fields, etc. The same is also essentially true, incidentally, for "weak topological spaces" (I don't know what these are actually called): say a weak topological space is a set $X$ together with a family $\tau$ of subsets of $X$ containing $X$ and $\emptyset$ and closed under finite unions and finite intersections. Then consider the language $\{E, P, S\}$, with a single binary relation $E$ and two unary relations $P, S$. Intuitively, $P$ refers to points, $S$ refers to sets (of points), and $E$ refers to membership. Now consider the following set of first-order sentences:

• $\forall x((P(x)\vee S(x))\wedge\neg(P(x)\wedge S(x)))$. The only things in our structure are points or sets, and these are disjoint from each other.

• $\forall x, y(E(x, y)\implies P(x), S(y))$. Membership is a relation between points and sets, only.

• $\forall x, y(S(x), S(y), \forall z(E(z, x)\iff E(z, y))\implies x=y)$. Sets with the same elements are the same.

• $\forall x, y(S(x), S(y)\implies \exists z(S(z)\wedge\forall w(E(w, z)\iff E(w, x)\wedge E(w, y)))).$ Intersection of two sets (hence finitely many sets is a set.

• $\forall x, y(S(x), S(y)\implies \exists z(S(z)\wedge\forall w(E(w, z)\iff E(w, x)\vee E(w, y)))).$ Finite unions.

A model of these axioms isn't necessarily literally a weak topological space - the $S$-elements might not actually be sets of $P$-elements - but they can be canonically identified with weak topological spaces: given a model $\mathcal{M}=(M; P^M, S^M, E^M)$, we can assign it a weak topological space $T_\mathcal{M}$ with underlying set $\{m\in M: \mathcal{M}\models P^M\}$ and "open sets" exactly those of the form $\{m\in M: \mathcal{M}\models E(m, s)\}$ for some $s\in\{m\in M: \mathcal{M}\models S(m)\}$. Conversely, each weak topological space can be viewed as a model of the theory above in the obvious way. So we have a dichotomy:

• Literally being a weak topological space isn't the same as satisfying some set of first-order axioms (whereas being a ring is the same as being a structure which satisfies the set of first-order ring axioms), but

• There is a set of first-order axioms, the class of whose models is equivalent to the class of weak topological spaces in a precise sense (there is a definable function between the two classes which is appropriately surjective and injective-up-to-isomorphism).

Finally, full topological spaces aren't even morally first-order: this is because of the infinite unions bit, which is fundamentally second-order. Instead, there is a set of second-order sentences such that the topological spaces are appropriately equivalent to the models of this set of sentences. Note, however, that in order to talk about satisfaction of second-order sentences we need to work in a more set-theoretic context than if we just care about satisfaction of first-order sentences, and set-theoretic issues are more relevant: for example, (your favorite set theory proves that) there is a second-order sentence which is true in every structure iff the continuum hypothesis holds!

---

EDIT: The key idea below is that definitions in an extension by definitions are essentially definitions in the original language already. Specifically, you can easily write a computer program that will convert a formula in a extension-by-definitions $L'$ of $L$ into a corresponding formula in $L$. So really, this all boils down to why the language of set theory has enough expansions-by-definitions, and this is provided pretty quickly by playing with the language (e.g. discover how to express "function," "sequence," "relation," "Cartesian product").

---

I'll do two examples (topological spaces and groups), and hopefully this will indicate why this stuff isn't usually done explicitly - it's very straightforward and quite tedious.

Topological spaces.

Usual definition: A topological space is an ordered pair $(X, \tau)$ where $X$ is a set, $\tau$ is a set of subsets of $X$, and $\tau$ is closed under finite intersections, arbitrary unions, and contains $X$ and $\emptyset$.

Formal definition in the language of set theory: $\varphi(x)$ is the formula, in the language of set theory, expressing:

• $\exists a, b[x=\langle a, b\rangle$ and

  • $b\subseteq\mathcal{P}(a)$;

  • $\forall s\subseteq b\exists c\in b(c=\bigcup s)$;

  • $\forall s\subseteq_{finite} b\exists c\in b\forall y(y\in c\iff \forall z(z\in s\implies y\in z))$;

  • $a\in b, \emptyset\in b$].

I've used symbols not explicitly in the language of set theory above - namely, $\langle\cdot,\cdot \rangle$, $\subseteq$, $\bigcup$, $\subseteq_{finite}$, $\emptyset$. But it's an easy exercise to get rid of these, and get a formula using only "$\in$." But given that the translation is completely straightforward, I'm not sure what value this provides.

Groups.

Usual definition: A set with a binary operation satisfying [stuff].

Formal definition in the language of set theory: $\psi(x)$ is the formula, in the language of set theory, expressing:

• $\exists a, b[x=\langle a, b\rangle$ and

  • $b$ is a binary function on $a$

  • [stuff].

Remember that functions, and Cartesian products, are elementary to define in the language of set theory; and so everything here is easy to write down.

---

One of the values of set theory is that concepts in mathematics translate without effort into the language of set theory. That said, they also translate tediously, so an argument can be made that we should use something other than ZFC; but this is why you don't see these kinds of definitions written out in full.