Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting

The concept relies on Smullyan’s unifying notation [39], introduced in the same paper, where formulas and their negations are classified as either $\alpha$-, $\beta$-, $\gamma$- or $\delta$-forms. The different forms relate to their respective sub-forms in different ways. The $\alpha$-forms act conjunctively: $\varphi \wedge \psi$ has $\alpha$-form with sub-forms ${\alpha }_1=\varphi$ and ${\alpha }_2=\psi$, but $\neg (\varphi \vee \psi )$ also has $\alpha$-form, with ${\alpha }_1=\neg \varphi$ and ${\alpha }_2=\neg \psi$. The $\beta$-forms act disjunctively: $\varphi \vee \psi$, $\varphi \to \psi$, and $\neg (\varphi \wedge \psi )$ all have $\beta$-form. The $\gamma$-forms act universally, as exemplified by the universal quantifier $\forall x.\varphi (x)$ or the negated existential $\neg (\exists x.\varphi (x))$, where the sub-forms $\gamma (t)$ are (possibly negated) instances of the quantified formulas. Finally, the $\delta$-forms act existentially: $\exists x.\varphi (x)$ and $\neg (\forall x.\varphi (x))$, again with instances, $\delta (t)$, as sub-forms.

The unified notation allows Smullyan to state consistency abstractly and succinctly by introducing consistency properties. Intuitively, a consistency property $C$ is a family of sets of formulas $S\in C$ closed under conditions that ensure that each member set $S$ is non-contradictory when understood as a (possibly infinite) conjunction. For instance, at most one of a propositional letter, $A$, and its negation, $\neg A$, can appear in a member set $S\in C$. Likewise, the consistency of a conjunction in a member set, $\varphi \wedge \psi \in S\in C$, must be evidenced by the consistency of the conjuncts together with the member set, $\{\varphi ,\psi \}\cup S\in C$. The idea is that the member set $S\in C$ is justified by another member set, namely $\{\varphi ,\psi \}\cup S\in C$. In this way, consistency is eventually justified at the level of atomic formulas. The following formulation is adapted from Fitting’s textbook [15] on first-order logic.

Given the above, Smullyan [39, 40] and Fitting [15] each prove variations of the key model existence theorem: Given a first-order consistency property $C$ (over $L$) any set $S\in C$ of sentences is satisfiable (in a Herbrand model over $L^{par}$). The proof relies crucially on imposing finite character on the family $C$, i.e., $\forall S.S\in C\iff (\forall S^{\prime }\subseteq S.\mathrm{𝑓𝑖𝑛𝑖𝑡𝑒}{S}^{\prime }⟶S^{\prime }\in C)$.

Given the axiom of choice, which we assume when working in Isabelle/HOL, finite character guarantees the existence of a maximal element with respect to set inclusion. We want to build our canonical model from exactly this maximal consistent set, by showing that it has various Hintikka properties. A Hintikka set $H$ justifies its own consistency. For example, the Hintikka property corresponding to alpha says that if $\alpha \in H$, then ${\alpha }_1\in H$ and ${\alpha }_2\in H$ as well. For beta, we have that if $\beta \in H$, then ${\beta }_1\in H$ or ${\beta }_2\in H$.

Unfortunately, imposing finite character does not necessarily preserve the delta_E kind as given above. Instead, we must use the following alternate kind that quantifies universally over all new parameters:

delta_A

if $\delta \in S$ then $\{\delta (p)\}\cup S\in C$ for every parameter $p$ new to $S$

The idea is then to recover satisfaction of the original delta_E kind by manually inserting witnesses during the construction of the maximal consistent set with Lindenbaum’s lemma.

The applications of the model existence theorem are many, which is why Smullyan called it a unifying principle. Gödel’s completeness theorem for a given (first-order) proof system follows immediately by proving that the concrete consistency of the proof system constitutes an abstract consistency property. The same model existence result can be reused for different proof systems. Notably, the conditions in Definition 1 all obey the sub-formula property, so we do not need to include cut rules in the proof systems. This is why Smullyan also called these analytic consistency properties [40]. Gentzen’s Hauptsatz, the cut-elimination theorem, is an immediate consequence. The compactness theorem follows by constructing a consistency property from all sets of sentences where every finite subset is satisfiable [15]. A weak version of the downward Löwenheim-Skolem theorem follows by restricting ourselves to a countable language, building a consistency property from all satisfiable sets of sentences, and noticing that the domain of the Herbrand model is also countable [15]. Craig’s interpolation theorem follows by proving that the sets with an interpolant-free partition constitute a consistency property [15]. In all cases, we need to restrict ourselves to sets that leave enough parameters new, so that we can always witness $\delta$-forms.

