Determining the size of a theory's models

Question

While these are technically separate questions, I think that the answer to either question will be clearer if both questions are answered together. So I'm asking them together.

Proposition 1 If $\mathcal{T}$ is a first-order theory, and $\mathcal{T}$ has a model, then it has a model of least cardinality.

proof-sketch: Let $\mathcal{T}$ be a first order theory. Suppose that $\mathcal{T}$ has a model, and that $\mathcal{T}$ has no finite models. Then by Löwenheim–Skolem, the smallest model of $\mathcal{T}$ has cardinality no less than that of language of $\mathcal{T}$ and we are done. Suppose that $\mathcal{T}$ has a finite model. Then the well-ordering of the natural numbers implies the existence of a smallest finite model.

Question 1

Is there a general algorithm to determine the cardinality of the least model of an arbitrary first-order theory $\mathcal{T}$ (provided that $\mathcal{T}$ has a model)?

Question 1.1 (optional)

Is there a general algorithm to determine the cardinality of the largest model, provided that one exists (i.e. $\mathcal{T}$ has only finite models or some bizarre contradiction involving large cardinals)? I'm almost certain that the answer is "no," but I can't quite pin down why.

Proposition 2 If $\mathcal{T}$ is a first-order theory, and $\mathcal{T}$ has a finite model, then there is a (possibly finite) sequence $\mathbf{a}(\mathcal{T})=(a_0,a_1,a_2,\ldots)$ of natural numbers such that for every finite model $\mathcal{M}\vDash\mathcal{T}$, there exists a natural number $n$ such that $|\mathcal{M}|=a_n$.

proof-sketch: Let $\mathcal{T}$ be a first order theory with a finite model. Define $\mathcal{M}_0$ to be the least model of $\mathcal{T}$ and $a_0=|\mathcal{M}_0|$. Because the natural numbers are well-ordered and closed under succession, if $\mathcal{T}$ has a model of cardinality $k>a_0$, then there exists a least $m$ such that $\mathcal{T}$ has a model of cardinality $s^m(a_0)$; define $a_1=s^m(a_0)$, rinse and repeat.

Question 2

For an arbitrary first-order theory $\mathcal{T}$, is $\mathbf{a}(\mathcal{T})$ primitive-recursive (provided that $\mathcal{T}$ has a finite model)? If yes, is there a general algorithm for determining $\mathbf{a}(\mathcal{T})$?

If no, is $\mathbf{a}(\mathcal{T})$ recursively enumerable? If yes, is there a general algorithm for determining $\mathbf{a}(\mathcal{T})$?

If no, when is $\mathbf{a}(\mathcal{T})$ / for which theories $\mathcal{T}$ is $\mathbf{a}(\mathcal{T})$ 1) recursively enumerable, 2) primitive recursive?

Note: If $\mathcal{T}$ has a model but no finite models, then $\mathbf{a}(\mathcal{T})$ is "as recursive" as the class of cardinals. What this means depends on the notion of "cardinal" employed. Accepting the strongest form of the continuum hypothesis and the axiom of choice, $\mathbf{a}(\mathcal{T})$ is "primitive-transfinite" recursive, with $a_0=\aleph_0$ and $a_{s(\kappa)}=2^{\aleph_\kappa}$.

Comment: I don't think this falls under the umbrella of "finite model theory" - even though finite models are being considered. I noticed that there does not seem to be a [finite-model-theory] tag, though. Should I create one?

Answer 1

First, let's make some quick comments about the basic model theory here.

It seems that by "least model" you mean "model of least possible cardinality." In this case Lowenheim-Skolem is irrelevant. The existence of models of least cardinality is trivial since the cardinals are well-ordered: every (nonempty) set of cardinals has a least element. Meanwhile, by upwards Lowenheim-Skolem - indeed, by compactness - if a theory $T$ has an infinite model then it has arbitrarily large infinite models. (Note that this doesn't require any assumption on the size of $T$!) So if $T$ has any infinite models at all, then it has no maximal-cardinality model. Conversely, if $T$ has arbitrarily large finite models then by compactness $T$ has an infinite model. So maximal-cardinality models only exist when all models of the theory have cardinality $<k$ for some finite $k$ (and I'll denote the least such $k$, when it exists, by "$k_T$").

Moreover, if $T$ is a countable theory - which it really needs to be in order for computability theory to be relevant - the full Lowenheim-Skolem theorem says that $T$ either has no infinite models or has infinite models of every infinite cardinality. So there isn't anything interesting to say about the sizes of infinite models of $T$. (Once we try to count the models $T$ of a given infinite cardinality up to isomorphism, then things get more interesting, but that's a different issue - and not really related to computability theory.)

As an aside, re: Lowenheim-Skolem note that you haven't stated it correctly in the OP. LS says that if $T$ has any infinite models then $T$ has a model of every infinite cardinality at least as large as the language of $T$ itself. A theory in an uncountable language need not have a countable model (e.g. take an uncountable set of constant symbols and axioms saying that they're all distinct). Now per the above this isn't really relevant here, but it's still worth pointing out.

---

Now let's move on to the computability-theoretic issues. Here there is some subtlety; we have some, but not too much, computability available to us.

The key point is that given a sentence $\varphi$ and a finite structure $A$, we can computably check whether $A\models\varphi$ (just by brute force). In particular, this means that we can computably find the least $n\in\mathbb{N}$ such that $\varphi$ has a model of size $n$ (in case such an $n$ exists at all). This also means that we can compute the set of finite models of a given sentence. And thinking about what's involved in that brute-force search, this is in fact all performable in exponential time - so much better than primitive recursive.

