Leibniz on the Logic of Conceptual Containment and Coincidence

Abstract

In a series of early essays written around 1679, Leibniz sets out to explore the logic of conceptual containment. In his more mature logical writings from the mid-1680s, however, his focus shifts away from the logic of containment to that of coincidence, or mutual containment. This shift in emphasis is indicative of the fact that Leibniz’s logic has its roots in two distinct theoretical frameworks: (i) the traditional theory of the categorical syllogism based on rules of inference such as Barbara, and (ii) equational systems of arithmetic and geometry based on the rule of substitution of equals. While syllogistic reasoning is naturally modeled in a logic of containment, substitutional reasoning of the sort performed in arithmetic and geometry is more naturally modeled in a logic of coincidence. In this paper, we argue that Leibniz’s logic of conceptual containment and his logic of coincidence can in fact be viewed as two alternative axiomatizations, in different but equally expressive languages, of one and the same logical theory. Thus, far from being incoherent, the varying syllogistic and equational themes that run throughout Leibniz’s logical writings complement one another and fit together harmoniously.

Appendix: Algebraic Semantics for Leibniz’s Containment Calculi

In this appendix, we provide an algebraic semantics for the containment calculi ⊢_c, ⊢_cp, and ⊢ (introduced in Definitions 3, 12, and 16 above). The three main results established in this appendix are:

• The calculus ⊢_c is sound and complete with respect to the class of semilattices (Theorem 20).

• The calculus ⊢_cp is sound and complete with respect to the class of Boolean algebras (Theorem 25).

• The calculus ⊢ is sound and complete with respect to the class of auto-Boolean algebras (Theorem 44).

1.1.1 I Semilattice Semantics for ⊢_c

In this section, we establish that the calculus ⊢_c is sound and complete with respect to the class of semilattice interpretations of the language $\mathcal {L}_{\mathrm {c}}$. As a preliminary step, we first note the following elementary fact about the calculus ⊢_c:

Theorem 17

For any terms A, B of $\mathcal {L}_{\mathrm {c}}$:

• (i) ⊢_cA ⊃ AA

• (ii) ⊢_cAB ⊃ BA

Proof

For (i): by C5, we have A ⊃ A ⊢_cA ⊃ AA. Hence, by C1, ⊢_cA ⊃ AA.

For (ii): by C2 and C3, we have ⊢_cpAB ⊃ A and ⊢_cpAB ⊃ B. Hence, by C5, ⊢_cpAB ⊃ BA. □

We now introduce an algebraic semantics for the language $\mathcal {L}_{\mathrm {c}}$:

Definition 18

An interpretation $(\mathfrak {A},\mu )$ of $\mathcal {L}_{\mathrm {c}}$ consists of (i) an algebraic structure $\mathfrak {A}=\langle \mathbb {A}, \wedge \rangle$, where $\mathbb {A}$ is a nonempty set and ∧ is a binary operation on $\mathbb {A}$; and (ii) a function μ mapping each term of $\mathcal {L}_{\mathrm {c}}$ to an element of $\mathbb {A}$ such that:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(AB)=\mu(A)\wedge\mu(B) \end{array} \end{aligned} $$

A proposition A ⊃ B of $\mathcal {L}_{\mathrm {c}}$ is satisfied in an interpretation $(\mathfrak {A},\mu )$ iff μ(A) = μ(A) ∧ μ(B). We write $(\mathfrak {A},\mu )\models A\supset B$ to indicate that $(\mathfrak {A},\mu )$ satisfies A ⊃ B.

Definition 19

An interpretation $(\langle \mathbb {A},\wedge \rangle ,\mu )$ of $\mathcal {L}_{\mathrm {c}}$ is a semilattice interpretation if $\langle \mathbb {A},\wedge \rangle$ is a semilattice. If Γ is a set of propositions of $\mathcal {L}_{\mathrm {c}}$ and φ a proposition of $\mathcal {L}_{\mathrm {c}}$, we write Γ⊧_slφ to indicate that, for any semilattice interpretation $(\mathfrak {A},\mu )$: if $(\mathfrak {A},\mu )\models \psi$ for all ψ ∈ Γ, then $(\mathfrak {A},\mu )\models \varphi$.

The following completeness proof employs the standard technique introduced by Birkhoff (1935) in his proof of the algebraic completeness of equational calculi.

Theorem 20

For any set of propositions Γ of $\mathcal {L}_{\mathrm {c}}$ and any proposition φ of $\mathcal {L}_{\mathrm {c}}$: Γ ⊢_cφ iff Γ⊧_slφ.

Proof

The left-to-right direction follows straightforwardly from the fact that the principles C1–C5 (as well as the general properties of calculi stated in Definition 2) are satisfied in every semilattice interpretation.

For the right-to-left direction, let Γ be a set of propositions of $\mathcal {L}_{\mathrm {c}}$, and let ≡ be the binary relation between terms of $\mathcal {L}_{\mathrm {c}}$ defined by:

$$\displaystyle \begin{aligned} \begin{array}{rcl} A\equiv B \quad\text{ iff} \quad\Gamma\vdash_{\mathrm{c}} A\supset B\quad\text{ and} \quad\Gamma\vdash_{\mathrm{c}} B\supset A \end{array} \end{aligned} $$

Clearly, if A ≡ B, then B ≡ A. Also, by C1, we have A ≡ A. By C4, we have: if A ≡ B and B ≡ C, then A ≡ C. Hence, ≡ is an equivalence relation on the set of all terms. Moreover, by Theorem 4, we have: if A ≡ B and C ≡ D, then AC ≡ BD. Thus, ≡ is a congruence relation on the algebra of terms formed by the operation of composition.

