A Canonical Model for Constant Domain Basic First-Order Logic

TL;DR

This paper constructs a canonical model for constant domain basic first-order logic (BQLCD) and demonstrates that it satisfies key logical properties like disjunction and existence, advancing the understanding of BQLCD's foundational aspects.

Contribution

The paper introduces a canonical model for BQLCD and verifies important logical properties, providing a foundational framework for this logic system.

Findings

BQLCD satisfies disjunction property

BQLCD satisfies existence property

Canonical model effectively demonstrates these properties

Abstract

I build a canonical model for constant domain basic first-order logic (BQLCD), the constant domain first-order extension of Visser's basic propositional logic, and use the canonical model to verify that BQLCD satisfies the disjunction and existence properties.

Equations

$${\text{BQL}}_{\text{CD}}$$

$$\top \to \varphi \vee \forall v(\top \to \psi )\forall v(\top \to \varphi \vee \psi )$$

$$|c|(\overline{a})$$

$$|v_i|(\overline{a})$$

$$|f^n(t_1,...,t_n)|(\overline{a})$$

$$w$$

$$w⊩R^n(t_1,...,t_n)(\overline{a})$$

$$w⊩(\varphi \wedge \psi )(\overline{a})$$

$$w⊩(\varphi \vee \psi )(\overline{a})$$

$$w⊩(\varphi \to \psi )(\overline{a})$$

$$w⊩\exists v\varphi (\overline{a})$$

$$w⊩\forall v\varphi (\overline{a})$$

$$[\top ](\top \text{-Int})\varphi \perp$$

$$\varphi \wedge \psi \text{lx@proof@logical@and}\varphi \psi \varphi /\psi \varphi \wedge \psi$$

$$\varphi \vee \psi \varphi /\psi \chi \text{lx@proof@logical@and}\varphi \vee \psi \chi [\varphi ]\chi [\psi ]$$

$$\varphi \to \psi \psi [\varphi ]\varphi \to \chi \text{lx@proof@logical@and}\varphi \to \psi \psi \to \chi$$

$$\varphi \to \psi \wedge \chi \text{lx@proof@logical@and}\varphi \to \psi \varphi \to \chi \varphi \vee \psi \to \chi \text{lx@proof@logical@and}\varphi \to \chi \psi \to \chi$$

$$\varphi \to \forall v\psi \forall v(\varphi \to \psi )\exists v\varphi \to \psi \forall v(\varphi \to \psi )$$

$$\forall v\varphi \varphi (a_i)\varphi (t)\forall v\varphi \varphi \vee \forall v\psi \forall v(\varphi \vee \psi )$$

$$\exists v\varphi \varphi (t)\psi \text{lx@proof@logical@and}\exists v\varphi \psi [\varphi (a_i)]$$

$$\psi \text{lx@proof@logical@and}\varphi \varphi \to \psi \mathcal{N}{\text{BQL}}_{\text{CD}}\Sigma$$

$$\text{lx@proof@logical@and}...\psi \text{lx@proof@logical@and}\varphi \varphi \to \psi {\chi }^i...$$

$$\bigwedge \Gamma \to \top [\top ]$$

$$\bigwedge \Gamma \to \varphi \varphi$$

$$\bigwedge \Gamma \to \varphi \varphi \wedge \text{-Elims}[\bigwedge \Gamma ]$$

$$\varphi \alpha {\Sigma }^{\prime },\Gamma$$

$$\bigwedge \Gamma \to \varphi \text{lx@proof@logical@and}\bigwedge \Gamma \to \alpha {\Sigma }^{\prime }\alpha \to \varphi \varphi [\alpha ]$$

$$\varphi \text{lx@proof@logical@and}\alpha {\Sigma }^{\prime },\Gamma \beta {\Sigma }^{\prime },\Gamma$$

$$\bigwedge \Gamma \to \varphi \text{lx@proof@logical@and}\bigwedge \Gamma \to \alpha \wedge \beta \text{lx@proof@logical@and}\bigwedge \Gamma \to \alpha {\Sigma }^{\prime }\bigwedge \Gamma \to \beta {\Sigma }^{\prime }\alpha \wedge \beta \to \varphi \varphi \text{lx@proof@logical@and}\alpha [\alpha \wedge \beta ]\beta [\alpha \wedge \beta ]$$

$$\varphi \text{lx@proof@logical@and}\alpha \vee \beta {\Sigma }^{\prime },\Gamma \varphi {\Sigma }^{\prime },\Gamma ,[\alpha ]\varphi {\Sigma }^{\prime },\Gamma ,[\beta ]$$

$$\top \to \varphi \text{lx@proof@logical@and}\top \to \alpha \vee \beta {\Sigma }^{\prime }\alpha \vee \beta \to \varphi \text{lx@proof@logical@and}\alpha \to \varphi {\Sigma }^{\prime }\beta \to \varphi {\Sigma }^{\prime }$$

$$\bigwedge \Gamma \wedge (\alpha \vee \beta )\to \varphi \text{lx@proof@logical@and}\bigwedge \Gamma \wedge (\alpha \vee \beta )\to (\bigwedge \Gamma \wedge \alpha )\vee (\bigwedge \Gamma \wedge \beta )(\bigwedge \Gamma \wedge \alpha )\vee (\bigwedge \Gamma \wedge \beta )[\bigwedge \Gamma \wedge (\alpha \vee \beta )](\bigwedge \Gamma \wedge \alpha )\vee (\bigwedge \Gamma \wedge \beta )\to \varphi \text{lx@proof@logical@and}(\bigwedge \Gamma \wedge \alpha )\to \varphi {\Sigma }^{\prime }(\bigwedge \Gamma \wedge \beta )\to \varphi {\Sigma }^{\prime }$$

