Syllogistic Logic with Cardinality Comparisons, On Infinite Sets

TL;DR

This paper extends classical syllogistic logic to include set size comparisons on infinite sets, providing a formal logical system with soundness, completeness, and efficient proof algorithms.

Contribution

It introduces a novel logical framework combining syllogistic reasoning with cardinality comparisons for infinite sets, along with soundness, completeness, and algorithmic proof methods.

Findings

Established a soundness and completeness theorem.

Developed efficient algorithms for proof search.

Formalized a logic for set size comparisons on infinite sets.

Abstract

This paper enlarges classical syllogistic logic with assertions having to do with comparisons between the sizes of sets. So it concerns a logical system whose sentences are of the following forms: {\sf All $x$ are $y$} and {\sf Some $x$ are $y$}, {\sf There are at least as many $x$ as $y$}, and {\sf There are more $x$ than $y$}. Here $x$ and $y$ range over subsets (not elements) of a given \emph{infinite} set. Moreover, $x$ and $y$ may appear complemented (i.e., as $\overset{-}{x}$ and $\overset{-}{y}$), with the natural meaning. We formulate a logic for our language that is based on the classical syllogistic. The main result is a soundness/completeness theorem. There are efficient algorithms for proof search and model construction.

Equations

$$\begin{array}[]{lcl}{\mathbf{P}}&=&(P,\overline{\phantom{p}})\end{array}$$

$$\begin{array}[]{lcl}{\cal M}\models\forall(p,q)&\quad\mbox{iff}&[\![p]\!]\subseteq[\![q]\!]\\ {\cal M}\models\exists(p,q)&\quad\mbox{iff}&[\![p]\!]\cap[\![q]\!]\neq\emptyset\\ {\cal M}\models\exists^{\geq}(p,q)&\quad\mbox{iff}&\mbox{card}\,[\![p]\!]\geq\mbox{card}\,[\![q]\!]\\ {\cal M}\models\exists^{>}(p,q)&\quad\mbox{iff}&\mbox{card}\,[\![p]\!]>\mbox{card}\,[\![q]\!]\\ \end{array}$$

$$\begin{array}[]{l@{\qquad}l}\mbox{$\varphi$}&\overline{\varphi}\\ \hline\cr\forall(p,q)&\exists(p,\overline{q})\\ \exists(p,q)&\forall(p,\overline{q})\\ \exists^{\geq}(p,q)&\exists^{>}(q,p)\\ \exists^{>}(p,q)&\exists^{\geq}(q,p)\\ \end{array}$$

$$\begin{array}[]{c@{\quad}c@{\quad}c}\forall(p,p)&\forall(n,q)\lx@proof@logical@and\forall(n,p)\forall(p,q)\\ \\ \exists(p,p)\exists(p,q)&\exists(p,q)\exists(q,p)\\ \\ \exists(p,q)\lx@proof@logical@and\exists(p,n)\forall(n,q)&\forall(\overline{q},\overline{p})\forall(p,q)\\ \\ \forall(p,q)\forall(p,\overline{p})&\forall(q,p)\forall(\overline{p},p)\\ \\ \exists^{\geq}(q,p)\forall(p,q)&\exists^{\geq}(n,q)\lx@proof@logical@and\exists^{\geq}(n,p)\exists^{\geq}(p,q)\\ \\ \exists(q,q)\lx@proof@logical@and\exists(p,p)\exists^{\geq}(q,p)&\exists^{\geq}(p,q)\exists^{>}(p,q)\\ \\ \exists^{>}(n,q)\lx@proof@logical@and\exists^{>}(n,p)\exists^{\geq}(p,q)&\exists^{>}(n,q)\lx@proof@logical@and\exists^{\geq}(n,p)\exists^{>}(p,q)\\ \\ \exists(p,\overline{q})\exists^{>}(p,q)&\\ \\ &\\ \\ \varphi\lx@proof@logical@and\exists(p,q)\forall(q,\overline{q})&\varphi\lx@proof@logical@and\exists^{>}(p,q)\exists^{\geq}(q,p)\end{array}$$

$$\begin{array}[]{c@{\qquad}c}\exists(p,p)\exists^{\geq}(p,\overline{p})&\exists^{>}(p,\overline{p})\forall(\overline{p},p)\\ \\ \exists^{\geq}(\overline{p},x)\exists^{>}(q,p)\par&\exists^{\geq}(x,q)\lx@proof@logical@and\exists^{\geq}(x,p)\exists^{\geq}(x,\overline{p})\\ \\ \end{array}$$

$$\begin{array}[]{l@{\qquad\qquad}l}\exists(x,x)\exists^{\geq}(x,\overline{x})\forall(\overline{x},x)&\exists(x,x)\exists^{>}(x,\overline{x})\forall(\overline{x},x)\end{array}$$

$${\exists }^{\ge }(p,q)\text{lx@proof@logical@and}{\exists }^{\ge }(p,\overline{p}){\exists }^{\ge }(p,p)\forall (p,p)$$

$${\exists }^{\ge }(q,x)\text{lx@proof@logical@and}{\exists }^{\ge }(q,p){\exists }^{\ge }(p,x){\exists }^{\ge }(p,\overline{p})$$

$${\exists }^{>}(p,q)\text{lx@proof@logical@and}{\exists }^{\ge }(p,x){\exists }^{\ge }(p,\overline{p}){\exists }^{>}(x,q)$$

$${\exists }^{\ge }(q,\overline{q}){\exists }^{>}(p,\overline{q})\text{lx@proof@logical@and}{\exists }^{>}(p,\overline{p}){\exists }^{\ge }(\overline{p},\overline{q})$$

$$\exists (p,q){\exists }^{>}(p,\overline{q})\text{lx@proof@logical@and}{\exists }^{\ge }(p,q){\exists }^{\ge }(p,\overline{p}){\exists }^{>}(q,\overline{q})$$

$$\exists (q,q)\text{lx@proof@logical@and}{\exists }^{\ge }(q,p){\exists }^{\ge }(q,\overline{q})\exists (p,p)$$

$$\phi \text{lx@proof@logical@and}{\exists }^{>}(q,q)\text{lx@proof@logical@and}{\exists }^{>}(q,\overline{x}){\exists }^{\ge }(\overline{x},q){\exists }^{>}(p,x){\exists }^{\ge }(q,q)\forall (q,q)$$

$${\exists }^{>}(q,q)\text{lx@proof@logical@and}{\exists }^{>}(q,p){\exists }^{\ge }(p,q)\text{lx@proof@logical@and}{\exists }^{\ge }(p,\overline{p}){\exists }^{\ge }(\overline{p},q){\exists }^{>}(q,p)$$

$$\begin{array}[]{lcl}\Gamma&=&\{\exists^{>}(x_{0},x_{1}),\exists^{>}(x_{1},x_{2}),\ldots,\exists^{>}(x_{n},x_{n+1}),\ldots\}\end{array}$$

$$\begin{array}[]{c@{\quad}c@{\quad}c}\forall(q,p)\lx@proof@logical@and\forall(p,q)\exists^{\geq}(p,q)&\exists^{>}(p,q)\lx@proof@logical@and\forall(q,p)\exists(p,\overline{q})\\ \\ \exists^{>}(\overline{p},\overline{q})\exists^{>}(q,p)&\exists^{\geq}(\overline{q},\overline{p})\exists^{\geq}(p,q)\\ \\ \exists^{>}(p,q)\lx@proof@logical@and\exists^{>}(p,\overline{p})\exists^{\geq}(\overline{q},q)&\exists(p,q)\lx@proof@logical@and\exists^{\geq}(p,\overline{p})\exists^{\geq}(q,\overline{q})\exists(\overline{p},\overline{q})\\ \\ \end{array}$$

$$\begin{array}[]{lcl}[\![p]\!]&=&\{3n:n\in N\}\\ [\![q]\!]&=&\{3n+1:n\in N\}\end{array}$$

$$\bigcup _{i=1}^n(\{i\}\times X_i).$$

$$\begin{array}[]{lcl}(X\cup Y)+Z&=&\{(1,x):x\in X\}\cup\{(1,y):y\in Y\}\cup\{(2,z):z\in Z\}\end{array}$$

$$\begin{array}[]{l@{\quad}c@{\quad}l}\Gamma\vdash\exists^{\geq}(q,p)&\mbox{and}&\Gamma\not\vdash\exists^{\geq}(p,q).\\ \end{array}$$

$$\begin{array}[]{lcl}[\![p]\!]_{{\cal N}}&=&\bigcup\{A_{i}:i\in[\![p]\!]_{{\cal M}}\}.\end{array}$$

$$\begin{array}[]{lcl}[\![\overline{p}]\!]_{{\cal N}}&=&\bigcup\{A_{i}:i\notin[\![p]\!]_{{\cal M}}\}.\end{array}$$

$$\begin{array}[]{lcl}Q&=&\{p\in\mbox{\sf small}:\Gamma\vdash\exists(p,p)\}\end{array}$$

$$(Q/{\equiv }_c,{<}_c),$$

$$[p_1],\dots ,[p_n].$$

$$\begin{array}[]{lcl}\Gamma_{i}&=&\{\varphi\in\Gamma:\mbox{ all variables in $\varphi$ belong to $[p_{i}]$}\}\\ \Delta_{i}&=&\{\varphi\in\Gamma_{i}:\mbox{$\varphi$ is a sentence in $\forall$ or $\exists$}\}\cup\{\exists(x,x):x\in[p_{i}]\}\end{array}$$

$${\text{SS}}_i\models {\Delta }_i$$

$$\text{mbox}card{S}_i={\kappa }_i$$

$$\text{mbox}card[[x]{]}_{{\text{SS}}_i}={\kappa }_i$$

$$p,q\in [p_i]$$

Full text

**Keywords: ** Logic of natural languages; completeness; syllogistic logic;

infinite sets; cardinality comparisons

1 Introduction

This paper is a contribution to the study of extended syllogistic logics. The idea is to take the classical syllogistic ${\mathcal{S}}$ as a base system and to extend this base with reasoning power for some phenomenon which is not expressible in first-order logic, and then to show that on top of the small base, the resulting system is still well-behaved. We thus take the logical system ${\mathcal{S}}$ whose sentences are of the form All $p$ are $q$ and Some $p$ are $q$, and No $p$ are $q$. We shall explain the semantics shortly, but for the time being we do without the semantics. To add expressive power, we also allow the variables to be complemented. So for each $p$ we would also have $\overline{p}$; the interpretation is the set theoretic complement of $[\![p]\!]$. The complementation operation also provides an extra natural sentence coming from the Aristotelian syllogistic to the system: Some $p$ are not $q$. In our work, this is expressed via the syntax Some $p$ are $\overline{q}$. We call this system ${\mathcal{S}}^{\dagger}$.

In formulating ${\mathcal{S}}^{\dagger}$, we may omit No $x$ are $y$, as it is equivalent to All $x$ are $\overline{y}$. This paper enlarges the syntax with assertions There are at least as many $x$ as $y$, and There are more $x$ than $y$. In this paper, we require the universe to be infinite. The case of finite universes was treated in [moss:forDunn] The syntax and semantics of the systems are exactly the same. But the main point of the paper is to craft a sound and complete proof system, and the proof system in this paper is different from the one in [moss:forDunn].

Syntax: preliminary

Here is the definition of the logical language $\mathcal{L}({\mathbf{P}})$ which we study in this paper. A noun system is a pair

[TABLE]

where $P$ is a set, and $p\mapsto\overline{p}$ is an involutive operation on $P$. Thus, $\overline{\overline{p}}=p$ for all $p\in{\mathbf{P}}$. We call the elements of ${\mathbf{P}}$ nouns. All Roman letters $p$, $q$, $x$, $y$, $\ldots$ denote nouns.