Now, let μ be the function mapping each term to its equivalence class under ≡, and let $\mathbb {T}$ be the set $\{\mu (A): A\ \text{is}\\text{a}\\text{term}\\text{of}\ \mathcal {L}_{\mathrm {c}}\}$. Since ≡ is a congruence relation with respect to the operation of composition, there is a binary operation ∧ on $\mathbb {T}$ such that, for any terms A and B:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(AB)=\mu(A)\wedge\mu(B) \end{array} \end{aligned} $$

This equation implies:

$$\displaystyle \begin{aligned} \begin{array}{rcl} (\mu(A)\wedge\mu(B))\wedge\mu(C)&\displaystyle =&\displaystyle \mu(AB)\wedge\mu(C) \\ &\displaystyle =&\displaystyle \mu(ABC) \\ &\displaystyle =&\displaystyle \mu(A)\wedge\mu(BC) \,\,\,\,= \,\,\,\,\mu(A)\wedge(\mu(B)\wedge\mu(C)) \end{array} \end{aligned} $$

In other words, the operation ∧ is associative. Now, by C2 and Theorem 17.i, we have ⊢_cAA ⊃ A and ⊢_cA ⊃ AA. It follows that μ(AA) = μ(A). Hence, ∧ is idempotent. Moreover, by Theorem 17.ii, we have ⊢_cAB ⊃ BA and ⊢_cBA ⊃ AB. It follows that μ(AB) = μ(BA). Hence, ∧ is commutative. All told, then, ∧ is an idempotent, associative, commutative operation on $\mathbb {T}$. Hence, $\mathfrak {T}=\langle \mathbb {T},\wedge \rangle$ is a semilattice, and $(\mathfrak {T},\mu )$ is a semilattice interpretation.

We now show that:

$$\displaystyle \begin{aligned} \begin{array}{rcl} (\mathfrak{T},\mu)\models A\supset B\text{\hspace{2mm} iff \hspace{2mm}} \Gamma\vdash_{\mathrm{c}} A\supset B \end{array} \end{aligned} $$

First, suppose that $(\mathfrak {T},\mu )\models A\supset B$. Then, μ(A) = μ(A) ∧ μ(B) = μ(AB), i.e., A ≡ AB. This implies that Γ ⊢_cA ⊃ AB, and so, since ⊢_cAB ⊃ B, it follows, by C4, that Γ ⊢_cA ⊃ B. Next, suppose that Γ ⊢_cA ⊃ B. Then, since ⊢_cA ⊃ A, by C5, we have Γ ⊢_cA ⊃ AB. But, since, by C2, ⊢_cAB ⊃ A, it follows that A ≡ AB, i.e., μ(A) = μ(AB) = μ(A) ∧ μ(B). But this means that $(\mathfrak {T}, \mu )\models A\supset B$.

Now, suppose Γ⊬_cφ. Then, $(\mathfrak {T},\mu )\not \models \varphi$. But since Γ ⊢_cψ for all ψ ∈ Γ, it follows that $(\mathfrak {T},\mu )\models \psi$ for all ψ ∈ Γ. Hence, since $(\mathfrak {T},\mu )$ is a semilattice interpretation, Γ⊭_slφ. □

1.1.2 I Boolean Semantics for ⊢_cp

In this section, we establish that the calculus ⊢_cp is sound and complete with respect to the class of Boolean interpretations of the language $\mathcal {L}_{\mathrm {cp}}$. As a preliminary step, we first note a few elementary facts about the calculus ⊢_cp.

Theorem 21

For any terms A, B of $\mathcal {L}_{\mathrm {cp}}$:

• (i) $A\supset \overline {B} \vdash _{\mathrm {cp}} AB\supset \overline {AB}$

• (ii) $A\supset \overline {B} \vdash _{\mathrm {cp}} B\supset \overline {A}$

• (iii) $\vdash _{\mathrm {cp}} A\supset \overline {\overline {A}}$

• (iv) $A\supset B \dashv \vdash _{\mathrm {cp}} A\overline {B}\supset \overline {A\overline {B}}$

• (v) $A\supset \overline {A} \vdash _{\mathrm {cp}} A\supset B$

• (vi) $\vdash _{\mathrm {cp}} A\overline {A} \supset B$

Proof

For (i): by C3 and CP1, we have $\vdash _{\mathrm {cp}} \overline {B} \supset \overline {AB}$. Also, by C2 and C4, $A \supset \overline {B} \vdash _{\mathrm {cp}} AB \supset \overline {B}$. Hence, by C4, $A\supset \overline {B} \vdash _{\mathrm {cp}} AB\supset \overline {AB}$.

For (ii): by Theorem 17.ii and CP1, we have $\vdash _{\mathrm {cp}} \overline {AB}\supset \overline {BA}$. Now, by (i) above and C4, we have $A\supset \overline {B} \vdash _{\mathrm {cp}} BA\supset \overline {BA}$. Hence, by CP3, $A\supset \overline {B} \vdash _{\mathrm {cp}} B\supset \overline {A}$.

For (iii): by (ii) above, we have $\overline {A}\supset \overline {A} \vdash _{\mathrm {cp}} A\supset \overline {\overline {A}}$. Hence, by C1, $\vdash _{\mathrm {cp}} A \supset \overline {\overline {A}}$.

For (iv): by CP3 and (i) above, $A\supset \overline {\overline {B}} \dashv \vdash _{\mathrm {cp}} A\overline {B}\supset \overline {A\overline {B}}$. But by (iii) above, CP2, and C4, we have $A\supset \overline {\overline {B}} \dashv \vdash _{\mathrm {cp}} A\supset B$. Hence, $A\supset B \dashv \vdash _{\mathrm {cp}} A\overline {B}\supset \overline {A\overline {B}}$.