$$\bigwedge \Gamma \to \varphi \text{lx@proof@logical@and}\bigwedge \Gamma \to \bigwedge \Gamma \wedge (\alpha \vee \beta )\text{lx@proof@logical@and}\bigwedge \Gamma \to \bigwedge \Gamma [\bigwedge \Gamma ]\bigwedge \Gamma \to \alpha \vee \beta {\Sigma }^{\prime }\bigwedge \Gamma \wedge (\alpha \vee \beta )\to \varphi {\Sigma }^{\prime }$$

$$\varphi \to \psi \psi {\Sigma }^{\prime },\Gamma ,[\varphi ]$$

Full text

1. Introduction

Basic propositional logic (BPL) is the subintuitionistic propositional logic obtained by dropping the requirement on the Kripke models for intuitionistic propositional logic (IPL) that the accessibility relation is reflexive. Most notably, dropping reflexivity invalidates modus ponens. Visser [7] introduced BPL and proved completeness by building a canonical model. Basic first-order logic (BQL), introduced by Ruitenburg [6], is the subintuitionistic first-order extension of BPL obtained by (i) dropping the requirement on the Kripke models for intuitionistic first-order logic (IQL) that the accessibility relation is reflexive, (ii) restricting the object language by replacing the clause $\phi:\forall v\phi$ in the inductive definition of formulas with the clause $\phi,\psi:\forall\overline{v}(\phi\rightarrow\psi)$ and (iii) setting $w\Vdash\forall\overline{v}(\phi\rightarrow\psi)(\overline{a})$ iff for every $u\succ w$ and all $\overline{b}\in dom(u)$: $u\Vdash\phi(\overline{a},\overline{b})$ only if $u\Vdash\psi(\overline{a},\overline{b}).$111This definition of BQL differs from the definition given in Ruitenburg’s original paper [6]. We identify BQL with the set of pairs $\langle\Gamma,\phi\rangle$ such that for every world $w$ in every BQL model: $w\Vdash\Gamma$ only if $w\Vdash\phi$ (where $\Gamma\cup\{\phi\}$ is a set of sentences in the language of BQL). By contrast, Ruitenburg identifies BQL with the set of sequents $\phi\implies\psi$ such that for every world $w$ in every BQL model: $w\Vdash\phi$ only if $w\Vdash\psi$ (where $\phi$ and $\psi$ are sentences in the language of BQL). So our definition of BQL essentially generalizes Ruitenburg’s definition to allow for arbitrarily many (including zero) premises. A natural way of extending BQL to the full object language was suggested by Restall [5], who advocated restricting the BQL models to those with constant domains and giving $\forall$ its classical satisfaction condition.222Restall also added an actual world and required the actual world see itself, thereby regaining modus ponens. We do not take this approach here. This results in constant domain basic first-order logic ($\textsf{BQL}_{\textsf{CD}}$). The relationship between $\textsf{BQL},\textsf{BQL}_{\textsf{CD}}$ and their intuitionistic counterparts is pictured below:333We identify a logic L with the set of pairs $\langle\Gamma,\phi\rangle$ such that $\Gamma\models_{\textsf{L}}\phi$.

[TABLE]

The proper inclusion $\textsf{BQL}\subset\textsf{BQL}_{\textsf{CD}}$ holds even when we restrict $\textsf{BQL}_{\textsf{CD}}$ to the language of BQL, as witnessed by the fact that the inference

[TABLE]

is valid in $\textsf{BQL}_{\textsf{CD}}$ but not in BQL. Restall attempted to prove completeness for $\textsf{BQL}_{\textsf{CD}}$ by building a canonical model but was unable to do so. More recently, Ishigaki and Kikuchi [2] proved completeness for $\textsf{BQL}_{\textsf{CD}}$ using a tree-sequent calculus. However, a canonical model proof of completeness would be preferable, since we could use the canonical model to verify that $\textsf{BQL}_{\textsf{CD}}$ satisfies the disjunction and existence properties. The major impediment to generalizing Visser’s canonical model construction for BPL to $\textsf{BQL}_{\textsf{CD}}$ is ensuring the existence of witnesses when extending prime saturated $\textsf{BQL}_{\textsf{CD}}$-theories to larger prime saturated $\textsf{BQL}_{\textsf{CD}}$-theories. Ordinarily, the existence of witnesses is guaranteed by adding fresh constant symbols to the object language. However, this would result in a Kripke model with varying domains. The same problem arises when trying to generalize the canonical model construction for IPL to $\textsf{IQL}_{\textsf{CD}}$. In the case of $\textsf{IQL}_{\textsf{CD}}$, a solution has been found (Gabbay, Shehtman and Skvortsov [1]). In this paper, I build a canonical model for $\textsf{BQL}_{\textsf{CD}}$ by carrying over the solution for $\textsf{IQL}_{\textsf{CD}}$. I use the canonical model to verify that $\textsf{BQL}_{\textsf{CD}}$ satisfies the disjunction and existence properties.

2. Constant Domain Basic First-Order Logic

2.1. Model Theory

Let $\mathcal{L}$ be a first-order language with primitive operators $\top$, $\bot$, $\wedge$, $\vee$, $\rightarrow$, $\forall$, $\exists$. A transitive frame is a pair $\langle W,\prec\rangle$ such that $W$ is a non-empty set (the set of worlds) and $\prec$ is a transitive binary relation on $W$ (the accessibility relation). An $\mathcal{L}$-model (for $\textsf{BQL}_{\textsf{CD}}$) is a $4$-tuple $\mathfrak{M}=\langle W,\prec,M,|\mathord{\cdot}|\rangle$ such that $\langle W,\prec\rangle$ is a transitive frame, $M$ is a non-empty set (the domain of quantification) and $|\mathord{\cdot}|$ is a function whose domain is the signature of $\mathcal{L}$ such that $|c|\in M$, $|f^{n}|:M^{n}\rightarrow M$ and $|R^{n}|:W\rightarrow\mathcal{P}(M^{n})$, subject to the constraint that $w\prec u$ only if $|R^{n}|(w)\subseteq|R^{n}|(u)$. For a term $t(\overline{v})\in\mathcal{L}$ and $\overline{a}\in M^{n}$, we recursively define $|t|(\overline{a})$ as follows:

