Formalising Continuous Logic

Stream: mathlib4

[Luigi Massacci]

Has anyone given any thought to formalizing continuous logic? Maybe @Aaron Anderson ? I'm trying to do the many-sorted case (so I can talk about dissections of unbounded spaces) but I'm rather unsure as to what to put directly in the language and what to leave to the interpretation. The single-sorted case is more reasonable but I feel less useful.

[Aaron Anderson]

I have indeed thought about this, and I've talked about it to some extent with James Hanson (who I don't think is on this server, but I believe is on the Isabelle Zulip). However, I don't think either of us has written any relevant code.

[Luigi Massacci]

Ok, well as soon as I have something halfway decent I'll write something here and we'll see.

[Aaron Anderson]

James's thesis contains an introduction to continuous logic - I think it includes many of the details relevant for formalization that the standard monograph introducing the subject didn't need to. https://people.math.wisc.edu/logic/theses/hanson.pdf

[Aaron Anderson]

If your only reason for working with the many-sorted case is to work with unbounded spaces, you might actually have an easier time instead using domains of quantification.

[Luigi Massacci]

Yes, the idea was to do the first order theory of Hilbert Spaces / C* algebras / ect by having one sort of each ball of radius n. What do you mean in practice by "using domains of quantification"?

[Luigi Massacci]

I might just stick to the single-sort case though

[Aaron Anderson]

I'm trying to find the best source for this - but the basic idea is to have a single sort which is an unbounded metric space, but every quantifier you use (actually an inf or a sup) is taken only over a particular ball.

[Aaron Anderson]

This is essentially the same as the many-sorted version, where each ball is a different sort, and every quantifier of course has to specify a sort it's quantifying over.

[Aaron Anderson]

I've also had thoughts about the many-sorted version of discrete logic that may be useful, but again, I haven't given it any real effort at a computer.

[Aaron Anderson]

This domains-of-quantification approach was taken waaay back in C. Ward Henson and José Iovino's "Ultraproducts in analysis". You may also want to take a look at this source that does an unbounded version of the logic, but it doesn't seem like the easiest approach to formalize: https://arxiv.org/pdf/0903.4957.pdf

[Luigi Massacci]

Ok. I'll switch to the single-sort case and see how far I can go with that, it will be a good jumping off point for anything else anyway. I did see that paper by Yaakov but it's still a variation on the many-sorted case. Thanks for the link to Hanson's thesis by the way, it looks useful even ignoring the formalization aspects

[Luigi Massacci]

This might betray my ignorance, but if I allow for unbounded metric spaces as structures, won't I loose the compactness theorem? The proof I know constructs the structure that satisfies the whole set of sentences as an ultraproduct, and I'm not sure (fairly confident) that the result is not necessarily a metric space at all if I allow unbounded structures

[Aaron Anderson]

Right - unbounded structures don’t have the compactness theorem, unless you restrict the quantifiers or equivalently model them as a limit of separate sorts.

[Aaron Anderson]

These notes use the idea of an “ultraproductive theory”, which is one where structures are uniformly bounded in the ways that allow for ultraproducts and compactness, rather than putting al that directly in the definition of a metric structure. https://james-hanson.github.io/publications/ConLogDisLog.pdf

[Luigi Massacci]

I'm an idiot, when I wrote that I didn't think that the same process that works for the separate sorts case (splitting up the set of sentences in a way that each subset belongs to some bounded sort, and then do the ultraproducts for each of those) works essentially the same for the bounded quantifier case. I forgot for a moment that sentences have no free variables, and I was scratching my head as to how to handle quantifier free formulas (with free variables) which wouldn't be bounded, but there aren't any! I should get checked. Thanks for the extra set of notes. Also, by now I've become convinced you are right and bounded quantifiers really are the best approach.