For (v): by C2 and CP1, we have both $\vdash _{\mathrm {cp}} A\overline {B}\supset A$ and $\vdash _{\mathrm {cp}} \overline {A}\supset \overline {A\overline {B}}$. So, by C4, $A\supset \overline {A} \vdash _{\mathrm {cp}} A\overline {B}\supset \overline {A\overline {B}}$. Hence, by (iv) above, $A\supset \overline {A} \vdash _{\mathrm {cp}} A\supset B$.

For (vi): by (iv) above, $A\supset A \vdash _{\mathrm {cp}} A\overline {A}\supset \overline {A\overline {A}}$. So, by C1, $\vdash _{\mathrm {cp}} A\overline {A}\supset \overline {A\overline {A}}$. Hence, by (v) above, $\vdash _{\mathrm {cp}} A\overline {A} \supset B$. □

Theorem 22

For any terms A, B, C of $\mathcal {L}_{\mathrm {cp}}$:

• (i) $A\overline {B}\supset C\overline {C}, C\overline {C}\supset A\overline {B}\vdash _{\mathrm {cp}} A\supset B$

• (ii) $A\supset B \vdash _{\mathrm {cp}} A\overline {B}\supset C\overline {C}$

• (iii) $A\supset B \vdash _{\mathrm {cp}} C\overline {C}\supset A\overline {B}$

Proof

For (i): by Theorem 21.vi, we have $\vdash _{\mathrm {cp}} C\overline {C}\supset \overline {A\overline {B}}$. So, by C4, $A\overline {B}\supset C\overline {C} \vdash _{\mathrm {cp}} A\overline {B}\supset \overline {A\overline {B}}$. But, by Theorem 21.iv, this implies $A\overline {B}\supset C\overline {C} \vdash _{\mathrm {cp}} A\supset B$. Hence, $A\overline {B}\supset C\overline {C}, C\overline {C}\supset A\overline {B}\vdash _{\mathrm {cp}} A\supset B$.

For (ii): by Theorem 21.iv, we have $A\supset B \vdash _{\mathrm {cp}} A\overline {B}\supset \overline {A\overline {B}}$. Hence, by Theorem 21.v, $A\supset B \vdash _{\mathrm {cp}} A\overline {B}\supset C\overline {C}$.

Lastly, (iii) follows by Theorem 21.vi. □

We now introduce an algebraic semantics for the language $\mathcal {L}_{\mathrm {cp}}$:

Definition 23

An interpretation $(\mathfrak {A},\mu )$ of $\mathcal {L}_{\mathrm {cp}}$ consists of (i) an algebraic structure $\mathfrak {A}=\langle \mathbb {A}, \wedge , '\rangle$, where $\mathbb {A}$ is a nonempty set, ∧ is a binary operation on $\mathbb {A}$, and ′ is a unary operation on $\mathbb {A}$; and (ii) a function μ mapping each term of $\mathcal {L}_{\mathrm {cp}}$ to an element of $\mathbb {A}$ such that:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(AB) &\displaystyle =&\displaystyle \mu(A)\wedge\mu(B)\\ \mu\left(\overline{A}\right) &\displaystyle =&\displaystyle \mu(A)' \end{array} \end{aligned} $$

A proposition A ⊃ B of $\mathcal {L}_{\mathrm {cp}}$ is satisfied in an interpretation $(\mathfrak {A},\mu )$ iff μ(A) = μ(A) ∧ μ(B). We write $(\mathfrak {A},\mu )\models A\supset B$ to indicate that $(\mathfrak {A},\mu )$ satisfies A ⊃ B.

Definition 24

An interpretation $(\langle \mathbb {A}, \wedge , '\rangle ,\mu )$ of $\mathcal {L}_{\mathrm {cp}}$ is a Boolean interpretation if $\langle \mathbb {A},\wedge , '\rangle$ is a Boolean algebra. If Γ is a set of propositions of $\mathcal {L}_{\mathrm {cp}}$ and φ a proposition of $\mathcal {L}_{\mathrm {cp}}$, we write Γ⊧_baφ to indicate that, for any Boolean interpretation $(\mathfrak {A},\mu )$: if $(\mathfrak {A},\mu )\models \psi$ for all ψ ∈ Γ, then $(\mathfrak {A},\mu )\models \varphi$.

The following completeness proof relies on a concise axiomatization of the theory of Boolean algebras discovered by Byrne (1946). In the language $\mathcal {L}_{\mathrm {cp}}$, the main principle in this axiomatization is given by Theorem 22.

Theorem 25

For any set of propositions Γ of $\mathcal {L}_{\mathrm {cp}}$ and any proposition φ of $\mathcal {L}_{\mathrm {cp}}$: Γ ⊢_cpφ iff Γ⊧_baφ.

Proof

The left-to-right direction follows straightforwardly from the fact that the principles C1–C5 and CP1–CP3 are satisfied in every Boolean interpretation.

For the right-to-left direction, let Γ be a set of propositions of $\mathcal {L}_{\mathrm {cp}}$, and let ≡ be the binary relation between terms of $\mathcal {L}_{\mathrm {cp}}$ defined by:

$$\displaystyle \begin{aligned} \begin{array}{rcl} A\equiv B \quad\text{iff}\quad\Gamma\vdash_{\mathrm{cp}} A\supset B \quad\text{and}\quad\Gamma\vdash_{\mathrm{cp}} B\supset A \end{array} \end{aligned} $$

Following the reasoning in the proof of Theorem 20, ≡ is an equivalence relation on the set of terms of $\mathcal {L}_{\mathrm {cp}}$. Moreover, by Theorem 4 and CP1, ≡ is a congruence relation on the algebra of terms formed by the operations of composition and privation.

Now, let μ be the function mapping each term to its equivalence class under ≡, and let $\mathbb {T}$ be the set $\{\mu (A): A\ \text{is}\\text{a}\\text{term}\\text{of}\ \mathcal {L}_{\mathrm {cp}}\}$. Since ≡ is a congruence relation with respect to the operations of composition and privation, there is a binary operation ∧ on $\mathbb {T}$ and a unary operation ′ on $\mathbb {T}$ such that, for any terms A and B:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(AB) &\displaystyle =&\displaystyle \mu(A)\wedge\mu(B)\\ \mu\left(\overline{A}\right) &\displaystyle =&\displaystyle \mu(A)' \end{array} \end{aligned} $$

The operation ∧ is associative and commutative (see the proof of Theorem 20). Moreover, by Theorem 22, we have for any terms A, B, C of $\mathcal {L}_{\mathrm {cp}}$:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(A)\wedge\mu(B)' = \mu(C)\wedge\mu(C)'\text{\hspace{2mm} iff \hspace{2mm}}\mu(A) = \mu(A)\wedge\mu(B) \end{array} \end{aligned} $$

Byrne (1946: 269–271) has shown that this latter condition, in conjunction with the associativity and commutativity of ∧, implies that $\mathfrak {T}=\langle \mathbb {T},\wedge ,'\rangle$ is a Boolean algebra. Hence $(\mathfrak {T},\mu )$ is a Boolean interpretation.

Following the reasoning in the proof of Theorem 20, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} (\mathfrak{T},\mu)\models A\supset B\text{\quad iff \quad } \Gamma\vdash_{\mathrm{cp}} A\supset B \end{array} \end{aligned} $$