[TABLE]

For a formula $\phi(\overline{v})\in\mathcal{L},\overline{a}\in M^{n}$ and $w\in W$, we inductively define $\mathfrak{M},w\Vdash\phi(\overline{a})$ as follows (suppressing $\mathfrak{M}$ for brevity):

[TABLE]

It follows by omission that $w\not\Vdash\bot(\overline{a})$.

Theorem 1** (Persistence).**

If $w\Vdash\phi(\overline{a})$ and $w\prec u$ then $u\Vdash\phi(\overline{a})$.

Proof.

An easy induction on the construction of $\mathcal{L}$-formulas. ∎

For sentences $\Gamma\cup\{\phi\}\subseteq\mathcal{L}$, we write $\Gamma\models\phi$ iff for every $\mathcal{L}$-model $\mathfrak{M}$ and every world $w\in\mathfrak{M}$: $w\Vdash\Gamma$ only if $w\Vdash\phi$.

Theorem 2** (Conditional Proof).**

If $\Gamma,\phi\models\psi$ then $\Gamma\models\phi\rightarrow\psi$.

Proof.

Suppose $\Gamma\not\models\phi\rightarrow\psi$. Then there exist $w\in\mathfrak{M}$ such that $w\Vdash\Gamma$ and $w\not\Vdash\phi\rightarrow\psi$. So $u\Vdash\phi$ and $u\not\Vdash\psi$ for some $u\succ w$. By Persistence, $u\Vdash\Gamma$. But then $\Gamma,\phi\not\models\psi$. ∎

Theorem 3** (Weak Modus Ponens).**

For $\Gamma\subseteq\mathcal{L}\setminus\{\rightarrow\}$: if $\Gamma\models\phi\rightarrow\psi$ then $\Gamma,\phi\models\psi$.

Proof.

Suppose $\Gamma,\phi\not\models\psi$. Then there exist $w\in\mathfrak{M}$ such that $w\Vdash\Gamma\cup\{\phi\}$ and $w\not\Vdash\psi$. Take the submodel of $\mathfrak{M}$ generated by $w$. Add a new world $u$ below $w$ such that $|R^{n}|(u)=|R^{n}|(w)$. Then $u\Vdash\Gamma$ and $u\not\Vdash\phi\rightarrow\psi$. So $\Gamma\not\models\phi\rightarrow\psi$. ∎

Theorem 4** (Compactness).**

If $\Gamma\models\phi$ then $\Gamma_{0}\models\phi$ for some finite $\Gamma_{0}\subseteq\Gamma$.

Proof.

Similar to the ultraproduct proof of compactness for classical first-order logic (see e.g. Poizat [3]). ∎

2.2. Proof Theory

We formulate the natural deduction system $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$ for $\textsf{BQL}_{\textsf{CD}}$ in the language $\mathcal{L}^{+}=\mathcal{L}\cup\{a_{i}\}_{i\in\omega}$, where each $a_{i}$ is a fresh constant symbol (the $a_{i}$ serve in proofs as names of arbitrarily chosen objects). $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$ consists of all trees of (possibly discharged) $\mathcal{L}^{+}$-sentences constructed in accordance with the following inference rules:444By restricting the formulas linked by an inference rule to sentences we determine which free variables, if any, a subformula may contain (e.g. $\phi$ may not contain free variables in CD).

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

In $\forall$-Int, $a_{i}$ does not occur in $\phi$ or in any open assumption in the main subproof. In $\exists$-Elim, $a_{i}$ does not occur in $\phi$, $\psi$ or in any open assumption besides $\phi(a_{i})$ in the right main subproof. We write $\Gamma\vdash\phi$ iff there exists a proof of $\phi$ from $\Gamma$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Theorem 5** (Soundness).**

If $\Gamma\vdash\phi$ then $\Gamma\models\phi$.

Proof.

By induction on the construction of proofs in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$. The base case is easy. The induction steps are also easy except for $\rightarrow$-Int, where we appeal to Conditional Proof. ∎

Lemma 1** (Distribution).**

$\phi\wedge(\psi\vee\chi)\vdash(\phi\wedge\psi)\vee(\phi\wedge\chi)$.

Lemma 2** (Infinite Distribution).**

$\phi\wedge\exists v\psi\vdash\exists v(\phi\wedge\psi)$.

For sentences $\Sigma\subseteq\mathcal{L}^{+}$, let $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$ denote the natural deduction system obtained by adding the rule

[TABLE]

to $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$ and adding a restriction which states that (i) no occurrence $\chi^{i}$ of an open assumption in position

[TABLE]

can be discharged (we say that such occurrences are unsafe) and (ii) no occurrence of $\phi(a_{i})$ in the right main subproof of $\exists$-Elim is unsafe. Write $\Gamma\vdash_{\Sigma}\phi$ iff there exists a proof of $\phi$ from $\Gamma$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. To state the next lemma concisely, let $\bigwedge\emptyset=\top$.

Lemma 3** (Relative Deduction).**