Approximately 5000 nonblank lines of formal text in Isabelle/HOL 2025 supplement this paper. We include parts of it here via Isabelle/HOL’s LaTeX export (which renders underscores as hyphens). We use the following symbols to denote different kinds of snippets:

• $\mathrm{△}$

  Triangle denotes a term by its assumed type or given definition.

• $\circ$

  Circle denotes the assumption of a lemma or theorem.

• $\therefore$

  Three dots denote the corresponding conclusion.

• $\ast$

  The asterisk denotes a proof obligation in a given context, typically a locale.

We write type variables as ${}^{\prime }$a and function types with $\Rightarrow$. We annotate types with $\mathrm{:}$$\mathrm{:}$. We often prefer Isabelle’s meta-logical universal quantifier, $\bigwedge$, and implication, $⟹$, to their object-logic counterparts $\forall$ and $⟶$. We apply functions and predicates without parentheses, e.g., $fxy$, and make ample use of anonymous functions $\lambda x.e$. The range of a function is its image. The image of a function f on a set S is denoted f ‘ S. We write lists enclosed in square brackets, $[\mathrm{\dots }]$, and use map to apply a function to every element, and set to get the set of elements. Sets are potentially infinite, and we write union ($\cup$), membership ($\in$), etc., as usual. The polymorphic term UNIV denotes the set of all elements of a type. We refer to Nipkow et al.’s book [34] for a thorough introduction.

We make heavy use of Isabelle/HOL’s locales [2]. Locales allow us to abstract over definitions subject to various properties and to build a hierarchy of these. They are key to generalizing consistency without losing user friendliness. For all their benefits, locales are still subject to the limitations of HOL and do not give us quantification over type variables. But, as we show, we can instead compose locales instantiated at the types we care about.

Fitting [16] extended the notion of abstract consistency property to cover term-modal logics with the following kind of condition:

modal

if ${\mathrm{◇}}_t\varphi \in S$ then $\{\varphi \}\cup \{\psi \mid {\mathrm{\square }}_t\psi \in S\}\in C$

The details here are not important. However, the condition has a different shape to Smullyan’s original ones: Fitting does not just extend the set $S$ with a sub-formula but transforms $S$ entirely with a set comprehension. Fitting [14] uses similar conditions to handle intuitionistic logics. This raises a central question of this paper:

How abstract can we make abstract consistency properties?

The kinds of conditions we have seen so far have several flavors: conflict outlaws certain formulas conditionally, while banned forbids them outright; double negation and alpha postulate that certain larger sets must also be consistent; beta postulates that at least one of two larger sets are consistent; gamma has an infinitary character; delta_E and delta_A draw on a set of parameters and are intimately tied to the construction of the maximal set; finally modal transforms the given set entirely. In the end, what matters is that these properties are preserved when we give the family of sets finite character.

In this paper, we mechanize an abstract consistency kind that generalizes all of the above, and build consistency properties over any finite set of such kinds. We implement the textbook definitions as special cases with the following generalizations:

• $\mathrm{■}$

  Some proof systems use gadgets such as labels. To accommodate this, we let the user choose what their “formulas” look like.

• $\mathrm{■}$

  We do not restrict ourselves to sentences.

• $\mathrm{■}$

  We do not restrict ourselves to conditioning on single formulas, but can treat finite sets of formulas as $\alpha$-, $\beta$-, and so on, -forms. This makes it easier to work with proof systems with rules contingent on multiple formulas.

• $\mathrm{■}$

  We generalize gamma to any notion of quantifier and any notion of term, including formulas themselves. Our second-order and hybrid logic examples rely crucially on this.

• $\mathrm{■}$

  We let the universe of terms that gamma quantifies over depend on the set of formulas that contains the $\gamma$-form. Our first-order example demonstrates that we only need to instantiate quantifiers with terms that already occur in the derivation.

• $\mathrm{■}$

  We support uncountable languages.

All of this is enabled by the locale feature [2] of Isabelle/HOL, which allows us to work very abstractly. In particular, we support as varied clauses as the following. For first-order logic (FOL), we evidence the universal quantifier by its instances over the terms at hand:

• $\mathrm{△}$

  $[$ $\forall$p $]$ $\mathrm{⤳}$_γ $($terms$\mathrm{,}$ $\lambda$t$\mathrm{.}$ $[$ $⟨$t$⟩$p $]$$)$

Here, $\forall$p binds de Bruijn variable 0 and $⟨$t$⟩$p instantiates it with the term $t$.