Now, suppose Γ⊬_cpφ. Then, $(\mathfrak {T},\mu )\not \models \varphi$. But since Γ ⊢_cpψ for all ψ ∈ Γ, it follows that $(\mathfrak {T},\mu )\models \psi$ for all ψ ∈ Γ. Hence, since $(\mathfrak {T},\mu )$ is a Boolean interpretation, Γ⊭_baφ. □

1.1.3 I Auto-Boolean Semantics for ⊢

In this section, we establish that the containment calculus ⊢ is sound and complete with respect to the class of auto-Boolean interpretations of the language $\mathcal {L}_{\supset }$. The proof of completeness will rely on the auto-Boolean completeness of the coincidence calculus developed by Leibniz’s in the Generales inquisitiones. We begin by establishing some preliminary facts about the containment calculus ⊢.

Definition 26

For any term A of $\mathcal {L}_{\supset }$, we write for the proposition $A\supset \overline {A}$.

Theorem 27

For any propositions φ, ψ, χ of $\mathcal {L}_{\supset }$:

• (i) If φ, ψ ⊢ χ, then $\varphi , \, \mathbf {F}(\ulcorner {\chi }\urcorner ) \, \vdash \, \mathbf {F}(\ulcorner {\psi }\urcorner )$

• (ii) φ ⊢ ψ iff $\vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\psi }\urcorner$

• (iii) If φ ⊢ ψ, then $\mathbf {F}(\ulcorner {\psi }\urcorner ) \, \vdash \, \mathbf {F}(\ulcorner {\varphi }\urcorner )$

Proof

For (i): suppose that φ, ψ ⊢ χ. By PT3, we have $\varphi \vdash \ulcorner {\psi }\urcorner \supset \ulcorner {\chi }\urcorner$. Hence, by CP1, $\varphi \vdash \overline {\ulcorner {\chi }\urcorner }\supset \overline {\ulcorner {\psi }\urcorner }$. By C4, PT1, and PT2, it follows that $\varphi \vdash \ulcorner {\mathbf {F}(\ulcorner {\chi }\urcorner )}\supset \ulcorner {\mathbf {F}(\ulcorner {\psi }\urcorner )}$. Hence, by PT3, $\varphi , \mathbf {F}(\ulcorner {\chi }\urcorner ) \vdash \mathbf {F}(\ulcorner {\psi }\urcorner )$.

For (ii): by PT3, A ⊃ A, φ ⊢ ψ iff $A\supset A\vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\psi }\urcorner$. Hence, by C1, φ ⊢ ψ iff $\vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\psi }\urcorner$.

For (iii): suppose that φ ⊢ ψ. Then, A ⊃ A, φ ⊢ ψ. By (i) above, we have $A \supset A, \mathbf {F}(\ulcorner {\psi }\urcorner ) \vdash \mathbf {F}(\ulcorner {\varphi }\urcorner )$. Hence, by C1, $\mathbf {F}(\ulcorner {\psi }\urcorner ) \vdash \mathbf {F}(\ulcorner {\varphi }\urcorner )$. □

Theorem 28

For any proposition φ of $\mathcal {L}_{\supset }$ :

• (i) $\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )}) \,\vdash \, \varphi$

• (ii) $\varphi \,\vdash \, \mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})$

Proof

For (i): by PT2, we have $\vdash \ulcorner {\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})} \supset \overline {\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )}}$. Moreover, by PT1 and CP1, we have $\vdash \overline {\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )}} \supset \overline {\overline {\ulcorner {\varphi }\urcorner }}$. Hence, by C4, $\vdash \ulcorner {\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})} \supset \overline {\overline {\ulcorner {\varphi }\urcorner }}$. By CP2 and C4, it follows that $\vdash \ulcorner {\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})} \supset \ulcorner {\varphi }\urcorner$. Hence, by Theorem 27.ii, $\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )}) \vdash \varphi$.

