Existential quantification on types in Isabelle

Question

We are currently working on a proof of compactness for classical first order logic using the ultraproduct-based proof.

theorem sat_compactness: ‹sat TYPE('m) T ⟷ (∀ T' ⊆ T. finite T' ⟶ sat TYPE('m) T')›
  oops

Here's the catch. We are using this definition for satisfiability of a set of closed formulas:

abbreviation sat :: ‹'m itself ⇒ ('f, 'p, 'v) th ⇒ bool› where
  ‹sat _ T ≡ (∃ ℳ :: ('f, 'p, 'm) model. is_model_of ℳ T)›

Note that the 'm itself is not required, but Isabelle will generate it for us (alongside a warning) if left out. Here, 'f is an abstraction for the type of function symbols, 'p is an abstraction for the type of predicate symbols, 'v is an abstraction for the type of variable symbols, and 'm is an abstraction for the type of values within the model.

Now unfortunately this definition does not quite convey the meaning that we'd like. What we would like to have is that there exists some 'm (with an associated model ℳ with 'm set as domain) such that ℳ is a model of T (i.e. a model of every closed formula in T) ─ in fact the proof of the compactness theorem cannot be finished without such a formulation, as it involves creating a model with a different domain (type).

Isabelle/HOL does not allow for quantification over type variables, as far as I'm aware, which is unfortunately what we require in the proof of compactness (since we don't care about which kind of model we get, as long as there is one).

I saw this post related to how can one fake existential types, but it requires the domain to be countable, which is too big a restriction in our setting¹.

The only other alternative that I can see would be to axiomatize quantification over type variables (not sure if it can even be done?), but this seems like a very hacky way of getting Isabelle to work with us. Is there any other way one would do this? More specifically, is there a way either to encode the existential/universal type within Isabelle, or not to have to depend on it somehow?

---

¹: The proof of compactness using ultraproducts makes use of equivalence classes on functions. In Isabelle/HOL, for a function to be countable, one needs its domain to be finite (as per the instance). Requiring the domain to be finite in turns requires us that T be finite, which completely voids the purpose of the compactness theorem.

Answer 1

Apologies for not speaking Isabelle/HOL syntax, but couldn't you split the theorem like this:

1. For all 'm and ℳ :: ('f, 'p, 'm) model, if is_model_of ℳ T then (∀ T' ⊆ T. finite T' ⟶ sat TYPE('m) T').

2. For all 'm, construct from (∀ T' ⊆ T. finite T' ⟶ sat TYPE('m) T') a particular type cow (may depend on 'm), a particular ℳ :: ('f, 'p, cow) model and show is_model_of ℳ T.

In essence you have the compactness theorem. The first statement shows that if there is a model then you get the finite-submodel property, and the second that from the finite-submodel property you know how to construct a model.

(All I really did was to split the equivalence into two implications and then use the fact that (∃ m . P(m)) → Q is equivalent to ∀ m . (P(m) → Q).)