For second-order logic (SOL), we can quantify over first-order terms, function symbols, and predicate symbols, and have three clauses to match, each with its own instantiation:

• $\mathrm{△}$

  $[$ $\forall$p $]$ $\mathrm{⤳}$_γ $($$\lambda$t$\mathrm{.}$ $[$ $⟨$t$/$0$⟩$p $]$$)$

• $\mathrm{△}$

  $[$ $\forall$_F p $]$ $\mathrm{⤳}$_γF $($$\lambda$s$\mathrm{.}$ $[$ $⟨$s$/$0$⟩$_F p $]$$)$

• $\mathrm{△}$

  $[$ $\forall$_P p $]$ $\mathrm{⤳}$_γP $($$\lambda$s$\mathrm{.}$ $[$ $⟨$s$/$0$⟩$_P p $]$$)$

Again, $\forall$p binds de Bruijn variable 0 and $⟨$t$/$0$⟩$p instantiates it with the term $t$.

For Prior’s Ideal Language (PIL) [4], a strong hybrid logic with propositional quantification, we use labels $i,k$ to name the point of evaluation, and these participate freely in our kinds:

• $\mathrm{△}$

  $[$ $($i$\mathrm{,}$ $\mathrm{\square }$p$)$$\mathrm{,}$ $($i$\mathrm{,}$ $\mathrm{◇}$$($$\mathbf{\bullet }$k$)$$)$ $]$ $\mathrm{⤳}$_α $[$$($k$\mathrm{,}$ p$)$$]$

• $\mathrm{△}$

  $[$ $($i$\mathrm{,}$ A p$)$ $]$ $\mathrm{⤳}$_γi $($$\lambda$k$\mathrm{.}$ $[$ $($k$\mathrm{,}$ p$)$ $]$$)$

The first clause states that if $p$ holds everywhere we look, and we can see world $k$, then $p$ holds at $k$. The second clause states that if $p$ holds globally, then $p$ holds at all labels $k$.

The ability to include more than one gamma kind at a time alleviates the absence of dependent types: each gamma can only quantify over one type of terms, but we can simply build our consistency property from multiple gammas. This once again demonstrates that simple type theory is not too simple [9].

In total, our contributions are:

• $\mathrm{■}$

  Abstract machinery for building maximal consistent sets with a wide range of applications.

• $\mathrm{■}$

  Generalized versions of the textbook consistency kinds, pre-defined as special cases using Isabelle/HOL’s locales.

• $\mathrm{■}$

  Completeness proofs for various proof systems for three different logics: first-order logic, second-order logic, and hybrid logic with propositional quantification.

• $\mathrm{■}$

  Compactness for first-order logic over a language of any cardinality.

However, we cannot use different type variables to represent, say, first-order constant symbols and second-order function symbols if we want delta_E kinds for both.

The outline above tells us that parameter substitutions are essential to our development.

In many instances, Isabelle/HOL’s datatype package [6] can automatically generate such operations. By building all our locales on top of this locale, we use the same parameter substitution throughout the development, and users need only prove these properties once.

We want to generalize properties as varied as those we saw in Definition 1: conflict, alpha, beta, etc., and modal too. At the same time, we need to be able to impose finite character on any set subject to these different kinds of conditions.

We note that each kind of condition in a consistency property only applies to a set $S\in C$ when $S$ contains a specific type of formula, and that when it does, this imposes a restriction on $S$ and $C$ specific to that formula. For example, the alpha kind associates $\alpha$-forms with conditions $\{{\alpha }_1,{\alpha }_2\}\cup S\in C$, and says nothing about sets without $\alpha$-forms. However, it does specialize to a Hintikka property on the maximal set. We also need the ability to interpret the (user’s choice of) $\delta$-forms in two different ways: existentially as in delta_E, and universally as in delta_A. This motivates our datatype of kinds.

Conditions have two components: (1) a relation between lists of (contained) formulas and conditions on $C$ and $S\in C$, and (2) a Hintikka property. Witnessings take a formula and a parameter and produce a (possibly empty) list of witnesses. With this definition, we see that a family of sets $C$ can satisfy a kind in three different ways.

We lift the above interpretations to lists of kinds in the expected way.

As outlined earlier, not all kinds suit our needs: the following locale carves out the consistency kinds that behave well with respect to giving the family of sets finite character. To state it, we first need to mechanize the operations needed for the three-step strategy:

• $\mathrm{△}$

  close C $\equiv$ $\{$S$\mathrm{.}$ $($$\exists$S${}^{\prime }$ $\in$ C$\mathrm{.}$ S $\subseteq$ S${}^{\prime }$$)$$\}$ and subset-closed C $\equiv$ $\forall$S${}^{\prime }$ $\in$ C$\mathrm{.}$ $\forall$S $\subseteq$ S${}^{\prime }$$\mathrm{.}$ S $\in$ C

• $\mathrm{△}$

  mk-alt-consistency C $\equiv$ $\{$S$\mathrm{.}$ $($$\exists$f$\mathrm{.}$ map-fm f ‘ S $\in$ C$)$$\}$

• $\mathrm{△}$

  mk-finite-char C $\equiv$ $\{$S$\mathrm{.}$ $($$\forall$S${}^{\prime }$ $\subseteq$ S$\mathrm{.}$ finite S${}^{\prime }$ $⟶$ S${}^{\prime }$ $\in$ C$)$$\}$

We now have all the structure we need for our first central theorem.

From here, Lindenbaum’s construction gives us a way to extend an element $S$ of an alternate consistency property $C$ of finite character into a maximal element. We need a well-ordering of formulas and the assumption that there are enough parameters new to $S$ to ensure consistency of the witnessings. In this more abstract setting than Smullyan and Fitting’s countable infinity, having enough new parameters means that the cardinality of new parameters is at least the cardinality of our universe of formulas.

• $\mathrm{△}$

  enough-new S $\equiv$ $\mid$UNIV $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$fm set$\mid$ $\le$o $\mid$$-$ params S$\mid$

We want to be clear that the enough-new predicate gives a more fine-grained account than extending the language with additional constants, but it does not preclude doing so.

We enumerate formulas by assuming an infinite cardinal order on their universe. Given infinitely many formulas, we can always impose one using the axiom of choice. We use well order recursion [7] to enumerate the consistent sets regardless of the language’s cardinality.

We witness a formula $p$ with respect to a list of kinds Ks by applying any witnessings in Ks to $p$ and a new parameter chosen by Hilbert’s choice operator.

To build the maximal element, we apply the Lindenbaum construction at the transformed consistency property:

• $\mathrm{△}$

  mk-mcs C S $\equiv$ Extend $($mk-alt-fin C$)$ S

The maximal element is consistent, maximal, and witnessed (alternatively $\delta$-complete). Inclusion in the (transformed) consistency property follows from its finite character. We can prove maximality because we closed the consistency property under subsets. Finally, the witnessing follows from the construction. These proofs are all available in the supplementary material. The following theorem consolidates them.

These first three kinds are very similar. Our flexible setup allows us to express conflict and banned from Definition 1 in one notion. Our pre-defined kinds all build on a user-provided relation between a list of formulas and its “consequence”, from which we derive the concrete kind. For Confl, Alpha, and Beta, we simply relate two lists of formulas, and use the infix notations: $\mathrm{⤳}$${}_{\text{<em class="ltx\_emph ltx\_font\_italic" style="font-size:80\%;">✗</em>}}$, $\mathrm{⤳}$_α, and $\mathrm{⤳}$_β, respectively. The user must prove, as the only thing, that parameter substitution preserves the relation. For instance for conflicts:

• $\ast$

  $\bigwedge$ps qs f$\mathrm{.}$ ps $\mathrm{⤳}$${}_{\text{<em class="ltx\_emph ltx\_font\_italic" style="font-size:80\%;">✗</em>}}$ qs $⟹$ map $($map-fm f$)$ ps $\mathrm{⤳}$${}_{\text{<em class="ltx\_emph ltx\_font\_italic" style="font-size:80\%;">✗</em>}}$ map $($map-fm f$)$ qs

We can then define the kinds as follows, recalling that for the variant Cond cond hint of Definition 3, the component cond relates two arguments: the list of formulas it is contingent on, and the induced requirement on $C$ and the set $S\in C$ that contained the formulas.

• $\mathrm{△}$

  ps $\mathrm{⤳}$${}_{\text{<em class="ltx\_emph ltx\_font\_italic" style="font-size:80\%;">✗</em>}}$ qs $⟹$ cond ps $($$\lambda$- S$\mathrm{.}$ set qs $\cap$ S $=$ $\{$$\}$$)$

• $\mathrm{△}$

  ps $\mathrm{⤳}$_α qs $⟹$ cond ps $($$\lambda$C S$\mathrm{.}$ set qs $\cup$ S $\in$ C$)$

• $\mathrm{△}$

  ps $\mathrm{⤳}$_β qs $⟹$ cond ps $($$\lambda$C S$\mathrm{.}$ $\exists$q $\in$ set qs$\mathrm{.}$ $\{$q$\}$ $\cup$ S $\in$ C$)$

