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?
Logic – What is an Axiom Schema?
logic
Related Solutions
There are specific deduction systems that have only a finite number of logical axioms, or even no logical axioms. One example is natural deduction, which trades away logical axioms for a more complicated set of inference rules.
However, the use of infinite axiom schemes of logical axioms is not a problem for many of the applications of finite axiomatizability. If we have a structure $M$, or are constructing it, and we want to tell whether $M$ satisfies a theory $T$, there are two main issues we face:
- For each non-logical axiom of $T$, how do we tell that $M$ satisfies the axiom?
- If $T$ has infinitely many axioms, we have to quantify over them somehow.
For finitely axiomatizable theories, the second question is not an issue, so we can focus just on the first one. In any case, we don't need to worry whether our structure $M$ satisfies the logical axioms - we know it does, because they are true in every structure. We only need to worry about whether the structure satisfies the additional axioms of $T$. This is why finite axiomatizability is defined in terms of the non-logical axioms only.
If there are only finitely many new axioms in $T$, we can put all these axioms into a single sentence $\phi$ so that an arbitrary structure satisfies $T$ if and only if it satisfies $\phi$. That is a nice situation to be in, and it allows us in some cases to prove more about finitely axiomatizable theories than we would be able to prove about non-finitely-axiomatizable ones.
The existence of the single sentence $\phi$ also means there is a sort of "absoluteness" to whether a model satisfies $T$. If $T$ has an infinite axiom scheme, then from the point of view of a nonstandard model of arithmetic the scheme may well have nonstandard axioms - this is a subtle issue that can cause various kinds of confusion when people work with Gödel's incompleteness theorem. For a finitely axiomatized theory, because we can work with the single sentence $\phi$, even nonstandard models of arithmetic agree about the axioms for $T$.
It is a simple task to show in $\mathsf{ZFC'}$. that $$ \tag1\exists s\,\exists x\,x\in s.$$ Let $\varphi$ be the well-formed formula $$ y\in y.$$ Then $$ \forall s\,\exists t\,\forall y\,(y\in t\leftrightarrow\exists x\,(x\in s\land \varphi),$$ specialized to an $s$ as in $(1)$, gives us $$ \exists t\,\forall y\,(y\in t\leftrightarrow \exists x\,(x\in s\land y\notin y).$$ By $(1)$, this becomes $$ \exists t\,\forall y\,(y\in t\leftrightarrow y\notin y).$$ So for such $t$, $$ \forall y\,(y\in t\leftrightarrow y\notin y)$$ and specialized to $t$, $$t\in t\leftrightarrow t\notin t. $$ I sincerely hope that this is not a theorm of $\mathsf{ZFC}$.
Best Answer
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.