In fact, with a bit more thought we can also find $k_{\{\varphi\}}$ - when it exists - in a computable way as well: model checking gives us lower bounds, and proof search gives us upper bounds (just search for proofs of sentences of the form $\varphi\rightarrow\exists x_1,...,x_m\forall y(\bigvee_{1\le i\le m}x_i=y$).)

Note, however, that the above only works for single sentences (or finitely axiomatizable theories presented via "canonical finite" axiomatizations - see Soare's book for what this means). Sets of sentences - even relatively simple ones - can be quite messy. E.g. consider the sentences $$\theta_m\equiv\exists x_1,...,x_m\forall y(\bigvee_{1\le i\le m}x_i=y$$ and $$\theta_{m,n}\equiv \theta_m\wedge\theta_m\wedge ...\wedge\theta_m\mbox{ ($n$ times)}.$$ Let $T_e=\{\theta_2\}\cup\{\theta_{1,s}: \Phi_e(e)[s]\uparrow\mbox{ but }\Phi_e(e)[s+1]\downarrow\}$. Then $T_e$ is always finite and is uniformly computable in $e$, but the map $e\mapsto k_{T_e}$ is not computable since $k_{T_e}=2$ iff $e\not\in\emptyset'$ and $k_{T_e}=1$ iff $e\in\emptyset'$. Similarly, we can't computably find the smallest finite model of a computably axiomatizable theory in a computable way; the best we can do is "approximate it from below" (the point being that the set of finite models of a computably axiomatizable theory is always co-c.e.).

---

Finally, it seems you're also interested in bringing infinite cardinalities into the picture. This takes serious work to formalize: a priori, computability theory doesn't really make sense in this context. In some situations it trivializes (e.g. for a countable theory $S$ it's obvious that the set of cardinalities of infinite models of $S$ should be computable, since it's "all of them," even if it's not clear what "computable" should mean in this context), but in general this is a serious issue. So the part of your question which looks at infinite models isn't really precise enough yet to admit an answer.

Answer 2

In general, we can't hope to computably answer questions about finite cardinalities of models of arbitrary theories. The main obstruction is Trakhtenbrot's theorem. Let FinSat be the following decision problem: Given a sentence $\varphi$ as input, return Yes if $\varphi$ has a finite model and No otherwise. Trakhtenbrot's theorem says that FinSat is undecidable (there is no algorithm which solves the decision problem).

Proposition 1: This is correct (but I would say "a model of least cardinality" rather than "a least model", because the latter could be interpreted to mean a model which embeds (elementarily) into every other model, i.e. a least model in the (elementary) embedability preorder).

Question 1: No. Suppose for contradiction that there is an algorithm to determine the least cardinality of a model of an arbitrary consistent theory $T$ (or even of a single sentence). Then we could solve FinSat (for a contradiction) as follows:

Let $\theta$ be the sentence $(\forall x\forall y\,(x\neq y\rightarrow f(x)\neq f(y))) \land (\exists y\forall x\, (f(x) \neq y))$. This asserts that $f$ is injective but not surjective, so $\theta$ is consistent but has only infinite models. Now given a sentence $\varphi$, apply our algorithm to the theory $T = \{\varphi\lor \theta\}$. This theory is consistent (any model of $\theta$ is a model of $T$), and it has a finite model if and only if $\varphi$ has a finite model. If our algorithm says the least cardinality of a model of $T$ is finite, return Yes, otherwise return No.

Question 1.1: By the compactness theorem, if a theory $T$ has arbitrarily large finite models, then it has an infinite model, and by Löwenheim-Skolem it has arbitrarily large infinite models. So $T$ has a model of maximal cardinality if and only if $T\vdash \varphi_{\leq k}$ for some $k$, where $\varphi_{\leq k}$ is the sentence asserting that there are at most $k$ elements in the domain: $\forall x_1\dots\forall x_{k+1}\left(\bigvee_{i\neq j} x_i = x_j\right)$.

Then your question has a positive answer (sort of). If we are handed a theory $T$ and promised that it is consistent and there is an upper bound on the cardinalities of its models, then we can compute this upper bound by simultaneously searching for proofs of $\varphi_{\leq k}$ from $T$ for all $k$ (provided that $T$ itself is recursively enumerable). This algorithm must terminate, since eventually we will find a proof of one of these sentences.

I said "sort of" because the algorithm I described will not halt if you hand me a theory $T$ which is consistent but has no upper bound on the cardinalities of its models. So the answer to the question may depend on what is meant by "an algorithm to determine (something) provided (some condition holds)". E.g. maybe you want an algorithm which is guaranteed to halt on all $T$, but where you only trust the answer in the case that $T$ has a model of maximum cardinality?

Proposition 2: This is correct. But there's nothing special about models here. All we have to do is form the set $\{n\in \mathbb{N}\mid \text{there exists }M\models T\text{ with }|M| = n\}$ and then use the basic fact that an arbitrary subset of $\mathbb{N}$ can be enumerated in increasing order as a sequence...

Question 2: In one sense, $\mathbf{a}(T)$ is not computable: by Trakhtenbrot's theorem, the question of whether or not $\mathbf{a}(T)$ is the empty sequence is undecidable, even when $T$ is a single sentence! But on the other hand, for a single sentence $\{\varphi\}$, $\mathbf{a}(\{\varphi\})$ is recursively enumerable just by searching for finite models of $T$ (as described in Noah's answer, which appeared as I was writing this).

Of course, if we are guaranteed that $\varphi$ has an upper bound on the sizes of its finite models (so $\mathbf{a}(\{\varphi\})$ is finite), then $\mathbf{a}(\{\varphi\})$ is computable by just searching for models of all the finite sizes up to the bound.