Conflicts are requirements only on the set $S$ and state that none of the “consequence” formulas can be present in the set. We can express banned by simply putting the disallowed formula on both sides of the $\mathrm{⤳}$${}_{\text{<em class="ltx\_emph ltx\_font\_italic" style="font-size:80\%;">✗</em>}}$ relation. The Alpha and Beta conditions look like the original ones from Definition 1 with the notable exception that we generalize to lists.

The corresponding Hintikka conditions all follow from the above when the set is maximal:

• $\mathrm{△}$

  $($$\bigwedge$ps qs q$\mathrm{.}$ ps $\mathrm{⤳}$${}_{\text{<em class="ltx\_emph ltx\_font\_italic" style="font-size:80\%;">✗</em>}}$ qs $⟹$ set ps $\subseteq$ H $⟹$ q $\in$ set qs $⟹$ q $\notin$ H$)$ $⟹$ hint H

• $\mathrm{△}$

  $($$\bigwedge$ps qs q$\mathrm{.}$ ps $\mathrm{⤳}$_α qs $⟹$ set ps $\subseteq$ H $⟹$ q $\in$ set qs $⟹$ q $\in$ H$)$ $⟹$ hint H

• $\mathrm{△}$

  $($$\bigwedge$ps qs$\mathrm{.}$ ps $\mathrm{⤳}$_β qs $⟹$ set ps $\subseteq$ H $⟹$ $\exists$q $\in$ set qs$\mathrm{.}$ q $\in$ H$)$ $⟹$ hint H

In Isabelle/HOL concretely, we define each kind as a locale, say Confl, and prove it to be a sub-locale of consistency kinds as given in Definition 7. The proofs follow Fitting’s work [15]. Users instantiate the sub-locale, prove the simpler obligations, and obtain a consistency kind that they can build their consistency property with.

Smullyan and Fitting only instantiate $\gamma$-forms with closed terms (or for term-modal logic [16] ground terms). In this paper, we leave the choice to the user, and work with any type of ${}^{\prime }$tm for which the user provides a parameter substitution map-tm. Due to this flexibility, the user relation looks a bit different for Gamma than for the simpler kinds:

• $\mathrm{△}$

  $\mathrm{⤳}$_γ $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$fm list $\Rightarrow$ $($${}^{\prime }$fm set $\Rightarrow$ ${}^{\prime }$tm set$)$ $\times$ $($${}^{\prime }$tm $\Rightarrow$ ${}^{\prime }$fm list$)$ $\Rightarrow$ bool

Here, we are asking the user to relate a list of formulas to two things: a selection function that turns a set of formulas into a set of terms, and a function that takes a term and instantiates the desired output with that term. The derived kind clarifies the use:

• $\mathrm{△}$

  ps $\mathrm{⤳}$_γ $($F$\mathrm{,}$ qs$)$ $⟹$ cond ps $($$\lambda$C S$\mathrm{.}$ $\forall$t $\in$ F S$\mathrm{.}$ set $($qs t$)$ $\cup$ S $\in$ C$)$

We are bounding the considered terms to the output of the user-provided function on the set $S$. Notably, the user can provide a function that simply ignores its argument and returns whatever list of terms they want to quantify over. We use this function for two of our examples: in first-order logic, we take only the terms of $S$, proving that instantiating with terms that already occur in the derivations is sufficient for completeness; for hybrid logic, we instantiate the propositional quantifiers with formulas that satisfy a specific predicate.

The complementary Hintikka condition states that a single set contains all instances:

• $\mathrm{△}$

  $($$\bigwedge$ps F qs$\mathrm{.}$ ps $\mathrm{⤳}$_γ $($F$\mathrm{,}$ qs$)$ $⟹$ set ps $\subseteq$ H $⟹$ $($$\forall$t $\in$ F H$\mathrm{.}$ set $($qs t$)$ $\subseteq$ H$)$$)$ $⟹$ hint H

The added flexibility imposes extra requirements:

• $\ast$

  $\bigwedge$ps F qs f$\mathrm{.}$ ps $\mathrm{⤳}$_γ $($F$\mathrm{,}$ qs$)$ $⟹$ $($$\exists$G rs$\mathrm{.}$ map $($map-fm f$)$ ps $\mathrm{⤳}$_γ $($G$\mathrm{,}$ rs$)$ $\wedge$

  $($$\forall$S$\mathrm{.}$ map-tm f ‘ F S $\subseteq$ G $($map-fm f ‘ S$)$$)$ $\wedge$

  $($$\forall$t$\mathrm{.}$ map $($map-fm f$)$ $($qs t$)$ $=$ rs $($map-tm f t$)$$)$$)$

