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

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

  • $\begingroup$ "these are not formal theories in first order logic." If the axiom ssytem (like e.g.that of probability theory) is "written" in the language of $\mathsf {ZF}$ set thoery (or similar) it is first-order. $\endgroup$ – Mauro ALLEGRANZA Jun 15 '17 at 9:19
  • $\begingroup$ What define univocally "to be first-order" or not is the language: if quantification is allowed only on individual variables, then it is FO. $\mathsf {ZF(C)}$ as well as $\mathsf {NBG}$ are FO. $\endgroup$ – Mauro ALLEGRANZA Jun 15 '17 at 9:20
  • $\begingroup$ Hilbert's axioms system is Second-Order: see "Axiom of completeness. To a system of points, straight lines, and planes, ..." there is a (universal) quantification on "system of points". $\endgroup$ – Mauro ALLEGRANZA Jun 15 '17 at 9:22
  • $\begingroup$ See Tarski's axioms (1959) for a system of axioms for elementary geometry that is formulated in first-order logic with identity, and requiring no set theory. $\endgroup$ – Mauro ALLEGRANZA Jun 15 '17 at 9:24
  • $\begingroup$ Mauro, I know about Tarski, and I also (like you) think that it is possible to somehow translate everything into a first order language, but before this is done the picture looks differently (and besides this I don't believe that this translation will always be easy). So I wonder if this construction has a reasonable description inside set theory. $\endgroup$ – Sergei Akbarov Jun 15 '17 at 9:26

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:

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.


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.

| cite | improve this answer | |
  • $\begingroup$ Noah, so your point is that there is no simpler definition of these ""non-1-order-logic-axiomatic-theories", than "extensions by definitions", right? $\endgroup$ – Sergei Akbarov Jun 15 '17 at 16:16
  • 1
    $\begingroup$ @SergeiAkbarov Well, these are first-order definitions; the point is that any definition of whatever order can be converted to a first-order definition in the language of set theory. The axioms of set theory, then, try to govern the behavior of these definitions appropriately. For instance, every commutative ring that's not a field has a nontrivial proper ideal - so our axioms of set theory should be able to prove that, about those objects satisfying the "is-a-ring" formula. This is one of the senses, by the way, in which ZFC is a foundation for mathematics: (cont'd) $\endgroup$ – Noah Schweber Jun 15 '17 at 16:28
  • $\begingroup$ It gives us a precise and straightforward way to "embed" normal math into a fixed axiomatic framework. Incidentally, there are subtleties in this approach. Classical version: assuming ZFC is consistent, we will have models $M\subseteq N$ such that $N$ thinks $M$ is transitive but there is some set $r\in M$ such that $M$ thinks $r$ is a topological space (that is, $M\models\varphi_{top}(r)$) but $N$ doesn't - this is because $N$ will have an infinite family of sets in the topology which $M$ doesn't, so $M$ doesn't "see" the missing union. (cont'd) $\endgroup$ – Noah Schweber Jun 15 '17 at 16:31
  • $\begingroup$ Formal version: "ZFC (or your favorite theory $T$) proves that [...]." Of course, you have to verify that this is true, and if you pick a bad choice of $T$ it won't be, but this isn't hard as long as you pick a reasonable $T$, and it's very easy in set theory. By contrast, it's a fun exercise to show that if $M\subseteq N$ are models of ZFC such that $N$ thinks $M$ is transitive, then anything $M$ thinks is a ring, $N$ also thinks is a ring! This is because the ring axioms are really first-order, with second-order parameters (the operations); unlike the arbitrary union axiom in topology. $\endgroup$ – Noah Schweber Jun 15 '17 at 16:32
  • $\begingroup$ Noah, I am afraid, we again don't understand each other. I know that the theories I listed here are extensions by definitions of ZFC, and that each extension by definitions of ZFC can be expressed in the 1st order language of ZFC (and can be presented as a formal theory in 1st order language). My question is another: do people use any other definitions of axiomatic theories, which can be applied to the theories in my list, and which are different from the wordings "formal theory" and "extension by definitions of a formal theory"? $\endgroup$ – Sergei Akbarov Jun 15 '17 at 17:04

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.

| cite | improve this answer | |
  • 1
    $\begingroup$ Giorgio, what you say Kenneth Kunen calls "extensions by definitions": books.google.ru/books/about/… (II.15). I acutally had a hope that there is a text where this kind of axiomatic theories are defned and compared with the formal theories in first order logic. And I thought this could be explained more or less simply, in the usual language of set theory. $\endgroup$ – Sergei Akbarov Jun 15 '17 at 15:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.