Ghilain Bergeron (Jun 27 2023 at 08:23): Ghilain Bergeron (Jun 27 2023 at 08:23):Hi everyone!
We are trying to prove the compactness of classical first order logic. We chose to go for the proof based on ultraproducts and model theory.
However, it seems that we are running into an expressivity problem of Isabelle/HOL.
Here is how we represented 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)›
'f, 'p and 'v are abstract types for function, predicate and variable symbols respectively.
The problem here is that we have to provide 'm ourselves (which is the type of values in the domain of the model).
This definition does not really convey the meaning we want: we would like to obtain any model on any domain, so something like ∃ m'. ∃ ℳ :: ('f, 'p, 'm) model. is_model_of ℳ T.
This problem appears further into the proof of compactness (which states that sat TYPE('m) T ⟷ (∀ T' ⊆ T. finite T' ⟶ sat TYPE('m) T')).
The left to right direction follows quite clearly from the definition of modelhood on set of closed formulas, but the other direction is quite tricky.
In the proof using ultraproducts, a model with another domain (of a different type) is constructed, which satisfies every closed formula in T.
Unfortunately, this does not allow us to conclude, because we have a model on (('f, 'p, 'v) statement set ⇒ 'm) set, not on 'm.
Here are the things that we considered to solve this issue:
∃ m'. P TYPE(m') or ∀ m'. P TYPE('m) for example), which does not appear to be doable in Isabelle/HOL;(('f, 'p, 'v) statement set ⇒ 'm) set set into 'm set, which does not seem to be quite doable in the general case (or our understanding of the problem isn't enough);T' are infinite, countable and more specifically the same. We have not looked into this much further yet, but this is on our TODO list;Is there anything that can be done regarding point 1.? Perhaps is it possible to axiomatize some definitions so as to encode ∃ and ∀ on types?
We are quite unsure about this, and we think that HOL isn't even expressive enough for such axioms.
Is there perhaps another way of stating this proof which does not involve explicit quantification over types?
Dmitriy Traytel (Jun 27 2023 at 09:00):Hi Ghilain, It is correct that you cannot quantify over types inside of HOL terms. In a different context, Andreas Lochbihler discusses different alternatives to this limitation (http://www.andreas-lochbihler.de/pub/lochbihler14iw.pdf, Section 6.2), including hard-coding the types of interest, or working with a universal domain (your point 3). The solution he opts for is to use a codatatype to represent the existentially quantified type. I'm not sure though what this would correspond to in your setting.
Manuel Eberl (Jun 27 2023 at 09:05):I don't really know very much about logic, or set theory, or type theory, but I do think that this is a common problem in HOL when one wants to define things such as semantic entailment. Hopefully somebody else who has faced these issues before can say something more about this. I do think that even in more powerful logics (like those used by Coq and Lean) one can run into similar levels due to universe levels, but I don't really know much about that.
One approach that sometimes works is to define your thing by quantifying not over all models of any type, but over all models of some specific type that is "big enough" and then, later, proving that this more restricted predicate implies the more general one for an arbitrary type. Or, in your case, probably the reverse: if there exists any model, then there also exists a model of the type that you chose in the definition.
Again, I don't know much about logic, but my guess would be that there is some kind of a-priori bound for how "big" the smallest model can (depending on the cardinality of the variable and constant symbols), or some kind of explicit construction for a model. I somehow vaguely remember something about Herbrand models? Aren't those even countable? In that case you could just hard-code the 'm in your definition to a Herbrand universe (or nat, but that is probably less convenient).
You might think that writing that the theorem that the existence of any model implies your (now much more restricted) sat predicate would again require quantifying over types, but it doesn't really, because in that case you only have universal quantification at the outermost level, which is okay in Isabelle/HOL through its ad-hoc polymorphism. The statement, with schematic type and term variables for emphasis, would look something like this: is_model_of (?M :: ('?f, '?p, '?m) model) ?T ⟹ sat ?T
Manuel Eberl (Jun 27 2023 at 09:09):Also, just in case you're not aware, there are already Isabelle/HOL formalisations of first-order logic in the AFP, including completeness. Not sure about compactness, but e.g. grepping for herbrand gives some results, but I don't know enough about logic to really see whether they are relevant to what you're doing.
In any case, if you can, I'd suggest you build on top of an existing formalisation to increase reusability instead of making an entirely new formalisation of first-order logic.
Ghilain Bergeron (Jun 27 2023 at 09:16):Manuel Eberl said:
Also, just in case you're not aware, there are already Isabelle/HOL formalisations of first-order logic in the AFP, including completeness. Not sure about compactness, but e.g. grepping for
herbrandgives some results, but I don't know enough about logic to really see whether they are relevant to what you're doing.In any case, if you can, I'd suggest you build on top of an existing formalisation to increase reusability instead of making an entirely new formalisation of first-order logic.
That's right.
The 4th point would make use of some already formalized proofs of completeness for first order logic in the AFP.
As far as my understanding goes, compactness should follow from completeness.
However, we were initially going for the proof of compactness using ultraproducts, which as far as I'm aware does not exist in the AFP.
We were still reusing parts of some entries though!
Some refactoring is needed anyway in my theory, I guess it would be a good time to use the entry FOL_Fitting for example (well, unless we have to scrap the entire proof anyway).
Ghilain Bergeron (Jun 27 2023 at 09:27):I'll have to understand and see for the other suggestions.
One approach that sometimes works is to define your thing by quantifying not over all models of any type, but over all models of some specific type that is "big enough" and then, later, proving that this more restricted predicate implies the more general one for an arbitrary type. Or, in your case, probably the reverse: if there exists any model, then there also exists a model of the type that you chose in the definition.
I think this is basically what we are trying to achieve with the 3rd point.
Not sure how far it'll go nor if it actually works at all.
Again, I don't know much about logic, but my guess would be that there is some kind of a-priori bound for how "big" the smallest model can (depending on the cardinality of the variable and constant symbols), or some kind of explicit construction for a model. I somehow vaguely remember something about Herbrand models? Aren't those even countable? In that case you could just hard-code the
'min your definition to a Herbrand universe (ornat, but that is probably less convenient).
The problem we faced with requiring the domain of models to be countable is that the restriction is too big on what we can express.
More specifically, since we make use of equivalence classes on functions (in the proof of Łoś' theorem), we would need to further restrict the domain of indices to be finite.
This doesn't seem to be such a big restriction, but this has as a consequence that in the proof of compactness, the set containing all finite subsets of T must be finite, which means that T must be finite.
Hence, the proof does not really make sense anymore.
In a different context, Andreas Lochbihler discusses different alternatives to this limitation (http://www.andreas-lochbihler.de/pub/lochbihler14iw.pdf, Section 6.2), including hard-coding the types of interest, or working with a universal domain (your point 3). The solution he opts for is to use a codatatype to represent the existentially quantified type. I'm not sure though what this would correspond to in your setting.
Thanks! I'll have a read and see if I can extract some precious knowledge out of it.
You might think that writing that the theorem that the existence of any model implies your (now much more restricted)
satpredicate would again require quantifying over types, but it doesn't really, because in that case you only have universal quantification at the outermost level, which is okay in Isabelle/HOL through its ad-hoc polymorphism. The statement, with schematic type and term variables for emphasis, would look something like this:is_model_of (?M :: ('?f, '?p, '?m) model) ?T ⟹ sat ?T
Mmmh, I don't really understand where this idea is going.
Do you mind expanding a bit on it?
Manuel Eberl (Jun 27 2023 at 09:29):Okay, so the idea would be to do something like
definition sat :: "formula ⇒ bool" where "sat (φ :: ('v,'c) formula) = (∃M :: ('v,'c) std_model. is_model φ M)"
where 'v and 'c are the types of the variables/constant symbols and std_model is some type that you defined in terms of 'v and 'c that is ‘big enough’ so that you can construct a model for any satisfiable formula with variables/constants of that size in it.
Clearly you can prove that if sat φ holds for some formula φ then there exists some type τ such that φ has a model of type τ. That's follows trivially from the definition of sat. The way to phrase this theorem in Isabelle would be
lemma satD: "sat (φ :: ('v,'c) formula) ⟹ ∃(M :: ('v,'c) std_model). is_model φ M"
The trickier part is to also prove the ‘converse’: if there is a model of some type τ then sat also holds:
lemma satI: "is_model (φ :: ('v,'c) formula) (M :: 'm) ⟹ sat φ"
Oh alright I see. Thanks!
Manuel Eberl (Jun 27 2023 at 09:33):That's just a sketch of course, but I hope you get what I mean.
Ghilain Bergeron (Jun 27 2023 at 09:34):Yep I got it!
Manuel Eberl (Jun 27 2023 at 09:34):How you define this std_model is of course the tricky question. But I guess that whatever it is that you're doing, you're probably going to prove somewhere that if there is some model for a formula, then there is also some kind of convenient ‘standard’ model. And then the structure of that standard model basically tells you what the std_model type should look like.
Ghilain Bergeron (Jun 27 2023 at 09:36):I checked out a proof of compactness in HOL Light a bit ago (not based on ultraproducts though), and they were mentioning "canonical models".
I still haven't yet researched about those, but I think this should be close to what you describe.
Manuel Eberl (Jun 27 2023 at 09:37):The existence of the algebraic closure is a similar example. There is no way to write down ‘every field has an algebraic closure’ in Isabelle/HOL in the "straightforward" way because you can't existentially quantify over types. But since the proof works by constructing a an algebraic closure for the type (I forgot how, probably some quotient over some multivariate polynomials over that field or whatever) you can just define something like 'a alg_closure = 'a mpoly set or whatever and then you just prove that "if I have a field of type 'a, then this function gives me a field of type 'a alg_closure that is an algebraic closure of the original field"
Manuel Eberl (Jun 27 2023 at 09:40):Similarly, I once had a student who was proving a statement on groups by induction, and the problem was that in the induction step he had to go from the group G to a quotient group G/H, which doesn't work because you cannot change the type over the thing you're doing induction on from 'a to 'a set.
I think what he ended up doing was to just use the choice operator to pick arbitrary ‘canonical’ representatives for each equivalence class in G/H and defined a group isomorphic go G/H on those instead. Then he could apply the induction hypothesis to that group instead and then pull the result through the isomorphism again to get it for G/H like he wanted.
Manuel Eberl (Jun 27 2023 at 09:42):At the end of the day I think most of these "type quantification problems" in HOL can be reduced simply to "cardinality problems". That is, instead of quantifying over all types just choose one fixed type that is guaranteed to be big enough for everything you want to do. And then just use isomorphism as needed to go in and out of that type. A bit hacky, but it works.
Ghilain Bergeron (Jun 27 2023 at 09:44):Quite unnatural to state and hacky yeah, but if I can keep what I've been working over the last month (instead of starting again from scratch) then I'm quite happy if it has the potential to work!
Ghilain Bergeron (Jun 27 2023 at 09:44):Thanks a lot!
Dmitriy Traytel (Jun 27 2023 at 09:52):Just for completeness: there is a proof of compactness of FOL (or rather clausal logic, which we use in that entry) in the Ordered_Resolution_Prover (theory Inference_System) entry. It is based on completeness, and not on ultraproducts.
Ghilain Bergeron (Jun 27 2023 at 09:59):Unfortunately it is only for unordered ground resolution... :(
Ghilain Bergeron (Jun 27 2023 at 10:00):Oh no sorry, misunderstood the comment above!
Ghilain Bergeron (Jun 27 2023 at 10:02):We'll have to check how to instantiate the locale containing this theorem though, and if it is possible for non-ground clausal logic.
Last updated: Apr 27 2024 at 20:14 UTC