A regular logic

definitionlogicmodel-theory

What is a regular logic?

A few posts (such as this question) cite Ebbinghaus/Flum/Thomas, but I don't have a copy of this book. The only definition I have found so far is this article on ncatlab, but I can't say with confidence that it's describing the same thing because I don't know enough about category theory.

This answer links to the ncatlab definition, so it probably refers to the same concept; I'm just not certain.

Here's what I've been able to find so far that doesn't use the notion of being the internal logic of a category.

According to this answer, a regular logic is

A regular logic is closely related to first-order logic: sentences are identified with the classes of structures which satisfy them, and we demand closure under Boolean operations and "relativization".

Relativization is defined here in SEP. More specifically:

If $\mathfrak{M}$ is a structure and $A \subset M$, then $\mathfrak{M}^A$ is obtained by restricting the relations $R^\mathfrak{M}$ and functions $F^\mathfrak{M}$ to $A$. This does not always result in a structure, but if it does, it is called the relativization of $\mathfrak{M}$ in $A$.

Based on these two bits of text, I think that we can assess the regularity of a given logic by inspecting, for each sentence $\varphi$, the class of models $\mathbb{K} = \{ M : M \models \varphi \} $.

After constructing $\mathbb{K}$, though, I'm not sure what to do with it. Relativizing a given $\mathfrak{M}$ with $A \subset M$ does not always produce a structure, let alone a model of $\varphi$. I'm also not sure how to apply boolean operations to a collection of models since the elements of the domain of a model are arbitrary in principle … and I'm really unsure about what the complement of a model would be.

Best Answer

Since this is a bit lengthy, let me open by summarizing. My answer has two parts: the first addresses what I think is the core confusion and gives the simple motivating picture, and the second then gives the full definition of regular logics. Throughout I'm working in some appropriate hyperclass theory for simplicity; as usual, there are various ways to respond to this if one cares, but I don't (at least initially).

I should separately mention Barwise's $1974$ paper Axioms for abstract model theory as an absolutely fantastic resource. (Admittedly the notion of logic which Barwise uses (see Section $7$) is more general than that of a regular logic if memory + a quick glance serve me well.)

Manipulating model classes

It seems to me that you're having a type confusion. You write

"I'm also not sure how to apply boolean operations to a collection of models since the elements of the domain of a model are arbitrary in principle ... and I'm really unsure about what the complement of a model would be."

This seems to be mixing up individual structures and classes of structures, which can be clarified by looking at a single signature.

Fix a signature $\Sigma$ and let $Struc_\Sigma$ be the class of $\Sigma$-structures. We can think of first-order logic, $\mathsf{FOL}$, in a "syntax-free" way by considering the hyperclass (= class of classes) it yields: $$\mathsf{FOL_{semantics}}:=\{Mod(\varphi): \varphi\in\mathsf{FOL}\}.$$ Perhaps surprisingly we can in fact recover some of the syntactical nature of $\mathsf{FOL}$ just from this syntax-free object. For example:

  • The fact that first-order logic has finite conjunctions is reflected in the fact that whenever $\mathbb{A},\mathbb{B}\in\mathsf{FOL_{semantics}}$ we also have $\mathbb{A}\cap\mathbb{B}\in\mathsf{FOL_{semantics}}$. This is because we always have $$Mod(\varphi)\cap Mod(\psi)= Mod(\varphi\wedge\psi).$$ Note that we're not intersecting structures here!

  • Similarly, the fact that first-order logic has negations is reflected in the fact that whenever $\mathbb{C}\in\mathsf{FOL_{semantics}}$ we also have $Struc_\Sigma\setminus\mathbb{C}\in\mathsf{FOL_{semantics}}$. This is because we always have $$Struc_\Sigma\setminus Mod(\varphi)=Mod(\neg\varphi).$$

And it's not just syntax which is reflected in such basic observations: the isomorphism-invariance of first-order logic is reflected in the fact that all elements of $\mathsf{FOL_{semantics}}$ are closed under $\cong$, in the sense that if $\mathcal{A}\in\mathbb{A}\in\mathsf{FOL_{semantics}}$ and $\mathcal{B}\cong\mathcal{A}$ then $\mathcal{B}\in\mathbb{A}$. Note that this is nontrivial, since "the class of all structures with domain $\omega$" is a perfectly meaningful class of structures.

Thinking about the case of first-order logic we might be led to the notion of "regular logic at $\Sigma$:"