• $\ast$

  $\bigwedge$ps F qs S S${}^{\prime }$$\mathrm{.}$ ps $\mathrm{⤳}$_γ $($F$\mathrm{,}$ qs$)$ $⟹$ S $\subseteq$ S${}^{\prime }$ $⟹$ F S $\subseteq$ F S${}^{\prime }$

• $\ast$

  $\bigwedge$ps F qs t A$\mathrm{.}$ ps $\mathrm{⤳}$_γ $($F$\mathrm{,}$ qs$)$ $⟹$ t $\in$ F A $⟹$ $\exists$B $\subseteq$ A$\mathrm{.}$ finite B $\wedge$ t $\in$ F B

The first one states that the user’s relation is compatible with parameter substitutions. The middle requirement restricts the selection function to ensure it behaves well with subsets closure. The last requirement states that selected terms always arise from finite subsets: we need this when giving the family of sets finite character.

We also provide a sub-locale, Gamma-UNIV, that specializes the Gamma locale to the full universe of terms. This simplifies the cases where the extra flexibility clutters the definitions.

The Delta locale is perhaps the simplest of them all, as we simply expose the Wits variant from the base locale (Definition 3). We only ask for a witnessing function that respects parameter substitutions:

• $\mathrm{△}$

  $\delta$ $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$fm $\Rightarrow$ ${}^{\prime }$x $\Rightarrow$ ${}^{\prime }$fm list

• $\ast$

  $\bigwedge$p f x$\mathrm{.}$ $\delta$ $($map-fm f p$)$ $($f x$)$ $=$ map $($map-fm f$)$ $($$\delta$ p x$)$

Our final specialization comes from Fitting’s paper on term-modal logic [16]. It remains future work to use it for a concrete logic and proof system, but we have proved that the locale constitutes a consistency kind as defined in Definition 7.

As the Hintikka property depends on the concrete logic, we make our locale parametric over both that and the relation on formulas. The obligations are similar to those for Gamma.

• $\mathrm{△}$

  $\mathrm{⤳}$_□ $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$fm list $\Rightarrow$ $($${}^{\prime }$fm set $\Rightarrow$ ${}^{\prime }$fm set$)$ $\times$ ${}^{\prime }$fm list $\Rightarrow$ bool

• $\mathrm{△}$

  hint $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$fm set $\Rightarrow$ bool

• $\mathrm{△}$

  ps $\mathrm{⤳}$_□ $($F$\mathrm{,}$ qs$)$ $⟹$ cond ps $($$\lambda$C S$\mathrm{.}$ set qs $\cup$ F S $\in$ C$)$

We have chosen to let the user specify the Hintikka condition associated with their consistency kind. Looking at the ones above, however, we see that they often closely resemble each other. If we had given a more restricted definition of abstract kinds, we might have been able to derive the Hintikka counterpart automatically. However, by using sub-locales, we have provided an interface where they are effectively pre-defined. As such, we have opted for the extra degree of freedom in our base locales. We have also made use of a compositionality that Smullyan and Fitting never seem to spell out explicitly: these kinds are all independent of each other. We do not have to fix a consistency property in advance, as in Definition 1, and provide one big, multi-case proof that we can impose finite character. Instead, we can prove the required properties of each kind separately and assemble the whole afterwards.

We call our first-order logic “bounded” in the sense of From and Jacobsen [22]: the instantiation rule for the universal quantifier only applies to already occurring terms, and we build the model over this bounded domain of terms.

We evaluate our first-order logic on models Model U E F G consisting of a domain U $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$a set, represented explicitly as a set, an environment E $\mathrm{:}$$\mathrm{:}$ nat $\Rightarrow$ ${}^{\prime }$a that maps (de Bruijn) variables to elements of the domain, a function denotation F $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$f $\Rightarrow$ ${}^{\prime }$a list $\Rightarrow$ ${}^{\prime }$a and a predicate denotation G $\mathrm{:}$$\mathrm{:}$ ${}^{\prime }$p $\Rightarrow$ ${}^{\prime }$a list $\Rightarrow$ bool. We only consider well formed models where the environment and function denotations respect the domain:

• $\mathrm{△}$

  wf-model $($Model U E F G$)$ $⟷$ $($$\forall$n$\mathrm{.}$ E n $\in$ U$)$ $\wedge$ $($$\forall$f ts$\mathrm{.}$ F f ts $\in$ U$)$

Higher-order logic makes the semantics straightforward to express. Note that bolded connectives, e.g. $⟶$, belong to the embedded logic (here first-order logic).