For (ii): by PT1, we have $\vdash \overline {\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )}} \supset \ulcorner {\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})}$. Moreover, by PT2 and CP1, we have $\vdash \overline {\overline {\ulcorner {\varphi }\urcorner }} \supset \overline {\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )}}$. Hence, by C4, $\vdash \overline {\overline {\ulcorner {\varphi }\urcorner }} \supset \ulcorner {\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})}$. By Theorem 21.iii and C4, it follows that $\vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})}$. Hence, by Theorem 27.ii, $\varphi \vdash \mathbf {F}(\ulcorner {\mathbf {F}(\ulcorner {\varphi }\urcorner )})$. □

Theorem 29

For any propositions φ, ψ of $\mathcal {L}_{\supset }$:

• (i)
• (ii)
• (iii)

Proof

For (i): since $\ulcorner {\varphi }\urcorner \supset \ulcorner {\mathbf {F}(\ulcorner {\psi }\urcorner )} \vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\mathbf {F}(\ulcorner {\psi }\urcorner )}$, by PT3 we have $\varphi , \ulcorner {\varphi }\urcorner \supset \ulcorner {\mathbf {F}(\ulcorner {\psi }\urcorner )} \vdash \mathbf {F}(\ulcorner {\psi }\urcorner )$. By C4 and PT1, it follows that $\varphi , \ulcorner {\varphi }\urcorner \supset \overline {\ulcorner {\psi }\urcorner } \vdash \mathbf {F}(\ulcorner {\psi }\urcorner )$. Hence, by Theorem 27.i, . The desired result follows by Theorem 28.ii.

For (ii): since φ, ψ ⊢ φ, by Theorem 27.i we have $\varphi , \mathbf {F}(\ulcorner {\varphi }\urcorner ) \vdash \mathbf {F}(\ulcorner {\psi }\urcorner )$. By PT3, it follows that $\mathbf {F}(\ulcorner {\varphi }\urcorner ) \vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\mathbf {F}(\ulcorner {\psi }\urcorner )}$. Hence, by PT2 and C4, $\mathbf {F}(\ulcorner {\varphi }\urcorner ) \vdash \ulcorner {\varphi }\urcorner \supset \overline {\ulcorner {\psi }\urcorner }$. By Theorem 27.iii, it follows that . The desired result follows by Theorem 28.i.

For (iii): since $\varphi , \mathbf {F}(\ulcorner {\psi }\urcorner ) \vdash \mathbf {F}(\ulcorner {\psi }\urcorner )$, by PT3 we have $\mathbf {F}(\ulcorner {\psi }\urcorner ) \vdash \ulcorner {\varphi }\urcorner \supset \ulcorner {\mathbf {F}(\ulcorner {\psi }\urcorner )}$. Hence, by C4 and PT2, $\mathbf {F}(\ulcorner {\psi }\urcorner ) \vdash \ulcorner {\varphi }\urcorner \supset \overline {\ulcorner {\psi }\urcorner }$. By Theorem 27.iii, it follows that . The desired result follows by Theorem 28.i. □

Definition 30

For any terms A, B of $\mathcal {L}_{\supset }$, we write A ≈ B for the proposition:

Theorem 31

For any terms A, B of $\mathcal {L}_{\supset }$:

• (i) A ⊃ B ⊣⊢ A ≈ AB

• (ii) ⊢ AA ≈ A

• (iii) ⊢ AB ≈ BA

• (iv) $\vdash \overline {\overline {A}}\approx A$

Proof

For (i): by C2, we have ⊢ AB ⊃ A, and so A ⊃ B ⊢ AB ⊃ A. Moreover, by C1 and C5, we have A ⊃ B ⊢ A ⊃ AB. Hence, by Theorem 29.i, A ⊃ B ⊢ A ≈ AB. For the converse, by Theorem 29.ii, we have A ≈ AB ⊢ A ⊃ AB. Hence, by C3 and C4, A ≈ AB ⊢ A ⊃ B.

For (ii): by C2, we have ⊢ AA ⊃ A. Moreover, by Theorem 17.i, we have ⊢ A ⊃ AA. Hence, by Theorem 29.i, ⊢ AA ≈ A.

For (iii): by Theorem 17.ii, we have both ⊢ AB ⊃ BA and ⊢ BA ⊃ AB. Hence, by Theorem 29.i, ⊢ AB ≈ BA.

For (iv): by CP2, we have $\vdash \overline {\overline {A}}\supset A$. Moreover, by Theorem 21.iii, we have $\vdash A\supset \overline {\overline {A}}$. Hence, by Theorem 29.i, $\vdash \overline {\overline {A}}\approx A$. □

In the remainder of this section, we establish that the calculus ⊢ is complete with respect to the class of auto-Boolean algebras. This completeness proof will rely on the auto-Boolean completeness of the coincidence calculus developed by Leibniz in the Generales inquisitiones. The crucial step in the proof will be to show that all the theorems of the latter calculus can be reproduced in the containment calculus ⊢. To this end, we first specify the language $\mathcal {L}_{=}$ of Leibniz’s coincidence calculus:

Definition 32

The terms and propositions of the language $\mathcal {L}_{=}$ are defined as follows:

• (1) Every simple term of the language $\mathcal {L}_{\supset }$ is a term.

• (2) If A and B are terms, then AB is a term.

• (3) If A is a term, then $\overline {A}$ is a term.

• (4) If A and B are terms, then A = B is a proposition.

• (5) If A = B is a proposition, then $\ulcorner {A=B}\urcorner$ is a term.

The following two definitions describe how the terms and propositions of $\mathcal {L}_{\supset }$ can be translated into the language $\mathcal {L}_{=}$ and vice versa:

Definition 33

The function σ maps every term or proposition of $\mathcal {L}_{\supset }$ to a term or proposition of $\mathcal {L}_{=}$ as follows:

• (1) If A is a simple term of $\mathcal {L}_{\supset }$, then σ(A) is the term A.

• (2) σ(AB) is the term σ(A)σ(B).

• (3) $\sigma (\overline {A})$ is the term $\overline {\sigma (A)}$.

• (4) σ(A ⊃ B) is the proposition σ(A) = σ(A)σ(B)

• (5) σ(⌜φ⌝) is the term ⌜σ(φ)⌝.

If Γ is a set of propositions of $\mathcal {L}_{\supset }$, we write σ( Γ) for the set {σ(φ) : φ ∈ Γ}.

Definition 34

The function τ maps every term or proposition of $\mathcal {L}_{=}$ to a term or proposition of $\mathcal {L}_{\supset }$ as follows:

• (1) If A is a simple term of $\mathcal {L}_{\supset }$, then τ(A) is the term A.

• (2) τ(AB) is the term τ(A)τ(B).

• (3) $\tau (\overline {A})$ is the term $\overline {\tau (A)}$.

• (4) τ(A = B) is the proposition τ(A) ≈ τ(B)

• (5) τ(⌜φ⌝) is the term ⌜τ(φ)⌝.

If Γ is a set of propositions of $\mathcal {L}_{=}$, we write τ( Γ) for the set {τ(φ) : φ ∈ Γ}.

Theorem 35

For any term A and any proposition φ of $\mathcal {L}_{\supset }$ :

• (i) ⊢ A ⊃ τ(σ(A)) and ⊢ τ(σ(A)) ⊃ A

• (ii) φ ⊣⊢ τ(σ(φ))

Proof

The proof proceeds by mutual induction on the structure of the terms and propositions of $\mathcal {L}_{\supset }$ (see Definition 13). First, suppose that A is a simple term of $\mathcal {L}_{\supset }$. Then τ(σ(A)) just is the term A, and so the claim follows by C1.

Next, suppose that the claim holds for the terms A and B. By Theorem 4, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \vdash AB\supset \tau(\sigma(A))\tau(\sigma(B))\\ {}\vdash \tau(\sigma(A))\tau(\sigma(B))\supset AB \end{array} \end{aligned} $$

But since τ(σ(A))τ(σ(B)) is the term τ(σ(AB)), the claim holds for the term AB. Moreover, by CP1, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \vdash \overline{A}\supset \overline{\tau(\sigma(A))}\\ \vdash \overline{\tau(\sigma(A))}\supset \overline{A} \end{array} \end{aligned} $$

But since $\overline {\tau (\sigma (A))}$ is the term $\tau (\sigma (\overline {A}))$, the claim holds for the term $\overline {A}$.

Next, given that the claim holds for the terms A and B, it follows by the rule of substitution for containment established in Theorem 15 that:

$$\displaystyle \begin{aligned} \begin{array}{rcl} A\approx AB\dashv \vdash \tau(\sigma(A))\approx \tau(\sigma(A))\tau(\sigma(B)) \end{array} \end{aligned} $$

Hence, by Theorem 31.i, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} A\supset B\dashv \vdash \tau(\sigma(A))\approx \tau(\sigma(A))\tau(\sigma(B)) \end{array} \end{aligned} $$

But since τ(σ(A)) ≈ τ(σ(A))τ(σ(B)) is the proposition τ(σ(A ⊃ B)), the claim holds for the proposition A ⊃ B.

Finally, suppose that the claim holds for the proposition φ. By Theorem 27.ii, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \vdash \ulcorner{\varphi}\supset\ulcorner{\tau(\sigma(\varphi))}\\ \vdash \ulcorner{\tau(\sigma(\varphi))}\supset\ulcorner{\varphi} \end{array} \end{aligned} $$

But since ⌜τ(σ(φ))⌝ is the term $\tau (\sigma (\ulcorner {\varphi }\urcorner ))$, the claim holds for the term $\ulcorner {\varphi }\urcorner$. This completes the induction. □

We now introduce the coincidence calculus, $\Vdash$, developed by Leibniz in the Generales inquisitiones (as reconstructed in Malink and Vasudevan 2016: 696–706):

Definition 36

The calculus $\Vdash$ is the smallest calculus in the language $\mathcal {L}_{=}$ such that:

(P1):

$\Vdash AA=A$

(P2):

$\Vdash AB=BA$

(P3):

$\Vdash \overline {\overline {A}}=A$

(P4):

(P5):

$\Vdash \overline {\ulcorner {\varphi }\urcorner } = \ulcorner {\ulcorner {\varphi }\urcorner =\ulcorner {\varphi }\urcorner \overline {\ulcorner {\varphi }\urcorner }}$

(P6):

$\varphi \Vdash \psi$ iff $\Vdash \ulcorner {\varphi }\urcorner =\ulcorner {\varphi }\urcorner \ulcorner {\psi }\urcorner$

(P7):

, where is the result of substituting B for an

occurrence of A, or vice versa, in φ.

The following result states that all theorems of the coincidence calculus $\Vdash$ can be reproduced under the translation τ in the containment calculus ⊢:

Theorem 37

For any set of propositions Γ of $\mathcal {L}_{=}$ and any proposition φ of $\mathcal {L}_{=}$: if $\Gamma \Vdash \varphi$, then τ( Γ) ⊢ τ(φ).

Proof

The proof proceeds by induction on the definition of the coincidence calculus $\Vdash$ (Definition 36). For P1–P6, it suffices to show that for any terms A, B of $\mathcal {L}_{\supset }$ and any propositions φ, ψ of $\mathcal {L}_{\supset }$:

• (i) ⊢ AA ≈ A

• (ii) ⊢ AB ≈ BA

• (iii) $\vdash \overline {\overline {A}}\approx A$