For $|\Gamma|<\omega$, if there exists a proof $\Pi\in\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$ of $\phi$ from $\Sigma^{\prime}\cup\Gamma$ such that every open assumption which occurs unsafely in $\Pi$ is contained in $\Sigma^{\prime}$ then $\Sigma^{\prime}\vdash\bigwedge\Gamma\rightarrow\phi$.

Proof.

By induction on the construction of proofs in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$.

Base Case Suppose we have a one-line proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$ of $\phi$ from $\Sigma^{\prime}\cup\Gamma$. There are three cases.

Case 1 $\phi=\top$. Then

[TABLE]

is a proof of $\bigwedge\Gamma\rightarrow\phi$ from $\Sigma^{\prime}$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 2 $\phi\in\Sigma^{\prime}$. Then

[TABLE]

is a proof of $\bigwedge\Gamma\rightarrow\phi$ from $\Sigma^{\prime}$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 3 $\phi\in\Gamma$. Then

[TABLE]

is a proof of $\bigwedge\Gamma\rightarrow\phi$ from $\Sigma^{\prime}$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Induction Steps There are seven cases.

Case 1 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$, where the final inference is $\bot$-Elim, $\wedge$-Elim, $\vee$-Int, Internal $\forall$-Int, Internal $\exists$-Elim, $\forall$-Elim, CD or $\exists$-Int. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 2 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$, where the final inference is $\wedge$-Int, Internal Transitivity, Internal $\wedge$-Int or Internal $\vee$-Elim. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 3 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. Since unsafe occurrences cannot be discharged, if $\alpha$ occurs unsafely in the center main subproof then $\alpha\in\Sigma^{\prime}$, and the same goes for $\beta$ in the right main subproof. There are two subcases to consider.

Subcase 1 $\Gamma=\emptyset$. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Subcase 2 $\Gamma\neq\emptyset$. Then, by Distribution and the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$. So, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 4 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. Since unsafe occurrences cannot be discharged, if $\phi$ occurs unsafely in the main subproof then $\phi\in\Sigma^{\prime}$. There are two subcases to consider.

Subcase 1 $\Gamma=\emptyset$. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Subcase 2 $\Gamma\neq\emptyset$. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 5 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 6 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. Let $\Sigma^{*}\subseteq\Sigma^{\prime},\Gamma^{*}\subseteq\Gamma$ contain exactly the open assumptions in the main subproof. Then $a_{i}$ does not occur in $\Sigma^{*}\cup\Gamma^{*}\cup\{\phi\}$. So, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Case 7 Suppose we have a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. Let $\Sigma^{*}\subseteq\Sigma^{\prime},\Gamma^{*}\subseteq\Gamma$ contain exactly the open assumptions other than $\psi(a_{i})$ in the right main subproof. Then $a_{i}$ does not occur in $\Sigma^{*}\cup\Gamma^{*}\cup\{\psi,\phi\}$. Furthermore, since $\psi(a_{i})$ does not occur unsafely in the right main subproof, $\Sigma^{*}$ contains all open assumptions which occur unsafely in the right main subproof.

Subcase 1 $\Gamma^{*}=\emptyset$. Then, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$.

Subcase 2 $\Gamma^{*}\neq\emptyset$. Then, by Infinite Distribution and the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$. So, by the induction hypothesis, we can find a proof of the form

[TABLE]

in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}$. ∎

Corollary 1**.**

For $|\Gamma|<\omega$, if $\Sigma,\Gamma\vdash_{\Sigma}\phi$ then $\Sigma\vdash\bigwedge\Gamma\rightarrow\phi$.

3. The Canonical Model

In order to prove the existence of the canonical model, we need to assume that $\mathcal{L}$ is countable (see Relative Extension below for an explanation). Fortunately, we can use compactness to leverage up our canonical model proofs of completeness, the disjunction property and the existence property to $\mathcal{L}$ of arbitrary cardinality.

A set of sentences $\Gamma\subseteq\mathcal{L}^{+}$ is called a prime saturated $\textsf{BQL}_{\textsf{CD}}$-theory iff $\Gamma$ satisfies the following properties:

[TABLE]

Let $Sat(\textsf{BQL}_{\textsf{CD}})$ denote the set of prime saturated $\textsf{BQL}_{\textsf{CD}}$-theories.

Lemma 4** (Extension).**

For $\Gamma$ such that $|\{i:a_{i}\not\in\Gamma\}|=\omega$: if $\Gamma\not\vdash\phi$ then there exists $\Gamma^{*}\supseteq\Gamma$ such that $\Gamma^{*}\in Sat(\textsf{BQL}_{\textsf{CD}})$ and $\phi\not\in\Gamma^{*}$.

Proof.

Similar to the proof of the Belnap Extension Lemma (see e.g. Priest [4] §6.2), except we draw witnesses from $\{a_{i}\}_{i\in\omega}$. Since $\mathcal{L}$ is countable, the assumption that $|\{i:a_{i}\not\in\Gamma\}|=\omega$ ensures we never run out of witnesses. ∎

Lemma 5** ($\exists$-Witness).**

For $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$, $|\Gamma|<\omega$: if $\Sigma,\Gamma,\psi(t)\vdash_{\Sigma}\phi$ for every $t\in\mathcal{L}^{+}$ then $\Sigma,\Gamma,\exists v\psi\vdash_{\Sigma}\phi$.

Proof.

Suppose $\Sigma,\Gamma,\psi(t)\vdash_{\Sigma}\phi$ for every $t\in\mathcal{L}^{+}$. There are two cases.

Case 1 $\Gamma=\emptyset$. Then, by Relative Deduction, $\Sigma\vdash\psi(t)\rightarrow\phi$ for every $t\in\mathcal{L}^{+}$. Since $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$, $\Sigma\vdash\forall v(\psi\rightarrow\phi)$. So $\Sigma\vdash\exists v\psi\rightarrow\phi$. But then $\Sigma,\exists v\psi\vdash_{\Sigma}\phi$.