• $\mathrm{△}$

  $($- $\vDash$ $\perp$$)$ $=$ False

• $\mathrm{△}$

  $($Model - E F G $\vDash$ $\cdot$P ts$)$ $=$ G P $($map $⟨|$$($E$\mathrm{,}$ F$)$$|⟩$ ts$)$

• $\mathrm{△}$

  $($Model U E F G $\vDash$ p $⟶$ q$)$ $=$ $($Model U E F G $\vDash$ p $⟶$ Model U E F G $\vDash$ q$)$

• $\mathrm{△}$

  $($Model U E F G $\vDash$ $\forall$p$)$ $=$ $($$\forall$x $\in$ U$\mathrm{.}$ Model U $($x $>>$ E$)$ F G $\vDash$ p$)$

The map $⟨|$-$|⟩$ evaluates terms to elements of the domain. Terms are either variables or function symbols applied to a list of terms. The operation x $>>$ E shifts environment $E$ by mapping variable 0 to $x$ and every other variable $n+1$ to $En$.

From these semantics, we write out the abstract consistency property in Figure 1 using the pre-defined kinds. Falsity conflicts with itself and negated predicates conflict with their non-negated counterparts. Negated implication has an $\alpha$-form, while implication itself has $\beta$-form. For the positive quantifier, we only instantiate with the terms of the given set, and for the negative quantifier we simply instantiate with a constant (denoted by the star). The declarations in Figure 1 are valid Isabelle/HOL code, and, in our opinion, almost as readable as the textbook declarations that we started from in Definition 1.

We use a Herbrand model with a small twist as our canonical model:

• $\mathrm{△}$

  canonical H $\equiv$

  Model $($terms H$)$ $($$\lambda$n$\mathrm{.}$ $\mathrm{\#}$n $\in$? terms H$)$ $($$\lambda$f ts$\mathrm{.}$ $\mathrm{○}$f ts $\in$? terms H$)$ $($$\lambda$P ts$\mathrm{.}$ $\cdot$P ts $\in$ H$)$

Here, $\mathrm{\#}$ and $\mathrm{○}$ form variables and composed terms, respectively. The domain consists only of the terms of the given (maximal consistent) set $H$. To guarantee well formedness, we guard the denotations with $\in$?, which returns the left-hand side if the right-hand side contains it, and an arbitrary element of the right-hand side otherwise. Assuming at least one term, we prove a truth lemma for the canonical model by induction on the size of the formula, using the Hintikka properties of the set to discharge each case.

Figure 2 shows a natural deduction system for first-order logic with two notable details: we are using sets of formulas, and we can only eliminate the universal quantifier with a term from the derivation. Proving completeness directly for this restricted calculus is a stronger result than typically found. We prove soundness over well formed models by rule induction. For strong completeness, we show that the sets from which we cannot derive falsity (and which leave enough parameters new) form a consistency property. Concretely we instantiate the derivational locales, benefitting from the close correspondence between Figures 1 and 2.

If we prefer lists of assumptions to sets, we can easily modify the proof system in Figure 2 to use lists instead. Strong completeness of the resulting system (if $p$ follows from a set $A$ then we can derive $p$ from a list of elements from $A$) follows by noticing that each proof rule in Figure 2 relies only on a finite kernel of formulas. Rule induction lets us go from a set derivation to derivation from a list of formulas, reusing the completeness result.

The supplementary material contains strong completeness for a tableau system whose elimination rule is limited to the already occurring terms. Since we can reuse model existence, we can define this system and prove its soundness and completeness in less than 150 lines of Isabelle/HOL. Reusing model existence to prove compactness takes around 200 lines. The first-order logic example in total consists of around 1000 lines.

We use the framework to obtain the, to our knowledge, first formalization in Isabelle/HOL of second-order logic and a natural deduction system for it. We also use the framework to obtain the, to our knowledge, first formalization in a proof assistant of an axiomatic system for second-order logic. The formalization of the syntax and semantics of second-order logic generalizes a formalization of first-order logic by From [18, 24]. The generalization consists of three steps. (1) defining predicate and function symbols as being either proper symbols or variables. (2) Using these symbols in the definition of predicate and function applications. (3) Introducing two new quantifiers – one, $\forall$_F, that binds variables to functions and another, $\forall$_P, that binds variables to predicates. Second-order logic is famously incomplete for standard models [33] where the quantifiers range over all functions and predicates over the universe. However completeness holds when considering general models, i.e., models that include the sets of predicates and functions over which the quantifiers can range. We formalize the latter. Note that we do not consider frugal models [1]; we do not know the sizes of the models.

A general model for our second-order logic is a tuple $(E,E_F,E_P,C,F,G,PS,FS)$, where $E::nat\Rightarrow {}_{}{}^{\prime }a$ is the environment for variables over elements, ${}_{}{}^{\prime }a$ is the type representing the domain or universe, $E_F::nat\Rightarrow {(}^{\prime }alist\Rightarrow {}_{}{}^{\prime }a)$ is the environment for function variables, $E_P::nat\Rightarrow {(}^{\prime }alist\Rightarrow bool)$ is the environment for predicate variables, $C::{}_{}{}^{\prime }b\Rightarrow {}_{}{}^{\prime }a$ is the constant denotation, $F::{}_{}{}^{\prime }b\Rightarrow {(}^{\prime }alist\Rightarrow {}_{}{}^{\prime }a)$ is the function denotation, $G::{}_{}{}^{\prime }b\Rightarrow {(}^{\prime }alist\Rightarrow bool)$ is the predicate denotation, $PS::{(}^{\prime }alist\Rightarrow bool)set$ is the predicate universe and $FS::{(}^{\prime }alist\Rightarrow bool)set$ is the function universe. A model is well formed when its predicate/function environments and denotations stay within the defined universes:

• $\mathrm{△}$

  wf-model $($E$\mathrm{,}$ E_F$\mathrm{,}$ E_P$\mathrm{,}$ C$\mathrm{,}$ F$\mathrm{,}$ G$\mathrm{,}$ PS$\mathrm{,}$ FS$)$ $⟷$

  range G $\subseteq$ PS $\wedge$ range E_P $\subseteq$ PS $\wedge$ range F $\subseteq$ FS $\wedge$ range E_F $\subseteq$ FS

Since the universe of elements is represented by the type ${}^{\prime }$a, the typing of $E$ and $C$ already ensures that these stay within the universe.

The conflict, alpha, and beta kinds are the same as for bounded first-order logic in Figure 1. Figure 3 defines gamma and delta rules for second-order logic that correspond to the three universal quantifiers of the language. Notably, we can use the framework with both single-point substitution (here) and simultaneous substitution (for FOL and PIL). We again build a Herbrand model over the resulting maximal consistent set. We do not care about distinguishing open and closed formulas, though such a distinction could easily be made by tweaking the consistency property and canonical model. Model existence follows almost immediately from the Hintikka properties.

Our axiomatic system for second-order logic generalizes From’s work [18, 24] by introducing axioms and rules for the second-order quantifiers. The rules are generalization rules for introducing universal quantifications over predicates and functions, respectively. The axioms are instantiation axioms stating that universal quantifications, over respectively predicates and functions, imply their immediate sub-formula with the quantified variable substituted with any symbol. Our natural deduction system is a variant of the natural deduction system for the first-order logic above without the elimination limitation, but with introduction and elimination rules for the second-order quantifiers. We prove weak completeness for the axiomatic system and strong completeness for the natural deduction system. The entire development consists of under 1200 lines.

We have mechanized the completeness of a recently developed [4] strong hybrid logic with propositional quantification. The combination of Kripke semantics and propositional quantification gives some second-order expressibility, resulting in a system of significant strength. The mechanization of this example consists of just under 1800 lines.

We interpret the logic on Kripke models with explicit sets of admissible propositions. This set must be closed under relative complement, finite intersection and modal projection, corresponding to negation, conjunction and the box modality. The three most interesting cases for the semantics are the global modality, downarrow binder, and propositional quantification:

• $\mathrm{△}$

  $($$($M$\mathrm{,}$ -$)$ $\vDash$ A p$)$ $=$ $($$\forall$v $\in$ $𝒲$ M$\mathrm{.}$ $($M$\mathrm{,}$ v$)$ $\vDash$ p$)$

• $\mathrm{△}$

  $($$($M$\mathrm{,}$ w$)$ $\vDash$ $\downarrow$ p$)$ $=$ $($$($M$(\mid$$𝔑$ $\mathrm{:}$$=$ $($w $>>$ $𝔑$ M$)$$\mid )$$\mathrm{,}$ w$)$ $\vDash$ p$)$

• $\mathrm{△}$

  $($$($M$\mathrm{,}$ w$)$ $\vDash$ $\forall$ p$)$ $=$ $($$\forall$P $\in$ $\mathrm{\Pi }$ M$\mathrm{.}$ $($M$(\mid$$𝔙$ $\mathrm{:}$$=$ $($P $>>$ $𝔙$ M$)$$\mid )$$\mathrm{,}$ w$)$ $\vDash$ p$)$