# finite axiomatizability of first order theories?

If we consider a single schema as a single axiom, so ZFC for example would be finitely axiomatizable after this kind of counting axioms.

By schema its meant a syntactical expression (string of symbols) that contains among its symbols free meta-theoretic variable symbols that range over a decidable set of formulas of the language of the theory in such a manner that each substitution of all those metatheoretic variables in the expression by instances (formulas) from what they range over would result in a sentence of the language of the theory. For example the separation schema of Zermelo written as: $$\forall A \exists x \forall y (y \in x \leftrightarrow y \in A \land \phi) \text { is an axiom }$$; Where $$\phi$$ is a metatheoretic variable that ranges over all formulas of the language in which $$A$$ doesn't occur free.

This is considered as a single axiom. While the separation schema written as: $$for \ n=1,2,3,...\\ \forall p_1,.., \forall p_n \forall A \exists x \forall y (y \in x \leftrightarrow y \in A \land \phi)$$, that is not a single schema, it is an infinite collection of schemas, so it is not considered as a single axiom.

Now is it the case that every effectively generated first order theory (with finitely many primitives) is finitely axiomatizable in this sense?

• You have to define "schema." – Noah Schweber Apr 29 '20 at 20:49
• Correct! I've added that, see my last edition. – Zuhair Apr 30 '20 at 5:17

Let $$n\mapsto\phi_n$$ be a recursive enumeration of the provable formulas in the given theory, and define $$\phi_n'$$ to be $$\phi_n\wedge\dots\wedge\phi_n$$ where $$\phi_n$$ is repeated $$n+1$$ times. Given a formula you can check if it's equal to some $$\phi_n'$$ by seeing if it's equal to some formula repeated $$n+1$$ times, and then using the fact that $$n\mapsto\phi_n$$ is computable to calculate $$\phi_n'$$ and check if it's your formula. Thus the $$\phi_n'$$s form a decidable set of formulas, and hence a single axiom schema. This construction is also used in the proof of Craig's Theorem.
• You said the $\phi'$s form a single schema! Do you mean a single schema in the sense defined in the question? or just as a decidable set of formulas. – Zuhair May 4 '20 at 21:41
• @Zuhair I was thinking of the schema '$\phi \text{ is an axiom}$', where $\phi$ is a metatheoretic variable that ranges over the $\phi'_n$. – Oscar Cunningham May 5 '20 at 6:52