Case 2 $\Gamma\neq\emptyset$. Then, by Relative Deduction, $\Sigma\vdash\bigwedge\Gamma\wedge\psi(t)\rightarrow\phi$ for every $t\in\mathcal{L}^{+}$. Since $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$, $\Sigma\vdash\forall v(\bigwedge\Gamma\wedge\psi\rightarrow\phi)$. So $\Sigma\vdash\exists v(\bigwedge\Gamma\wedge\psi)\rightarrow\phi$. But then, by Infinite Distributivity, $\Sigma\vdash\bigwedge\Gamma\wedge\exists v\psi\rightarrow\phi$. So $\Sigma,\Gamma,\exists v\psi\vdash_{\Sigma}\phi$. ∎

Lemma 6** ($\forall$-Witness).**

For $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$, $|\Gamma|<\omega$: if $\Sigma,\Gamma\vdash_{\Sigma}\phi\vee\psi(t)$ for every $t\in\mathcal{L}^{+}$ then $\Sigma,\Gamma\vdash_{\Sigma}\phi\vee\forall v\psi$.

Proof.

Suppose $\Sigma,\Gamma\vdash_{\Sigma}\phi\vee\psi(t)$ for every $t\in\mathcal{L}^{+}$. Then, by Relative Deduction, $\Sigma\vdash\bigwedge\Gamma\rightarrow\phi\vee\psi(t)$ for every $t\in\mathcal{L}^{+}$. Since $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$, $\Sigma\vdash\forall v(\bigwedge\Gamma\rightarrow\phi\vee\psi)$. So $\Sigma\vdash\bigwedge\Gamma\rightarrow\forall v(\phi\vee\psi)$. But then, by CD, $\Sigma\vdash\bigwedge\Gamma\rightarrow\phi\vee\forall v\psi$. Hence $\Sigma,\Gamma\vdash_{\Sigma}\phi\vee\forall v\psi$. ∎

We define $Sat(\textsf{BQL}_{\textsf{CD}}(\Sigma))$ analogously to $Sat(\textsf{BQL}_{\textsf{CD}})$.

Lemma 7** (Relative Extension).**

For $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$, $|\Gamma|<\omega$: if $\Sigma,\Gamma\not\vdash_{\Sigma}\phi$ then there exists $(\Sigma\cup\Gamma)^{*}\supseteq\Sigma\cup\Gamma$ such that $(\Sigma\cup\Gamma)^{*}\in Sat(\textsf{BQL}_{\textsf{CD}}(\Sigma))$ and $\phi\not\in(\Sigma\cup\Gamma)^{*}$.

Proof.

Suppose $\Sigma,\Gamma\not\vdash_{\Sigma}\phi$. Since $\mathcal{L}$ is countable, we can fix an enumeration $\{\phi_{n}\}_{n\in\omega}$ of $\mathcal{L}^{+}$-sentences. We then inductively define a pair $\{\Gamma_{n}\}_{n\in\omega},\{\Delta_{n}\}_{n\in\omega}$ of increasing sequences of sets of sentences $\Gamma_{n},\Delta_{n}\subseteq\mathcal{L}^{+}$ as follows, where $\Pi^{L}_{n}(\psi)=\{t\in\mathcal{L}^{+}:\Sigma,\Gamma_{n},\psi(t)\not\vdash_{\Sigma}\bigvee\Delta_{n}\}$ and $\Pi^{R}_{n}(\psi)=\{t\in\mathcal{L}^{+}:\Sigma,\Gamma_{n}\not\vdash_{\Sigma}\bigvee\Delta_{n}\vee\psi(t)\}$:

[TABLE]

In order for this construction to be well-defined, we require $\Pi^{L}_{n}(\psi)\neq\emptyset$ at the stages where we choose $t\in\Pi^{L}_{n}(\psi)$ (likewise for $\Pi^{R}_{n}(\psi)$). We prove this by appealing to $\exists$-Witness ($\forall$-Witness), which requires $|\Gamma_{n}|<\omega$. Hence $\mathcal{L}$ must be countable, for otherwise we would need to iterate the above construction into the transfinite.

Subclaim 1** (Separation).**

For all $n$: (i) $\Gamma_{n},\Delta_{n}$ exist, (ii) $|\Gamma_{n}|,|\Delta_{n}|<\omega$ and (iii) $\Sigma,\Gamma_{n}\not\vdash_{\Sigma}\bigvee\Delta_{n}$.

Proof.

By induction on $n$. The base case is immediate.

Induction Step There are two cases.

Case 1 $\Sigma,\Gamma_{n},\phi_{n}\not\vdash_{\Sigma}\bigvee\Delta_{n}$. Then $\Delta_{n+1}=\Delta_{n}$. So if $\phi_{n}\neq\exists v\psi$ then $\Gamma_{n+1}=\Gamma_{n}\cup\{\phi_{n}\}$ and we’re done. Suppose, then, that $\phi_{n}=\exists v\psi$. Then, by $\exists$-Witness, $\Pi^{L}_{n}(\psi)\neq\emptyset$ and so $\Gamma_{n+1}=\Gamma_{n}\cup\{\exists v\psi,\psi(t)\}$ for some $t\in\Pi^{L}_{n}(\psi)$ exists. Suppose for a reductio that $\Sigma,\Gamma_{n+1}\vdash_{\Sigma}\bigvee\Delta_{n+1}$. Then, by Relative Deduction, $\Sigma\vdash\bigwedge\Gamma_{n+1}\rightarrow\bigvee\Delta_{n+1}$. There are two subcases.

