What is an axiom schema?

ZFC is not finitely axiomatizable. But it is, (and I know this is not precise yet) finitely axiom-schematizable. So my question is, what exactly is an axiom schema of a logical calculus like first order logic or propositional logic, such as ((A AND B) IMPLIES B)? Well, I guess it would be a set of statements. But what exactly makes a set of statements schematic?

Solution 1:

An axiom schema is an infinite set of axioms, all of which have a similar form.

For example, in Peano Arithmetic, there is the axiom schema of induction; for each first order predicate $\phi$ in the language of PA, we have an axiom:

$$(\phi(0) \wedge \forall n (\phi(n) \rightarrow \phi(n+1))) \rightarrow \forall n \phi(n)$$

For different formulas $\phi$, we get completely separate axioms. For example, we can replace $\phi$ with the formula $n+1+1 = n+2$ or with the formula $\forall m (((\exists l) n + l = m) \vee ((\exists l) n = m + l))$ or whatever other formula we can write down.

However, each of these axioms has the same "shape" - they're given by substituting some formula in for $\phi$. This is not a finite set of axioms, and you can show that there can be no finite set of axioms that works, but if we were to allow a symbol $\forall^* \phi$ which quantified over all formulas $\phi$ (which is basically what second-order logic is), we would be able to write this down as a single axiom.

Solution 2:

As mentioned above, "scheme" isn't a fully-precise term (and incidentally, see here for an analysis of the role of schemes in the history of logic). However, there is a natural candidate for what this should mean, and it's basically Dorebell's answer (to which this answer is really just an excessively long footnote):

An scheme of sentences in a signature $\Sigma$ is a sentence $\sigma$ in the language $\Sigma\sqcup\{R\}$ for some $k$-ary (usually unary) relation symbol $R$. An instance of $\sigma$ is then a sentence of the form $$\forall y_1,...,y_n(\sigma[R/\varphi(y_1,...,y_n,x_1,....,x_k)])$$ where $\varphi$ is some $(n+k)$-ary formula in the original language $\Sigma$ and $\sigma[R/\varphi(y_1,...,y_n,x_1,..., x_k)]$ is the $L$-formula gotten by replacing each "$R(t_1,...,t_k)$" with "$\varphi(y_1,...,y_n,t_1,...,t_k)$" throughout $\sigma$.

The additional $y_i$s and the outermost $\forall$ amount to allowing object parameters in the scheme.

For example, let's look at the language of arithmetic $\Sigma_{arith}=\{0,1,+,\cdot, \le\}$. We pick some yet-unused unary relation symbol $U$, and the induction scheme $\eta$ is then just (represented by) the $\Sigma_{arith}\sqcup\{U\}$-formula $$[U(0)\wedge \forall x(U(x)\rightarrow U(x+1))]\rightarrow \forall xU(x).$$ Taking $\varphi(y,x)$ to be the formula $$y\le x$$ we get the $\eta$-instance $$\forall y([\varphi(y,0)\wedge \forall x(\varphi(y,x)\rightarrow \varphi(y,x+1))]\rightarrow\forall x\varphi(y,x)),$$ or more simply $$\forall y([y\le 0\wedge\forall x(y\le x\rightarrow y\le x+1)]\rightarrow \forall x(y\le x)).$$ This is of course a very silly thing to say (although true), but it's a good example of an instance of a scheme.

For most purposes, we don't really care about this precise notion - the vastly weaker notion of computably axiomatizable theory is generally enough for our purposes. However, there is one particular situation in which schemes as defined above shine, and that is abstract model theory.

A scheme $\sigma$ is formulated in some "basic logic" - say, first-order logic. However, we can then interpret $\sigma$ in larger logics (e.g. second-order logic) by allowing the instances of $\sigma$ to come from $\varphi$s in that larger logic. Fixating on first-order logic for the moment, this is to say the following:

From a scheme $\sigma$ in a signature $\Sigma$, we get a map $M_\sigma$ assigning to each logic $\mathcal{L}$ which is at least as strong as first-order logic a set $M_\sigma(\mathcal{L})$ of $\mathcal{L}$-sentences of signature $\Sigma$, namely the set of all instances of $\sigma$ gotten from allowing $\mathcal{L}$-formulas (as opposed to merely $\mathsf{FOL}$-formulas) as input $\varphi$s.

(I'm ignoring the issue of precisely defining "logic" here, but see e.g. Ebbinghaus' chapter in the Model-Theoretic Logics collection.)

This lets us treat "schematic" theories like $\mathsf{PA}$ or $\mathsf{ZFC}$ as instances of a broader construction:

• $\mathcal{PA}$ is the map sending a logic $\mathcal{L}$ containing first-order logic to the $\mathcal{L}$-theory $$P^-+M_\eta(\mathcal{L}),$$ where $\eta$ is the induction scheme above and $P^-$ is the axiom for discrete ordered semirings.

• $\mathcal{ZFC}$ is the map sending a logic $\mathcal{L}$ containing first-order logic to the $\mathcal{L}$-theory $$\mathsf{PPIUECR}+M_\rho(\mathcal{L})+M_\xi(\mathcal{L}),$$ where $\mathsf{PPIUECR}$ is the conjunction of the Powerset, Pairing, Infinity, Union, Extensionality, Choice, and Regularity axioms and $\rho$ and $\xi$ are schemes corresponding to Replacement and Separation respectively.

(Incidentally, this "parameterized-by-logics" idea occurs in other contexts too - such as analogues of Godel's constructible universe.)

Personally, I like this recasting of "schematic" theories as "parameterized" theories because it helps us cleanly separate two often-entangled questions:

• What are our basic mathematical intuitions for natural numbers/sets/whatever?

• What is the right logical system for analyzing natural numbers/sets/whatever?

We can say "Well, the natural numbers are a discrete ordered semiring + induction" in a vague-but-compelling answer to the first bulletpoint without yet settling on first-order logic as the correct answer to the second. The map $\mathcal{PA}$ described above constitutes a formalization of this answer without committing to an answer to the second bulletpoint. The utter dominance of first-order logic means that this isn't something we care about too much, but it is an example of a very simple idea facilitated by the precise notion of "scheme" articulated above for which more general notions like "computably axiomatizable theory" don't really cut the mustard.