Quantitive compactness theorem, getting explicit bounds

Question

consider the wonderful theorem in logic that says that if an infinite set of formulas is not satisfiable, then some finite subset of it isn't.

Given bounds on lengths of formulas, number of variables appearing in them, etc. is it possible to derive a quantitive version? Meaning a bound on the size of the smallest finite subset that is not satisfiable.

EDIT: I am not claiming any theorem, I haven't put much thought into the exact conditions. I'd rather YOU tell me what needs to happen and if there is an interesting theorem here.

Answer 1

You might be interested in a notion from model theory called the finite cover property. Instead of defining the finite cover property, I'm going to define what it means for a formula to not have the finite cover property. This definition makes the connection with the compactness theorem more obvious.

Definition: Fix a complete theory $T$ and consider a formula $\varphi(x,y)$. [Here $x$ and $y$ are both tuples of variables, and by writing this I mean that we've partitioned the free variables appearing in $\varphi$ the two tuples $x$ and $y$.] Then $\varphi$ does not have the finite cover property (modulo $T$) if there is a natural number $k$ such that whenever $M$ is a model of $T$ and $\Sigma$ is a set of formulas, such that every formula in $\Sigma$ has the form $\varphi(x,a)$ or $\lnot\varphi(x,a)$ where $a$ is a tuple from $M$, if $\Sigma$ is inconsistent, then some subset of $\Sigma$ of size $\leq k$ is inconsistent. [As usual for a set of formulas with parameters from $M$, inconsistent here means not realized in any elementary extension of $M$, i.e. inconsistent with the elementary diagram of $M$, which includes $T$.]

In other words, the number $k$ is an uniform bound for the compactness theorem of the kind you're looking for, in the special case of $\varphi$-types (sets of positive and negative instances of $\varphi$), with parameters from a model of $T$.

We also define this notion for theories:

Definition: $T$ does not have the finite cover property if every formula $\varphi(x,y)$ does not have the finite cover property modulo $T$.

Now in Classification Theory, Shelah proved that $T$ does not have the finite cover property if and only if $T$ is a stable theory which eliminates the quantifier $\exists^\infty$ in $T^\text{eq}$. This is technical terminology, but it means that 1. $T$ does not define a linear order on any infinite sequence from a model, and 2. given formulas $\theta(x,z)$ and $\psi(x,y,z)$, there is a uniform bound $N_{\theta,\psi}$, such that for any $c$, if $\psi(x,y,c)$ defines an equivalence relation on the set defined by $\theta(x,c)$, the quotient by this equivalence relation is either infinite or has size at most $N_{\theta,\psi}$.

To be a stable theory which eliminates $\exists^\infty$ in $T^{eq}$ is a pretty special condition. In other words, if you consider a random theory $T$, it probably has the finite cover property, so you probably won't have any sort of uniform bound on applications of compactness modulo $T$ in general.

On the other hand, there are lots of well-known theories which do not have the finite cover property. Any strongly minimal theory will do, for example the theory of algebraically closed fields of a given characteristic. Such theories have uniform bounds for applications of compactness to $\varphi$-types, but how to actually compute these bounds is going to depend heavily on the theory in question. For example, doing this for the theory of algebraically closed fields will get you into the realm of computational algebraic geometry, with Gröbner bases and the like.

Answer 2

As Eric Wofsey commented, with a bounded length for formulas and a finite alphabet the question is trivial. So let's make it slightly less trivial by allowing the lengths of the $n$'th formula to grow with $n$ (logarithmic growth will do), thus allowing the appearance of infinitely many different variables (where variable $x_m$ will have length $O(\log m)$). Consider the following $M$ formulas in Peano arithmetic:

$$\eqalign{x_2 &= S(x_1) \cr x_3 &= S(x_2) \cr x_4 &= S(x_3) \cr & \ldots\cr x_M &= S(x_{M-1})\cr x_1 &= S(x_M)}$$ This has the property that every proper subset is satisfiable. You can get an infinite sequence of formulas whose smallest unsatisfiable subset has cardinality $M$, by following these by repetitions of $1=1$. Thus there is no bound on cardinality of the smallest unsatisfiable subset of such a sequence of formulas.