Subcase 1 $\Gamma_{n}=\emptyset$. Then we can construct the following proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$:

[TABLE]

which contradicts the fact that $t\in\Pi^{L}_{n}(\psi)$.

Subcase 2 $\Gamma_{n}\neq\emptyset$. Then we can construct the following proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$:

[TABLE]

which contradicts the fact that $t\in\Pi^{L}_{n}(\psi)$.

Case 2 $\Sigma,\Gamma_{n},\phi_{n}\vdash_{\Sigma}\bigvee\Delta_{n}$. Then $\Gamma_{n+1}=\Gamma_{n}$. Also, by the induction hypothesis, $\phi_{n}\not\in\Sigma$. There are two subcases.

Subcase 1 $\phi_{n}\neq\forall v\psi$. Then $\Delta_{n+1}=\Delta_{n}\cup\{\phi_{n}\}$. Suppose for a reductio that $\Sigma,\Gamma_{n+1}\vdash_{\Sigma}\bigvee\Delta_{n+1}$. Since $\phi_{n}\not\in\Sigma$, $\phi_{n}$ never occurs unsafely in a proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$. So we can construct the following proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$:

[TABLE]

which contradicts the induction hypothesis.

Subcase 2 $\phi_{n}=\forall v\psi$. By the same argument as Subcase 1: $\Sigma,\Gamma_{n}\not\vdash_{\Sigma}\bigvee\Delta_{n}\vee\forall v\psi$. So, by $\forall$-Witness, $\Pi^{R}_{n}(\psi)\neq\emptyset$ and hence $\Delta_{n+1}=\Delta_{n}\cup\{\forall v\psi,\psi(t)\}$ for some $t\in\Pi^{R}_{n}(\psi)$ exists. Suppose for a reductio that $\Sigma,\Gamma_{n+1}\vdash_{\Sigma}\bigvee\Delta_{n+1}$. Then we can construct the following proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}(\Sigma)$:

[TABLE]

which contradicts the fact that $t\in\Pi^{R}_{n}(\psi)$. ∎

Let $(\Sigma\cup\Gamma)^{*}=\Sigma\cup\bigcup_{n\in\omega}\Gamma_{n}$. It is easy to verify using Separation that $(\Sigma\cup\Gamma)^{*}$ is the desired prime saturated $\textsf{BQL}_{\textsf{CD}}(\Sigma)$-theory. ∎

The canonical frame (for $\textsf{BQL}_{\textsf{CD}}$) is $\langle Sat(\textsf{BQL}_{\textsf{CD}}),\prec\rangle$, where $\Sigma\prec\Gamma$ iff for all $\phi,\psi$: if $\phi\rightarrow\psi\in\Sigma$ and $\phi\in\Gamma$ then $\psi\in\Gamma$. By soundness, $R^{n}(a_{1},...,a_{n})\not\vdash\bot$. So, by Extension, $Sat(\textsf{BQL}_{\textsf{CD}})$ is non-empty.

Lemma 8** (Subset).**

If $\Sigma\prec\Gamma$ then $\Sigma\subseteq\Gamma$.

Proof.

Suppose $\Sigma\prec\Gamma$ and $\phi\in\Sigma$. Then $\top\rightarrow\phi\in\Sigma$. So, since $\top\in\Gamma$, $\phi\in\Gamma$. ∎

To verify transitivity, suppose $\Sigma\prec\Gamma\prec\Delta$, $\phi\rightarrow\psi\in\Sigma$ and $\phi\in\Delta$. Then, by Subset, $\phi\rightarrow\psi\in\Gamma$. So $\psi\in\Delta$. Hence the canonical frame is in fact a transitive frame. The canonical model (for $\textsf{BQL}_{\textsf{CD}}$) is $\mathfrak{C}=\langle Sat(\textsf{BQL}_{\textsf{CD}}),\prec,T,|\mathord{\cdot}|\rangle$, where $T$ is the set of closed $\mathcal{L}^{+}$-terms and

[TABLE]

By Subset, we have

[TABLE]

So $\mathfrak{C}$ is in fact an $\mathcal{L}^{+}$-model.

Lemma 9** (Truth).**

$\mathfrak{C},\Sigma\Vdash\phi$ iff $\phi\in\Sigma$.

Proof.

By induction on the complexity of $\mathcal{L}^{+}$-sentences. The base case is easy. The induction steps are also easy except for $\rightarrow$.

$\rightarrow$ $\impliedby$ Easy.

$\implies$ Suppose $\phi\rightarrow\psi\not\in\Sigma$. Then $\Sigma\not\vdash\phi\rightarrow\psi$. By Relative Deduction: $\Sigma,\phi\not\vdash_{\Sigma}\psi$. Hence, by Relative Extension, there exists $(\Sigma\cup\{\phi\})^{*}\supseteq\Sigma\cup\{\phi\}$ such that $(\Sigma\cup\{\phi\})^{*}\in Sat(\textsf{BQL}_{\textsf{CD}}(\Sigma))$ and $\psi\not\in(\Sigma\cup\{\phi\})^{*}$. So $(\Sigma\cup\{\phi\})^{*}\in Sat(\textsf{BQL}_{\textsf{CD}})$. Then, by the induction hypothesis, $(\Sigma\cup\{\phi\})^{*}\Vdash\phi$ and $(\Sigma\cup\{\phi\})^{*}\not\Vdash\psi$. But $\Sigma\prec(\Sigma\cup\{\phi\})^{*}$. So $\Sigma\not\Vdash\phi\rightarrow\psi$. ∎

4. Completeness

We now drop that assumption that $\mathcal{L}$ is countable. We prove that completeness holds over the extended language $\mathcal{L}^{+}$.

Lemma 10** (Weak Completeness).**