• (iv) $A\overline {B}\approx A\overline {B}\overline {A\overline {B}}\dashv \vdash A\approx AB$

• (v) $\vdash \overline {\ulcorner {\varphi }\urcorner } \approx \ulcorner {\ulcorner {\varphi }\urcorner \approx \ulcorner {\varphi }\urcorner \overline {\ulcorner {\varphi }\urcorner }}$

• (vi) φ ⊢ ψ iff $\vdash \ulcorner {\varphi }\urcorner \approx \ulcorner {\varphi }\urcorner \ulcorner {\psi }\urcorner$

Claims (i)–(iii) are stated in Theorem 31.ii–iv. Claim (iv) follows by Theorems 21.iv and 31.i. For claim (v), by Theorems 31.i and 27.ii, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \vdash\ulcorner{\ulcorner{\varphi}\supset\overline{\ulcorner{\varphi}}}\supset \ulcorner{\ulcorner{\varphi}\urcorner\approx\ulcorner{\varphi}\urcorner\overline{\ulcorner{\varphi}\urcorner}} \\ \vdash\ulcorner{\ulcorner{\varphi}\urcorner\approx \ulcorner{\varphi}\urcorner\overline{\ulcorner{\varphi}\urcorner}}\supset \ulcorner{\ulcorner{\varphi}\supset\overline{\ulcorner{\varphi}}} \end{array} \end{aligned} $$

Hence, by PT1, PT2, and C4, we have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \vdash\overline{\ulcorner{\varphi}}\supset \ulcorner{\ulcorner{\varphi}\urcorner\approx\ulcorner{\varphi}\urcorner\overline{\ulcorner{\varphi}\urcorner}} \\ \vdash\ulcorner{\ulcorner{\varphi}\urcorner\approx \ulcorner{\varphi}\urcorner\overline{\ulcorner{\varphi}\urcorner}}\supset \overline{\ulcorner{\varphi}} \end{array} \end{aligned} $$

Claim (v) then follows by Theorem 29.i.

Claim (vi) follows by Theorems 27.ii and 31.i.

Finally, for P7 we must show that, for any terms A, B of $\mathcal {L}_{=}$ and any proposition φ of $\mathcal {L}_{=}$: if is the result of substituting B for an occurrence of A, or vice versa, in φ, then . To see this, we first note that, given Definition 34, if is the result of substituting A for an occurrence of B, or vice versa, in φ, then is the result of substituting τ(A) for one or more occurrences of τ(B), or vice versa, in τ(φ). Moreover, it follows by Theorems 15 and 29.ii–iii that, if is the result of substituting τ(A) for one or more occurrences of τ(B), or vice versa, in τ(φ), then . This completes the induction. □

We now introduce an algebraic semantics for the language $\mathcal {L}_{=}$:

Definition 38

An interpretation $(\mathfrak {A},\mu )$ of $\mathcal {L}_{=}$ consists of (i) an algebraic structure $\mathfrak {A}=\langle \mathbb {A}, \wedge , '\rangle$, where $\mathbb {A}$ is a nonempty set, ∧ is a binary operation on $\mathbb {A}$, and ′ is a unary operation on $\mathbb {A}$; and (ii) a function μ mapping each term of $\mathcal {L}_{=}$ to an element of $\mathbb {A}$ such that:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(AB) &\displaystyle =&\displaystyle \mu(A)\wedge\mu(B)\\ \mu\left(\overline{A}\right) &\displaystyle =&\displaystyle \mu(A)' \end{array} \end{aligned} $$

A proposition A = B of $\mathcal {L}_{=}$ is satisfied in an interpretation $(\mathfrak {A},\mu )$ iff μ(A) = μ(B). We write to indicate that $(\mathfrak {A},\mu )$ satisfies A = B.

Definition 39

