1
$\begingroup$

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?

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

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Zuhair May 4 '20 at 21:41
  • $\begingroup$ @Zuhair I was thinking of the schema '$\phi \text{ is an axiom}$', where $\phi$ is a metatheoretic variable that ranges over the $\phi'_n$. $\endgroup$ – Oscar Cunningham May 5 '20 at 6:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.