# Is there a theory in a finite language that is computably axiomatizable but not by a finite number of axiom schemas?

I was told to ask this question on mathoverflow. I asked on math stack exchange whether there is a computably axiomatizable theory that can't be axiomatized by a finite number of axiom schemas. I got an answer, but it was a theory in an infinite language. Now, I am asking whether there is an example in a finite language.

EDIT by non-OP: this is the above-mentioned MSE question, and this answer gives the definition of "scheme" being used.

• If it’s computable, then can’t you write it down as one “schema”? – Monroe Eskew Jun 19 at 22:11
• Hmm. I missed schema. Maybe the poster has a limited meaning of schema which (for my example below hopefully) excludes hyperidentities. There may be a theory which does not have a finite hyperbase. Gerhard "Look Up Padmanabhan And Penner" Paseman, 2020.06.19. – Gerhard Paseman Jun 19 at 22:29
• I believe there is a theorem of Kleene about this, saying that, if the language (or perhaps the theory) is rich enough then a computable set of axioms can be replaced with a schema. But I failed to find the paper now. There is a paper by Vaught, "Axiomatizability by a schema"; maybe this is what I remembered, and I was wrong about Kleene. I'd expect that the result fails if the language is very poor. Suppose you have only a constant 0, unary function S, and unary predicate P, with axioms $P(S^n0)$ for prime $n$ and $\neg P(S^n0)$ for composite $n$. That doesn't look schematic to me. – Andreas Blass Jun 19 at 22:57
• I've edited to link the reader to the relevant definition - remember that "scheme" is not actually a technical term, as the answers to your original question stated. – Noah Schweber Jun 19 at 23:51
• Following up on the comment by Andreas Blass: Vaught proved that if a theory $T$ is computable and has "a modicum of coding", then $T$ is axiomatizable by a scheme. Vaught's result was improved by Visser, in the paper below, who reduced "the modicum of coding" used by Vaught to "has a definable pairing function" A. Visser, Vaught's theorem on axiomatizability by a scheme, The Bulletin of Symbolic Logic, vol. 18 (2012), pp. 382-402. – Ali Enayat Jun 20 at 0:06

Let me give an example of a theory that is computably axiomatizable but isn't axiomatizable by finitely many schemas.

Fix any finite signature $$\Omega$$ with equality. Further by finite $$\Omega$$-models I'll mean models encoded by binary strings in a natural way. Observe that for any $$\Omega$$-theory $$T$$ axiomatized by finitely many schemas the set of all finite models of $$T$$ is $$\mathtt{co}\text{-}\mathtt{NP}$$. And observe that given a finite $$\Omega$$-model $$\mathfrak{M}$$ we could effectively construct an $$\Omega$$-sentence $$\chi_{\mathfrak{M}}$$ such that for any $$\Omega$$-model $$\mathfrak{N}$$ we have $$\mathfrak{N}\models \chi_{\mathfrak{M}}\iff \mathfrak{N}\simeq\mathfrak{M}.$$ Consider arbitrary computable set of finite $$\Omega$$-models $$A$$ that is closed under isomorphisms and isn't $$\mathtt{NP}$$. Let $$U_A$$ be the theory axiomatized by sentences $$\lnot\chi_{\mathfrak{M}}$$ for $$\mathfrak{M}\in A$$. Clearly $$U_A$$ is computably axiomatizable. However, the set of finite models of $$U_A$$ is the complement of $$A$$ and thus isn't $$\mathtt{co}\text{-}\mathtt{NP}$$. Hence $$U_A$$ couldn't be axiomatized by finitely many schemas.

• I meant that a scheme $S(P_1,\ldots,P_n)$ is a first-order formulas in the language expanded by fresh predicate symbols $P_1,\ldots,P_n$. A scheme $S(P_1,\ldots,P_n)$ generates the set of formulas that are obtained from $S$ by replacing $P_1,\ldots,P_n$ with arbitrary first-order formulas of the target language. – Fedor Pakhomov Jun 19 at 23:56
• Any set of $n$-tuples from a finite model $\mathfrak{M}$ is definable by some formula with parameters. Hence a schemata $S(P_1,\ldots,P_n)$ holds in a finite model $\mathfrak{M}$ iff it holds in $\mathfrak{M}$ under all possible interpretations of $P_i$'s as predicates of appropriate arities. This clearly leads to a $\mathtt{co}\text{-}\mathtt{NP}$ check of whether a finite models satisfy a given scheme. – Fedor Pakhomov Jun 20 at 0:00
• ... oh wow that's embarrassing. My bad! I'm going to blame it on me not having had enough coffee. – Noah Schweber Jun 20 at 0:32

This answers complements Fedor Pakhamov's, who provided an example of a computable theory that is not axiomatizable by finitely many schemas.

Following up on the comment by Andreas Blass to the question: Vaught proved that if a theory $$T$$ is computable and has "a modicum of coding", then $$T$$ is axiomatizable by a scheme. Vaught's result was improved by Albert Visser, in the paper below, where "the modicum of coding" used by Vaught is reduced to the modest demand that $$T$$ interprets a non-surjective unordered pairing, where pairing need not be functional.

A. Visser, Vaught's theorem on axiomatizability by a scheme, The Bulletin of Symbolic Logic, vol. 18 (2012), pp. 382-402.

A preprint of Visser's paper can be found here.

There are a number of algebraic theories (in equational logic specifically, no predicate symbols besides equality) which are of finite type (so the language has only finitely many function symbols) but not finitely axiomatizable. Often one demonstrates this with an infinite sequence of structures for the language, but in some cases one can establish this linguistically.

A simple example involves work with hyperidentities (check out my arxiv preprint for details, 1408.something something). We posit the theory given by the hyperidentity F(F(x)) ideq F(F(F(x))), which is short hand for an equational theory that says every unary function term t in a language has its square equal its cube, or forall x t(t(x)) = t(t(t(x)).

If we choose a language with one binary function symbol, we get a finitely axiomatizable theory. I forget what happens with two unary function symbols. With three, you get a recursively axiomatizable theory which is not finitely axiomatizable. You show this by looking at the Thue Morse sequence and use square free fragments to build long terms and show long instances are not derivable from short instances of the axioms.

It gets real fun with more complicated hyperidentities and larger sets of function symbols. Check out the preprint for other families of examples.

Gerhard "Is The Question Computably Decidable?" Paseman, 2020.06.19.

• While this is intereting, as far as I can tell it doesn't address the question which is about axiomatizability by finitely many schemes, not finite axiomatizability itself. – Noah Schweber Jun 20 at 0:33
• That's right. (I missed schema.) When I have an example of a variety which has no finite hyperbasis, I will post it. That won't conclusively answer the question, but it will get closer. There may even be a semigroup variety which is not finitely hyperbased, but I don't see it yet. Gerhard "Has Not Finished Scheming Yet" Paseman, 2020.06.19. – Gerhard Paseman Jun 20 at 0:43