An interpretation $(\langle \mathbb {A}, \wedge , '\rangle , \mu )$ of $\mathcal {L}_{=}$ is an auto-Boolean interpretation iff $\langle \mathbb {A}, \wedge , '\rangle$ is a Boolean algebra such that, for any terms A, B of $\mathcal {L}_{=}$:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu\left(\ulcorner{A=B}\right) =\left\{\begin{array}{ll} 1 &\displaystyle \quad\text{if}\\ \mu(A) = \mu(B)\\ 0 &\displaystyle \quad\text{otherwise}\end{array}\right. \end{array} \end{aligned} $$

Here, 1 and 0 are the top and bottom elements of the Boolean algebra $\langle \mathbb {A}, \wedge , '\rangle$, respectively. If Γ is a set of propositions of $\mathcal {L}_{=}$ and φ a proposition of $\mathcal {L}_{=}$, we write to indicate that, for any auto-Boolean interpretation $(\mathfrak {A},\mu )$ of $\mathcal {L}_{=}$: if for all ψ ∈ Γ, then .

The following theorem asserts that the coincidence calculus $\Vdash$ is complete with respect to the class of auto-Boolean interpretations of $\mathcal {L}_{=}$:

Theorem 40

For any set of propositions Γ of $\mathcal {L}_{=}$ and any proposition φ of $\mathcal {L}_{=}$: if , then $\Gamma \Vdash \varphi$.

The proof of this completeness theorem is given in Malink and Vasudevan 2016: 744–8 (Theorem 4.94).

With this completeness theorem for the coincidence calculus $\Vdash$ in hand, we are now in a position to establish the auto-Boolean completeness of the cointainment calculus ⊢. To this end, we first introduce an algebraic semantics for the language $\mathcal {L}_{\supset }$:

Definition 41

An interpretation $(\mathfrak {A},\mu )$ of $\mathcal {L}_{\supset }$ consists of (i) an algebraic structure $\mathfrak {A}=\langle \mathbb {A}, \wedge , '\rangle$, where $\mathbb {A}$ is a nonempty set, ∧ is a binary operation on $\mathbb {A}$, and ′ is a unary operation on $\mathbb {A}$; and (ii) a function μ mapping each term of $\mathcal {L}_{\supset }$ to an element of $\mathbb {A}$ such that:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu(AB)&\displaystyle =&\displaystyle \mu(A)\wedge\mu(B)\\ \mu\left(\overline{A}\right)&\displaystyle =&\displaystyle \mu(A)' \end{array} \end{aligned} $$

A proposition A ⊃ B of $\mathcal {L}_{\supset }$ is satisfied in an interpretation $(\mathfrak {A},\mu )$ iff μ(A) = μ(A) ∧ μ(B). We write $(\mathfrak {A},\mu )\models A\supset B$ to indicate that $(\mathfrak {A},\mu )$ satisfies A ⊃ B.

Definition 42

An interpretation $(\langle \mathbb {A}, \wedge , '\rangle , \mu )$ of $\mathcal {L}_{\supset }$ is an auto-Boolean interpretation iff $\langle \mathbb {A}, \wedge , '\rangle$ is a Boolean algebra such that, for any terms A, B of $\mathcal {L}_{\supset }$:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu\left(\ulcorner{A\supset B}\right) =\left\{\begin{array}{ll} 1 &\displaystyle \quad\text{if}\\ \mu(A) = \mu(A)\wedge \mu(B)\\ 0 &\displaystyle \quad\text{otherwise}\end{array}\right. \end{array} \end{aligned} $$

Here, 1 and 0 are the top and bottom elements of the Boolean algebra $\langle \mathbb {A}, \wedge , '\rangle$, respectively. If Γ is a set of propositions of $\mathcal {L}_{\supset }$ and φ a proposition of $\mathcal {L}_{\supset }$, we write Γ⊧φ to indicate that, for any auto-Boolean interpretation $(\mathfrak {A},\mu )$ of $\mathcal {L}_{\supset }$: if $(\mathfrak {A},\mu )\models \psi$ for all ψ ∈ Γ, then $(\mathfrak {A},\mu )\models \varphi$.

Theorem 43

For any set of propositions Γ of $\mathcal {L}_{\supset }$ and any proposition φ of $\mathcal {L}_{\supset }$: if Γ⊧φ, then .

Proof

Let $(\mathfrak {A},\mu )=(\langle \mathbb {A}, \wedge , '\rangle , \mu )$ be an auto-Boolean interpretation of $\mathcal {L}_{=}$, and let be the function mapping each term of $\mathcal {L}_{\supset }$ to an element of $\mathbb {A}$ defined by:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu^*(A) = \mu(\sigma(A)) \end{array} \end{aligned} $$

We then have:

$$\displaystyle \begin{aligned} \begin{array}{rcl} \mu^*(\ulcorner{A\supset B}) &\displaystyle =&\displaystyle \mu(\sigma(\ulcorner{A\supset B})) \\ &\displaystyle =&\displaystyle \mu(\ulcorner{\sigma(A\supset B)}) \\ &\displaystyle =&\displaystyle \mu(\ulcorner{\sigma(A)=\sigma(A)\sigma(B)}) \\ &\displaystyle =&\displaystyle \left\{\begin{array}{ll} 1 &\displaystyle \quad\text{if}\ \ \mu(\sigma(A)) = \mu(\sigma(A)\sigma(B))\\ 0 &\displaystyle \quad\text{otherwise}\end{array}\right. \\ &\displaystyle =&\displaystyle \left\{\begin{array}{ll} 1 &\displaystyle \quad\text{if}\ \ \mu(\sigma(A)) = \mu(\sigma(A))\wedge\mu(\sigma(B))\\ 0 &\displaystyle \quad\text{otherwise}\end{array}\right. \\ &\displaystyle =&\displaystyle \left\{\begin{array}{ll} 1 &\displaystyle \quad\text{if}\ \ \mu^*(A) = \mu^*(A)\wedge\mu^*(B)\\ 0 &\displaystyle \quad\text{otherwise}\end{array}\right. \end{array} \end{aligned} $$

Hence, by Definition 42, is an auto-Boolean interpretation of $\mathcal {L}_{\supset }$.

Now, suppose that Γ⊧φ and that for all ψ ∈ σ( Γ). By Definition 41 and the definition of , we have for any proposition ψ of $\mathcal {L}_{\supset }$: iff . Hence, for all ψ ∈ Γ. But since is an auto-Boolean interpretation of $\mathcal {L}_{\supset }$, it follows that . Thus, by the above biconditional, . So, if for all ψ ∈ σ( Γ), then . But since $(\mathfrak {A},\mu )$ was an arbitrary auto-Boolean interpretation of $\mathcal {L}_{=}$, this means that . □

The following theorem asserts that the containment calculus ⊢ is sound and complete with respect to the class of auto-Boolean interpretations of $\mathcal {L}_{\supset }$:

Theorem 44

For any set of propositions Γ of $\mathcal {L}_{\supset }$ and any proposition φ of $\mathcal {L}_{\supset }$: Γ ⊢ φ iff Γ⊧φ.

Proof

The left-to-right direction follows straightforwardly from the fact that the principles C1–C5, CP1–CP3, and PT1–PT3 are satisfied in every auto-Boolean interpretation.

For the right-to-left direction, suppose that Γ⊧φ. Then, by Theorem 43, . By Theorem 40, $\sigma (\Gamma )\Vdash \sigma (\varphi )$. By Theorem 37, τ(σ( Γ)) ⊢ τ(σ(φ)). Hence, by Theorem 35.ii, it follows that Γ ⊢ φ. □