We fix a noun system ${\mathbf{P}}$ for the rest of this paper.

Syntax of $\mathcal{L}({\mathbf{P}})$:

$\mathcal{L}({\mathbf{P}})$ has sentences $\forall(p,q)$ and $\exists(p,q)$, $\exists^{\geq}(p,q)$, $\exists^{>}(p,q)$. We read “$\exists^{\geq}(p,q)$” as “there are at least as many $p$ as $q$”, and we read “$\exists^{>}(p,q)$” as “there are more $p$ than $q$.” There are no connectives.

Semantics

Definition 1.1**.**

A structure $\SS$ is a pair consisting of a set $S$ and an interpretation function $[\![\ ]\!]:{\mathbf{P}}\to\mathcal{P}(S)$, where $\mathcal{P}(S)$ is the power set of $S$. That is, a structure is a set $S$ together with a function which interprets nouns as subsets of $S$. A model is a structure ${\cal M}=(M,[\![\ ]\!])$ with the additional property that for all $p$, $[\![\overline{p}]\!]=M\setminus[\![p]\!]$ for all nouns $p$.

We define the satisfaction relation between models and sentences as follows:

[TABLE]

On the right in (1), the symbol $\mbox{card}\,S$ stands for the cardinality of a given set $S$.

Remark 1.2**.**

Our treatment of cardinality and of cardinal comparison is completely standard. We recall that $\mbox{card}\,(X)\leq\mbox{card}\,(Y)$ means that there is a one-to-one $f:X\to Y$. Also, $\mbox{card}\,(X)<\mbox{card}\,(Y)$ means that $\mbox{card}\,(X)\leq\mbox{card}\,(Y)$, but $\neg(\mbox{card}\,(Y)\leq\mbox{card}\,(X))$. All of our work with infinite cardinals is also standard. We remind the reader that if $X$ and $Y$ are infinite sets, then $\mbox{card}\,(X\cup Y)=\max(\mbox{card}\,(X),\mbox{card}\,(Y))$.

In addition, we use the Axiom of Choice at several points in this paper. For example, if ${\cal M}\models\exists^{>}(p,q)$ is false, then ${\cal M}\models\exists^{\geq}(q,p)$ is true. We also use it equivalent, Zorn’s Lemma, in the proof of Lemma 5.4.

Let us also mention that the main result in this paper needs very little set theory. The only notable point is that there are infinitely many infinite cardinals.

Remark 1.3**.**

We study our logic on infinite models ${\cal M}$ in this paper. However, $[\![p]\!]$ is not required to be infinite. It might even be empty.

Special attention should be given to sentences $\exists^{\geq}(p,\overline{p})$. When the universe of a model is finite, $\exists^{\geq}(p,\overline{p})$ says that there are at least as many $p$s as non-$p$s. This sentence $\exists^{\geq}(p,\overline{p})$ might, therefore, be read as “the $p$’s are at least half of the objects in the universe.” Similarly, $\exists^{\geq}(\overline{p},p)$ might be read as “the $p$’s are at most half of the objects in the universe.” We can also read $\exists^{>}(p,\overline{p})$ as “the $p$’s are more than half of the objects in the universe,” and $\exists^{>}(\overline{p},p)$ as “the $p$’s are less than half of the objects in the universe.” However, in this paper, all models ${\cal M}$ have an infinite universe $M$. So our talk about “half” must be taken with a grain of salt. To say that ${\cal M}\models\exists^{\geq}(p,\overline{p})$ in fact says that $\mbox{card}\,[\![p]\!]=\mbox{card}\,M$. To say that $\exists^{>}(p,\overline{p})$ says that $\mbox{card}\,[\![p]\!]=\mbox{card}\,M$ and also $\mbox{card}\,[\![\overline{p}]\!]<\mbox{card}\,M$.

Definition 1.4**.**

For every sentence $\varphi$, there is a sentence $\overline{\varphi}$ such that ${\cal M}\models\overline{\varphi}$ iff ${\cal M}\not\models\varphi$. Here is how this works:

[TABLE]

The operation symbol $\overline{\phantom{\varphi}}$ on sentences is not part of the language $\mathcal{L}({\mathbf{P}})$.

Definition 1.5**.**

Let $\Gamma\cup\{\varphi\}\subseteq\mathcal{L}({\mathbf{P}})$. ${\cal M}\models\Gamma$ means that ${\cal M}\models\varphi$ for all $\psi\in\Gamma$ and $\Gamma\models\varphi$ means that if ${\cal M}\models\Gamma$, then also ${\cal M}\models\psi$.

1.1 Proof system

The main goal of this paper is to present a sound and complete logic for the semantic consequence relation $\Gamma\models\varphi$. This section describes the system and provides examples. The rules of the logic are shown in Figures 1 and 2.

Let $\Gamma$ be a set of sentences in $\mathcal{L}({\mathbf{P}})$. A proof tree over $\Gamma$ is a finite tree ${\cal T}$ whose nodes are labelled with sentences, and each node is either a leaf node labelled with an element of $\Gamma$, or else matches one of the rules in the proof system in one of Figures 1 or 2. $\Gamma\vdash\varphi$ means that there is a proof tree ${\cal T}$ for over $\Gamma$ whose root is labelled $\varphi$.

Proposition 1.6** (Soundness).**

If $\Gamma\vdash\varphi$, then $\Gamma\models\varphi$.

Proof.

By induction on the heights of proof trees. The proof reduces to showing that all of the rules are individually sound. The rules in Figure 1 discussed in [moss:forDunn], and in any case they are easy to justify.

We show the soundness of the rules in Figure 2 by considering a single (arbitrary) infinite model ${\cal M}$, say of size $\kappa$. We assume the hypotheses of the rules in turn and show the conclusions. This will show that our logic is sound.

Let us show the soundness of (non-empty). If $\exists^{\geq}(p,\overline{p})$, then $[\![p]\!]=\kappa>0$.

The rule (non-empty-more) is sound because infinite sets are not empty.

Consider (weak-more-anti). If $\mbox{card}\,[\![q]\!]>\mbox{card}\,[\![p]\!]$, then $\mbox{card}\,[\![p]\!]<\kappa$. And so $\mbox{card}\,[\![\overline{p}]\!]=\kappa$. Thus $\mbox{card}\,[\![\overline{p}]\!]\geq\mbox{card}\,[\![x]\!]$ for all $x$.

Turning to (up), suppose that $[\![x]\!]$ is at least as large as both $[\![p]\!]$ and $[\![\overline{p}]\!]$. Then $[\![x]\!]$ is at least as their maximum. And this maximum is $\mbox{card}\,M$. So $[\![x]\!]$ is at least as large as the size of any set. ∎

This concludes our discussion of the soundness of the logic. We turn to examples.

Example 1.7**.**

$\forall(\overline{x},x)\vdash\exists(x,x)$. Here are two different derivations:

[TABLE]

Example 1.8**.**

$\exists^{\geq}(p,\overline{p})\vdash\exists^{\geq}(p,q)$. Here is a derivation:

[TABLE]

Example 1.9**.**

$\exists^{\geq}(p,\overline{p}),\exists^{\geq}(q,p)\vdash\exists^{\geq}(q,x)$. Here is a derivation which quotes the result just above:

[TABLE]

Example 1.10**.**

$\exists^{\geq}(p,\overline{p}),\exists^{>}(x,q)\vdash\exists^{>}(p,q)$:

[TABLE]

Example 1.11**.**

$\exists^{>}(p,\overline{p}),\exists^{\geq}(\overline{p},\overline{q})\vdash\exists^{>}(q,\overline{q})$:

[TABLE]

Example 1.12**.**

$\exists^{\geq}(p,\overline{p}),\exists^{>}(q,\overline{q})\vdash\exists(p,q)$:

[TABLE]

Example 1.13**.**

Here is a rules from [moss:forDunn] called (int). We include this rule because it is used later in this paper. (int) says $\exists(p,p),\exists^{>}(q,\overline{q})\vdash\exists(q,q)$. Here is a derivation:

[TABLE]

Example 1.14**.**

We have a derivation of $\exists^{>}(p,x),\exists^{>}(q,\overline{x})\vdash\varphi$. That is, we derive a contradiction from the two assumptions $\exists^{>}(p,x)$ and $\exists^{>}(q,\overline{x})$.

[TABLE]

Example 1.15**.**

$\exists^{\geq}(p,\overline{p}),\exists^{>}(q,p)\vdash\varphi$. Here is a derivation:

[TABLE]

And the rest at the bottom is as in Example 1.14.

Remark 1.16**.**

In the remainder of this paper, $\Gamma$ denotes a finite set of sentences. The reason for this restriction is that the logic is not compact. Specifically, the set

[TABLE]

has no model, but every finite subset of it does have a model. So $\Gamma\models\forall(p,q)$. But clearly we cannot have $\Gamma\vdash\exists(p,q)$, no matter what the rules of the (sound) proof system are. That is, we cannot hope to define a proof system and show that for all (possibly infinite) $\Gamma$ and all $\varphi$: $\Gamma\models\varphi$ iff $\Gamma\vdash\varphi$.

1.2 Prior work

We make a short digression at this point to mention the difference between the logical system in [moss:forDunn] and the one here. The reader not interested in this point may safely skip ahead to Section 1.3.

The syntax used in this paper is exactly the same as the one in [moss:forDunn]. The definition of ${\cal M}\models\varphi$ is the same, too. The difference lies in the fact that in [moss:forDunn], the models were taken to be finite, while in this paper they are taken to be infinite. The rules in Figure 3 are from [moss:forDunn]; they are not sound on infinite models.

Let us check that these are not sound when we allow the universe to be infinite. We give some counterexamples. In all cases, we take $M=\omega$.

For (card-mix), let $[\![q]\!]=\omega\setminus\{0\}$ and $[\![p]\!]=\omega$.

For (more), let $[\![q]\!]=\omega\setminus\{0\}$ and $[\![p]\!]=\omega$.

For (more-anti), let $[\![q]\!]=\{0,1\}$ and let $[\![p]\!]=\{0\}$.

For (card-anti), $[\![p]\!]=\omega$ and let $[\![q]\!]=\omega\setminus\{0\}$.

For (strict-half), let $[\![p]\!]=\omega$, and let $[\![q]\!]$ be the set of even numbers. Then $\mbox{card}\,[\![p]\!]>\mbox{card}\,[\![\overline{p}]\!]$, and $\mbox{card}\,[\![q]\!]=\mbox{card}\,[\![\overline{q}]\!]$; but $\mbox{card}\,[\![p]\!]\not>\mbox{card}\,[\![q]\!]$.

For (maj), let

[TABLE]

Then $\mbox{card}\,[\![p]\!]=\mbox{card}\,[\![\overline{p}]\!]=\mbox{card}\,[\![q]\!]=\mbox{card}\,[\![\overline{q}]\!]$. Then $2\in[\![\overline{p}]\!]\cap[\![\overline{q}]\!]$, but $[\![p]\!]\cap[\![q]\!]=\emptyset$.

Theorem 1.17**.**

[moss:forDunn] The logical system whose rules are shown in Figures 1 and 3 is sound and complete for the class of all finite models.

1.3 Consistent sets

A set of sentences in any logic is consistent if it is not the case that $\Gamma\vdash\varphi$ for all $\varphi$. In our setting, this is equivalent to saying that there are no derivations from $\Gamma$ which use one of the two ex falso quodlibet rules, (x) or (x-card).

Example 1.18**.**