For $|\Gamma|<\omega$: if $\Gamma\models\phi$ then $\Gamma\vdash\phi$.

Proof.

Suppose $\Gamma\not\vdash\phi$. Since $|\Gamma|<\omega$, we can find a countable first-order language $\mathcal{L}_{0}\subseteq\mathcal{L}$ such that $\Gamma\cup\{\phi\}\subseteq\mathcal{L}_{0}^{+}$. A forteriori, there does not exist a proof in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}\upharpoonright\mathcal{L}_{0}^{+}$ of $\phi$ from $\Gamma$. Since $\{i:a_{i}\not\in\Gamma\}=\omega$, Extension gives $\Gamma^{*}\supseteq\Gamma$ such that $\Gamma^{*}\in Sat(\textsf{BQL}_{\textsf{CD}})$ (where $Sat(\textsf{BQL}_{\textsf{CD}})$ is defined over $\mathcal{L}_{0}^{+}$) and $\phi\not\in\Gamma^{*}$. Let $\mathfrak{C}$ be the canonical model over $\mathcal{L}_{0}^{+}$. Then, by Truth: $\mathfrak{C},\Gamma^{*}\Vdash\Gamma$ and $\mathfrak{C},\Gamma^{*}\not\Vdash\phi$. So an arbitrary expansion of $\mathfrak{C}$ to $\mathcal{L}^{+}$ gives $\Gamma\not\models\phi$. ∎

Theorem 6** (Completeness).**

If $\Gamma\models\phi$ then $\Gamma\vdash\phi$.

Proof.

Immediate from compactness and weak completeness. ∎

5. Disjunction and Existence Properties

The canonical model is useful for finding families of models which share a domain and agree on the interpretations of all constant symbols and function symbols. This allows us to prove that $\textsf{BQL}_{\textsf{CD}}$ (over the original language $\mathcal{L}$) satisfies the disjunction and existence properties.

Lemma 11** (Intersection).**

For $I\neq\emptyset$, let $\{w\}\cup\{u_{i}\}_{i\in I}\subseteq\mathfrak{M}$ be such that $|R^{n}|(w)=\bigcap_{i\in I}|R^{n}|(u_{i})$. Then, for $\phi(\overline{v})\in\mathcal{L}\setminus\{\rightarrow,\vee,\exists\}$: $w\Vdash\phi(\overline{a})$ iff for all $i$: $u_{i}\Vdash\phi(\overline{a})$.

Proof.

An easy induction on the construction of $\mathcal{L}\setminus\{\rightarrow,\vee,\exists\}$-formulas. ∎

Lemma 12** (Weak Disjunction Property).**

For $\Gamma\subseteq\mathcal{L}\setminus\{\rightarrow,\vee,\exists\}$ such that $|\Gamma|\leq\omega$: if $\Gamma\models\phi\vee\psi$ then $\Gamma\models\phi$ or $\Gamma\models\psi$.

Proof.

Suppose $\Gamma\not\models\phi$ and $\Gamma\not\models\psi$. Then, by soundness, $\Gamma\not\vdash\phi$ and $\Gamma\not\vdash\psi$. Since $|\Gamma|\leq\omega$, we can find a countable first-order language $\mathcal{L}_{0}\subseteq\mathcal{L}$ such that $\Gamma\cup\{\phi,\psi\}\subseteq\mathcal{L}_{0}$. A forteriori, neither $\phi$ nor $\psi$ is provable from $\Gamma$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}\upharpoonright\mathcal{L}_{0}^{+}$. Since $\{i:a_{i}\in\Gamma\}=\emptyset$, Extension gives $\Gamma_{\phi},\Gamma_{\psi}\in Sat(\textsf{BQL}_{\textsf{CD}})$ (where $Sat(\textsf{BQL}_{\textsf{CD}})$ is defined over $\mathcal{L}_{0}^{+}$) such that (i) $\Gamma\subseteq\Gamma_{\phi}$ and $\phi\not\in\Gamma_{\phi}$ and (ii) $\Gamma\subseteq\Gamma_{\psi}$ and $\psi\not\in\Gamma_{\psi}$. Let $\mathfrak{C}$ be the canonical model over $\mathcal{L}_{0}^{+}$. Then, by Truth, we have (i) $\mathfrak{C},\Gamma_{\phi}\Vdash\Gamma$ and $\mathfrak{C},\Gamma_{\phi}\not\Vdash\phi$ and (ii) $\mathfrak{C},\Gamma_{\psi}\Vdash\Gamma$ and $\mathfrak{C},\Gamma_{\psi}\not\Vdash\psi$. Let $f(\mathfrak{C})$ be a worlds-disjoint copy of $\mathfrak{C}$ obtained by replacing every $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$ with $f(\Sigma)$ and leaving everything else unchanged. Let $\mathfrak{C}_{\phi}$ denote the submodel of $\mathfrak{C}$ generated by $\Gamma_{\phi}$ and $f(\mathfrak{C})_{\psi}$ denote the submodel of $f(\mathfrak{C})$ generated by $f(\Gamma_{\psi})$. Consider the following $\mathcal{L}^{+}_{0}$-model:

[TABLE]

where the root $w$ is a new world such that $|R^{n}|(w)=|R^{n}|(\Gamma_{\phi})\cap|R^{n}|(f(\Gamma_{\psi}))$. By Intersection, $w\Vdash\Gamma$. By Persistence, $w\not\Vdash\phi$ and $w\not\Vdash\psi$. So $w\not\Vdash\phi\vee\psi$. Taking the reduct of this model to $\mathcal{L}_{0}$ and then arbitrarily expanding to $\mathcal{L}$ gives $\Gamma\not\models\phi\vee\psi$. ∎

