What language are axioms expressed in?

Question

We can form axioms of Boolean algebra or Set theory by forming some expression like:

$a=f(a,b,c,d)$

Which are sort of replacement rules on expression trees. Now people say arithmetic is built on the axioms set theory. But it must also be built on the language that expresses the axioms in the first place.

But this language can express many axioms. Thus it must be able to express axioms that are not part of mathematics.

A program like Coq or Isabelle Proof Assistant is built on a language that allows one to express axioms.

Why isn't this language itself called "mathematics"? And allow any axioms whatsoever? i.e. "Under axiom system A, prove C".

If the language that axioms can be written in is not called "mathematics". What is it called?

Answer 1

I'll first give a very short overview of the language of "First-order logic" (FOL) to make sure we're on the same page about what "language" means, and then give a more specific reply to your questions.

---

A logical language usually consists of the following logical symbols:

• Logical constants $\top$ (truth) and $\bot$ (falsehood)
• Logical operators $\land$ (and), $\lor$ (or), $\lnot$ (not), $\to$ (implies), $\forall$ (for all) and $\exists$ (there exists)
• A countable set of variables $x,y,z,\dots$
• Brackets $($ and $)$
• The equality operator $=$

Furthermore we extend this logical language with mathematical symbols denoting, depending on what we wish to express:

• Constants
• Functions
• Relatons

We usually write only the mathematical symbols when describing the language. For example:

• $\mathsf{ZFC}$ uses the language $\{\in\}$, with no constants and functions, and one binary relation $\in$;
• Peano arithmetic uses the language $\{0,S\}$ with constant $0$ and unary function $S$;
• the theory of groups uses $\{e,+,-\}$ with constant $e$, binary function $+$ and unary function $-$.

Axioms are then written as sentences of FOL. To determine what constitutes a sentence, there are grammatical rules that tell us what is a valid sentence. We do this by recursion, which you can find in any resource describing FOL. A collection of axioms is called a theory.

For example, the axioms of the theory of groups would be:

1. $\forall xyz((x+y)+z=x+(y+z))$
2. $\forall x(x+(-x)=e\land(-x)+x=e)$
3. $\forall x(x+e=x\land e+x=x)$

Now what is important, is that as far as logic is concerned, none of this has a meaning yet. The meaning arises when we interpret our mathematical symbols in a model. This is the setting where most mathematicians work in. A model is a collection of objects, in which we can interpret the mathematical symbols in such a way that the logical axioms are true (according to the rules of FOL).

For example, a model of groups would be to take the set $\mathbb N$, interpret $e$ as $0$, interpret $+$ as the usual addition operator and interpret $-$ as the function that sends $x$ to $-x$ in the usual way. Another model would be to take the set $\mathbb Q$, interpret $e$ as $1$, $+$ as multiplication and $-$ as taking the reciprocal.

Most mathematicians study these models individually, study properties that follow from these axioms directly, or study the relations between similar theories (such as the theory of Abelian groups, that also include the axiom $\forall xy(x+y=y+x)$ for commutativity). Most of the proofs in this are done informally, in the sense that they are often not done in pure first-order logic. We kind of hope that all of the reasoning can be translated into a formal argument when we would really try this.

---

Now people say arithmetic is built on the axioms set theory. But it must also be built on the language that expresses the axioms in the first place.

This would be the rules that express first-order logic. Naturally these rules live in some kind of "meta-theory" of logic, however, just as most mathematicians are not too concerned about the meta-theory of their work (i.e. FOL), most logicians are not too concerned about the meta-logic of logic. As long as we work in a finitistic setting, in particular where proofs are finite, most people don't seem to have a problem with this; we have to start with something before we can start building anything.

I should mention that there are mathematicians who disagree with FOL being the proper framework for mathematics. For instance, the constructivist / intuitionist movement has strong objections to proof by contradiction. In FOL it is a valid to start with assuming $\lnot\phi$ and then prove that this results in a contradiction, from which it follows that $\phi$ has to be true. As an alternative, we could discard this rule, and work in a logic that does not have proof by contradiction.

But this language can express many axioms. Thus it must be able to express axioms that are not part of mathematics.

Well, kind of by definition anything that can be described as a consistent theory is part of mathematics. However, we mostly study those theories that arise from an application, e.g. groups arising from the study of symmetry. We could take some collection of arbitrary axioms, and study the theory, but if we don't have a way to interpret the models as something useful and intuitive, there seems to be not a lot of reason for doing this. I would still certainly describe it as mathematics, however.

A program like Coq or Isabelle Proof Assistant is built on a language that allows one to express axioms.

Why isn't this language itself called "mathematics"? And allow any axioms whatsoever? i.e. "Under axiom system A, prove C".

The languages that proof assistants use are similar to the logical language that I described above. Proofs in these languages are based on the syntactic rules of a proof system such as the Calculus of Constructions (CoC) or Higher-Order Logic (HOL). The study of the power of these syntactic rules is generally not considered mathematics per se, but rather a field of mathematical logic. In particular the fields of type theory, proof theory and recursion theory.