3
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ Do the comments to this question help? proofassistants.stackexchange.com/questions/2130/… $\endgroup$
    – Jason Rute
    Jun 26, 2023 at 10:37
  • $\begingroup$ Unfortunately not...as Sigma does not allow quantifying over the type of values in the domain of the model, only the domain itself. The type is still implicitly universally quantified over in the proposition. $\endgroup$
    – Mesabloo
    Jun 26, 2023 at 12:13
  • $\begingroup$ What we'd want is some sort of type-level Sigma (which is the encoding of existential types in dependently typed languages) though, which doesn't exist in Isabelle/HOL as far as I'm aware. $\endgroup$
    – Mesabloo
    Jun 26, 2023 at 12:36
  • $\begingroup$ After some goo googling you might want to look at this paper: besides bring the theorem you are interested (if not the proof), it the abstract suggests he goes into discussion of the difficulties involved with the type system: link.springer.com/chapter/10.1007/BFb0055135 $\endgroup$
    – Jason Rute
    Jun 27, 2023 at 9:47
  • $\begingroup$ Free preprint: cl.cam.ac.uk/~jrh13/papers/model.pdf $\endgroup$
    – Jason Rute
    Jun 27, 2023 at 9:54

1 Answer 1

0
$\begingroup$

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).)

$\endgroup$
5
  • $\begingroup$ Thanks for the answer! This goes along what is suggested in J. Harrisson's paper (sent in the comments). What we don't like about the approach in your second point is that we have to fix cow to the type (('f, 'p, 'v) formula set ⇒ 'm) set because of the use of ultraproducts. $\endgroup$
    – Mesabloo
    Jul 5, 2023 at 7:42
  • $\begingroup$ However, what we are currently trying is to show that if there exists any model of a set of formula, then there exists a Herbrand model of this set of formula (this was suggested by Manuel Eberl on the Zulip chat). This is also what is done in J. Harrisson's paper linked above, to avoid having to quantify over types. $\endgroup$
    – Mesabloo
    Jul 5, 2023 at 7:43
  • $\begingroup$ What is wrong with fixing cow to a specific type, can you say a bit more? If you're going to prove that some type 'm exists, it'll be "fixed" to be something. $\endgroup$ Jul 5, 2023 at 10:40
  • $\begingroup$ I can't remember exactly but the argument to be made is that we don't really care about the type of the domain, as any type will work for us (which is why we wanted this existential quantification on types, to hide the true type of model since we don't care about it, as long as there is one). Moreover, fixing the type cow to something prevents us from putting the two cases within a single lemma, but this is not really a big deal. $\endgroup$
    – Mesabloo
    Jul 6, 2023 at 8:58
  • $\begingroup$ Well, you don't have existential quantifiers. $\endgroup$ Jul 6, 2023 at 10:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.