Theorem 7** (Disjunction Property).**

For $\Gamma\subseteq\mathcal{L}\setminus\{\rightarrow,\vee,\exists\}$: if $\Gamma\models\phi\vee\psi$ then $\Gamma\models\phi$ or $\Gamma\models\psi$.

Proof.

Immediate from compactness and the weak disjunction property. ∎

Lemma 13** (Weak Existence Property).**

Suppose $\mathcal{L}$ contains at least one constant symbol. Then, for $\Gamma\subseteq\mathcal{L}\setminus\{\rightarrow,\vee,\exists\}$ such that $|\Gamma|\leq\omega$: $\Gamma\models\exists v\phi$ only if $\Gamma\models\phi(t)$ for some $t\in\mathcal{L}$.

Proof.

Suppose $\Gamma\not\models\phi(t)$ for every $t\in\mathcal{L}$. Suppose for a reductio that $\Gamma\models\phi(t)$ for some $t\in\mathcal{L}^{+}$. Then, since $t=t_{0}(\overline{a_{i}})$ for some $t_{0}(\overline{u})\in\mathcal{L}$, we have by $\forall$-Int that $\Gamma\models\forall\overline{u}\phi(t_{0})$. So $\Gamma\models\phi(t_{0}(c,...,c))$ for some $c\in\mathcal{L}$, which is a contradiction. Therefore $\Gamma\not\models\phi(t)$ for every $t\in\mathcal{L}^{+}$. So, by soundness, $\Gamma\not\vdash\phi(t)$ for every $t\in\mathcal{L}^{+}$. Since $|\Gamma|\leq\omega$, we can find a countable first-order language $\mathcal{L}_{0}\subseteq\mathcal{L}$ such that $\Gamma\cup\{\phi\}\subseteq\mathcal{L}_{0}$. A forteriori, for all $t\in\mathcal{L}_{0}^{+}$ there does not exist a proof of $\phi(t)$ from $\Gamma$ in $\mathcal{N}\textsf{BQL}_{\textsf{CD}}\upharpoonright\mathcal{L}_{0}^{+}$. Since $\{i:a_{i}\in\Gamma\}=\emptyset$, Extension gives us a family $\{\Gamma_{t}\}_{t\in\mathcal{L}_{0}^{+}}\subseteq Sat(\textsf{BQL}_{\textsf{CD}})$ (where $Sat(\textsf{BQL}_{\textsf{CD}})$ is defined over $\mathcal{L}_{0}^{+}$) such that $\Gamma\subseteq\Gamma_{t}$ and $\phi(t)\not\in\Gamma_{t}$. Let $\mathfrak{C}$ be the canonical model over $\mathcal{L}_{0}^{+}$. Then, by Truth: $\mathfrak{C},\Gamma_{t}\Vdash\Gamma$ and $\mathfrak{C},\Gamma_{t}\not\Vdash\phi(t)$. Let $\{f_{t}(\mathfrak{C})\}_{t\in\mathcal{L}_{0}^{+}}$ be a family of pairwise worlds-disjoint copies of $\mathfrak{C}$ such that $f_{t}(\mathfrak{C})$ is obtained by replacing every $\Sigma\in Sat(\textsf{BQL}_{\textsf{CD}})$ with $f_{t}(\Sigma)$ and leaving everything else unchanged. Let $f_{t}(\mathfrak{C})^{*}$ denote the submodel of $f_{t}(\mathfrak{C})$ generated by $f_{t}(\Gamma_{t})$. Consider the following $\mathcal{L}_{0}^{+}$-model:

[TABLE]

where the root $w$ is a new world such that $|R^{n}|(w)=\bigcap_{t\in\mathcal{L}_{0}^{+}}|R^{n}|(f_{t}(\Gamma_{t}))$. By Intersection, $w\Vdash\Gamma$. By Persistence, $w\not\Vdash\phi(t)$ for all $t\in\mathcal{L}_{0}^{+}$. So $w\not\Vdash\exists v\phi$. Taking the reduct of this model to $\mathcal{L}_{0}$ and then arbitrarily expanding to $\mathcal{L}$ gives $\Gamma\not\models\exists v\phi$. ∎

Theorem 8** (Existence Property).**

Suppose $\mathcal{L}$ contains at least one constant symbol. Then, for $\Gamma\subseteq\mathcal{L}\setminus\{\rightarrow,\vee,\exists\}$: $\Gamma\models\exists v\phi$ only if $\Gamma\models\phi(t)$ for some $t\in\mathcal{L}$.

Proof.

Immediate from compactness and the weak existence property. ∎

6. References

[1] Gabbay D. M., Shehtman V. B., and Skvortsov D. P., Quantification in Non-Classical Logic: Volume 1, Elsevier, 2009.

[2] Ishigaki R., and Kikuchi K., Tree-Sequent Methods for Subintuitionistic Predicate Logics, in Olivetti N. (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: 16th International Conference Proceedings, Springer, 2007, pp. 149 – 164.

[3] Poizat B., A Course in Model Theory: An Introduction to Contemporary Mathematical Logic, Springer, 2000.

[4] Priest G., Paraconsistent Logic, in Gabbay D. M. and Guenthner F. (eds.), Handbook of Philosophical Logic, 2nd Edition: Volume 6, Kluwer Academic Publishers, 2002, pp. 287 – 393.

[5] Restall G., Subintuitionistic Logics, Notre Dame Journal of Formal Logic 35(1): 116 – 129, 1994.

[6] Ruitenburg W., Basic Predicate Calculus, Notre Dame Journal of Formal Logic 39(1): 18 – 46, 1998.

[7] Visser A., A Propositional Logic with Explicit Fixed Points, Studia Logica 40(2): 155 – 175, 1981.