Let $L$ be a signature (in the sense of model theory), and let $T$ be an $L$-theory. Also, let $T_\forall$ (respectively, $T_\exists$) be the deductive closure of the universal (respectively, existential) sentences of $T$. Prima facie, there are $8$ possible combinations of finite/non-finite axiomatizability for each of $T$, $T_\forall$, and $T_\exists$. For instance, they could all be finitely axiomatizable, or they could all be non-finitely axiomatizable, or $T_\forall$ could be finitely axiomatizable while both $T$ and $T_\exists$ are non-finitely axiomatizable, etc. My question is, which of these $8$ combinations are actually realized? In other words, for each of those $8$ combinations, I want either an example of a signature $L$ and a $L$-theory $T$ which is an example of that combination along with the proof that it is indeed an example, or, a proof that there is no signature $L$ and no $L$-theory $T$ which has that combination.
The 8 combinations of finitely axiomatizable for full, universal, and existential theories.
logicmodel-theory
Related Solutions
Here are a few observations:
Any finite extension of a decidable theory is decidable. That is, if $T_1$ is decidable and $T_2$ is obtained by adding finitely many additional axioms $\varphi$, then $T_2$ is also decidable, since $T_2\vdash\psi$ is the same as $T_1\vdash\varphi\to\psi$.
If $T_2$ is c.e. and complete, then it is decidable, since to decide whether $T_2\vdash\varphi$ one searches either for $\varphi$ or for $\neg\varphi$ in $T_2$.
As I point out in the comment to Chris's answer, a theory is c.e. if and only if it is computably axiomatizable. The reverse implication is just enumerating proofs. For the forward direction, replace each axiom $\varphi$ with an enormous conjunction $\varphi\wedge\cdots\wedge\varphi$ whose length is the time it takes to appear in the computable enumeration. The set of these conjunctions (although a silly trick) axiomatizes the same theory and is decidable.
There are finitely axiomatizable theories in the language of arithmetic that have no decidable extensions. For example, Robinson's $Q$ is an example of this. One reason is that if $Q\subset T$ and $T$ were decidable and consistent, then we could find a computable separation of the two sets $A$ and $B$ consisting of the TM programs that halt with output $0$ and $1$, respectively. The reason is that any such halting behavior would be provable by $Q$ and hence also by $T$, and so we would find a computable set $C$ containing $A$ and disjoint from $B$. But this contradicts that these sets are computably inseparable---by the recursion theorem we could create a program that halts without output $0$ iff it is not in $C$, a contradiction.
There are numerous examples of finitely axiomatizable $T_1$ with c.e. $T_2$ that are not decidable. Chris Eagle gave one in his answer, if you take his set $A$ to be c.e. but not decidable. You can do his trick with any decidable theory $T_1$, provided that it has models with at least two elements. Just add new constant symbols $c_i$ and add the axioms $c_i=c_j$ whenever $i,j\in A$, for some fixed c.e. non-decidable set $A$. We can enumerate these axioms, so the resulting theory $T_2$ is c.e., but not decidable, since from a decision procedure for $T_2$ we could decide membership in $A$.
If the theory were finitely axiomatisable, consider sentences $B_1, ..., B_n$ which axiomatise it. Since $B_1, ..., B_n$ are in $T$, each can be deduced from a the $A_i$s. In particular, let $B_i$ be deducible from $A_{m_{i, 1}}, A_{m_{i, 2}}, ..., A_{m_{i, n_i}}$. Now let $k = 1 + \max_{1 \leq i \leq n, 1 \leq j \leq n_i} m_{i, j}$. Then $A_k$ is deducible from $B_1, ..., B_n$ and hence is deducible from the $A_{m_{i, j}}$. But this is a contradiction, since $k > m_{i, j}$ for all $i, j$ such that $1 \leq i \leq n$ and $1 \leq j \leq n_i$ and no $A_k$ is deducible from the previous sentences.
Best Answer
Here are examples of all $8$ of the possible behaviors. I tried my best to give the simplest most "combinatorial" and transparent examples I could think of. If anyone has suggestions of simpler examples, I'd be happy to hear them (especially for cases 7 and 8, which are more complicated than I would like).
Note that any consistent existential sentence has a finite model. If $T$ has no finite model, then $T_\exists$ has no finite model (it includes the schema saying "there are more than $n$ elements" for every $n$), so $T_\exists$ is not finitely axiomatizable. We'll use this observation a few times.
$T$, $T_\forall$, $T_\exists$ all FA: The empty theory.
$T$, $T_\forall$, $T_\exists$ all $\lnot$FA: We can take any non-finitely-axiomatizable theory axiomatized by quantifier-free sentences, since then $T = T_\forall = T_\exists$. For example, in the language with a constant symbol $c$ and a unary function symbol $f$, $\{f^n(c)\neq c\mid n\in \omega\}$.
$T$ and $T_\exists$ $\lnot$FA, $T_\forall$ FA: The theory of an infinite set (in the empty language). This is an existential theory, so $T = T_\exists$ is $\lnot$FA (since it has no finite models), and $T$ has no non-trivial universal consequences.
$T$ and $T_\forall$ $\lnot$FA, $T_\exists$ FA: Similarly to the last point, it suffices to find a $\lnot$FA universal theory with no non-trivial existential consequences. For example, in the language with a binary relation $R$, consider the theory which says "there is no $R$-cycle of length $n$" for all $n\in\omega$.
$T$ and $T_\forall$ FA, $T_\exists$ $\lnot$FA: The theory of non-empty dense linear orders without endpoints. $T$ is FA, and $T_\forall$ is the theory of linear orders, which is FA. $T$ has no finite models, so $T_\exists$ is $\lnot$FA.
$T$ $\lnot$FA, $T_\forall$ and $T_\exists$ FA: Consider the language with a unary predicate $P$. Let $T$ have one axiom for each $n\in \omega$, which says $(\exists x\, P(x))\rightarrow (\exists^{\geq n} x\, \top)$. A model of $T$ is either a set in which no elements satisfy $P$ or an infinite set in which $P$ is interpreted arbitrarily. $T$ is not finitely axiomatizable, but it has no non-trivial universal or existential consequences.
$T$ and $T_\exists$ FA, $T_\forall$ $\lnot$FA: Consider the theory in the language with a unary relation $G$, a binary relation $R$, and a ternary relation $E$. The theory says: (1) If $R(a,b)$, then $G(a)$ and $G(b)$. (2) If $E(a,b,c)$, then $\lnot G(a)$, $G(b)$, and $G(c)$. (3) $R$ is a graph relation on $G$ (it is symmetric and antireflexive). (4) For all $a$ such that $\lnot G(a)$, $E(a,y,z)$ is an equivalence relation on $G$ with two classes, establishing a bipartition of the graph $(G,R)$. That is, for all $b$ and $c$, if $R(b,c)$, then $\lnot E(a,b,c)$. (5) There exists $a$ such that $\lnot G(a)$. I have given a finite axiomatization of $T$, and $T_\exists$ just says that there exists an element $x$ satisying $\lnot G(x)$, $\lnot R(x,x)$ and $\lnot E(x,x,x)$, so this is also finitely axiomatizable. But $T_\forall$ says, in addition to (1)-(4), that the graph $R$ has no $n$-cycles for all odd $n\geq 3$. The point is that the existence of a bipartition implies these conditions, but since $T_\forall$ can't ensure the existence of an element $a$ satisfying $\lnot G(a)$, so that $E(a,x,y)$ witnesses that the graph is bipartite, $T_\forall$ has to rule out odd cycles explicitly.
$T$ FA, $T_\forall$ and $T_\exists$ $\lnot$FA: The idea is to combine examples 5 and 7. Take the previous example (7), add a new binary relation symbol $<$, and add axioms asserting that $<$ is a dense linear order without endpoints on the set of $x$ satisfying $\lnot G(x)$. The same considerations as in 7 show that $T_\forall$ is not finitely axiomatizable. And now $T_\exists$ is not finitely axiomatizable, because $T$ has no finite models.