A regular logic at $\Sigma$ (for a fixed signature $\Sigma$ is a hyperclass $\mathfrak{X}$ of classes of $\Sigma$-structures with the following properties:

  • For each quantifier-free first-order $\Sigma$-sentence $\varphi$, we have $Mod(\varphi)\in\mathfrak{X}$ (this rules out absurdly weak "logics").

  • $\mathfrak{X}$ is set-sized: there are only set-many classes in $\mathfrak{X}$. (This is somewhat unimportant and can be ignored if you want to; it's just capturing the fact that there are only set-many first-order sentences. Note that a set-sized hyperclass need not be a set!)

  • $\mathfrak{X}$ is closed under finite Boolean operations: if $\mathbb{A},\mathbb{B}\in\mathfrak{X}$ then $\mathbb{A}\cap\mathbb{B}\in\mathfrak{X}$, and if $\mathbb{C}\in\mathfrak{X}$ then $(Struc_\Sigma\setminus\mathbb{C})\in\mathfrak{X}$.

  • Each element of $\mathfrak{X}$ is isomorphism-invariant: if $\mathcal{A}\in\mathbb{A}\in\mathfrak{X}$ and $\mathcal{B}\cong\mathcal{A}$ then $\mathcal{B}\in\mathbb{A}$.

  • Both $\emptyset$ and $Struc_\Sigma$ are in $\mathfrak{X}$ (this is just considering $\top$ and $\perp$ as first-order sentencse).

For example, both second-order logic $\mathsf{SOL}$ and any "small" infinitary $\mathcal{L}_{\kappa,\lambda}$ (restricted to a fixed signature $\Sigma$) fit the above definition. However, even the rather nice "big" infinitary logic $\mathcal{L}_{\infty,\omega}$ does not since it${}$(s associated hyperclass) is not set-sized. Whether this indicates a genuine negative feature of $\mathcal{L}_{\infty,\omega}$ or an error in our definition will depend on one's context.

The full definition

Now this ignores two key features of regular logics - relativization and, far more embarrassingly, quantification. To see these in action we need to consider multiple signatures, and at this point it is convenient to bring in at least a bit of syntax (which is why regular logics are usually defined as pairs $\mathcal{L}=(Sent_\mathcal{L},\models_\mathcal{L})$ rather than as assignments of hyperclasses to signatures).

Here's the full definition:

A (small) regular logic $\mathcal{L}$ is a pair $(Sent_\mathcal{L}, \models_\mathcal{L})$ with the following properties, which I've broken down into sections.

First, the boring properties:

  • $Sent_\mathcal{L}$ is a class relation $\subseteq Signatures\times V$, assigning to each (set-sized) signature $\Sigma$ a set $Sent_\mathcal{L}[\Sigma]$ of "$\mathcal{L}$-sentences in $\Sigma$."

  • $Sent_\mathcal{L}$ is monotonic in the sense that $$\Sigma_0\subseteq \Sigma_1\implies Sent_\mathcal{L}[\Sigma_0]\subseteq Sent_\mathcal{L}[\Sigma_1].$$

  • $\models_\mathcal{L}$ is a class subrelation of $$Structures\times\bigcup_{\Sigma\in Signatures}Sent_\mathcal{L}[\Sigma],$$ with the property that if $(\mathcal{A},\varphi)\in\models_\mathcal{L}$ (or more colloquially, $\mathcal{A}\models_\mathcal{L}\varphi$) then $\varphi\in Sent_\mathcal{L}Sig(\mathcal{A})$.

  • $\models_\mathcal{L}$ is isomorphism-and-reduct-invariant: if $\varphi\in Sent_\Sigma$, $\mathcal{A}\in Struc_{\Sigma_1}$, $\mathcal{B}\in Struc_{\Sigma_2}$, $\Sigma\subseteq \Sigma_1\cap \Sigma_2$, and $\mathcal{A}_{\vert\Sigma}\cong\mathcal{B}_{\vert\Sigma}$, then $$\mathcal{A}\models_\mathcal{L}\varphi\iff\mathcal{B}\models_\mathcal{L}\varphi.$$ (This is usually split up into two criteria, isomorphism invariance and reduct invariance, but I think it makes more sense as a single bulletpoint.)

    • Note that we're using the usual notion of isomorphism here, just as we're not generalizing the notions of "signature" or "structure." The theory of regular logics keeps the "semantic universe" of first-order logic unchanged.

Now the "local niceness" condition:

  • For each signature $\Sigma$ the corresponding hyperclass $$\{\{\mathcal{A}\in Struc_\Sigma:\mathcal{A}\models_\mathcal{L}\varphi\}: \varphi\in Sent_\mathcal{L}[\Sigma]\}$$ is a regular logic at $\Sigma$.

Next, quantifiers (specifically existential quantifiers - we only need one or the other):

  • For each signature $\Sigma$, each constant symbol $c\not\in\Sigma$, and each $\varphi\in Sent_\mathcal{L}[\Sigma\sqcup\{c\}]$, there is some $\psi\in Sent_\mathcal{L}[\Sigma]$ such that for every $\Sigma$-structure $\mathcal{A}$ we have $$\mathcal{A}\models\psi\iff\exists a\in dom(\mathcal{A})\mbox{ such that }\mathcal{A}[c\mapsto a]\models\varphi,$$ where "$\mathcal{A}[c\mapsto a]$" is the $\Sigma\sqcup\{c\}$-structure gotten by expanding $\mathcal{A}$ to interpret $c$ as $a$.

Note that we could have avoided bringing in larger signatures if we'd approached regular logics via formulas instead of sentences. There's a (largely inessential) stylistic choice being made here.

Finally, we just have relativization. I think it's easiest to pose it this way:

  • Suppose $\Sigma$ is a finite signature, $U\not\in\Sigma$ is a unary predicate symbol, and $\varphi$ is a $\Sigma$-sentence. Then there is a $\Sigma\sqcup\{U\}$-sentence $\psi$ such that for every $\Sigma\sqcup\{U\}$-structure$\mathcal{A}$ we have $\mathcal{A}\models\varphi$ iff $U^\mathcal{A}$ is a substructure of $\mathcal{A}$ which satisfies $\varphi$.

Really, though, I'd argue that a stronger form of relativization should be employed - roughly speaking, we should be able to relativize along any "$\mathcal{L}$-interpretation," not just a unary predicate symbol. But at this point we start seriously hitting the point of diminishing returns in terms of the tedium generated. I'd focus on relativization last, and even then focus on relational structures only (so that we don't have to worry about substructurehood).

Related Question