In this question, I asked what an axiom schema was. In one of the answers, I was told that computably axiomatizable is a vastly weaker notion than "finite number of axiom schemas". Is this really true? Can someone exhibit a computably axiomatizable first order theory which can't be axiomatized by a finite number of axioms and axiom schemas?
Is there a computably axiomatizable first order theory which is not finitely axiom schematizable
logic
Related Question
- Is more than one free variable necessary for the axiom schemas in Peano arithmetic and ZFC set theory
- Finite axiomatizability of first order theories
- Suppose $A_1, A_2, \ldots$ are sentences such that no $A_i$ is deducible from earlier sentences. Demonstrate that this is not finitely axiomatizable.
- Successor arithmetic is not finitely axiomatizable
- (Fake proof) How are axiom schemas not “set theory in sheep’s clothing”
Best Answer
If you allow an infinite language, there are very easy examples. For instance, say you have a unary relation $R_n$ for each $n\in\mathbb{N}$, and you have as axioms $$\forall x R_n(x)$$ for each even $n$. This cannot be axiomatized by finitely many axiom schemes, since such schemes could only involve finitely many of the $R_n$, and therefore the resulting theory would have to be unchanged by any permutation of the $R_n$ that fixes those finitely many. But there is such a permutation that swaps an even and odd $R_n$, so that is impossible.
If you restrict to a finite language, then there should be similar examples, but proving they actually are not axiomatizable by finitely many schemes seems difficult. For instance, you could modify the example above to instead have a constant $0$, a unary operation $s$, and a binary relation $R$, and then take as axioms $$\forall x R(s^n(0),x)$$ for each even $n$. I don't know how to prove this cannot be axiomatized by finitely many schemes, but it seems extremely unlikely that it can be. (For that matter, the same applies to the version that includes such axioms for all $n$ rather than just for all even $n$.) Basically, if you write down some reasonable infinite family of axioms, the resulting theory will be computably axiomatizable, but there will typically be no reason to think the resulting theory can be axiomatized by finitely many schemes. As mentioned in Noah's answer there are some exceptions for theories that can encode enough of arithmetic, but if you have some random very weak theory there is no reason to expect any shenanigans like that.