Continuous Logic

Stream: maths

[Keith J. Bauer]

Has anyone ever looked into formalizing theorems of continuous logic?

[Ruben Van de Velde]

Such as?

[Keith J. Bauer]

At this moment, I'm not sure if its basic definitions have been formalized at all, although I also can't say I'm good at searching through libraries.

[Aaron Liu]

I remember helping someone a while ago in #maths > Extensional Equality for Recursively Defined Fuzzy Sets

[Keith J. Bauer]

Ah, maybe I should start using "fuzzy" as a search term?

[Aaron Anderson]

Fuzzy sets and continuous logic are not the same thing, although they are related.

[Aaron Anderson]

Fuzzy set theory is a bit of a catch-all term for systems where asking if a point belongs to a set can give you a non-boolean answer. There are a few main ways this can be developed.

[Aaron Anderson]

Continuous Logic, at least the version that I study, is a variation of model theory using specifically real-valued instead of boolean-valued formulas: https://math.univ-lyon1.fr/~begnac/articles/mtfms.pdf

[Aaron Anderson]

Sometimes, one can take one of these real-valued formulas, and use it to define some fuzzy sets, like in this paper: https://math.univ-lyon1.fr/~begnac/articles/RandomVC.pdf

[Aaron Anderson]

Keith J. Bauer said:

At this moment, I'm not sure if its basic definitions have been formalized at all, although I also can't say I'm good at searching through libraries.

Back to the original question, no, we haven't formalized any of the main definitions. This is something I would like to do, but I've only done a bit of tinkering on my computer. I think it will be a large undertaking.

[James E Hanson]

@Aaron Anderson I know we've talked about this in the past but do you have any intuition about what the right approach to defining formulas would be (i.e., trying to match the formalism of Model Theory for Metric Structures closely vs. taking restricted formulas as the primary notions or something else)?

[Aaron Anderson]

I would start with restricted formulas - restricted in whatever way makes the construction easiest.
Once we have that, I would follow Section 1.4 of your thesis - if L.RestrictedFormula α is the type of restricted formulas in the language L with variables indexed by α, we can use the logical norm to, modulo some theory, provide the instances [SeminormedRing (L.RestrictedFormula α)] [NormedAlgebra ℝ (L.RestrictedFormula α)].

[Aaron Anderson]

Once we have that, mathlib has a good enough understanding of Gelfand duality that defining types and completing to definable predicates is easy:

def CompleteTypeSpace := WeakDual.characterSpace ℝ (SeparationQuotient (L.RestrictedFormula α))

def DefinablePredicate := C(WeakDual.characterSpace ℝ (SeparationQuotient (L.RestrictedFormula α)), ℝ)

[Aaron Anderson]

See https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/CStarAlgebra/GelfandDuality.html

[Aaron Anderson]

Because all of this is done mod some theory, I'd also consider defining L-structures in an extremely vague way, without any Lipschitz constant, uniform continuity, or even continuity axiom on the interpretations of symbols at first, and then work over an ultraproductive theory like you did in https://james-hanson.github.io/publications/ConLogDisLog.pdf

[Aaron Anderson]

I'm less confident in this second suggestion, but I think it could be helpful to have a simple definition of an L-structure, even if basically no theorems would apply at that level.

[Aaron Anderson]

Another thing I've thought about, which I can express for the record - the topometric nature of type spaces is, at least on the face of it, annoying to do - to work with two topologies on the same space, we really need to define two spaces with a bijection between them.

[Aaron Anderson]

My suggestion for how to deal with this is to have a space of complete types, defined as before, with the logic topology, with an injection into the space of partial types. Then we can give the space of partial types a pseudometric, which turns out to be a proper metric on the image of our injection. We can then show that the inverse of this injection is continuous (the metric refines the logic topology).

[Keith J. Bauer]

(I will probably avoid this topic now that I see how much of an undertaking it would be, but I wonder if someone else will try in my stead, inspired by Anderson's road map. I guess time will tell.)

[James E Hanson]

Aaron Anderson said:

Once we have that, mathlib has a good enough understanding of Gelfand duality that defining types and completing to definable predicates is easy:

How easily do you then get the various maps between type spaces (i.e., maps between type spaces corresponding to different sets of variables, different sets of parameters, and different languages)?

[James E Hanson]

Aaron Anderson said:

Another thing I've thought about, which I can express for the record - the topometric nature of type spaces is, at least on the face of it, annoying to do - to work with two topologies on the same space, we really need to define two spaces with a bijection between them.

I remember you mentioning this issue. Is this something that also happens with stuff like the weak* topology on a dual Banach space?

[Aaron Liu]

James E Hanson said:

Aaron Anderson said:

Another thing I've thought about, which I can express for the record - the topometric nature of type spaces is, at least on the face of it, annoying to do - to work with two topologies on the same space, we really need to define two spaces with a bijection between them.

I remember you mentioning this issue. Is this something that also happens with stuff like the weak* topology on a dual Banach space?

docs#NormedSpace.Dual.continuousLinearMapToWeakDual

[Aaron Anderson]

James E Hanson said:

Aaron Anderson said:

Once we have that, mathlib has a good enough understanding of Gelfand duality that defining types and completing to definable predicates is easy:

How easily do you then get the various maps between type spaces (i.e., maps between type spaces corresponding to different sets of variables, different sets of parameters, and different languages)?

Probably reasonably easily. If we can define the map between the Banach spaces of predicates, then we can get the map between type spaces with docs#WeakDual.CharacterSpace.compContinuousMap