If $\Gamma$ is consistent and contains $\exists^{>}(p,x)$, then $\Gamma\not\vdash\exists^{>}(q,\overline{x})$ for all $q$. This follows from Example 1.14. Similarly, Example 1.15 shows that if $\Gamma$ is consistent and contains $\exists^{>}(q,p)$, then $\Gamma\not\vdash\exists^{\geq}(p,\overline{p})$.

Example 1.19**.**

For all consistent $\Gamma$, there is some $x$ such that $\Gamma\not\vdash\forall(x,\overline{x})$. To see this, take any variable $x$. Suppose that $\Gamma\vdash\forall(x,\overline{x})$. By (non-empty), $\Gamma\vdash\exists(\overline{x},\overline{x})$. If we also had $\Gamma\vdash\forall(\overline{x},x)$, then $\Gamma$ would be inconsistent.

1.4 Architecture of the completeness result in this paper

The main result in this paper is the Completeness Theorem 7.1. We shall show the following: (1) For a given set $\Gamma$ and sentence $\varphi$, if $\Gamma\not\vdash\varphi$, then there is a model of $\Gamma$ where $\varphi$ is false.

Before we prove this theorem, we show the weaker statement (2) every consistent set $\Gamma$ has a model. Let us explain why (2) is weaker than (1). If we take the special case of (1) when $\Gamma$ is $\exists(x,\overline{x})$, then we get: if $\Gamma$ is consistent, then $\Gamma$ has a model. So we basically get (2) as a special case of (1). Now in logics with a rule of reductio ad absurdum (raa), (2) implies (1). Here is the argument. Suppose that $\Gamma\not\vdash\varphi$. Then $\Gamma\cup\{\neg\varphi\}$ is consistent. (This is exactly where (raa) is used. And us by (2), we have a model ${\cal M}$ of $\Gamma$ where $\varphi$ fails; so (1) holds. Now our logic does not have (raa), since it complicates the proof search to add it. (That is, (raa) is an admissible rule, as we shall prove following completeness. But adopting (raa) from the start would lead to a proof search algorithm that is more complicated that necessary. As far as we can see, it would not be in polynomial time. So the extra work that we shall do by using the (x) rules leads to a more efficient proof search algorithm.

2 Preliminaries

In this section, we gather some preliminary background material which will be used later in the paper.

2.1 Preliminary: listings of finite transitive relations

A listing of a set $X$ is a sequence $x_{1},\ldots,x_{n}$ from $X$ so that if $i\neq j$, then $x_{i}\neq x_{j}$. Let $(T,<)$ be a finite set with a transitive, irreflexive relation. A proper listing of $(T,<)$ is a listing of the set $T$ with the property that if $t_{i}<t_{j}$, then $i<j$. In words, the $<$-predecessors of each point are listed before it. This is also called a topological sort.

Lemma 2.1**.**

Let $(T,<)$ be a finite set with a transitive, irreflexive relation. Then $(T,<)$ has a proper listing.

Lemma 2.2**.**

Let $(T,<)$ be a finite set with a transitive, irreflexive relation. Let $y\in T$. Then there is a proper listing of $(T,<)$ in which every $x$ such that $y\not\leq x$ comes before $y$ in the listing.

Lemma 2.1 is standard, and Lemma 2.2 is small refinement. One source for the proofs is [moss:forDunn].

2.2 Preliminary: unions and disjoint unions

Beginning in Section 5.3, we shall need to keep track of the difference between unions and disjoint unions. Given sets $X_{1}$, $\ldots$, $X_{n}$, we write $X_{1}+\cdots+X_{n}$ for

[TABLE]

We also write $\sum_{i=1}^{n}\,X_{i}$ for this same set. We make use of this notation even when some of the sets $X_{i}$ are themselves unions of other sets. For example,

[TABLE]

3 The relations $\leq$, $\leq_{c}$, $<_{c}$, $<_{more}$, and $\equiv$

The method of proof of (1) in Section 1.4 is model-construction. We fix a consistent set $\Gamma$ throughout this section. It is convenient to suppress $\Gamma$ from the notation. We also will adopt suggestive notation for various assertions in the logic.

Definition 3.1**.**

Let $\Gamma$ be a (finite) set of sentences. We write $x\leq y$ for $\Gamma\vdash\forall(x,y)$. Note that $\Gamma$ is left off the notation. And we write $x\equiv y$ for $x\leq y\leq x$.

We write $x\leq_{c}y$ for $\Gamma\vdash\exists^{\geq}(y,x)$. We also write $x\equiv_{c}y$ for $x\leq_{c}y\leq_{c}x$, and $x<_{c}y$ for $x\leq_{c}y$ but $x\not\equiv_{c}y$.

Finally, we write $x<_{more}y$ if $\Gamma\vdash\exists^{>}(y,x)$.

Proposition 3.2**.**

Let ${\cal V}$ be the set of variables in $\Gamma$, and let $w$, $x$, $x^{\prime}$, $y$, $y^{\prime}$, $z\in{\cal V}$.

If $x\leq y$, then $x\leq_{c}y$. 2. 2.

$({\cal V},\leq_{c})$ is a preorder: a reflexive and transitive relation. 3. 3.

$({\cal V},<_{c})$ is a strict preorder. 4. 4.

If $x\leq_{c}y$, $x\equiv x^{\prime}$, and $y\equiv y^{\prime}$, then $x^{\prime}\leq_{c}y^{\prime}$. 5. 5.

If $w\leq_{c}x<_{more}y\leq_{c}z$, then $w\leq_{more}z$.

Proof.

Part (1) uses the (subset-size) rule. In part (2), the reflexivity of $\leq_{c}$ comes from that of $\leq$ and part (1); the transitivity is by (card-trans). Part (3) follows from the previous part. Part (4) uses part (1) and transitivity. Part (5) uses (more-left) and (more-right). ∎

Remark 3.3**.**

Let us emphasize that there is a difference between $<_{c}$ and $<_{more}$. When we write $p<_{c}q$, we mean that

[TABLE]

This is weaker than $p<_{more}q$; recall that this last assertion means that $\Gamma\vdash\exists^{>}(q,p)$. For example, if $\Gamma$ contains just the sentence $\exists^{\geq}(q,p)$ (and nothing else), then $p<_{c}q$ but not $p<_{more}q$.

4 Small, large, and half

Let $\Gamma$ be consistent in $\mathcal{L}({\mathbf{P}})$. Define a partition of variables of $\mathcal{L}({\mathbf{P}})$ into three classes, as follows:

For all $p$ such that $p\leq_{c}\overline{p}\leq_{c}p$, put both $p$ and $\overline{p}$ into half. 2. 2.

For all $p$ such that $p<_{more}q$ for some $q$, put $p\in\mbox{\sf small}$ and $\overline{p}\in\mbox{\sf large}$. 3. 3.

Put all other nouns in half.

We call this the standard partition of the nouns according to $\Gamma$.

Lemma 4.1**.**

Let $\Gamma$ be consistent in $\mathcal{L}({\mathbf{P}})$. The standard partition puts each $p$ and $\overline{p}$ into exactly one of the three class small, half, and large. Moreover, this partition has the following properties:

1. (i)

If ($p\leq_{c}\overline{p}$ and $\overline{p}\leq_{c}p$), then $p,\overline{p}\in\mbox{\sf half}$. 2. (ii)

If $p<_{more}q$ for some $q$, then $p\in\mbox{\sf small}$. 3. (iii)

$p\in\mbox{\sf large}$ iff $\overline{p}\in\mbox{\sf small}$. 4. (iv)

If $p\in\mbox{\sf small}$ and $q\leq_{c}p$, then $q\in\mbox{\sf small}$. 5. (v)

If $p\leq_{c}\overline{p}$, then either ($p\in\mbox{\sf small}$ and $\overline{p}\in\mbox{\sf large}$), or else $p,\overline{p}\in\mbox{\sf half}$. 6. (vi)

If $p\in\mbox{\sf half}$ and $q\leq_{c}p$, then either $q\in\mbox{\sf small}$ or $q\in\mbox{\sf half}$. 7. (vii)

If $\overline{p}\leq p$ (that is, $\Gamma\vdash\forall(\overline{p},p)$), then $\overline{p}\in\mbox{\sf small}$ and $p\in\mbox{\sf large}$.

Proof.

The main thing is to check that the first two points in the definition of the standard partition cannot conflict. Here are the verifications. If $p\leq_{c}\overline{p}\leq_{c}p$, then we cannot also have $p<_{more}q$. (See Example 1.15.) We cannot have both $p<_{more}q$ and $\overline{p}<_{more}x$. (See Example 1.14.)

Parts (i) – (iii) are immediate from the construction. Part (iv) follows from Proposition 3.2.

Then, we check that (v) holds. Suppose that $p\leq_{c}\overline{p}$ but that neither of the conditions in (v) hold. By (iii), $\overline{p}\in\mbox{\sf small}$ and $p\in\mbox{\sf large}$. But then by (iv), $p\in\mbox{\sf small}$. And this is a contradiction.

For (vi), suppose that $p\in\mbox{\sf half}$ and $q\leq_{c}p$, and towards a contradiction that $q\in\mbox{\sf large}$. Then $\overline{p}\leq_{c}q$. But also $p\leq_{c}\overline{p}$, so we have $p\equiv_{c}q$. And this is a contradiction, since $q\in\mbox{\sf large}$. (So again we are using Proposition 3.2.)

Part (vii) follows immediately from (non-empty-more). ∎

4.1 Refinement

We also need a refined version of the standard partition. Let $\Gamma$ be consistent. Fix a noun $p^{*}$. Suppose that $\neg(\overline{p}^{*}\leq_{c}p^{*})$, and also that there are no $x$ such that $\overline{p}^{*}<_{more}x$. Then the standard partition might put $p^{*}\in\mbox{\sf half}$ (due to the final step in the definition of the standard partition), and it might put $p^{*}\in\mbox{\sf small}$. But it cannot put $p^{*}\in\mbox{\sf large}$. In case it puts $p^{*}\in\mbox{\sf half}$, we might want a modification which instead puts $p^{*}\in\mbox{\sf small}$.

Therefore we modify the standard partition, as follows:

For all $p$ such that $p\leq_{c}p^{*}$, put $p\in\mbox{\sf small}$ and $\overline{p}$ in large. 2. 2.

For all $p$ such that $p\leq_{c}\overline{p}\leq_{c}p$, put both $p$ and $\overline{p}$ into half. 3. 3.

For all $p$ such that $p<_{more}q$ for some $q$, put $p\in\mbox{\sf small}$ and $\overline{p}\in\mbox{\sf large}$. 4. 4.

Put all other nouns in half.

Lemma 4.2**.**

Let $\Gamma$ be consistent in $\mathcal{L}({\mathbf{P}})$. Let $p^{*}$ be such that $\neg(\overline{p}^{*}\leq_{c}p^{*})$, and also that there are no $x$ such that $\overline{p}^{*}<_{more}x$. Then the refined version of the standard partition puts $p^{*}\in\mbox{\sf small}$, and it also puts each of $p$ and $\overline{p}$ into exactly one of the three classes small, half, and large. Moreover, all of the points in Lemma 4.1 hold.

Proof.

This time, we must check that the first three points in the definition of the standard partition cannot conflict. Since there are no conflicts between (2) and (3), we only need to check conflicts between (1) for a noun $p$ and its complement $\overline{p}$, conflicts between (1) and (2), and finally conflicts between (1) and (3)

For all $p$, we cannot have $p\leq_{c}p^{*}$ and also $\overline{p}\leq_{c}p^{*}$. This is by (up), taking $x$ to be $p^{*}$.

Concerning conflicts between (1) and (2), suppose that $p\leq_{c}\overline{p}\leq_{c}p$ and also that $p\leq_{c}p^{*}$. Then by Example 1.9, we have $\overline{p}^{*}\leq_{c}p^{*}$, and this contradicts our assumption on $p^{*}$ in this result.

As for conflicts between (1) and (3), suppose that $\overline{p}<_{more}q$ and $p\leq_{c}p^{*}$. Then by Example 1.10, $\overline{p}^{*}<_{more}q$. So again we have a contradiction.

The verification of (i) – (vii) is nearly the same as what we saw in Lemma 4.1. That is, (i)–(iv) are immediate from the construction, and (v) and (vi) follow easily from these. ∎

The work in this section is used in Section 7.2.

4.2 A result on infinite models and the logic of All, Some, and complemented variables

Lemma 4.3**.**

Let $\kappa$ be an infinite cardinal. Let $\Delta$ be a finite consistent set of sentences of the form $\exists(p,q)$ and $\forall(p,q)$. Then $\Delta$ has a model with the following properties:

All nouns $p$ have the property that either $[\![p]\!]=\emptyset$, or $[\![\overline{p}]\!]=\emptyset$, or both $[\![p]\!]$ and $[\![\overline{p}]\!]$ are sets of cardinality exactly $\kappa$. 2. 2.

For all $p$ and $q$, $[\![p]\!]\cap[\![q]\!]\neq\emptyset$ iff $\Gamma\vdash\exists(p,q)$. (A special case is when $p=q$, We see that $[\![p]\!]=\emptyset$ iff $\Gamma\not\vdash\exists(p,p)$.)

Proof.

Since our logic includes a complete syllogistic logic of $\exists$ and $\forall$, $\Delta$ is consistent in the syllogistic logic of sentences $\forall(p,q)$, and $\exists(p,q)$. By [logic:moss08], $\Delta$ has a finite model ${\cal M}$ with the extra property that if $\Delta\not\vdash\exists(p,q)$, then $[\![p]\!]\cap[\![q]\!]=\emptyset$. Fix such a model ${\cal M}$. Let $p_{1}$, $\overline{p}_{1}$, $\ldots$, $p_{k}$, $\overline{p}_{k}$ include the finite set of nouns that occur in sentences in $\Delta$. (Since we are only dealing with finite sets of sentences, this is a finite set.) Let the universe $M$ of the model ${\cal M}$ be $\{1,\ldots,m\}$. Let $A_{1}$, $\ldots$, $A_{k}$ be a pairwise disjoint family of sets of size exactly $\kappa$. (For example, we might have $A_{i}=\kappa\times\{i\}$.) Then make a new model ${\cal N}$ by taking the universe $N$ to be $\bigcup\{A_{i}:1\leq i\leq k\}$, and then by interpreting each $p$ thus:

[TABLE]

It then follows that

[TABLE]

The assertions about $[\![p]\!]$ and $[\![\overline{p}]\!]$ in our result are easy to check.

Claim 4.4**.**

${\cal M}$ and ${\cal N}$ agree on all sentences using $\forall$ and $\exists$.

Proof.

Consider first a sentence $\forall(a,b)$. Assume that ${\cal M}\models\forall(a,b)$. So $[\![a]\!]_{\cal M}\subseteq[\![b]\!]_{\cal M}$. Let $\alpha\in[\![a]\!]_{\cal N}$. So for some $i\in[\![a]\!]_{\cal M}$, $\alpha\in A_{i}$. But this $i$ belongs also to $[\![b]\!]_{\cal M}$. And therefore $\alpha\in[\![b]\!]_{\cal N}$. This for all $\alpha$ shows that $[\![a]\!]_{\cal N}\subseteq[\![b]\!]_{\cal N}$. In the other direction, assume that $[\![a]\!]_{\cal N}\subseteq[\![b]\!]_{\cal N}$. Let $i\in[\![a]\!]_{\cal M}$. Since $A_{i}$ is infinite, it is non-empty. Let $\alpha\in A_{i}$. Thus $\alpha\in[\![a]\!]_{\cal N}$. By our assumption, $\alpha\in[\![b]\!]_{\cal N}$. And since the sets $A_{j}$ are pairwise disjoint, we see that $i\in[\![b]\!]_{\cal M}$. This for all $i$ shows that $[\![a]\!]_{\cal M}\subseteq[\![b]\!]_{\cal M}$.

We turn to the sentences $\exists(a,b)$. Assume that ${\cal M}\models\exists(a,b)$, and let $i\in[\![a]\!]_{\cal M}\cap[\![b]\!]_{\cal M}$. Let $\alpha\in A_{i}$. Then $\alpha\in[\![a]\!]_{\cal N}\cap[\![b]\!]_{\cal N}$. So ${\cal N}\models\exists(a,b)$. Going the other way, assume that ${\cal N}\models\exists(a,b)$. Let $\alpha\in[\![a]\!]_{\cal N}\cap[\![b]\!]_{\cal N}$. We have $i\in[\![a]\!]_{\cal M}$ and $j\in[\![b]\!]_{\cal M}$ so that $\alpha\in A_{i}\cap A_{j}$. But since the $A$’s are pairwise disjoint, we have $i=j$. Then $i\in[\![a]\!]_{\cal M}\cap[\![b]\!]_{\cal M}$. And $i$ shows us that ${\cal M}\models\exists(a,b)$, as desired. ∎

By this claim, ${\cal N}\models\Delta$. Finally, suppose that $\Gamma\not\vdash\exists(p,q)$. Then in ${\cal M}$, $[\![p]\!]\cap[\![q]\!]=\emptyset$. It follows that the same is true in ${\cal N}$. Finally, suppose that $[\![p]\!]_{{\cal N}}\neq\emptyset$. As we have just seen, this means that $\Gamma\vdash\exists(p,p)$.

Finally, each interpretation $[\![p]\!]_{{\cal N}}$ is either empty or has size $\kappa$, by construction. ∎

5 Consistent sets have models

Theorem 5.1**.**

Every consistent (finite) set $\Gamma$ has a model ${\cal M}$. Moreover, given a partition of the nouns into three classes as in Lemma 4.1, we can find a model ${\cal M}$ with the following additional properties:

If $p,q\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$ and $[\![p]\!]\cap[\![q]\!]\neq\emptyset$, then $\Gamma\vdash\exists(p,q)$. 2. 2.

If $[\![p]\!]\neq\emptyset$, then $[\![p]\!]$ is infinite.

The rest of this section is devoted to the construction of a model; the verification that it works is in Section 6. The actual completeness theorem of the logic is a stronger result, and it appears as Theorem 7.1 below.

Before the construction: find the partition and the listing

Fix $\Gamma$, and hence $\leq$, $\leq_{c}$, $<_{more}$, and $\equiv$. Let

[TABLE]

Note that if $p\in Q$ has this property and $p\equiv_{c}q$, then also $q\in Q$. This is due to the rule (int) which is derivable in our system.

To begin, use Lemma 4.1 to partition the nouns into the three sets small, half, and large. The relation $\equiv_{c}$ is an equivalence relation on the nouns, and $<_{c}$ is an irreflexive and transitive relation on the quotient set. We write $[p_{i}]$ for $\{q:q\equiv_{c}p_{i}\}$. Use Lemma 2.1, and fix a listing of the strict (irreflexive) order on the quotient set

[TABLE]

say as

[TABLE]

(This sequence is finite because $\Gamma$ is a finite set of sentences.)

Our construction has several steps. In Steps $1$, $\ldots$, $n$, we carry out a construction for each term in (3). Step $i$ builds something which is a structure (see Definition 5.2 just below) but probably not a model in our sense.

Definition 5.2**.**

Let $A$ be a set of nouns. A structure over $A$ is a set $S$ together with interpretations $[\![x]\!]$ of all $x\in A$. (Again, the difference between a structure and a model is that a structure need not interpret $\overline{x}$ for $x\in A$. For that matter, $A$ could be empty; in that case, a structure over $A$ is just a set.) We denote structures by letters $\SS$.

Step $i$ will produce a structure $\SS_{i}$ over $[p_{i}]$. We also use the notation $\kappa_{i}$ for $\mbox{card}\,\SS_{i}$. In Step $n+1$, we do the same thing for half, obtaining a structure over half. Note that half is closed under complements, unlike all of the classes $[p_{i}]$ in (3). After this, we put the models $\SS_{1}$, $\SS_{2}$, $\ldots$, $\SS_{n}$, $\SS_{n+1}$ together, in a non-obvious way. And at the end, we have a final step for the nouns in large. Then we turn our structure into a model.

5.1 Construction:

$i=1,\ldots n$.

We remind the reader that the listing in (3) is a topological sort of the equivalence classes $[x]$ modulo $\equiv_{c}$ which are in small and which have the property that $\Gamma\vdash\exists(x,x)$. It is possible that $n=0$, and in that case we skip ahead to Section 5.2.

Let $\kappa_{1}=\aleph_{0}$. Given $\kappa_{i-1}$, we first give the definition of $\kappa_{i}$, and then this is used in the definition of $\SS_{i}$.

Definition 5.3**.**

Let $2\leq i\leq n$. We say that $i$ demands a larger size if for some $j<i$, $p_{j}<_{more}p_{i}$ but $\kappa_{j}=\kappa_{i-1}$. (Please note that for $i=n+1$ we shall see a different definition in Section 5.2.)

(Here is the point of this definition: Suppose that $i$ demands a larger size. We make sure that $\SS_{i}$ is of size strictly larger than $\SS_{i-1}$, and we interpret all $x\in[p_{i}]$ by sets whose size is that of the universe $S_{i}$ of $\SS_{i}$. Thus, $[\![x]\!]$ will be a set which is larger than the size of $[\![y]\!]$ whenever $\exists^{>}(x,y)$ is in $\Gamma$.)

If $i=1$, then as we have mentioned, $\kappa_{i}=\aleph_{0}$. If $i>1$ demands a larger size, set $\kappa_{i}=(\kappa_{i-1})^{+}$. (This is the smallest infinite cardinal larger than $\kappa_{i}$.) If $i>1$ does not demand a larger size, set $\kappa_{i}=\kappa_{i-1}$.

Continuing, let

[TABLE]

Let $\SS_{i}$ be a structure obtained by applying Lemma 4.3 so that

[TABLE]

[TABLE]

[TABLE]

[TABLE]

5.2 Construction: step $n+1$, for the nouns in half

At this point, we take care of the nouns in half. Even if $\mbox{\sf half}=\emptyset$, our construction still might need to increase the overall size of the model to be sure that the interpretations of variables in large are truly larger than those in small.

At step $n+1$, we have structures $\SS_{1}$, $\ldots$, $\SS_{n}$ and also $\kappa_{1}$, $\ldots$, $\kappa_{n}$. Before building $\SS_{n+1}$, we need a slightly different notion of $n+1$ demands a larger size. We say that $n+1$ demands a larger size if either (a) for some $j<n+1$, $p_{j}<_{more}p_{n+1}$, but $\kappa_{j}=\kappa_{n}$; or (b) for some $x\in\mbox{\sf large}$, there is some $j<n+1$ so that $p_{j}<_{more}x$, but $\kappa_{j}=\kappa_{n}$; or (c) $\kappa_{n}=0$. As before, if $n+1$ demands a larger size, set $\kappa_{n+1}=(\kappa_{n})^{+}$; otherwise, set $\kappa_{n+1}=\kappa_{n}$. (In case (c) just above, we take $\kappa_{n+1}=\aleph_{0}$.)

Then build $\SS_{n+1}$ exactly in Section 5.1, using $\Delta_{n+1}$ and $\kappa_{n+1}$. Note that for $h\in\mbox{\sf half}$, both $h$ and $\overline{h}$ are interpreted in $\SS_{n+1}$.

5.3 Construction: combining $\SS_{1}$, $\ldots$, $\SS_{n+1}$ into a structure $\SS$

Let

[TABLE]

where $\Gamma_{\exists}$ is the set of sentences $\exists(a,b)$ which belong to $\Gamma$. (The $+$ notation is explained in Section 2.2.) $S$ is made into a structure called $\SS$, as follows. For $x\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$,

[TABLE]

Once again, note that $\SS$ is a structure, not necessarily a model. An overall requirement of our models is that they interpret $x$ and $\overline{x}$ as complements for all $x$. This is probably not the case for $x\in\mbox{\sf half}$, and so this is why we need Section 5.4 just below.

5.4 Construction: taking care of the variables in half

For $x,\overline{x}\in\mbox{\sf half}$, there is more to do. The sets $[\![x]\!]$ and $[\![\overline{x}]\!]$ are disjoint, and their cardinalities are the same. But it need not be the case that $[\![x]\!]\cup[\![\overline{x}]\!]$ is all of $S$. (See [moss:forDunn] for the easy details.) And now we use Lemma 5.4 just below to define the semantics in this case.

Lemma 5.4**.**

Let $\kappa$ be an infinite cardinal, let $W$ be a set of size $\kappa$. Let $N$ be a set of nouns which is closed under complements. For each $x\in N$, let $\langle x\rangle$ be a subset of $W$. We assume two properties:

$\langle x\rangle$ and $\langle\overline{x}\rangle$ are disjoint for all $x$. 2. 2.

If $x\leq y$, then $\langle x\rangle\subseteq\langle y\rangle$.

Then, there are sets $\langle\!\langle x\rangle\!\rangle$ for all $x\in N$ with the following properties:

$\langle\!\langle x\rangle\!\rangle$ and $\langle\!\langle\overline{x}\rangle\!\rangle$ are disjoint for all $x$. 2. 2.

If $x\leq y$, then $\langle\!\langle x\rangle\!\rangle\subseteq\langle\!\langle y\rangle\!\rangle$. 3. 3.

$\langle x\rangle\subseteq\langle\!\langle x\rangle\!\rangle$. 4. 4.

$\langle\!\langle x\rangle\!\rangle\cup\langle\!\langle\overline{x}\rangle\!\rangle=W$.

Moreover, if $\langle x\rangle$ has size $\kappa$ for all $x$, then so does $\langle\!\langle x\rangle\!\rangle$.

Proof.

We consider the family of all functions $\langle\!\langle\ \rangle\!\rangle:N\to\mathcal{P}(W)$ where $\mathcal{P}(W)$ is the set of subsets of $W$, and where we satisfy (1)–(3) in our result. This family ordered by pointwise inclusion. The resulting poset is closed under unions of chains, and so we may use Zorn’s Lemma. Let $\langle\!\langle\ \rangle\!\rangle$ be a maximal element. We claim that for all $x$, $\langle\!\langle x\rangle\!\rangle\cup\langle\!\langle\overline{x}\rangle\!\rangle=W$.

Suppose towards a contradiction that this is false. Fix some $x$ so that $\langle\!\langle x\rangle\!\rangle\cup\langle\!\langle\overline{x}\rangle\!\rangle\neq W$, and also fix $w\notin\langle\!\langle x\rangle\!\rangle\cup\langle\!\langle\overline{x}\rangle\!\rangle$. If for some $y\geq x$, $w\in\langle\!\langle y\rangle\!\rangle\cup\langle\!\langle\overline{y}\rangle\!\rangle$, then $w$ can only belong to one of those sets (since they are disjoint). Let us assume that $w\in\langle\!\langle y\rangle\!\rangle$ and that $y\geq x$. (Other options include: $w\in\langle\!\langle\overline{y}\rangle\!\rangle$ and that $y\geq x$; or $w\in\langle\!\langle y\rangle\!\rangle$ and that $y\geq\overline{x}$. All of the details are similar in these cases, mutatis mutandis.) In this case, put $w\in\langle\!\langle z\rangle\!\rangle$ for $z\geq y$. This gives a larger $\langle\!\langle\ \rangle\!\rangle$ function. And if there is no $y$ like this, we can simply put $w\in\langle\!\langle z\rangle\!\rangle$ for $z\geq y$. Either way, we have a larger $\langle\!\langle\ \rangle\!\rangle$ function. So we have our contradiction.

This shows the claim, and hence condition (4) holds. The last assertion (on cardinalities) is easy. ∎

We apply Lemma 5.4 to interpret all of the nouns in half. We take $\kappa=\kappa_{n+1}$, $W$ to be $M$ from (8), $N$ to be half, and $\langle x\rangle=[\![x]\!]$ from (9). The properties which we have seen to insure that all of the assumptions in Lemma 5.4 hold. Also, if $x\in\mbox{\sf half}$, then $\Gamma\vdash\exists(x,x)$ by (non-empty). Thus, $[\![x]\!]_{\SS_{n+1}}\neq\emptyset$ for all such $x$. The same holds when we move from $\SS_{n+1}$ to $\SS$. Thus the size of $[\![x]\!]$ in ${\cal N}$ is exactly $\kappa_{n+1}$.

5.5 Construction: the remaining nouns, and the overall model ${\cal M}$

Up until this point, we have not interpreted the nouns which are in small but not in the set $Q$ of (2). For each $x$ in that set, we take $[\![x]\!]=\emptyset$. So we now have interpreted all nouns in $\mbox{\sf small}\,\cup\,\mbox{\sf half}$.

For $x\in\mbox{\sf large}$, we would like to set

[TABLE]

However, we also would like the size of $[\![x]\!]$ to be at least that of $S$. If any $y\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$ has $\mbox{card}\,(S\setminus[\![y]\!]_{\SS})<\mbox{card}\,S$, then add a copy of $S$ to the universe without expanding the size of any variable in $\mbox{\sf small}\,\cup\,\mbox{\sf half}$. That is, replace $S$ by $S+S$ with all $[\![y]\!]$ taken from the copy on the left. Then interpret $[\![x]\!]$ by (10) above, For the nouns $h\in\mbox{\sf half}$, we need to chose one of $h$ or $\overline{h}$ to include the new points. And we need to be sure that any inequalities $h_{1}\leq h_{2}$ are respected. So on top of all this, we need to appeal to Lemma 5.4 again.

At long last, we have interpreted all nouns: we have arranged that $[\![\overline{x}]\!]=S\setminus[\![x]\!]$ for $x\in\mbox{\sf small}$. It follows that the same fact is true for $x\in\mbox{\sf large}$. And for $x\in\mbox{\sf half}$, we have arranged for this in Section 5.4. So we have a bona fide model. We write this model as ${\cal M}$, we change the name of the universe from $S$ to $M$, and we let $\kappa=\mbox{card}\,\SS$. The proof that $\SS\models\Gamma$ comes next.

6 Verifying the properties of the model

We must verify that ${\cal M}\models\Gamma$. For this, we split the argument into a number of claims.

Claim 6.1**.**

Let $x\notin Q$, where $Q$ is as in (2). Then $[\![x]\!]=\emptyset$.

Proof.

This was directly established in Section 5.5. ∎

Claim 6.2**.**

If $i\leq j$, then $\kappa_{i}\leq\kappa_{j}$. $\kappa_{n+1}$ is an infinite cardinal.

Proof.

An easy induction shows the monotonicity assertion in our claim. Suppose that some $j\leq n$, $j$ demands a larger size. Let $j$ be least with this property. Then $\kappa_{j}$ is infinite, and so $\kappa_{n+1}$ also will be. If no $j\leq n$ demands a larger size, then $\kappa_{n}=0$. So by condition (c) in Section 5.2, we see that $\kappa_{n+1}=\aleph_{0}$. ∎

Claim 6.3**.**

If $z\leq w$ are in $\mbox{\sf small}\,\cup\,\mbox{\sf half}$, then $[\![z]\!]\subseteq[\![w]\!]$.

Proof.

First, if $z\notin Q$, then $[\![z]\!]=\emptyset$, and we are done. So we shall assume that $z\in Q$. If $w\notin Q$, then $z\notin Q$. For if $z\in Q$ and $z\leq w$, then it is easy to use the logic to see that $\Gamma\vdash\exists(w,w)$; this is a contradiction to $w\notin Q$. Thus, we only need to verify this claim when $z$ and $w$ are not in $Q$.

In $\SS$, we have $[\![z]\!]\subseteq[\![w]\!]$ by the definition of the semantics in (9) and the (easy to check) fact that $\exists_{z}\subseteq\exists_{w}$. So even when $x$ and $y$ are in half and we use Lemma 5.4 to expand their interpretations in ${\cal M}$, we still see that $[\![z]\!]\subseteq[\![w]\!]$. ∎

Claim 6.4**.**

Let $1\leq i\leq n+1$. If $x\in[p_{i}]$, then $\mbox{card}\,[\![x]\!]=\kappa_{i}$.

Proof.

If $\Gamma\not\vdash\exists(x,x)$, then also $\Gamma\not\vdash\exists(p_{i},p_{i})$ by (int); see Example 1.13. In this case $\kappa_{i}=0$, $[\![x]\!]=\emptyset$, and our result follows. The more interesting case is when $\Gamma\vdash\exists(p_{i},p_{i})$. According to (9), $[\![x]\!]$ is the disjoint union of a family of sets $\bigcup\{[\![y]\!]_{\SS_{i}}:y\leq x\}$ and a finite set $\exists_{x}$. Since all the interpretations are infinite, we ignore the finite set $\exists_{x}$.

If $y\leq x$, then the unique $j$ such that $y\in[p_{j}]$ is at most $i$. This is by (subset-size). Thus $\mbox{card}\,[\![y]\!]_{\SS_{j}}=\kappa_{j}\leq\kappa_{i}$. Hence $[\![x]\!]$ in our model ${\cal M}$ is a finite union of sets of size $\leq\kappa_{i}$. So $\mbox{card}\,([\![x]\!])\leq\kappa_{i}$. But in $\SS_{i}$, $\mbox{card}\,([\![x]\!])=\kappa_{i}$. (For $i\leq n$, this is by (6). For $i=n+1$, this was noted at the end of Section 5.4.) So the same is true in ${\cal M}$. ∎

Claim 6.5**.**

Let $x,y\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$. If $[\![x]\!]\cap[\![y]\!]\neq\emptyset$, then $\Gamma\vdash\exists(x,y)$.

Proof.

Let $i$ and $j$ be such that $x\in[p_{i}]$ and $y\in[p_{j}]$. The interpretations $[\![x]\!]$ and $[\![y]\!]$ in ${\cal M}$ are disjoint unions, and so there is some $k$ such that

[TABLE]

Let $\alpha$ belong to the set on the left. There are $p\leq x$ and $q\leq y$ in $[p_{k}]$ such that $\alpha\in[\![p]\!]_{{\cal M}_{k}}\cap[\![q]\!]_{{\cal M}_{k}}$. But then $[\![p]\!]_{{\cal M}_{k}}\cap[\![q]\!]_{{\cal M}_{k}}\neq\emptyset$. And so by (7), $\Gamma\vdash\exists(p,q)$. Together with $p\leq x$ and $q\leq y$, we have our result. ∎

Claim 6.6**.**

Let $x\in\mbox{\sf large}$. Then $\mbox{card}\,[\![x]\!]=\kappa_{n+1}$. If in addition, $y<_{more}x$, then $\mbox{card}\,[\![y]\!]<\kappa_{n+1}$.

Proof.

The fact that $\mbox{card}\,[\![x]\!]=\kappa_{n+1}$ follows from what we did in Section 5.5.

Note that $y$ belongs to small by Lemma 4.1. Let $j\leq n$ be such that $y\in[p_{j}]$.

Suppose that $\kappa_{j}=\kappa_{n}$. Then $n+1$ demands a larger size (due to $x$ and $y$), and so $\kappa_{j}=\kappa_{n}<\kappa_{n+1}$. And if $\kappa_{j}<\kappa_{n}$, then of course $\kappa_{j}<\kappa_{n}\leq\kappa_{n+1}$. Either way, $\kappa_{j}<\kappa_{n+1}$. Now our result follows from Claim 6.4: $\mbox{card}\,[\![y]\!]=\kappa_{j}<\kappa_{n+1}$. ∎

Claim 6.7**.**

${\cal M}$ satisfies all $\exists$ sentences in $\Gamma$.

Proof.

Consider first a sentence $\exists(x,y)\in\Gamma$, where $x$ and $y$ both belong to $\mbox{\sf small}\,\cup\,\mbox{\sf half}$. The sentence $\exists(x,y)$ itself belongs to $\exists_{x}\cap\exists_{y}$, hence to $[\![x]\!]\cap[\![y]\!]$ in ${\cal M}$. Therefore, ${\cal M}\models\exists(x,y)$.

Now let us consider sentences $\exists(x,y)\in\Gamma$, where $x\in(\mbox{\sf small}\,\cup\,\mbox{\sf half})$ and $y\in\mbox{\sf large}$. Then $\exists(x,y)\in[\![x]\!]$. Suppose towards a contradiction that $\exists(x,y)\in[\![\overline{y}]\!]$. Note that $\overline{y}\in\mbox{\sf small}$. In view of our definition of $\exists_{\overline{y}}$, either $x\leq\overline{y}$ or $y\leq\overline{y}$. Either of these alternatives, together with $\exists(x,y)\in\Gamma$ shows that $\Gamma$ is inconsistent.

Finally, we consider $\exists(x,y)$, where $x,y\in\mbox{\sf large}$. In this case, we argue that ${\cal M}\models\exists(x,y)$, even when this sentence does not belong to $\Gamma$.

As shown in Claim 6.6, the nouns in small are interpreted by sets whose size is strictly smaller than the size of the universe, $\kappa_{n+1}$. Thus $[\![\overline{x}]\!]\cup[\![\overline{y}]\!]$ has size $<\kappa$. So the size of $M\setminus([\![\overline{x}]\!]\cup[\![\overline{y}]\!])$ is $\kappa_{n+1}$. In particular, it is non-empty. This is to say that $[\![x]\!]\cap[\![y]\!]$ is non-empty. ∎

Claim 6.8**.**

${\cal M}$ satisfies every $\forall(x,y)$ sentence in $\Gamma$.

Proof.

We consider a number of cases.

$x,y\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$. This case follows by Claim 6.3. 2. 2.

$x\in\mbox{\sf small}$ and $y\in\mbox{\sf large}$. Let us check that $[\![x]\!]\cap[\![\overline{y}]\!]=\emptyset$, since this implies the result. Note that $\overline{y}\in\mbox{\sf small}$. Suppose towards a contradiction that $[\![x]\!]\cap[\![\overline{y}]\!]\neq\emptyset$. By Claim 6.5, $\Gamma\vdash\exists(x,\overline{y})$. But then $\Gamma$ is inconsistent. This contradiction shows that $[\![x]\!]\cap[\![\overline{y}]\!]=\emptyset$. 3. 3.

$x\in\mbox{\sf half}$ and $y\in\mbox{\sf large}$. Consider $\overline{y}$ and $\overline{x}$, and then appeal to Case 2 above. 4. 4.

$x\in\mbox{\sf large}$. Then we also have $y\in\mbox{\sf large}$. Consider $\overline{y}$ and $\overline{x}$, and then appeal to Case 1.

This completes the proof. ∎

Claim 6.9**.**

${\cal M}$ satisfies every $\exists^{>}(x,y)$ sentence in $\Gamma$.

Proof.

Consider a sentence $\exists^{>}(x,y)\in\Gamma$. So $y<_{more}x$. Thus $y<_{c}x$ as well. We first consider the case that $x\in\mbox{\sf small}$. In our listing (3), we must list $[y]$ before $[x]$. We must check that our construction insures that $\mbox{card}\,[\![y]\!]<\mbox{card}\,[\![x]\!]$. That is, let $j<i$ be such that $x\in[p_{i}]$ and $y\in[p_{j}]$. Let $k$ be least such that $j<k\leq i$ and $k$ demands a larger size. There must exist such a $k$; it is the least number such that there is some $w$ in $[p_{w}]$ with $\Gamma\vdash\exists^{>}(w,y)$. Our construction arranges that $\kappa_{i}\geq\kappa_{k}=(\kappa_{k-1})^{+}>\kappa_{k}\geq\kappa_{j}$. And by Claim 6.4, we see that $\mbox{card}\,[\![x]\!]>\mbox{card}\,[\![y]\!]$.

We next turn to the case $x\in\mbox{\sf half}$. Here we must have $y\in\mbox{\sf small}$, by Lemma 4.1. Let $j\leq n$ be such that $y\in[p_{j}]$. If $\kappa_{n}>\kappa_{j}$, then

[TABLE]

If $\kappa_{n}=\kappa_{j}$, then $n+1$ demands a larger size. So $\kappa_{n+1}>\kappa_{n}$, and we have the same fact: $\exists^{>}(x,y)$ is true in ${\cal M}$.

Finally, the case of $x\in\mbox{\sf large}$ follows immediately from Claim 6.6.

This completes the proof. ∎

Claim 6.10**.**

${\cal M}$ satisfies every $\exists^{\geq}(x,y)$ sentence in $\Gamma$.

Proof.

First, when $x\in\mbox{\sf half}\ \cup\ \mbox{\sf large}$, $\mbox{card}\,[\![x]\!]=\kappa_{n+1}$. (See Claims 6.4 and 6.6.) In this case our result follows.

We are left with $x\in\mbox{\sf small}$. In this case, $y\in\mbox{\sf small}$, too, by Lemma 4.1, part (iv). Let $i$ and $j$ be such that $x\in[p_{i}]$ and $q\in[p_{j}]$. Since $y\leq_{c}x$, have $x\equiv_{c}y$ or $x<_{c}y$. In the first case, $i=j$ and so $\mbox{card}\,[\![y]\!]=\mbox{card}\,[\![x]\!]$. In the second case, $[p_{i}]$ comes before $[p_{j}]$ in the listing (3); this is by our definition of a listing. So $i\leq j$, and thus $\kappa_{i}\leq\kappa_{j}$. Now our result follows by Claim 6.4. ∎

6.1 Completing the proof of Theorem 5.1

The work in the previous part of this section constitutes a proof of Theorem 5.1. Although we did not discuss the additional properties of the model which were stated in that theorem, the construction has arranged them.

Remark 6.11**.**

At this point, we need an important remark on the entire construction of this section. At various places, we needed to know that various numbers demanded a larger size. We never used the assumption that any numbers did not demand a larger size. (We shall need this in Section 7.2 below.) And examining all of our claims, we see that the verifications all go through when more numbers demand a larger size.

This remark gives a certain flexibility to our construction which we shall exploit in Section 7.1.

Remark 6.12**.**

Let $\Gamma$ be a consistent set of sentences and suppose that $(x\leq_{c}y)$. Claim 6.10 showed that ${\cal M}$ satisfies $\exists^{\geq}(y,x)$. Since ${\cal M}$ satisfies $\exists^{\geq}(y,x)$, we also have ${\cal M}\not\models\exists^{>}(x,y)$. In this case, we have a model whenever any numbers do not demand a larger size (see Claims 6.4 and 6.10). We shall use this remark in Section 7.2.

7 The full result

This section refines Theorem 5.1 and also proves the completeness of the logic.

Theorem 7.1**.**

If $\Gamma\not\vdash\varphi$, then there is a model of $\Gamma$ in which $\varphi$ is false.

Caution

We review the point made in Section 1.4. It is very tempting at this point to argue as follows for the completeness of the logic. “If $\Gamma\not\vdash\varphi$, then $\Gamma\cup\{\overline{\varphi}\}$ is consistent, where $\overline{\varphi}$ is the negation of $\varphi$ which we saw in Definition 1.4. Thus by Theorem 5.1, this set has a model. Such a model will satisfy $\Gamma$ and falsify $\varphi$.” The problem with this is that we do not have reductio ad absurdum in the logic. And so we are not entitled to say that $\Gamma\cup\{\overline{\varphi}\}$ is consistent. In fact, this set is consistent, and this follows from the work in this section. We could try to prove the consistency of $\Gamma\cup\{\overline{\varphi}\}$ proof-theoretically rather than semantically, but this seems much harder.

Assumptions at this point

Here is how we show the completeness of the logic. We split into cases according to $\varphi$. We show that either $\Gamma\vdash\varphi$, or that $\Gamma$ is inconsistent, or else there is a model of $\Gamma$ where $\varphi$ is false.

Reminder

The model construction involves many choices that can be manipulated. First, the order of the atomic sentences makes a difference in the three-fold partition in Lemma 4.1. And even after that partition is determined, the particular listing which we use in (3) also affects the model in a big way.

7.1 The first case: $\varphi$ is of the form $\exists^{\geq}(x,y)$

There are a number of cases. Our first is when $\overline{x}\leq_{c}x$. In this case, $\Gamma\vdash\varphi$. And so we contradict the assumption in this case. Thus, we assume that $\neg(\overline{x}\leq_{c}x)$ in what follows.

The second case is when $\overline{x}<_{more}z$ for some $z$. In this case, we again have $\Gamma\vdash\varphi$. So we assume that for all $z$, $\neg(\overline{x}<_{more}z)$.

Thus, we may refine the standard partition as in Lemma 4.2: we get a partition with $x\in\mbox{\sf small}$.

We further break into cases as to whether $y\in\mbox{\sf small}$ or $y\in\mbox{\sf half}\ \cup\ \mbox{\sf large}$.

If both $x$ and $y$ are in small, let $i,j\leq n$ be such that $x\in[p_{i}]$ and $y\in[p_{j}]$. We take a listing whether the class of $[p_{i}]$ comes before $[p_{j}]$. We can do this by Lemma 2.2. And then in our construction, when we come to Step $j$, we decide that $j$ demands a bigger size. Thus we arrange that $\kappa_{j}>\kappa_{j-1}\geq\kappa_{i}$. This builds a model where $[\![x]\!]$ is a set of smaller size than $[\![y]\!]$.

If $x\in\mbox{\sf small}$ and $y\in\mbox{\sf half}\ \cup\ \mbox{\sf large}$, then change the construction so that $n+1$ demands a larger size. (This might be true according to our work before, but even if $n+1$ did not demand a larger size, we can insist on it: see Remark 6.11.) We get a model with $[\![y]\!]$ a set of strictly larger size than $[\![x]\!]$. So $\exists^{\geq}(x,y)$ is false in that model.

7.2 The next case: $\varphi$ is of the form $\exists^{>}(x,y)$

Consider the standard partition according to $\Gamma$. If $x$ and $y$ are both in $\mbox{\sf half}\ \cup\ \mbox{\sf large}$, we have a model where $\mbox{card}\,[\![x]\!]=\mbox{card}\,[\![y]\!]$, as desired. If $x\in\mbox{\sf small}$ and $y\in\mbox{\sf half}\ \cup\ \mbox{\sf large}$, we get a model where $\mbox{card}\,[\![x]\!]\leq\mbox{card}\,[\![y]\!]$.

If $x\in\mbox{\sf half}$ and $y\in\mbox{\sf small}$, then we have two further cases. In case $x\in\mbox{\sf half}$ because $x\leq_{c}\overline{x}\leq_{c}x$, of even if just $\overline{x}\leq_{c}x$, we argue as follows. Since $y\in\mbox{\sf small}$ in the standard partition, there is some $z$ such that $y<_{c}z$. So by Example 1.10, $y<_{c}x$. And if $\neg(\overline{x}\leq_{c}x)$, then we may refine the standard partition as in Lemma 4.2. At this point, we have a partition where $x$ and $y$ are both in small, and we treat this below.

If $x\in\mbox{\sf large}$ and $y\in\mbox{\sf small}$, then we have $p$ and $q$ such that $\overline{x}<_{c}p$ and $y<_{c}q$. By (weak-more-anti), $q\leq_{c}x$. And so $y<_{c}x$ as well. This contradicts the assumption in this section that $\neg(y<_{c}x)$.

We turn to the case when $x$ and $y$ are both in small, either in the standard partition or in a refinement thereof. (It makes no difference.) By the hypothesis in this section, we do not have $y<_{more}x$. If $x\equiv_{c}y$, then $[x]=[y]$. We thus get a model where $\mbox{card}\,[\![x]\!]=\mbox{card}\,[\![y]\!]$. We have two more cases. First, consider what happens when $[y]\not{\!\!\!}{\leq}_{c}[x]$. We chose a listing of the $\equiv_{c}$-classes that puts $x$ first. And then we get a model where $\mbox{card}\,[\![x]\!]<\mbox{card}\,[\![y]\!]$. Finally, we have the case when $y\leq_{c}x$. So $[y]$ precedes $x$ in the listing. In this case, we must alter the listing even further. Some of the classes between $[y]$ and $[x]$ might demand a larger size. We move those (in order) to after $[x]$ in the listing. We must be sure that all of the classes which are $<_{c}[x]$ still come before it in the listing. In other words, the classes $[z]$ between $[y]$ and $[x]$ which demand a larger size may be moved to after $[x]$ without falsifying the key property of the listing. The reason is that if such a class $[z]$ were problematic, then we would contradict $\neg(y<_{more}x)$. In this case, we get a model where $[\![x]\!]$ and $[\![y]\!]$ have the same size.

7.3 The next case: $\varphi$ is of the form $\forall(x,y)$

We break into a number of subcases. In each case, we take the model ${\cal M}$ of $\Gamma$ from Section 5 and modify it by adding a point. ${\cal M}$ has the property that the interpretation of everything is either empty or infinite. We shall be adding one point, call it $*$, to this model. The point is added in such a way that it makes $\forall(x,y)$ false. The addition of one point to any set doesn’t change the truth of any sentences involving cardinality. Also, none of the $\exists(p,q)$ sentences changes truth value when a point is added to a model. But we shall be interested to check that the $\forall(p,q)$ sentences from $\Gamma$ are true even after the point is added.

$x\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$, $y\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$. Add one fresh point $*$ to $[\![z]\!]$ for all $z$ such that $x\leq z$.

Here are the details on the $\forall(p,q)$ sentences in $\Gamma$. Review the argument in Claim 6.8. The only case which we must consider is when $p\in\mbox{\sf small}$ and $q\in\mbox{\sf large}$. If the new point $*$ belongs to the interpretation of $p$ and $\overline{q}$, then $x\leq p$ and $x\leq\overline{q}$. But $\overline{q}\leq\overline{p}$. And so $x\leq\overline{p}$. Together with $x\leq p$, we see that $x\leq\overline{x}$. And so $\Gamma\vdash\forall(x,y)$. This contradiction shows that indeed $\forall(p,q)$ is true after $*$ is added. Thus we obtain a model of $\Gamma$ which falsifies $\varphi$, as desired. 2. 2.

$x\in\mbox{\sf half}\ \cup\ \mbox{\sf large}$ and $y\in\mbox{\sf half}\ \cup\ \mbox{\sf large}$: replace $x$ and $y$ by $\overline{y}$ and $\overline{x}$, and apply the last case. We get a model falsifying $\forall(\overline{y},\overline{x})$, and thus a model falsifying $\forall(x,y)$. 3. 3.

$x\in\mbox{\sf small}$, $y\in\mbox{\sf large}$. This time, we add a single fresh point $*$ to $[\![z]\!]$ whenever $x\leq z$ or $\overline{y}\leq z$. We assume that $*$ gets added to $[\![a]\!]$, since otherwise $[\![a]\!]\subseteq[\![b]\!]$ after the addition. If $*$ also gets added to $[\![b]\!]$, then again $[\![a]\!]\subseteq[\![b]\!]$.

We have two cases as to why $*$ gets added to $[\![a]\!]$: $x\leq a$, and $\overline{y}\leq a$. Since $*$ was not added to $[\![b]\!]$, it was added to $[\![\overline{b}]\!]$. (Notice that $\overline{b}\in\mbox{\sf small}$.) So again, we have two cases: $x\leq\overline{b}$, and $\overline{y}\leq\overline{b}$. The second is equivalent to $b\leq y$.

We shall examine all four cases and show that in each of them we have $x\leq y$. This contradicts the overall assumptions in this section.

(a) $x\leq a$ and $x\leq\overline{b}$. So $x\leq a\leq b$, and also $x\leq\overline{b}$. Thus $x\leq\overline{x}$. As a result, $x\leq y$.

(b) $x\leq a$ and $b\leq y$. So $x\leq a\leq b\leq y$. Thus $x\leq y$.

(c) $\overline{y}\leq a$ and $x\leq\overline{b}$. The $\overline{y}\leq a\leq b\leq\overline{x}$. So we have $\overline{y}\leq\overline{x}$, and thus $x\leq y$.

(d) $\overline{y}\leq a$ and $b\leq y$. This time $\overline{y}\leq y$. This implies $x\leq y$.

7.4 The last case: $\varphi$ is of the form $\exists(x,y)$

Consider the standard partition of the variables according to $\Gamma$. When $x$ and $y$ are in $\mbox{\sf small}\,\cup\,\mbox{\sf half}$, the model ${\cal M}$ constructed in the previous section works: see part 1 of Theorem 5.1. When $x$ and $y$ are both in large, or when one is in half and the other in large are easy: in these cases $\Gamma\vdash\exists(x,y)$. (See Example 1.12.)

We are left with the case that one of the variables, say $x$, is in small, and the other one, $y$, is in large. Both $x$ and $\overline{y}$ belong to small. Further, we cannot have $\Gamma\vdash\exists^{>}(x,\overline{y})$, since this implies $\Gamma\vdash\exists(x,y)$, using (more-some). Since $\Gamma\not\vdash\exists^{>}(x,\overline{y})$, we know from our work in Section 7.2 that there is a model of $\Gamma$ where $\mbox{card}\,[\![x]\!]\leq\mbox{card}\,[\![\overline{y}]\!]$.

If ${\cal M}\models\forall(y,\overline{y})$, then again we are done. So we shall assume that ${\cal M}\models\exists(\overline{y},\overline{y})$. And since $\overline{y}\in\mbox{\sf small}$, Theorem 5.1 tells us that $\Gamma\vdash\exists(\overline{y},\overline{y})$.

We modify ${\cal M}$ to obtain a different model to be called ${\cal N}$. The two models have the same set of points: $N=M$. The interpretation function of ${\cal N}$ will be written $[\![\ ]\!]^{*}$.

For $p\in\mbox{\sf small}$,

If $\overline{y}\leq p$, then $[\![p]\!]^{*}=[\![p]\!]\cup[\![x]\!]$ and $[\![\overline{p}]\!]^{*}=[\![\overline{p}]\!]\cap[\![\overline{x}]\!]$. 2. 2.

If $\neg(\overline{y}\leq p)$, then $[\![p]\!]^{*}=[\![p]\!]$ and $[\![\overline{p}]\!]^{*}=[\![\overline{p}]\!]$.

These clauses also define $[\![p]\!]^{*}$ for $p\in\mbox{\sf large}$.

For $p\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$, note that we cannot have $\overline{y}\leq p,\overline{p}$. (For if we did, then $\overline{y}\leq y$, and we contradict our assumption that $\Gamma\vdash\exists(\overline{y},\overline{y})$.)

If $p\in\mbox{\sf half}$ and $\overline{y}\leq p$, then $[\![p]\!]^{*}=[\![p]\!]\cup[\![x]\!]$ and $[\![\overline{p}]\!]^{*}=[\![\overline{p}]\!]\cap[\![\overline{x}]\!]$. 2. 2.

If $p\in\mbox{\sf half}$ and $\overline{y}\leq\overline{p}$, then $[\![\overline{p}]\!]^{*}=[\![\overline{p}]\!]\cup[\![x]\!]$ and $[\![p]\!]^{*}=[\![p]\!]\cap[\![\overline{x}]\!]$. 3. 3.

If $p\in\mbox{\sf half}$, and neither $\overline{y}\leq p$ nor $\overline{y}\leq\overline{p}$, then $[\![p]\!]^{*}=[\![p]\!]$ and $[\![\overline{p}]\!]^{*}=[\![\overline{p}]\!]$.

Again, at most one of every pair of complementary nouns in half gets a larger interpretation in ${\cal N}$ than in ${\cal M}$. This completes the definition of ${\cal N}$. Now this model ${\cal N}$ does not change the sizes of any interpretations. (This is where we use the assumption that in ${\cal M}$, $\mbox{card}\,[\![y]\!]\leq\mbox{card}\,[\![\overline{x}]\!]$.) So it satisfies the same $\exists^{\geq}$ and $\exists^{>}$ sentences as ${\cal M}$. In particular, it satisfies all of the $\exists^{\geq}$ and $\exists^{>}$ sentences which happen to belong to $\Gamma$.

Claim 7.2**.**

${\cal N}$ satisfies all sentences $\forall(a,b)$ which are true in ${\cal M}$, hence all sentences $\forall(a,b)$ which belong to $\Gamma$.

Proof.

We have the following cases: (1) $a,b\in\mbox{\sf small}$; (2) $a\in\mbox{\sf small}$, $b\in\mbox{\sf half}$; (3) $a\in\mbox{\sf small}$, $b\in\mbox{\sf large}$; (4) $a,b\in\mbox{\sf half}$; The other possible cases (such as $a,b\in\mbox{\sf large}$) follow from these by taking complements.

(1) Suppose that both $a,b\in\mbox{\sf small}$. Since our sentence $\forall(a,b)$ is in $\Gamma$, and ${\cal M}\models\Gamma$, $[\![a]\!]\subseteq[\![b]\!]$. Note that $[\![a]\!]^{*}$ is either $[\![a]\!]$ or the larger set $[\![a]\!]\cup[\![x]\!]$. If $[\![a]\!]^{*}=[\![a]\!]$, then clearly $[\![b]\!]^{*}\supseteq[\![a]\!]^{*}$. And if $[\![a]\!]^{*}=[\![a]\!]\cup[\![x]\!]$, then $\overline{y}\leq a$. But then $\overline{y}\leq b$ as well, and so $[\![b]\!]^{*}=[\![b]\!]\cup[\![x]\!]$. So again we have $[\![a]\!]^{*}\subseteq[\![b]\!]^{*}$.

(2) Suppose that $a\in\mbox{\sf small}$, $b\in\mbox{\sf half}$.

The only extra step beyond what we saw in (1) is for the case when $[\![a]\!]^{*}=[\![a]\!]$ and $[\![b]\!]^{*}=[\![b]\!]\cap[\![\overline{x}]\!]$. This case happens when $\neg(\overline{y}\leq a)$, but $\overline{y}\leq\overline{b}$. So $b\leq y$. We must show that $[\![a]\!]\subseteq[\![\overline{x}]\!]$. For if not, $[\![a]\!]\cap[\![x]\!]\neq\emptyset$. Then $\Gamma\vdash\exists(a,x)$; this is due to the fact that both $a$ and $x$ are in small. But since $a\leq b\leq y$, we have $\exists(x,y)$ from $\Gamma$. This contradicts the basic assumption in this section.

(3) We next consider the case $a\in\mbox{\sf small}$, $b\in\mbox{\sf large}$. Let us first assume that $[\![a]\!]^{*}=[\![a]\!]$. If $[\![b]\!]^{*}=[\![b]\!]$, then of course we are done. So we assume that $[\![b]\!]^{*}=[\![b]\!]\cap[\![\overline{x}]\!]$, and thus that $\overline{y}\leq\overline{b}$. So $b\leq y$. The rest of the argument at this point is exactly what we saw in (2) just above.

We continue with (3), turning to the subcase $[\![a]\!]^{*}=[\![a]\!]\cup[\![x]\!]$. So $\overline{y}\leq a$. We show that $[\![b]\!]^{*}=[\![b]\!]$ and that $[\![x]\!]\subseteq[\![b]\!]$. Suppose that $\overline{y}\leq\overline{b}$. As we noted above, $\Gamma\vdash\exists(\overline{y},\overline{y})$. Thus we have $\exists(a,\overline{b})$; this contradicts $a\leq b$. This contradiction goes to show that $\neg(\overline{y}\leq\overline{b})$. Thus $[\![\overline{b}]\!]^{*}=[\![\overline{b}]\!]$. It follows that $[\![b]\!]^{*}=[\![b]\!]$. To show that $[\![a]\!]^{*}\subseteq[\![b]\!]^{*}$, we only need to see that $[\![x]\!]\subseteq[\![b]\!]$. Now if not, $[\![x]\!]\cap[\![\overline{b}]\!]\neq\emptyset$. Since $x$ and $\overline{b}$ belong to small, $\Gamma\vdash\exists(x,\overline{b})$. But $\overline{b}\leq\overline{a}\leq y$. Thus $\Gamma\vdash\exists(x,y)$; this again contradicts the basic assumption in this section.

Finally, (4) is when $a,b\in\mbox{\sf half}$. If $[\![a]\!]^{*}=[\![a]\!]\cup[\![x]\!]$, then we have $\overline{y}\leq a$. So in this case, $\overline{y}\leq b$, and thus $[\![b]\!]^{*}=[\![b]\!]\cup[\![x]\!]$. So $[\![a]\!]^{*}\subseteq[\![b]\!]^{*}$ in this case. We thus have the case $[\![a]\!]^{*}=[\![a]\!]$ because $\neg(\overline{y}\leq a)$. The only interesting subcase on $[\![b]\!]^{*}$ is when $[\![b]\!]^{*}=[\![b]\!]\cap[\![\overline{x}]\!]$, and thus that $\overline{y}\leq\overline{b}$. The argument is exactly as in (2) above, with the slight change that $a\in\mbox{\sf half}$ rather than small. ∎

Claim 7.3**.**

${\cal N}$ satisfies all $\exists(a,b)$ sentences in $\Gamma$.

Proof.

Take a sentence $\varphi=\exists(a,b)$ from $\Gamma$. We know that ${\cal M}\models\exists(a,b)$. We still must check that $\exists(a,b)$ is true in ${\cal N}$. This is obvious when $a,b\in\mbox{\sf small}\,\cup\,\mbox{\sf half}$. As we know, when $a,b\in\mbox{\sf large}$, we always have $\exists(a,b)$ on grounds of cardinality. We thus need only check the case when $a$ (say) belongs to $\mbox{\sf small}\,\cup\,\mbox{\sf half}$ and $b$ to large. We know from Section 6.7 that $\varphi$ itself belongs to $[\![a]\!]\cap[\![b]\!]$. We thus only need to show that $\varphi\in[\![b]\!]^{*}$ when $[\![b]\!]^{*}=[\![b]\!]\cap[\![\overline{x}]\!]$; i.e., when $\overline{y}\leq\overline{b}$. So we must show that $\varphi\notin[\![x]\!]$. For if we had $\exists(a,b)\in[\![x]\!]$, then either $a\leq x$ or $b\leq x$. In the case that $a\leq x$, we have $a\leq x$ and $b\leq y$. So since $\exists(a,b)\in\Gamma$, $\Gamma\vdash\exists(x,y)$. This also happens in the second case, when $b\leq x$. For in this case, we have $b\leq x,y$. Together with $\exists(a,b)\in\Gamma$, we again see that $\Gamma\vdash\exists(x,y)$. Either way, we contradict the basic assumption in this section. ∎

We have proven Claim 7.3. As a result, ${\cal N}\models\Gamma$. But $[\![\overline{y}]\!]^{*}=[\![x]\!]\cup[\![\overline{y}]\!]=[\![x]\!]^{*}\cup[\![\overline{y}]\!]$. Thus $[\![x]\!]^{*}\subseteq[\![\overline{y}]\!]^{*}$. It follows that $[\![x]\!]^{*}\cap[\![y]\!]^{*}=\emptyset$. The upshot is that ${\cal N}\not\models\exists(x,y)$, as desired.

This concludes the work in Section 7.4. We have proved Theorem 7.1.

Corollary 7.4**.**

If $\Gamma\not\vdash\varphi$, then $\Gamma\cup\{\overline{\varphi}\}$ is consistent.

As a corollary to the proof of our theorem, we also have the following result.

Theorem 7.5**.**

If $\Gamma$ has a model, then $\Gamma$ has a model of size $\aleph_{n}$ for some $n\in N$.

Since the proof system is direct (i.e., reductio ad absurdum is not used), we also have the following result.

Theorem 7.6**.**

The question of whether $\Gamma\models\varphi$ or not can be decided in logspace.

See [phmoss] for a general discussion of complexity matters concerning syllogistic logics. The reason for the efficient proof search is that the logic did not use reductio ad absurdum. Instead it uses ex falso quo quodlibet. In effect, one tries to see whether $\Gamma\vdash\varphi$ by generating all of the proofs from $\Gamma$. One needs to know that if $\Gamma\vdash\varphi$, then a derivation may be found using only the atoms in $\Gamma\cup\{\varphi\}$ and their complements. We omit the details. There are only polynomially many such sentences, and the proof search is a generalization of searching for paths in graphs. If $\Gamma\not\vdash\varphi$, then there is a counter-model. It may be chosen to be of size $\aleph_{n}$ for some natural number $n$. Further, it may be taken to be finitely describable in a strong sense.

Remark 7.7**.**

One way to extend the completeness result in this paper is to add the boolean connectives $\wedge$ and $\neg$ to the sentences. So in effect, one has propositional logic with the sentences of $\mathcal{L}({\mathbf{P}})$ as atomic sentences. The semantics is the obvious one. For the proof theory, one takes a Hilbert style axiomatization of propositional logic, and adds implicational sentences corresponding to the rules of $\mathcal{L}({\mathbf{P}})$. (For example, corresponding to (non-empty), we would have $\exists^{\geq}(p,\overline{p})\rightarrow\exists^{\geq}(\overline{p},x)$.) The argument is an adaptation of one from [logic:moss08]. The completeness boils down to showing that every consistent sentence $\varphi$ in the new logic has a model. Using disjunctive normal forms, we may assume that $\varphi$ is a conjunction of atomic sentences or their negations. But the atomic sentences in this language are closed under (semantic) negation, so we may assume that $\varphi$ is a conjunction $\bigwedge S$ of a (finite) set $S$ of sentences of $\mathcal{L}({\mathbf{P}})$. And here, we claim that the set of conjuncts of $\varphi$ is consistent in $\mathcal{L}({\mathbf{P}})$. For this, we argue by induction on proofs in $\mathcal{L}({\mathbf{P}})$ which don’t use the (x) rules that if $S\vdash\psi$ in $\mathcal{L}({\mathbf{P}})$, then $\vdash\bigwedge S\rightarrow\psi$.

8 Examples

Let $\Gamma$ be the set of sentences shown in Figure 4.

Example 8.1**.**

Notice that in any model of $\Gamma$, $[\![c]\!]$ and $[\![d]\!]$ would be sets of the same size, and yet $[\![c]\!]$ is a proper subset of $[\![d]\!]$. So $[\![c]\!]$ and $[\![d]\!]$ must be infinite. Further, since we have $\exists^{>}(e,c)$ in $\Gamma$, $[\![e]\!]$ must be uncountable.

Example 8.2**.**

The standard partition of $\Gamma$ is

[TABLE]

Example 8.3**.**

The set $Q$ in (2) is $\{c,d\}$. This set is an equivalence class for $\equiv_{c}$. The one and only listing of $Q$ is the one-term sequence $\{c,d\}$.

In terms of our earlier notation, $[p_{1}]=\{c,d\}$; for later, $p_{2}=\mbox{\sf half}$.

$\Delta_{1}$ is the set

[TABLE]

One possible finite model of $\Delta_{1}$ with the right properties has universe $\{1,2\}$, $[\![c]\!]=\{1\}$, and $[\![d]\!]=\{1,2\}$. So for our $\SS_{1}$ we take two disjoint sets $A_{1}$ and $A_{2}$, each of cardinality $\aleph_{0}$, and then set $\SS_{1}=A_{1}\cup A_{2}$, $[\![c]\!]=A_{1}$, and $[\![d]\!]=A_{1}\cup A_{2}$. Next, $n+1=2$ demands a larger size. So we set $\kappa_{2}=\aleph_{1}$. Also,

[TABLE]

One finite structure of $\Delta_{2}$ has universe $\{1,2,3\}$, $[\![e]\!]=\{1\}$, $[\![f]\!]=\{1,2\}$, and $[\![g]\!]=\{3\}$. (Note that $[\![g]\!]$ could also be $\{1\}$ or $\{2\}$.) So for $\SS_{2}$, we take disjoint sets $B_{1}$, $B_{2}$, $B_{3}$ of size $\aleph_{1}$, and $S_{2}=B_{1}\cup B_{2}\cup B_{3}$, $[\![e]\!]=B_{1}$, $[\![f]\!]=B_{1}\cup B_{2}$, and $[\![g]\!]=B_{3}$. Thus $[\![\overline{e}]\!]=B_{2}\cup B_{3}$, $[\![\overline{f}]\!]=B_{3}$, and $[\![\overline{g}]\!]=B_{1}\cup B_{2}$.

We are almost ready to define the model of $\Gamma$ produced by our method. We take the $\exists$ sentences in $\Gamma$ and number them:

[TABLE]

And now we can say what our structure $\SS$ is. The universe is

[TABLE]

where the $A_{i}$ have size $\aleph_{0}$ and the $B_{j}$ have size $\aleph_{1}$. The interpretations of the nouns is

[TABLE]

Example 8.4**.**

The work on refinements in Section 4.1 applies to both $g$ and also to $\overline{g}$. So we would get two different partitions with all the required properties:

[TABLE]

9 Conclusion

This paper has shown a soundness and completeness theorem of the logic $\mathcal{L}({\mathbf{P}})$ when interpreted on infinite sets. The main point of the paper is that the language has cardinality comparison features are not expressible in first order logic, and yet it has a complete proof system with an efficient proof search algorithm. Some may find these results to be surprising. The message is that the very weak system of syllogistic logic has extensions which are well-behaved and expressive.

This paper contributes to the project of finding larger and larger well-behaved logics which talk about sizes of sets. One next question would be to take the logic of [moss:forDunn] and add the quantifier most, interpreted by strict majority.