1 Introduction
Main philosophical goals and ideas of the Quantified argument calculus (which avoids the alphabet-soup approach to logical nomenclature by conveniently abbreviating to “Quarc”) were laid out by Hanoch Ben-Yami in [Reference Ben-Yami1] and it received the first formal treatment in [Reference Lanzet, Ben-Yami, Hendricks, Neuhaus, Scheffler, Pedersen and Wansing12], with a seminal formal presentation in [Reference Ben-Yami2]. Since then Quarc has attracted a fair amount of philosophical and logical interest. It was used to investigate assertoric syllogistic [Reference Raab22], natural logic [Reference Ben-Yami4] and necessary existence and the Barcan formulas [Reference Ben-Yami4]. On a more formal side a sequent calculus was developed [Reference Pavlović19], which in turn led to establishing a close connection Quarc shares with free logic [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18]. Finally (but slightly earlier), a three-valued system of Quarc was developed in [Reference Lanzet11]. The present paper will mostly extend the results from the last two papers, primarily by utilizing recent developments in proof theory of free logic from [Reference Pavlović20].
It has been argued, in [Reference Ben-Yami1] and most recently in [Reference Ben-Yami3], that compared to the Predicate calculus, Quarc approximates the syntax of natural languages more accurately, at least when it comes to the features it incorporates, such as (obviously, in addition to quantification) copular structure, converse relations and anaphora. We will take the claim of the relationship of Quarc and natural languages as prima facie plausible, if not yet definitively established, and will rather focus primarily (though not exclusively) on its relationship with the Predicate calculus.
It has so far been established in [Reference Lanzet11] that Quarc extended by defining clauses and by a predicate
${\mathcal T}$
(which can be intuitively read as “thing,” and function similarly to a domain, since it is meant to approximate the quantification of Predicate calculus) contains a semantically isomorphic image of the Predicate calculus (for brevity, from now on ‘PC’). Therefore, such an extension of Quarc is at least as strong as PC. On the other hand, PC extended with the schema
$\exists x Sx$
for every unary predicate S (corresponding to the rule of instantiation in Quarc [Reference Pavlović19]) is at least as strong as Quarc [Reference Raab21]. These two results do not, however, suffice to establish the exact relationship between the two systems. This open problem is the main question we address in this paper.
Our task here is complicated by the aforementioned implementation of the features of natural language, and a method of dealing with those will be crucial. To this end we develop a method of translating every formula of Quarc into what we label a shallow normal form (for reasons explained in [Reference Pavlović19], converse relations and copular structure can be considered “deep” operations on predicates and connectives, respectively) which, combined with the appropriate treatment of the predicate
${\mathcal T}$
, allows us to develop a system of Quarc which is deductively equivalent to PC. This, should we give some credence to the claim that Quarc more accurately represents natural language quantification, also serves to shine some light onto the relationship between PC and natural language quantification. Moreover, the fact that the addition of
${\mathcal T}$
allows for the demonstration (shown in this paper) of the Craig interpolation property is likewise informative of what is special about that predicate.
We then note that all the additions we have thus far discussed had been of a simple kind, namely of quantifiers binding only unary predicates. This, of course, need not be the case, as it is common in natural language to quantify over more complex phrases (this was a central goal in [Reference Lanzet11]). The proof-theoretic approach we have adopted in this paper will give an elegant formulation of this while also guaranteeing schematic proofs of all the required structural properties.
1.1 Plan of the paper
Utilizing recent developments in structural proof theory, in Section 2 we develop a G3-style sequent calculus for Quarc and briefly demonstrate its structural properties. We put these properties to use immediately to construct direct proofs of the meta-theoretical properties of the system. In Section 3 we then incorporate the predicate
${\mathcal T}$
into the system in a way that preserves all the structural properties. This allows us to identify a system of Quarc which is deductively equivalent to PC, and also yields a constructive method of demonstrating the Craig interpolation theorem. In Section 4 we generalize the extension from the previous section and allow for quantified arguments to include more complex formulas of the language, and finally in Section 5 we lay out avenues of future research.
2 The formal system
Quarc gets its name from allowing (like natural languages) for quantified arguments (QAs) of the form
$\forall S$
and
$\exists S$
, where S is a unary predicate, to occupy the same argument position as names, or singular arguments (SAs). So while
Example 2.1.
$(a)P$
is a sentence of Quarc, so is
Example 2.2.
$(\forall S)P$
where 2.1 is read as “a is P” and 2.2 as “all S are P.” A detailed explanation of the motivation for these can be found in [Reference Ben-Yami2]. Since this will be relevant later in the paper, let us point out that quantified arguments (just like singular ones) are not themselves sentences. Note also that when we simply mention “arguments,” we encompass both the singular and the quantified variety.
We define (in BNF) the formula of Quarc as follows, where t indicates a singular argument,
$A[a]$
indicates the formula A which contains an occurrence of the argument a, the list
$t_{1}\ldots t_{n}$
indicates n occurrences of the singular argument t,
$A[b/c]$
indicates the result of the substitution of an instance of an argument c by an argument or anaphor b in formula A, and
$A[b//c]$
of all instances of c.
Definition 2.3 (Formula of Quarc).
$$ \begin{align*} &A::= (t_{1}\ldots t_{n})P^{n} |\ (t_1 ... t_n)P^{\pi n}\ |(t_{1}\ldots t_{n})\neg P |\ \neg (A)^{*} \ |\ (A)\times (A)^{*}| \\ & A[t_{\alpha }/t_{1},\alpha /t_{i},\ldots , \alpha /t_{j}]^{**}\ |\ A[\forall S/t]^{***}\ |\ A[\exists S/t]^{***} \end{align*} $$
where formulas of the form
$(t_{1}\ldots t_{n})P^{n}$
are called basic (parentheses omitted whenever possible),
$\times \in \{\wedge , \vee , \to \}$
and
-
* the parentheses in
$(A)$
are called sentential, and omitted if no ambiguity arises -
** A contains k occurrences of a singular argument t none of which are a source of any anaphors, and
$1<i\leq j\leq k$
-
***
$A[\forall S/t]$
and
$A[\exists S/t]$
are governed (definition below) by the displayed occurrence of the quantified argument (QA)
$\forall S$
and
$\exists S$
, respectively.
Definition 2.4 (Governance).
An occurrence
$qP$
of a QA governs a formula A just in case
$qP$
is the leftmost QA in A and A does not contain any other string of symbols
$(B)$
in which the parentheses are a pair of sentential parentheses, such that B contains
$qP$
and all the anaphors of all the QAs in B.
Remark 2.5. We will from now on as a matter of convention assume that whenever several rules can be applied in different order and yield the same formula, the anaphora rule, if used, is applied last.
2.1 The system G3Q
In [Reference Pavlović19], an LK-style sequent calculus [Reference Gentzen9, Reference Gentzen10] was developed for Quarc, and shown that it (as well as its subsystems) possesses the prerequisite structural properties, chief of which is the cut-elimination property. The subsystems are labeled ‘Quarc
$_{3}$
’ for the system without identity rules, ‘Quarc
$_{2}$
’ for the one without instantiation rule, and ‘Quarc
$_{B}$
’ for the one without either. When these need to be distinguished from the original system the latter is referred to as full Quarc. After we have added a few more systems we will offer (Figure 5) a schematic representation of all the systems and their relations. Throughout the paper we adopt the convention of using symbols in subscript to indicate systems with certain elements removed (like the ones we just introduced), and in superscript to indicate systems with elements added.
In [Reference Pavlović19] the authors suggest, and it has since been shown in [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18], that Quarc bears a structural similarity to free logic. This is fortunate, since recent developments in the proof theory of free logics in [Reference Pavlović20] (the same approach was used for intuitionistic logic of existence in [Reference Maffezioli and Orlandelli14]), allow us to simplify the quantifier rules, and thereby also the proofs of structural and meta-theoretic properties, as well as proof search. To this end we here switch to a G3-style sequent calculus we call G3Q (Figure 1). Given that the cut elimination for a related system was already demonstrated we only give a brief and schematic proof focusing on the new cases, but we also present other structural properties required in that proof since some of those, like height-preserving admissibility of contraction, are in any case not present in the LK-style calculus.
Fig. 1 G3Q.
The basic unit of a sequent calculus is a sequent
$\Gamma \Rightarrow \Delta $
, where
$\Gamma $
and
$\Delta $
are finite multisets of formulas. All the formulas except
$\Gamma $
and
$\Delta $
are called active formulas of the rule if they occur only in the upper sequent(s), or premises, and principal if they occur in the lower sequent, or the conclusion, of the rule.
2.2 Structural properties
The standard range of structural properties holds for G3Q, a fact shown here briefly and schematically. We begin by defining the weight of a formula, following [Reference Pavlović19].
Definition 2.6 (Weight of a formula).
The weight w of a formula is defined as follows:
$$ \begin{align*} \begin{array}{ll} w((t_{1}\ldots t_{n})P^{n})=0 &w(A\times B)=w(A)+w(B)+1\\ w((t_{1}\ldots t_{n})P^{\pi n})=1 &w(A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}])=w(A[t])+1\\ w((t_{1}\ldots t_{n})\neg P)=w((t_1...t_n)P) + 1 &w(A[\forall S/t])=w(A[t])+1\\ w(\neg A)=w(A)+1\ \ \ \ \ \ \ \ \ &w(A[\exists S/t])=w(A[t])+1 \end{array} \end{align*} $$
Lemma 2.7 (Substitution).
If
$\vdash _{n}\Gamma \Rightarrow \Delta $
in G3Q (where
$\vdash _{n}$
denotes derivability with height bounded by n), then
$\vdash _{n}\Gamma [s/t] \Rightarrow \Delta [s/t]$
is derivable in G3Q.
Proof. By induction on the height of the derivation.
Basic case. If
$\Gamma \Rightarrow \Delta $
is an initial sequent, so is
$\Gamma [s/t] \Rightarrow \Delta [s/t]$
.
Inductive case. If the last step used was one of the propositional rules the step is straightforward, as they do not alter the singular arguments between the premise(s) and the conclusion. The rules L
$NP$
and R
$NP$
likewise do not alter the singular arguments between their premise(s) and conclusion, and
$=_{Repl}$
, LA, RA, L
$Rd$
and R
$Rd$
only alter the order or number of appearances of the singular arguments. In all those cases the application of the inductive hypothesis to the upper sequents, followed by an application of the rule, is routine.
If the last step used was Ins, the premise is
$cM, \Gamma \Rightarrow \Delta $
, where c does not occur in
$\Gamma , \Delta $
. If c is precisely s, we first use the inductive hypothesis to obtain some
$dM, \Gamma \Rightarrow \Delta $
, and then again for
$dM, \Gamma [s/t]\Rightarrow \Delta [s/t]$
, and applying the rule Ins we get
$\Gamma [s/t]\Rightarrow \Delta [s/t]$
. If c is not s, we skip the first application of the inductive hypothesis. From
$cM, \Gamma \Rightarrow \Delta $
we get by the inductive hypothesis
$cM, \Gamma [s/t]\Rightarrow \Delta [s/t]$
and then by Ins
$\Gamma [s/t]\Rightarrow \Delta [s/t]$
.
If the last step used was R
$\forall $
, and the eigenvariable (defined in Figure 1 below) of the rule was s (otherwise we skip the first application of the inductive hypothesis), then its premise is
$ sM, \Gamma \Rightarrow \Delta , A [ s/\forall M] $
. Using the inductive hypothesis we first obtain the sequent
$ cM, \Gamma \Rightarrow \Delta , A [ c/\forall M] $
(s does not occur in
$\Gamma $
or
$\Delta $
), then using the inductive hypothesis again we obtain
$ cM, \Gamma [s/t] \Rightarrow \Delta [s/t], A [ c/\forall M][s/t] $
, and then applying the rule R
$\forall $
we get
$ \Gamma [s/t] \Rightarrow \Delta [s/t], A [\forall M][s/t] $
. Symmetrical for L
$\exists $
and routine for L
$\forall $
and R
$\exists $
. Likewise routine for identity rules, noting that in the case of
$=_{Repl}$
the replacing constant can’t be the same s as used in the rule.□
Lemma 2.8 (Axiom generalization).
For any A, the sequent
$A,\Gamma \Rightarrow \Delta , A$
is derivable in G3Q.
Proof. By induction on the weight of A.
Basic step. Follows immediately from initial sequents.
Inductive step. Straightforward for special symbols and routine for connectives and identity rules. The interesting cases are the quantifiers. In the case of the universal quantifier:
Symmetrical in the case of
$\exists $
.□
Lemma 2.9 (Weakening).
Height-preserving weakening is admissible in G3Q:
-
1. If
$\vdash _{n} \Gamma \Rightarrow \Delta $
then
$\vdash _{n} C, \Gamma \Rightarrow \Delta $
. -
2. If
$\vdash _{n} \Gamma \Rightarrow \Delta $
then
$\vdash _{n} \Gamma \Rightarrow \Delta , C$
.
Proof. Routine by induction on the height of the derivation, using Lemma 2.7 when necessary.□
Lemma 2.10 (Invertibility).
All the rules of G3Q are height-preserving invertible. For each rule R, if
$\vdash _{n}A, \Gamma \Rightarrow \Delta , B$
, then
$\vdash _{n}A', \Gamma \Rightarrow \Delta , B'$
(and
$\vdash _{n}A'', \Gamma \Rightarrow \Delta , B''$
), where A or B are the principal (sometimes two) formulas of the rule R, while
$A'$
and
$B'$
(and
$A''$
,
$B''$
) are the active formulas of the rule (some of these will be empty).
Proof. Straightforward for propositional rules, follows immediately from Lemma 2.9 for identity rules, L
$\forall $
and R
$\exists $
. We check for the remaining rules by induction on the height of the derivation.
Basic step. For all the remaining rules, if a sequent of the same form as the lower sequent of the rule is an initial sequent, then so is
$\Gamma \Rightarrow \Delta $
. Therefore by adding the formulas from the upper sequent of the rule other than
$\Gamma $
,
$\Delta $
to it, we likewise obtain an initial sequent.
Inductive step. For each of the rules, if the last step in the derivation of the sequent did not use that rule with A or B principal, we apply the inductive hypothesis (and maybe Lemma 2.7) to the premises, and then apply the last rule used to produce the desired sequents. Otherwise the premises of the last rule used are already the desired sequents.
As an illustration we show the case of L
$\exists $
. We want to show that if
$\vdash _{n} A[\exists M], \Gamma \Rightarrow \Delta $
, then
$\vdash _{n} tM, A[t/\exists M], \Gamma \Rightarrow \Delta $
. If the formula
$A[\exists M]$
was not principal in the last rule used, then it has the form
If t is the eigenvariable of R we apply the Lemma 2.7, and then we apply the inductive hypothesis to the upper sequents to obtain
$tM, A[t/\exists M], \Gamma ^\prime \Rightarrow \Delta ^\prime $
(and
$tM, A[t/\exists M], \Gamma ^{\prime \prime } \Rightarrow \Delta ^{\prime \prime }$
). Finally, applying R to these sequents, we obtain
$tM, A[t/\exists M], \Gamma \Rightarrow \Delta $
.
If
$A[\exists M]$
is principal in the last rule used, the upper sequent of the rule is already
$tM, A[t/\exists M], \Gamma \Rightarrow \Delta $
, derived with the height of
$n-1$
.□
Lemma 2.11 (Contraction).
Height-preserving contraction is admissible in G3Q:
-
1. If
$\vdash _{n} C,C,\Gamma \Rightarrow \Delta $
then
$\vdash _{n} C, \Gamma \Rightarrow \Delta $
. -
2. If
$\vdash _{n} \Gamma \Rightarrow \Delta ,C,C$
then
$\vdash _{n} \Gamma \Rightarrow \Delta , C$
.
Proof. Simultaneous for (1) and (2) by induction on the height of the derivation. Most of the proof is routine, with the interesting part when the formula C is principal in R
$\forall $
or L
$\exists $
.
So, assume that C is
$A[\forall M]$
and principal in R
$\forall $
in the last step. Then the last step of the derivation is
$ \Gamma \Rightarrow \Delta , A[\forall M], A[\forall M]$
, derived by R
$\forall $
from
$tM, \Gamma \Rightarrow \Delta , A[\forall M], A[t/\forall M]$
. Applying the Lemma 2.10 to that sequent we get
$ tM, tM, \Gamma \Rightarrow \Delta , A[t/\forall M], A[t/\forall M]$
with the same height of
$\leq n-1$
. We then apply the inductive hypotheses (1) and (2) to obtain
$t M, \Gamma \Rightarrow \Delta ,A[t/\forall M]$
and then R
$\forall $
to finally obtain
$ \Gamma \Rightarrow \Delta , A[\forall M]$
. Similar for L
$\exists $
.□
Theorem 2.12 (Cut).
Cut is admissible in G3Q.
Proof. By induction on the weight of a formula and subinduction on the sum of heights of the two upper sequents of a cut. The proof is standard, so we just illustrate the procedure for the example of a cut formula quantified by
$\forall $
and principal in both upper sequents of the cut. The instance of the cut then has the following form:
This is then transformed in the following way (Lemma 2.7 is applied to the sequent
$sM, \Gamma \Rightarrow \Delta , A[s/\forall M]$
).
The upper cut has the same weight, but lower height, while the lower cut has lower weight. Similar for
$\exists $
.□
It immediately follows that
Corollary 2.13 (Weak subformula property).
Every formula occurring in a derivation of
$\Gamma \Rightarrow \Delta $
is either a subformula (under the usual definition) of some formula occurring in
$\Gamma $
,
$\Delta $
, or basic.
and from there
Corollary 2.14 (Consistency).
The calculus G3Q is consistent.
2.3 Deductive equivalence
In order to prove that the system G3Q is deductively equivalent to LK-Quarc, given that the special rules of the two systems, as well as the rules R
$\forall $
and L
$\exists $
are identical, and that the propositional rules display the standard relationship between LK and G3 systems, we need only to prove the admissibility of L
$\forall $
and R
$\exists $
(Figure 2).
Fig. 2 L
$\forall $
and R
$\exists $
in LK-Quarc.
Lemma 2.15. The rules L
$\forall $
and R
$\exists $
of LK-Quarc are admissible in G3Q.
Proof.
Parallel for R
$\exists $
.□
Lemma 2.16. The rules L
$\forall $
and R
$\exists $
of G3Q are admissible in LK-Quarc.
Proof.
Parallel for R
$\exists $
.□
Combined, these two lemmas suffice to show that
Theorem 2.17. The systems G3Q and LK-Quarc, as well as their subsystems B, 2 and 3, are deductively equivalent.
All the subsequent structural and meta-theoretical properties will likewise, mutatis mutandis, hold for any of the subsystems. Since this is straightforward (requires simply removing several inductive steps), explicit reference to them will be omitted in the rest of this section.
2.4 Meta-theoretical properties
To prove the meta-theoretical properties, we adopt the semantics presented in [Reference Pavlović19], which is for the most part the same as [Reference Ben-Yami2]. The only difference is that in [Reference Pavlović19], valuation of the quantifiers is clearly defined in the absence of the semantic rule of instantiation, while in [Reference Ben-Yami2] this is not explicitly the case. This opens up the possibility of either approaching Quarc without the semantic rule as a free logic [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18], or as three-valued [Reference Lanzet11]. In [Reference Ben-Yami4] both are discussed, but since here we are interested only in the bivalent approach, we have adopted the semantics from the first paper.
Definition 2.18 (Truth-value assignment
${\mathcal V}$
).
-
1.
${\mathcal V}(t=t)=1$
, -
2.
${\mathcal V}(s=t)\in \{0,1\},$
-
3.
${\mathcal V}(p)\in \{0,1\}$
, such that if
${\mathcal V}(s=t)=1$
then
${\mathcal V}(p[t])={\mathcal V}(p[s/t])$
, -
4.
${\mathcal V}(t_{\pi 1},\ldots ,t_{\pi n}P^{\pi n})={\mathcal V}(t_{1},\ldots ,t_{n}P^{n})$
, -
5.
${\mathcal V}(\neg A)=1$
iff
${\mathcal V}(A)=0$
,
${\mathcal V}(A\wedge B)=1$
iff
${\mathcal V}(A)=1$
and
${\mathcal V}(B)=1$
, etc, -
6.
${\mathcal V}(t_{1},\ldots ,t_{n}\neg P)={\mathcal V}(\neg t_{1},\ldots ,t_{n}P)$
, -
7.
${\mathcal V}(A[ t_{\alpha }/t_{1}, \alpha /t_{2},\ldots ,\alpha /t_{n}] )={\mathcal V}(A)$
, -
8.
${\mathcal V}(A [ \forall P] )=1$
iff for every SA t for which
${\mathcal V}(tP)=1$
,
${\mathcal V}(A [ t/\forall P])=1$
, -
9.
${\mathcal V}(A [ \exists P] )=1$
iff for some SA t for which
${\mathcal V}(tP)=1$
,
${\mathcal V}(A [ t/\exists P])=1$
.
In addition to these, the rule needed for full Quarc is that for instantiation:
-
10. (Instantiation) For any unary predicate P there is an SA t such that
${\mathcal V}(tP)=1$
.
2.4.1 Soundness
Soundness of the system follows from the same result for Quarc [Reference Ben-Yami2], deductive equivalence of it to the system in [Reference Pavlović19], and Theorem 2.17. We therefore only sketch out the proof here, but we present it nonetheless since it is considerably less roundabout. To begin, we define the notion of validity of a sequent.
Definition 2.19 (Validity).
A formula is valid under
${\mathcal V}$
if
${\mathcal V}(A)=1$
. A sequent
$\Gamma \Rightarrow \Delta $
is valid under an assignment
${\mathcal V}$
iff in case all formulas in
$\Gamma $
are valid under
${\mathcal V}$
, some formula in
$\Delta $
also is. A sequent is simply valid iff it is valid under any assignment.
We prove that
Theorem 2.20 (Soundness).
If a sequent
$\Gamma \Rightarrow \Delta $
is derivable in G3Q, it is valid under any assignment
${\mathcal V}$
.
Proof. By induction on the height of the derivation of
$\Gamma \Rightarrow \Delta $
. Straightforward for the basic case, and simple for connectives, identity, special rules and
$Ins$
. We illustrate on the example of the latter.
If the last step of the derivation is obtained by
$Ins$
, then it has the form
Assume all the formulas in
$ \Gamma $
are valid. By Definition 2.18 there is some t for which
$tM$
is true. Let that be t (otherwise use Lemma 2.7). Then by the inductive hypothesis, some formula in
$\Delta $
is valid.
If the last step of the derivation is obtained by L
$\forall $
, then it has the form
Assume
$tM, A[\forall M]$
and all the formulas in
$ \Gamma $
are valid. Then, since
$tM$
and
$A[\forall M]$
are valid, by Definition 2.18 so is
$A[t/\forall M]$
, therefore all of
$tM$
,
$A[t/\forall M]$
,
$A[\forall M]$
,
$\Gamma $
are valid, and by the inductive hypothesis so is some formula in
$\Delta $
.
If the last step of the derivation is obtained by R
$\forall $
, then it has the form
Assume all the formulas in
$\Gamma $
are valid. By Definition 2.18 there is some t such that
$tM$
is valid (simple otherwise). Let t be any such SA (using Lemma 2.7 as necessary). By the inductive hypothesis, if for any such t the formula
$A [ t/\forall M]$
is not valid, then some formula in
$\Delta $
is, and otherwise
$A[\forall M]$
is valid.
Parallel, respectively, for R
$\exists $
and L
$\exists $
.□
2.4.2 Completeness
Completeness proofs for systems related to Quarc were provided in [Reference Lanzet11, Reference Lanzet, Ben-Yami, Hendricks, Neuhaus, Scheffler, Pedersen and Wansing12], but no proof of that property for Quarc proper has been published so far.Footnote 1 In any case the completeness proof here is worth presenting since it is exceedingly simple and follows the method typical of sequent calculi [Reference Buss and Buss7, Reference Schütte23]. This particular version is adapted from [Reference Pavlović20], which itself follows the presentation of [Reference Negri and von Plato15]. We start by the definition of a reduction tree (which intuitively represents a bottom-up proof search).
Definition 2.21 (Reduction tree).
A reduction tree for a sequent
$\Gamma \Rightarrow \Delta $
is built in steps. At step 0, the tree is just
$\Gamma \Rightarrow \Delta $
. Any sequent that does not contain the same basic formula in both the antecedent and the consequent is called active.
Each subsequent step consists of stages. At each stage and for each sequent
$\Gamma _{i}\Rightarrow \Delta _{i}$
active at the beginning of it, we apply to any eligible (pair of) formulas in the sequent the rule of the stage once (thereby extending the height of the tree by n, for n such formulas in
$\Gamma _{i}\Rightarrow \Delta _{i}$
, and creating at most
$2^{n}$
branches, before proceeding to the next stage). We call an application of a rule to formulas their reduction.
The order of stages is:
(1)
$Ins$
, for every unary predicate occurring in
$\Gamma _{i}\Rightarrow \Delta _{i}$
, and taking from the denumerable list of singular arguments the first that does not occur in
$\Gamma _{i}\Rightarrow \Delta _{i}$
and had not yet been used in any reductions.
(2) L
$\wedge $
(3) R
$\wedge $
(4) L
$\vee $
(5) R
$\vee $
(6) L
$\neg $
(7) R
$\neg $
(8) L
$\to $
(9) R
$\to $
(10) L
$\forall $
, for every pair of formulas
$A[\forall M]$
and
$tM$
in
$\Gamma _{i}$
.
(11) R
$\forall $
, taking for the reduction of each formula
$A[\forall M]$
in
$\Delta _{i}$
from the denumerable list of singular arguments the first such argument t not yet used in the reduction tree.
(12) L
$\exists $
, treated symmetrically to R
$\forall $
(13) R
$\exists $
, treated symmetrically to L
$\forall $
(13)
$=_{Repl}$
(14)
$=_{Ref}$
, for any singular argument t such that it occurs in
$\Gamma _{i}\Rightarrow \Delta _{i}$
but
$t=t$
does not occur in
$\Gamma _{i}$
(15) LA (16) RA (17) L
$Rd$
(18) R
$Rd$
(19) L
$NP$
(20) R
$NP$
.
For each active sequent to which no rule can be applied, we just copy it.
We now show that
Lemma 2.22. For any sequent
$\Gamma \Rightarrow \Delta $
its reduction tree either produces a proof or it produces a valuation that validates all the formulas in
$\Gamma $
and none of the formulas in
$\Delta $
.
Proof. It is clear that a reduction tree with no active sequents will produce, read top down (and thus beginning with initial sequents and ending with
$\Gamma \Rightarrow \Delta $
), a finite derivation of that sequent. The second part is more involved and goes through several lemmas below.□
We build an invalidating valuation from an (infinite) reduction tree to prove the second part. The existence of an infinite branch is guaranteed by Kőnig’s lemma in the usual way ([Reference Negri and von Plato15], p. 82).
Definition 2.23 (Refutation valuation
$\mathcal{C}$
).
Take an infinite branch
$$ \begin{align*}\Pi \equiv \Gamma_{0} \Rightarrow \Delta_{0},\ldots, \Gamma_{i} \Rightarrow \Delta_{i}, \ldots\end{align*} $$
of a reduction tree for a sequent
$\Gamma \Rightarrow \Delta $
(where
$\Gamma _{0} \Rightarrow \Delta _{0}$
is
$\Gamma \Rightarrow \Delta $
) and consider sets
$\Gamma ^{*} \equiv \bigcup \Gamma _{i}$
and
$\Delta ^{*} \equiv \bigcup \Delta _{i}$
for
$0\leq i$
. A refutation valuation
${\mathcal C}$
for a sequent
$\Gamma \Rightarrow \Delta $
is built by assigning
$1$
to all basic formulas in
$\Gamma ^{*}$
and
$0$
to all other basic formulas (thus including those in
$\Delta ^{*}$
), and otherwise the same as in Definition 2.18.
It is easy too see
${\mathcal C}$
is an appropriate Quarc truth-value assignment. Namely, it satisfies Instantiation. We can now show that
Lemma 2.24. Any formula A occurring in
$\Gamma ^{*}$
is assigned
$1$
by the refutation valuation
${\mathcal C}$
and any formula B occurring in
$\Delta ^{*}$
is assigned
$0$
by it.
Proof. By induction on the weight of A and B.
Basic step. Immediate from Definition 2.23 and noting that
$\Gamma ^{*}$
and
$\Delta ^{*}$
share no basic formulas (by Definition 2.21 and Corollary 2.13).
Inductive step. We illustrate for one example of a connective, as all are straightforward.
(
$\wedge $
) If A is a formula
$C\wedge D$
, then by stage (2) of Definition 2.21, C and D are also in
$\Gamma ^{*}$
, and by inductive hypothesis assigned
$1$
, and so
$C\wedge D$
is
$1$
.
If B is a formula
$C\wedge D$
, then by stage (3) of Definition 2.21, either C or D are also in
$\Delta ^{*}$
, and by inductive hypothesis assigned
$0$
, and so
$C\wedge D$
is
$0$
.
Similar for other connectives.
(
$\forall $
) If A is a formula
$C[\forall M]$
, then by stage (10) of Definition 2.21, for every singular argument t, if
$tM$
is in
$\Gamma ^{*}$
(and by inductive hypothesis
$1$
) then
$C[t/\forall M]$
is in
$\Gamma ^{*}$
(and by inductive hypothesis
$1$
), and so
$C[\forall M]$
is assigned
$1$
.
If B is a formula
$D[\forall M]$
, then by stage (11) of Definition 2.21, for some singular argument t,
$tM$
is in
$\Gamma ^{*}$
(and by inductive hypothesis
$1$
) and
$D[t/\forall M]$
is in
$\Delta ^{*}$
(and by inductive hypothesis
$0$
), and so
$D[\forall M]$
is
$0$
.
Similar for
$\exists $
.□
Finally, we have that
Theorem 2.25 (Completeness).
If
$\Gamma \Rightarrow \Delta $
is valid, then
$\Gamma \Rightarrow \Delta $
is derivable in G3Q.
3 Abstracting quantification
We now move on to add to the language the predicate
${\mathcal T}$
, meant (in Quarc) to approximate the conception of quantification and the role of the domain in the Predicate calculus [Reference Ben-Yami4], to produce the resulting language Quarc
$^{A}$
. However, since the standard approach of simply adding that predicate produces a system that is (as we will demonstrate shortly) too strong for that purpose, we instead add to our language the quantified arguments
$\forall {\mathcal T}$
and
$\exists {\mathcal T}$
, and to G3Q the corresponding rules for quantification over
${\mathcal T}$
listed below, to produce the system G3Q
$^{A}$
(Figure 3). We do not add
${\mathcal T}$
to the list of predicates.
Fig. 3 G3Q
$^{{A}}$
.
In a nutshell, instead of treating quantification over
${\mathcal T}$
as regular, but
${\mathcal T}$
as a special predicate, we treat quantification over
${\mathcal T}$
as special. Note that the QAs we add are not themselves sentences, so nothing is said of
${\mathcal T}$
outside of its use in quantification, which we feel better captures the intention cited in the paragraph above.
Since under the standard approach
${\mathcal T}$
would be considered an abstraction (entirely devoid of content) of a unary predicate—even though it is conveniently read as “thing,” it is more general than that [Reference Ben-Yami4]—we claim that here we are dealing with an abstract form of quantification. By the end of this section we will be able to say a few more things about the exact status of this predicate.
3.1 Sequent calculus G3Q
$^{A}$
G3Q
$^{A}$
is obtained by adding to G3Q the quantifier rules in Figure 3.
It is important to note that the cut elimination theorem would fail were we to here treat
${\mathcal T}$
as any other predicate. For instance, consider the following application of Cut:
Here, no way of transforming the cut that will get rid of
$t{\mathcal T}$
is available. The problem is avoided by disallowing such a formula in our language in the first place (so formula of the form
$A[\forall {\mathcal T}]$
can be principal in both upper sequents of the cut only if the rule used in the left sequent is R
$\forall {\mathcal T}$
).
But with the rules formulated as they are, it is easy to see that
Theorem 3.26 (Structural properties G3Q
$^{A}$
).
Axiom generalization holds for G3Q
$^{A}$
, substitution, weakening, invertibility and contraction hold height-preserving for G3Q
$^{A}$
, and cut is admissible. The same likewise holds for its subsystems.
Proof. The proofs exactly mirror the ones for G3Q, with the new rules a simpler case of quantification of G3Q.□
It follows from this that
Corollary 3.27 (Conservativity G3Q
$^{A}$
).
G3Q
$^{A}$
is a conservative extension of G3Q. That is to say, if
$\Gamma \Rightarrow \Delta $
is derivable in G3Q
$^{A}$
and
$\Gamma $
,
$\Delta $
do not contain
${\mathcal T}$
, then
$\Gamma \Rightarrow \Delta $
is derivable in G3Q. This likewise holds for the corresponding subsystems of the two.
Proof. It follows from the Corollary 2.13 that the derivation of an endsequent not containing
${\mathcal T}$
does not involve the use of rules specific to G3Q
$^{A}$
. Note that every derivation in G3Q is also a derivation in G3Q
$^{A}$
. Parallel for the subsystems.□
3.1.1 Meta-theoretical properties
To establish the meta-theoretical properties of G3Q
$^{A}$
, we extend Definition 2.18 for new cases of quantification as follows:
Definition 3.28 (Truth-value assignment
${\mathcal V}$
for Quarc
$^{A}$
).
-
11.
${\mathcal V}(A [ \forall {\mathcal T}] )=1$
iff for every t,
${\mathcal V}(A [ t/\forall {\mathcal T}])=1$
. -
12.
${\mathcal V}(A [ \exists {\mathcal T}] )=1$
iff for some t,
${\mathcal V}(A [ t/\exists {\mathcal T}])=1$
.
It is easy to show that
Theorem 3.29 (Meta-theoretical properties G3Q
$^{A}$
).
G3Q
$^{A}$
is sound and complete with respect to its semantics.
Proof. The proof extends the proofs of Theorems 2.20 and 2.25 with the new cases which are exactly alike the standard quantification of [Reference Negri and von Plato15].□
3.2 Sequent calculus G3Q
$^{{\mathcal T}}$
G3Q
$^{{\mathcal T}}$
(Figure 4) is a system obtained by adding to G3Q the rule for the predicate
${\mathcal T}$
and extending our language with a unary predicate
${\mathcal T}$
to produce Quarc
$^{{\mathcal T}}$
. So, unlike the previous system, here we are treating quantification over
${\mathcal T}$
as standard, but
${\mathcal T}$
as special predicate. This is the approach to the predicate opted for in [Reference Ben-Yami4, Reference Lanzet11], where it is treated as a syntactically regular, albeit semantically special and maximally general, predicate.
Fig. 4 G3Q
$^{{{\mathcal T}}}$
.
It is again easy to see that all the structural rules hold for this system as well (all the inductive steps for the new rule are parallel to those for
$=_{Ref}$
).
To establish the meta-theoretic properties of G3Q
$^{{\mathcal T}}$
, we extend Definition 2.18 for new cases of quantification as follows:
Definition 3.30 (Truth-value assignment
${\mathcal V}$
for Quarc
$^{{\mathcal T}}$
).
-
11. For every t,
${\mathcal V}(t{\mathcal T})=1$
.
It is easy to show that
Theorem 3.31 (Meta-theoretical properties G3Q
$^{{\mathcal T}}$
).
G3Q
$^{{\mathcal T}}$
is sound and complete with respect to its semantics.
Proof. The proof extends the proofs of Theorem 3.29 with the case of the new rule
${\mathcal T}$
.
For soundness, assume the last step of the derivation was
${\mathcal T}$
and all the formulas in
$\Gamma $
are valid. Then, by Definition 3.30,
$a{\mathcal T}, \Gamma $
are all valid, and so some formula in
$\Delta $
is as well.
For completeness, we add the stage
(21)
${\mathcal T}$
, for any SA t occurring in
$\Gamma _{i}\Rightarrow \Delta _{i}$
such that
$t{\mathcal T}$
does not occur in
$\Gamma _{i}$
.
It is then easy to see the refutation valuation is an appropriate truth-value assignment, namely for all SAs t,
$t{\mathcal T}$
holds. Completeness follows like in the proof of Theorem 2.25 (
$\forall {\mathcal T}$
and
$\exists {\mathcal T}$
are just cases of regular quantification).□
3.3 Relation between G3Q
$^{A}$
and G3Q
$^{{\mathcal T}}$
After presenting a range of systems in the previous section, we now explore the relation they hold to one another. We have already seen that G3Q
$^{A}$
is a conservative extension of G3Q. We now investigate the relation between G3Q
$^{A}$
and G3Q
$^{{\mathcal T}}$
. Several lemmas are straightforward.
Lemma 3.32.
$\Rightarrow t{\mathcal T}$
is derivable in G3Q
$^{{\mathcal T}}$
Proof.
□
Lemma 3.33. The quantification rules of G3Q
$^{A}$
are all admissible in G3Q
$^{{\mathcal T}}$
.
Proof. The proof is very simple and similar in all cases, so we just provide the case of L
$\forall {\mathcal T}$
as an example.
□
Lemma 3.34.
$\Rightarrow a{\mathcal T}$
is not derivable in G3Q
$^{A}$
.
Proof. Follows from Subformula property (a corollary to Theorem 3.26) for G3Q
$^{A}$
.□
Finally, we get that
Theorem 3.35. G3Q
$^{A}$
is an intermediate system between G3Q and G3Q
$^{{\mathcal T}}$
.
Proof. That G3Q
$^{A}$
is stronger than G3Q follows from Corollary 3.27. That G3Q
$^{{\mathcal T}}$
is stronger than it follows from Lemmas 3.32–3.34.□
We interpret this theorem the following way—the difference between G3Q
$^{A}$
and G3Q
$^{{\mathcal T}}$
is that the former has an implicit use of the abstract predicate (it is rather a pseudo-predicate there, only implemented into the quantified arguments, but not added to the list of predicates), while in the latter it is explicit (a separate rule). Consequently, in the latter we are able to show something more about the predicate itself, while in the former we can only address quantification. Therefore, while G3Q
$^{{\mathcal T}}$
addresses the abstract predicate, G3Q
$^{A}$
deals with abstract predication only.
What this theorem moreover demonstrates is that our analysis of the predicate
${\mathcal T}$
differs from previous approaches to it [Reference Ben-Yami4, Reference Lanzet11], which in the next section will allow us to paint a more fine-grained picture of the relationship of Quarc and PC. More specifically, the system involved will be G3Q
$^{A}_{2}$
, which is G3Q
$^{A}$
without the instantiation rule (since PC allows for empty extensions of unary predicates). As a first step, we prove a corollary
Corollary 3.36. The system G3Q
$^{A}_{2}$
, which is the system G3Q
$^{A}$
without the rule
$Ins$
, is an intermediate system between G3Q
$_{2}$
and G3Q
$^{{\mathcal T}}$
.
Proof. From Corollary 3.27 and (since G3Q
$^{A}_{2}$
is straightforwardly weaker than G3Q
$^{A}$
) Theorem 3.35.□
We have so far in this section introduced a multitude of systems of Quarc. Moreover the subsystems
$2$
,
$3$
and B are now taking center stage. So let us, before proceeding, sketch out the relationships of all the versions of Quarc (Figure 5) to make keeping track of them easier.
Fig. 5 Systems of Quarc.
Here subscripts represent removal of rules (
$2$
removal of instantiation,
$3$
of identity and B of both), while superscripts represent additions (A of abstract quantification,
${\mathcal T}$
of that predicate). Therefore, Q represents full Quarc, as introduced in [Reference Pavlović19], and which also appears in [Reference Ben-Yami4], while the system in [Reference Ben-Yami2] corresponds to
$Q_{3}$
.
Of the systems introduced in this paper
$Q^{A}$
stands for Quarc
$^{A}$
while its subsystems are laid out in the same way as for full Quarc, and
$Q^{{\mathcal T}}$
stands for Quarc
$^{{\mathcal T}}$
, with its subsystems again represented the same way (for systematicity, but they will be of no importance going forward).
$Q^{{\mathcal T}}$
is the system with the predicate
${\mathcal T}$
discussed in [Reference Ben-Yami4].
3.4 Relation between Quarc and the Predicate calculus
In order to proceed with the comparison of Quarc and PC, we first need to define a translation procedure between the two systems. This will proceed in several steps, with the initial ones concerned with transforming the sentences of Quarc into a shallow normal form. The issue with coming up with a translation procedure for Quarc is that some formula formation rules operate within a sentence, and this form will avoid such a situation.
Definition 3.37 (Shallow normal form, SNF).
A formula of Quarc is in a shallow normal form iff it contains no reordered predicates nor negative predications.
We now demonstrate how to reduce all of Quarc to just its SNF fragment.
Lemma 3.38 (Reorder reduction).
Let A be a formula
$(a_{\pi 1},\ldots ,a_{\pi n})R^{\pi n}$
which does not contain anaphoric expressions
$\alpha _{i},\ldots ,\alpha _{j}$
, where
$R^{\pi n}$
is an n-ary reordered predicate (with
$R^{n}$
its null-permutation) and
$a_{\pi 1},\ldots ,a_{\pi n}$
arguments, of which
$q_{i}P_{i}, \ldots , q_{j}P_{j}$
,
$0\leq i\leq j\leq n$
are all the quantified arguments (with
$q\in \{\forall , \exists \}$
) appearing in that order from left to right. Then A is equivalent to
$$ \begin{align*}(q_{i}P_{i_{\alpha i}})P_{i}\wedge \cdots \wedge(q_{j}P_{j_{\alpha j}})P_{j}\wedge((a_{1},\ldots ,a_{n})R^{n}[\alpha_{i}/q_{i}P_{i},\ldots ,\alpha _{j}/q_{j}P_{j}])\end{align*} $$
Proof. By induction on the number of quantified arguments in A for each direction of the equivalence. In the basic case, this is simply an application of the Reorder rules.
In the inductive case, we distinguish two options—when the governing quantifier
$q_{i}$
is
$\forall $
and when it is
$\exists $
. We tackle these in turn.
(
$\forall $
) In the L-R case the derivation is:
In the R-L case the derivation is:
(
$\exists $
) Parallel to the corresponding cases above.□
Lemma 3.39 (Negative predication reduction).
Let A be a formula
$(a_{1},\ldots ,a_{n})\neg R^{n}$
which does not contain anaphoric expressions
$\alpha _{i},\ldots ,\alpha _{j}$
, where
$R^{n}$
is an n-ary predicate or reordered predicate and
$a_{ 1},\ldots ,a_{ n}$
arguments, of which
$q_{i}P_{i}, \ldots , q_{j}P_{j}$
,
$0\leq i\leq j\leq n$
are all the quantified arguments appearing in that order from left to right. Then A is equivalent to
$$ \begin{align*} (q_{i}P_{i_{\alpha i}})P_{i}\wedge \cdots \wedge(q_{j}P_{j_{\alpha j}})P_{j}\wedge(\neg (a_{1},\ldots ,a_{n})R^{n}[\alpha_{i}/q_{i}P_{i},\ldots ,\alpha _{j}/q_{j}P_{j}]). \end{align*} $$
Proof. Parallel to the proof of Lemma 3.38.□
We can now show that
Theorem 3.40. Every formula A of Quarc is equivalent to some Quarc formula
$A'$
which is in SNF.
Proof. By induction, simultaneous for both directions, on the weight of A. For trivial cases, which also includes the basic case, this is an instance of Lemma 2.8. For
$(t_{\pi 1}\ldots t_{\pi n})P^{\pi n} $
and
$(t_{1}\ldots t_{n})\neg P^{ n} $
this is a simple application of reorder and negative predication rules. The cases containing no
$\wedge $
,
$\vee $
,
$\to $
nor sentential negation are covered by Lemmas 3.38 and 3.39. We examine the remaining cases.
If the last formation rule applied was the one for anaphora, then A is equivalent to some
$A[t/t_{\alpha }, t/\alpha _{1}, \ldots , t/\alpha _{n}]$
, to which we can apply the inductive hypothesis and obtain the requisite
$A'[t/t_{\alpha }, t/\alpha _{1}, \ldots , t/\alpha _{n}]$
.
If the last formation rule applied was the one for
$\wedge $
, we have the following derivation.
Note that if
$A'$
and
$B'$
are in SNF, then
$A'\wedge B'$
is in SNF. Similar for the other connectives and in the other direction.
If the last formation rule applied was the one for
$\forall $
, we have the following derivation.
Similar for the
$\exists $
and in the other direction.□
In the discussion of the relationship of Quarc and PC in [Reference Ben-Yami4], the reordered predicates are omitted. We are not forced to take this route thanks to this theorem. Keeping it in mind, in the proceeding we can focus simply on the SNF fragment of Quarc. We can now offer a definition (greatly simplified from [Reference Lanzet11]) of the translation procedure from Quarc to PC and vice versa.
Definition 3.41 (Translation procedure
$\varphi ^{q}_{pc}$
).
The translation procedure from the SNF fragment of Quarc into the Predicate calculus is a function
$\varphi ^{q}_{pc}: \mathcal {L}_{\textrm{Quarc}}^{\textrm{SNF}} \to \mathcal {L}_{\textrm{PC}}$
. The languages are assumed to share the list of individual constants and predicates.
$\forall {\mathcal T}_{\langle \alpha \rangle }$
marks that the quantified argument is the source of anaphora
$\alpha $
, if at all,
$\alpha _{1}, \ldots , \alpha _{n}$
mark all n occurrences of the anaphora
$\alpha $
and t marks either a variable
$x,y,\ldots $
or a constant
$a,b,\ldots $
The function
$\varphi ^{q}_{pc}$
(written just as
$\varphi $
for legibility) is then defined as:
$\varphi (t_{1},\ldots ,t_{n}P^{n}) = P^{n}t_{1},\ldots ,t_{n}$
$\varphi (A[t_{\alpha }])=\varphi (A[t/t_{\alpha }, t/\alpha _{1},\ldots ,t/\alpha _{n}])$
$\varphi (\neg A)= \neg \varphi (A)$
$\varphi (A\times B)= \varphi (A)\times \varphi (B)$
$\varphi (A[\forall {\mathcal T}])= \forall x \varphi (A[x/\forall {\mathcal T}_{\langle \alpha \rangle }, x/\alpha _{1}, \ldots , x/\alpha _{n}])$
$\varphi (A[\exists {\mathcal T}])= \exists x \varphi (A[x/\exists {\mathcal T}_{\langle \alpha \rangle }, x/\alpha _{1}, \ldots , x/\alpha _{1}])$
$\varphi (A[\forall M])= \forall x(Mx \to \varphi (A[x/\forall M_{\langle \alpha \rangle }, x/\alpha _{1}, \ldots , x/\alpha _{n}]))$
$\varphi (A[\exists M])= \exists x (Mx \wedge \varphi (A[x/\exists M_{\langle \alpha \rangle }, x/\alpha _{1}, \ldots , x/\alpha _{1}])).$
The translation of a formula A is complete when there are no more strings of symbols containing
$\varphi $
.
Definition 3.42 (Translation procedure
$\varphi ^{pc}_{q}$
).
The translation procedure from the Predicate calculus into Quarc is a function
$\varphi ^{pc}_{q}: \mathcal {L}_{\textrm{PC}} \to \mathcal {L}_{\textrm{Quarc}}$
(that this will be the SNF fragment of it is trivial). The languages are again assumed to share the list of individual constants and predicates, and t marks either a variable
$x,y,\ldots $
or a constant
$a,b,\ldots $
. The function
$\varphi ^{pc}_{q}$
(written just as
$\varphi $
for legibility) is then defined as:
$\varphi (P^{n}t_{1},\ldots ,t_{n}) = t_{1},\ldots ,t_{n}P^{n}$
$\varphi (\neg A)= \neg \varphi (A)$
$\varphi (A\times B)= \varphi (A)\times \varphi (B)$
$\varphi (\forall xA)= \forall {\mathcal T}_{\alpha } = \alpha \wedge \varphi (A[\alpha //x])$
$\varphi (\exists xA)= \exists {\mathcal T}_{\alpha }= \alpha \wedge \varphi (A[\alpha //x]).$
The translation of a formula is complete when there are no more strings of symbols containing
$\varphi $
. For simplicity, in the quantified cases A is assumed to contain x.
Having established the means of correlating the languages, we can now show what the relationship between the systems is:
Lemma 3.43. If
$\Gamma \Rightarrow \Delta $
is derivable in G3Q
$^{A}_{2}$
, then
$\varphi ^{q}_{pc}(\Gamma )\Rightarrow \varphi ^{q}_{pc}(\Delta )$
is derivable in G3c, where
$\varphi ^{q}_{pc}(\Gamma )$
is a multiset of
$\varphi ^{q}_{pc}(A)$
,
$A\in \Gamma $
, and likewise for
$\Delta $
.
Proof. By induction on the height of the derivation. The basic case is straightforward. In the inductive case we inspect the last rule of the derivation. Since the propositional rules are identical, we can omit those cases here and focus on the quantifiers, using the universal quantifier as an illustration. We will mark
$\varphi ^{q}_{pc}(\Gamma )$
as
$\Gamma '$
, and likewise for
$\Delta $
.
(L
$\forall $
) If this is the last rule used, the derivation ends as:
Then, by inductive hypothesis, the following sequent is derivable in G3c:
(i)
$Mt, \varphi (A[t/\forall M]), \forall x (Mx\to \varphi (A[x/\forall M])) , \Gamma ^\prime \Rightarrow \Delta ^\prime $
.
We can then continue the derivation as follows (with (i) the top right sequent):
Here
$\forall x (Mx\to \varphi (A[x/\forall M]))$
is precisely
$\varphi ^{q}_{pc}(A[\forall M])$
(and
$Mt$
is
$\varphi ^{q}_{pc}(tM)$
), as required.
(R
$\forall $
) If this is the last rule used, the derivation ends as:
Then, by inductive hypothesis, the following sequent is derivable in G3c:
(i)
$ Mt, \Gamma ^\prime \Rightarrow \Delta ^\prime , \varphi (A [ t/\forall M]) $
We can then continue the derivation as follows:
Here
$\forall x (Mx\to \varphi (A[x/\forall M]))$
is precisely
$\varphi ^{q}_{pc}(A[\forall M])$
, as required.
The cases for
$\exists $
are parallel, and applying the translation to the rules L
$\forall {\mathcal T}$
, L
$\exists {\mathcal T}$
, R
$\forall {\mathcal T}$
and R
$\exists {\mathcal T}$
simply produces the quantifier rules of G3c. Given that we are dealing with the SNF fragment of Quarc we know by Corollary 2.13 extended to G3Q
$^{A}$
the rules for the reordered predicates and negative predication will not occur. Finally, the rules for anaphora are simple, since
$\varphi ^{q}_{pc}(A[t_{\alpha }])=\varphi ^{q}_{pc}(A[t/t_{\alpha }, t/\alpha _{1},\ldots ,t/\alpha _{n}])$
.□
Lemma 3.44. If
$\Gamma \Rightarrow \Delta $
is derivable in G3c, then
$\varphi ^{pc}_{q}(\Gamma )\Rightarrow \varphi ^{pc}_{q}(\Delta )$
is derivable in G3Q
$^{A}_{2}$
.
Proof. As above by induction on the height of a derivation. This is simple for propositional rules since they are again the same and similar to above for the quantifier rules, so we just illustrate for L
$\forall {\mathcal T}$
.
(L
$\forall $
) If this is the last rule used, the derivation ends as:
Then, we apply the inductive hypothesis and continue the derivation as follows:
□
Moreover, to account for non-derivability we need to prove the following lemma:
Lemma 3.45 (Back-translation).
For any formula A of Quarc
$^{A}$
,
$A \equiv \varphi ^{pc}_{q}\circ \varphi ^{q}_{pc}(A)$
and for any formula B of the Predicate calculus,
$B \equiv \varphi ^{q}_{pc}\circ \varphi ^{pc}_{q}(B)$
.
Proof. By induction on the weight of A and B respectively (the latter is defined in the usual way). Most cases are trivial, so we just illustrate for the case of the universal quantifier. For legibility we write
$\varphi ^{pc}_{q}\circ \varphi ^{q}_{pc}$
as
$\varphi '$
and
$\varphi ^{q}_{pc}\circ \varphi ^{pc}_{q}$
as
$\varphi ''$
.
If A is
$C[\forall M]$
, then
$\varphi '(A)$
is
$\forall {\mathcal T}_{\alpha }=\alpha \wedge (\alpha M \to \varphi ' (C[\alpha /\forall M _{<\alpha>}, \alpha /\alpha _{1},\ldots ,\alpha /\alpha _{n}]))$
. We then have the following derivations:
Left to right:
Right to left:
If B is
$\forall x D$
then
$\varphi ''(B)$
is
$\forall x (x=x \wedge \varphi '' (D))$
and the proof is simple. Similar for
$\exists $
,
$\forall {\mathcal T}$
and
$\exists {\mathcal T}$
.□
These three lemmas combined show that
Theorem 3.46 (Deductive equivalence G3Q
$^{A}_{2}$
and PC).
G3Q
$^{A}_{2}$
and the Predicate calculus are deductively equivalent.
3.4.1 Philosophical import
This theorem explains the existing results, namely that Quarc without instantiation is weaker than the Predicate Calculus, with its strength along the lines of negative free logic [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18], and that there is an image of the Predicate Calculus within Quarc expanded with an abstract predicate [Reference Lanzet11].
The theorem systematizes and refines those results—recalling the schematic representation of the relationships between different systems of Quarc in Figure 5, we can now disregard the B and
$3$
elements to obtain a clearer picture in Figure 6 (which will still contain some redundancies, but these can be left for completeness).
Fig. 6 Relationship of Quarc and PC.
This shows us that extending PC (i.e., G3Q
$_{2}^{A}$
, given Theorem 3.46) with the rule for instantiation (which corresponds to the schema
$\exists x S x$
for any unary predicate S) results in a system at least as strong as Quarc. Likewise, extending Quarc with abstract quantification creates a system at least as strong as PC. In fact, while PC and Quarc are not directly comparable, we are now able to find the least upper bound of the two (as both of these extensions yield the same system), namely the system Quarc
$^{A}$
, introduced in this paper and corresponding to the sequent calculus G3Q
$^{A}$
. Therefore, we are now provided with a uniform picture of the relationship between the two which accounts for, and further expands, all the results on the topic present in the literature on Quarc so far. Moreover, we can also see (by Theorem 3.35) that the expansion of Quarc by the predicate
${\mathcal T}$
that has been considered so far (corresponding to Quarc
$^{{\mathcal T}}$
and sequent calculus G3Q
$^{{\mathcal T}}$
of this paper) potentially obfuscated the issue by being stronger than what is required.
We now turn to investigating some further (philosophically fruitful, it will turn out) properties of the systems we have here formulated.
3.5 Craig interpolation property for G3Q
$^{A}$
and G3Q
$^{{\mathcal T}}$
Given Theorem 3.46, it comes as no surprise that G3Q
$^{A}_{2}$
has the Craig interpolation property [Reference Craig8], but this would require an indirect (twice) route via the SNF and then the Predicate calculus.
Here we instead provide a constructive method of finding the interpolant for both G3Q
$^{A}$
and G3Q
$^{{\mathcal T}}$
, as well as (if one observes the steps for the appropriate rules) their subsystems. Moreover, in this way we are able to construct the interpolant for the full G3Q
$^{A}$
and not just the SNF fragment.
The proof uses some elements of the proof in [Reference Boolos, Burgess and Jeffrey6], but is primarily an adaptation of [Reference Maehara13] method, as found in [Reference Ono16]. After proving that the Craig interpolation property holds for G3Q
$^{A}$
we also extend the result to G3Q
$^{{\mathcal T}}$
. This helps shed some light on the status of the predicate
${\mathcal T}$
(remember that in G3Q
$^{{\mathcal T}}$
it is a predicate).
Definition 3.47 (Craig interpolation property).
A system has the interpolation property when, if
$\Gamma \Rightarrow \Delta $
is derivable, then there is a formula C, called the interpolant, such that
$\Gamma \Rightarrow C$
and
$C\Rightarrow \Delta $
are derivable and
$V(C)\subseteq V(\Gamma )\cap V(\Delta )$
, (where
$V(A)$
is a set of all the non-logical predicates in A), or either
$\Gamma \Rightarrow $
or
$\Rightarrow \Delta $
are derivable.
To prove that G3Q
$^{A}$
has the Interpolation property, we will prove the following lemma:
Lemma 3.48. If
$\Gamma \Rightarrow \Delta $
is derivable in G3Q
$^{A}$
and
$\langle (\Gamma _{1}:\Delta _{1});(\Gamma _{2}:\Delta _{2})\rangle $
is any partition of
$\Gamma , \Delta $
, then there is a formula C such that
$\Gamma _{1}\Rightarrow \Delta _{1}, C$
and
$C, \Gamma _{2}\Rightarrow \Delta _{2}$
, as well as
$V(C)\subseteq V(\Gamma _{1},\Delta _{1})\cap V(\Gamma _{2},\Delta _{2})$
.
Proof. By induction on the height of the derivation. Since this involved proof requires meticulous case checking, it has been deferred to Appendix A.□
We now eliminate the constants
$\top $
and
$\bot $
:
Lemma 3.49. Every interpolant can be reduced to either
$\top $
,
$\bot $
or one that contains no occurrence of either.
Proof. This proof can likewise be found in Appendix A.□
These lemmas immediately show that
Theorem 3.50 (Craig interpolation property G3Q
$^{A}$
).
G3Q
$^{A}$
possesses the Craig interpolation property.
Proof. Applying Lemma 3.48 to the partition
$(\langle \Gamma \!:\rangle ;\langle :\!\Delta \rangle )$
of
$\Gamma \Rightarrow \Delta $
(i.e., taking
$\Gamma _{1}=\Gamma $
,
$\Delta _{1}=\emptyset $
,
$\Gamma _{2}=\emptyset $
and
$\Delta _{2}=\Delta $
) we obtain the interpolant C such that
$\Gamma \Rightarrow C$
and
$C\Rightarrow \Delta $
as well as
$V(C)=V(\Gamma )\cap V(\Delta )$
.
If C contains
$\top $
or
$\bot $
we apply Lemma 3.49. If the interpolant is now
$\top $
then
$\Rightarrow \Delta $
holds, and if it is
$\bot $
then
$\Gamma \Rightarrow $
holds.□
To prove that G3Q
$^{{\mathcal T}}$
has the interpolation property, we prove the following lemma:
Lemma 3.51. If
$\Gamma \Rightarrow \Delta $
is derivable in G3Q
$^{{\mathcal T}}$
and
$\langle (\Gamma _{1}:\Delta _{1});(\Gamma _{2}:\Delta _{2})\rangle $
is any partition of
$\Gamma , \Delta $
, then there is a formula C such that
$\Gamma _{1}\Rightarrow \Delta _{1}, C$
and
$C, \Gamma _{2}\Rightarrow \Delta _{2}$
, as well as
$V(C)\subseteq V(\Gamma _{1},\Delta _{1})\cap V(\Gamma _{2},\Delta _{2})$
.
Proof. Required for the proof is the assumption that
${\mathcal T}$
is a logical predicate. This is plausible since it is easy to demonstrate that in G3Q
$^{{\mathcal T}}$
it holds for any t that
$t=t \Leftrightarrow t{\mathcal T}$
. With this in place, the proof is the same as that of Lemma 3.48, with the new case of the rule
${\mathcal T}$
exactly like that for
$=_{Ref}$
.□
The lemma corresponding to Lemma 3.49 is simplified:
Lemma 3.52. Every interpolant can be reduced to one that contains no occurrences of
$\top $
or
$\bot $
.
Proof. Every occurrence of
$\top $
is replaced by
$(\exists {\mathcal T}){\mathcal T}$
and every occurrence of
$\bot $
by
$\neg (\exists {\mathcal T}){\mathcal T}$
.□
From these it follows that
Theorem 3.53 (Craig interpolation property G3Q
$^{{\mathcal T}}$
).
G3Q
$^{{\mathcal T}}$
possess the Craig interpolation property.
3.5.1 Philosophical import
The addition of the predicate
${\mathcal T}$
, either as a proper predicate or as merely a part of a quantified argument, allows the direct demonstration of the Craig interpolation property (otherwise we are unable to proceed when the partitions share no unary predicates, see Appendix A, e.g., case of R
$\forall $
). As already mentioned, given Theorem 3.46 this is to be expected, but in addition to providing a constructive method of finding the interpolant (an open logical question in its own right) Theorems 3.50 and 3.53 are also philosophically indicative of the status of that predicate, namely that in addition to being abstract, it should be considered a logical predicate.
In this way, the theorems further reveal the distinction in approach between Quarc and PC—Quarc is interested in actual (i.e., natural language) predicates and/or quantification, whereas to match the strength of PC it needs to introduce abstractions of either of those (which is also why the addition of
${\mathcal T}$
to Quarc is not entirely natural, and not part of its regular vocabulary).
4 Complex quantification
So far, every extension to the quantification in Quarc we have done had been of the simple kind, namely binding only a unary predicate. However, in this section, we show that it is possible to elegantly extend this to more complex forms of quantification.
One of the important contributions of Lanzet [Reference Lanzet11] to the research on Quarc is the introduction of defining clauses, which allows it to capture more involved instances of natural language quantification. But the system there is cumbersome in several respects. Given that it quantifies over predicates with defining clauses, which themselves cannot always be expected to be instantiated, it needs to abandon instantiation, and it opts for a three-valued system as a result. Consequently, it contains a multitude of rules to account for different scopes of negation. Moreover, it also contains rules for compound predicates.
However, as Pavlovic and Gratzl [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18] shows, it is possible to treat Quarc without instantiation as a bivalent system, in which case it displays a structural similarity to free logic and therefore meshes easily with the approach of this paper. This makes for a significantly more streamlined sequent calculus, and one which allows a simpler structural analysis (the calculus in [Reference Lanzet11] is not shown to be cut-free) and demonstration of meta-theoretical properties.
The system can be further simplified by omitting the requirement that the quantifiers bind just predicates (which then need to have their own compounding rules). Instead, we allow for quantifiers to bind sentences of a certain kind (note, however, that none of the quantified expressions are sentences in their own right). This allows for a greater variety of clauses one can quantify over, which at the same time require no new rules of their own. In addition, this provides greater modularity, since it does not necessitate abandoning instantiation.
For example, while it is a straightforward matter to translate into Quarc the natural language sentence
Example 4.54. Every person is rich.
One might want to likewise account for the more complicated (though quite common in natural language) sentences of the form [Reference Lanzet11]:
Example 4.55. Every person who owns a private jet is rich.
4.1 Formal language of Quarc
$^{C}$
To obtain this system of quantification we call complex, we first extend the language as follows:
Definition 4.56 (Formula of Quarc
$^{C}$
).
$$\begin{align*} & A::= (t_{1}\ldots t_{n})P^{n} |\ (t_{1}\ldots t_{n})P^{\pi n} |\ (t_{1}\ldots t_{n})\neg P |\ \neg (A) \ |\ (A)\times (A)| \\ & A[t_{\alpha }/t_{1},\alpha /t_{i},\ldots , \alpha /t_{j}]\ |\ A[\forall S/t]\ |\ A[\exists S/t]\ |\ A[\forall s (A)^{*}/t]\ |\ A[\exists s (A)^{*}/t] .\end{align*}$$
where all the previous stipulations hold, and in addition, the formula
$(A)^{*}$
is not a basic formula containing a unary predicate, and it contains precisely one occurrence of the singular argument s.
Moreover,
$A[\forall s (A)^{*}/t]$
and
$ A[\exists s (A)^{*}/t]$
are governed by the quantified clauses (QC)
$\forall s (A)$
and
$\exists s (A)$
, respectively (the parentheses around A can be dropped in the quantified clauses if no ambiguity arises).
Finally, the definition of governance is extended from QAs to quantified expressions, which include both QAs and QCs.
Using this definition, the sentence from Example 4.55 would be formalized as:
Example 4.57.
${\rm (\forall s (s_{\alpha }Person\wedge (\alpha ,\exists PrivateJet )Owns))Rich}$
.
Notice here that, per the requirements of Definition 4.56, ‘
$\exists PrivateJet $
’ is a quantified argument, while ‘
$\forall s (s_{\alpha }Person\wedge (\alpha ,\exists PrivateJet )Owns)$
’ is a quantified clause, and ‘
$s_{\alpha }Person\wedge (\alpha ,\exists PrivateJet )Owns$
’ is a formula which contains only a single occurrence of the singular argument ‘s’.
By comparison, in Lanzet [Reference Lanzet11] the same sentence would be formalized as
Example 4.58.
$(\forall Person_{x}\!:\![(x,\exists PrivateJet )Owns])Rich$
.
While our notation minimally increases the length of the notation, the cost of introducing a new type of quantification is offset by not having to use two types of anaphora (e.g., x in Example 4.58 attaches only to the predicate
$Person$
, not to the argument, and is thus an anaphora of a separate type), and there is the considerable upside of now being able to also formalize sentences such as:
Example 4.59. All those who own private jets are rich.
This would require the predicate
${\mathcal T}$
to be formalized in the previous system, but here comes out as:
Example 4.60.
${\rm (\forall s (s,\exists PrivateJet)Owns)Rich}$
.
Moreover, instead of introducing rules for compound predicates, we can straightforwardly use regular rules of the system for the same purpose. And finally, since quantified clauses do not use unary predicates, the question of whether the latter have instances is separated, resulting in a more modular system.
We now continue the formal presentation of the system by extending the definition of truth for quantification as follows:
Definition 4.61 (Truth-value assignment
${\mathcal V}$
for Quarc
$^{C}$
).
-
9.
${\mathcal V}(A [ \forall sB] )=1$
iff for every t for which
${\mathcal V}(B[t/s])=1$
,
${\mathcal V}(A [ t/\forall sB])=1$
. -
10.
${\mathcal V}(A [ \exists sB] )=1$
iff for some t for which
${\mathcal V}(B[t/s])=1$
,
${\mathcal V}(A [ t/\exists sB])=1$
.
We reflect these definitions in the sequent calculus by adding the complex quantification rules to G3Q (Figure 7).
Fig. 7 G3QC.
4.2 Structural properties
Demonstration of the structural properties of G3QC is a straightforward extension of those results for G3Q. We just need to define the weight of a formula in the appropriate way, namely
Definition 4.62 (Complex formula weight).
$$ \begin{align*} w(A[\forall s B])&= w(A[t/\forall s B])+w(B)+1\\ w(A[\exists s B])&= w(A[t/\exists s B])+w(B)+1.\end{align*} $$
With this addition, proofs of all the structural properties follow immediately:
Theorem 4.63 (Structural properties G3QC).
Axiom generalization holds for G3QC, substitution, weakening, invertibility of rules, and contraction hold height-preserving for G3QC, and cut is admissible.
Proof. The proofs for all of these extend those for G3Q. The only new case in each proof is the one for complex quantification. Axiom generalization, substitution and weakening are exactly alike the case for G3Q while invertibility and contraction are guaranteed by the form of the new rules in the usual way [Reference Negri and von Plato15]. For cut the new case to check is when the cut formula is a complex quantification and principal in both premises of cut:
This is transformed into:
(1)
where Cut
$_1$
and Cut
$_2$
are of lower height, while Cut
$_3$
and Cut
$_4$
are of lower weight. Similar for
$\exists c$
.□
4.3 Meta-theoretical properties
As with the structural properties, the proofs of meta-theoretical properties of G3QC easily extend the corresponding ones for G3Q.
Theorem 4.64 (Soundness G3QC).
If
$\Gamma \Rightarrow \Delta $
is derivable in G3QC, then
$\Gamma \Rightarrow \Delta $
is valid under Definition 4.61.
Proof. The proof extends the proof of Theorem 2.20 with the new cases.
If last step of the derivation is obtained by L
$\forall c$
then it has the form
Assume
$ A[\forall s B]$
and all the formulas in
$\Gamma $
are valid. Then by the inductive hypothesis either (i) some formula in
$\Delta $
is valid, or (ii)
$B[t/s]$
is. In the first case we are done and otherwise since
$B[t/s]$
and
$A[\forall s B]$
are valid, by Definition 4.61 so is
$A[t/\forall s B] $
, therefore all of
$A[t/\forall s B]$
,
$A[\forall s B]$
,
$\Gamma $
are valid, and by the inductive hypothesis so is some formula in
$\Delta .$
If the last step of the derivation is obtained by R
$\forall c$
, then it has the form
Assume all of the formulas in
$\Gamma $
are valid, but neither
$A[\forall s B]$
nor any formula in
$\Delta $
are. Then by Definition 4.61 there is some t (let it just be t) such that
$B[t/s]$
is valid but
$A[t/\forall s B]$
is not. Since
$B[t/s]$
and all of
$\Gamma $
are valid, by the inductive hypothesis so is either some formula in
$\Delta $
, or
$A[t/\forall s B]$
. Contradiction either way.
Parallel, respectively, for R
$\exists c$
and L
$\exists c$
.□
Theorem 4.65 (Completeness G3QC).
If
$\Gamma \Rightarrow \Delta $
is valid under Definition 4.61 then it is derivable in G3QC.
Proof. We first extend the definition of the reduction tree with the clauses for the new rules:
(21) L
$\forall c$
, for every singular argument t in
$\Gamma _{i}\cup \Delta _{i}$
.
(22) R
$\forall c$
, taking for the reduction of each formula
$A[\forall s B]$
in
$\Delta _{i}$
from the denumerable list of singular arguments the first such argument t not yet used in the reduction tree.
(23) L
$\exists c$
, treated symmetrically to R
$\forall c$
(24) R
$\exists c$
, treated symmetrically to L
$\forall c$
.
We then show that the refutation valuation
${\mathcal C}$
assigns the correct values to the new formulas.
(
$\forall s$
) If A is a formula
$C[\forall s D]$
, then by stage (21), for every singular argument t, either
$D[t/s]$
is in
$\Delta ^{*}$
(and by inductive hypothesis
$0$
) or
$C[t/\forall s D]$
is in
$\Gamma ^{*}$
(and by inductive hypothesis
$1$
). So for every t it holds that if
$D[t/s]$
, then
$C[t/\forall s D]$
and therefore
$C[\forall s D]$
is assigned
$1$
.
If B is a formula
$C[\forall s D]$
, then by stage (22), for some singular argument t,
$D[t/s]$
is in
$\Gamma ^{*}$
(and by inductive hypothesis
$1$
) and
$C[t/\forall s D]$
is in
$\Delta ^{*}$
(and by inductive hypothesis
$0$
), and so
$C[\forall s D]$
is
$0$
.
Similar for
$\exists s$
.□
5 Concluding remarks
The primary goal of this paper was to definitively answer the question of mutual relation of the Quantified argument calculus and the Predicate calculus. To achieve this, we have noted that previous additions of the predicate
${\mathcal T}$
to simulate the role of the domain have been too strong, and that all that is required is for that predicate to appear in the titular quantified arguments of Quarc. Finding a form of sentences that allows us to put some special linguistic features of Quarc aside has enabled us to show that the result of such a weaker addition to a subsystem of Quarc is deductively equivalent to PC. Given that
${\mathcal T}$
is an abstract predicate entirely devoid of meaning, and also (since this assumption enables the demonstration of Craig interpolation property, which by the equivalence is expected to hold) a logical one, we can better understand the distinction between Quarc and PC in their respective approaches to quantification. Namely, the quantification of PC can be seen as an abstraction of that of Quarc.
Moreover, it has been argued to some extent [Reference Ben-Yami2, Reference Ben-Yami3] that Quarc better captures the quantification of natural language. While we do not consider this matter settled, we find it prima facie plausible enough to conclude that the results here also shine some light on the relation of quantification of PC to that of natural language—namely, that the former is an abstraction of the latter.
Following the thread of thought of the main result has also enabled us to elegantly incorporate defining clauses into the proof-theoretic framework of Quarc while keeping it bivalent. Of course, there is significant literature [Reference Ben-Yami4, Reference Lanzet11] that suggests it should be trivalent, and in any case it seems that the original intention in the formulation in [Reference Ben-Yami2] was to have it trivalent when the predicate in the quantified argument has no instances. It remains a task for the future to adapt the proof-theoretic framework developed here to that approach while maintaining all the desirable properties of a good proof system.
A Craig interpolation property
Lemma 3.48. If
$\Gamma \Rightarrow \Delta $
is derivable in G3Q
$^{A}$
and
$\langle (\Gamma _{1}:\Delta _{1});(\Gamma _{2}:\Delta _{2})\rangle $
is any partition of
$\Gamma , \Delta $
, then there is a formula C such that
$\Gamma _{1}\Rightarrow \Delta _{1}, C$
and
$C, \Gamma _{2}\Rightarrow \Delta _{2}$
, as well as
$V(C)\subseteq V(\Gamma _{1},\Delta _{1})\cap V(\Gamma _{2},\Delta _{2})$
(where
$V(A)$
is a set of all the non-logical predicate variables in A).
Proof. By induction on the height of the derivation.□
1.1 Basic step
If
$\Gamma \Rightarrow \Delta $
is an initial sequent, the partitions to be considered are
$\langle (\Gamma _{1}, p:\Delta _{1}, p);(\Gamma _{2}:\Delta _{2})\rangle $
, with the interpolant
$\bot $
,
$\langle (\Gamma _{1}:\Delta _{1});(\Gamma _{2},p:\Delta _{2},p)\rangle $
with the interpolant
$\top $
,
$\langle (\Gamma _{1},p:\Delta _{1});(\Gamma _{2}:\Delta _{2},p)\rangle $
with the interpolant p, and
$\langle (\Gamma _{1}:\Delta _{1},p);(\Gamma _{2},p:\Delta _{2})\rangle $
with the interpolant
$\neg p$
.
1.2 Inductive step
In proceeding to the inductive step we consider the last step of the derivation.
(L∀) The partitions to be considered are
-
1.
$\langle (tM, A[\forall M], \Gamma _{1}:\Delta _{1});(\Gamma _{2}:\Delta _{2})\rangle $
By the inductive hypothesis, there is a C such that-
(i)
$tM, A[\forall M], A[t/\forall M], \Gamma _{1}\Rightarrow \Delta _{1},C$
, -
(ii)
$C,\Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(iii)
$V(C)\subseteq V(tM, A[\forall M], A[t/\forall M], \Gamma _{1}, \Delta _{1})\cap V(\Gamma _{2}, \Delta _{2})$
Applying L
$\forall $
to (i), we get C as the interpolant, since
$V(tM, A[\forall M], A[t/\forall M], \Gamma _{1}, \Delta _{1}) = V(tM, A[\forall M], \Gamma _{1}, \Delta _{1})$
-
-
2.
$\langle (\Gamma _{1}:\Delta _{1});(tM, A[\forall M], \Gamma _{2}:\Delta _{2})\rangle $
Parallel to the previous case. -
3.
$\langle (tM,\Gamma _{1}:\Delta _{1});( A[\forall M], \Gamma _{2}:\Delta _{2})\rangle $
By the inductive hypothesis, there is a C such that-
(i)
$tM, \Gamma _{1}\Rightarrow \Delta _{1},C$
, -
(ii)
$C,A[\forall M], A[t/\forall M],\Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(iii)
$V(C)\subseteq V(tM, \Gamma _{1}, \Delta _{1})\cap V(A[\forall M], A[t/\forall M],\Gamma _{2}, \Delta _{2})$
The interpolant is
$tM\wedge C$
, sinceandMoreover,
$V(A[\forall M],\Gamma _{2}, \Delta _{2})= V(A[\forall M], A[t/\forall M],\Gamma _{2}, \Delta _{2})$
and
$M\in V(tM, \Gamma _{1}, \Delta _{1})\cap V(A[\forall M],\Gamma _{2}, \Delta _{2})$
. -
-
4.
$\langle (A[\forall M],\Gamma _{1}:\Delta _{1});( tM,\Gamma _{2}:\Delta _{2})\rangle $
Parallel to the previous case, with the interpolant
$tM\to C$
.
(R∀) The partitions to be considered are
-
1.
$\langle (\Gamma _{1}:\Delta _{1},A[\forall M]);( \Gamma _{2}:\Delta _{2})\rangle $
By the inductive hypothesis, there is a C such that-
(i)
$tM,\Gamma _{1}\Rightarrow \Delta _{1},A[t/\forall M], C$
, -
(ii)
$C,\Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(iii)
$V(C)\subseteq V( \Gamma _{1}, \Delta _{1})\cap V(tM, \Gamma _{2}, \Delta _{2},A[t/\forall M])$
If C does not contain t, applying R
$\forall $
to (i) we get C as the interpolant, since
$V(tM, \Gamma _{2}, \Delta _{2},A[t/\forall M])=V( \Gamma _{2}, \Delta _{2},A[\forall M])$
.If C contains t, then it must contain some n-ary predicate
$R^{n}$
. The interpolant is then
$((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n})R^{n}\vee \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\wedge C[\beta /t]$
, sinceandMoreover
$V(\Gamma _{2}, \Delta _{2},A[\forall M])=V(tM, \Gamma _{2}, \Delta _{2},A[t/\forall M])$
and
$V(((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n}) R^{n}\vee \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\wedge C[\beta /t])=V(C)$
, since
${\mathcal T}$
is not considered a predicate in G3Q
$^{A}$
. -
-
2.
$\langle (\Gamma _{1}:\Delta _{1});( \Gamma _{2}:\Delta _{2},A[\forall M])\rangle $
Parallel to the previous case, with the interpolant
$((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n})R^{n}\wedge \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\vee C[\beta /t]$
.
(R∃) Parallels L
$\forall $
. The partitions to be considered are
-
1.
$\langle (tM, \Gamma _{1}:\Delta _{1}, A[\exists M]);(\Gamma _{2}:\Delta _{2})\rangle $
, with the interpolant C, -
2.
$\langle ( \Gamma _{1}:\Delta _{1});(tM,\Gamma _{2}:\Delta _{2}, A[\exists M])\rangle $
, with the interpolant C, -
3.
$\langle (tM, \Gamma _{1}:\Delta _{1});(\Gamma _{2}:\Delta _{2}, A[\exists M])\rangle $
, with the interpolant
$tM\wedge C$
, -
4.
$\langle ( \Gamma _{1}:\Delta _{1}, A[\exists M]);(tM,\Gamma _{2}:\Delta _{2})\rangle $
, with the interpolant
$tM\to C$
.
(L∃) Parallels R
$\forall $
. The partitions to be considered are
-
1.
$\langle (A[\exists M]), \Gamma _{1}:\Delta _{1};(\Gamma _{2}:\Delta _{2})\rangle $
, with the interpolant
$((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n})R^{n}\vee \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\wedge C[\beta /t]$
(or C if it contains no t), -
2.
$\langle ( \Gamma _{1}:\Delta _{1});(A[\exists M],\Gamma _{2}:\Delta _{2})\rangle $
, with the interpolant
$((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n})R^{n}\wedge \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\vee C[\beta /t]$
(or C if it contains no t).
$(\mathrm{L} \forall {\mathcal T}, \mathrm{R} \forall {\mathcal T}, \mathrm{L} \exists {\mathcal T}, \mathrm{R} \exists {\mathcal T})$
Parallel exactly the rules L
$\forall $
, R
$\forall $
, L
$\exists $
and R
$\exists $
.
(Special rules) With the rules RA, LA, L
$NP$
, R
$NP$
, L
$Rd$
and R
$Rd$
the procedure is straightforward, and the interpolant always C, noting that the reordered predicates are treated as operations on predicates, and therefore
$R^{n}\in V(A)$
iff
$R\in V(A)$
.
(Ins) Only one type of partition needs to be considered here. By the inductive hypothesis, there is a C such that
-
(i)
$tM, \Gamma _{1}\Rightarrow \Delta _{1}, C$
, -
(ii)
$C, \Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(iii)
$V(C)\subseteq V(tM,\Gamma _{1},\Delta _{1})\cap V(\Gamma _{2},\Delta _{2})$
.If
$M\notin V(C)$
, we distinguish two cases. If C does not contain t, applying
$Ins$
to (i) we get C as the interpolant. Otherwise, if C contains t, it contains some predicate
$R^{n}$
, and the interpolant is
$((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n})R^{n}\vee \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\wedge C[\beta /t]$
.If
$M\in V(C)$
, the interpolant is the same as in the two cases above if
$M\in V(\Gamma _{1},\Delta _{1})$
. Otherwise, by the inductive hypothesis, there is a D such that -
(iv)
$ \Gamma _{1}\Rightarrow \Delta _{1}, D$
, -
(v)
$D, tM,\Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(vi)
$V(D)\subseteq V(\Gamma _{1},\Delta _{1})\cap V(tM,\Gamma _{2},\Delta _{2})$
.
Since
$M\notin V(\Gamma _{1},\Delta _{1})$
, we know that
$M\notin V(D)$
. If D doesn’t contain t we get that D is the interpolant by applying
$Ins$
to (v), and otherwise D contains some predicate
$R^{n}$
, and the interpolant is
$((\exists {\mathcal T}_{\beta },\ldots ,\beta _{n})R^{n}\vee \neg (\beta _{1},\ldots ,\beta _{n}) R^{n})\wedge D[\beta /t]$
.
$(=_{\textbf {\textit {Ref}}})$
Only one type of partition needs to be considered here. By the inductive hypothesis, there is a C such that
-
(i)
$t=t, \Gamma _{1}\Rightarrow \Delta _{1}, C$
, -
(ii)
$C, \Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(iii)
$V(C)\subseteq V(t=t, \Gamma _{1}, \Delta _{1}) \cap V(\Gamma _{2}, \Delta _{2})$
Applying
$=_{Ref}$
to (i), we get C as the interpolant, since
$=$
is a logical predicate, so
$V(t=t, \Gamma _{1}, \Delta _{1})=V(\Gamma _{1}, \Delta _{1})$
, and therefore
$V(C)\subseteq V(\Gamma _{1}, \Delta _{1}) \cap V(\Gamma _{2}, \Delta _{2})$
.
$(=_{\textbf {\textit {Repl}}})$
The partitions to be considered here are
-
1.
$\langle (t=s, A[ t/s], \Gamma _{1}:\Delta _{1});(\Gamma _{2}:\Delta _{2} )\rangle $
, with the interpolant C, -
2.
$\langle (\Gamma _{1}:\Delta _{1});(t=s, A[ t/s], \Gamma _{2}:\Delta _{2} )\rangle $
, with the interpolant C, -
3.
$\langle (A[ t/s], \Gamma _{1}:\Delta _{1});(t=s, \Gamma _{2}:\Delta _{2} )\rangle $
By the inductive hypothesis, there is a C such that-
(i)
$A[ s], A[ t/s], \Gamma _{1}\Rightarrow \Delta _{1}, C$
, -
(ii)
$C, t=s, \Gamma _{2}\Rightarrow \Delta _{2}$
, and -
(iii)
$V(C)\subseteq V(A[ s], A[ t/s], \Gamma _{1}, \Delta _{1}) \cap V(t=s, \Gamma _{2}, \Delta _{2})$
The interpolant is
$C\vee \neg t=s$
, sinceandMoreover,
$V(A[ s] )=V(A[ t/s] )$
, so
$V(A[ s], A[ t/s], \Gamma _{1}, \Delta _{1})=V(A[ t/s], \Gamma _{1}, \Delta _{1})$
. Since identity is a logical predicate, it follows that
$V(t=s, \Gamma _{2}, \Delta _{2})=V(\Gamma _{2}, \Delta _{2})$
. Therefore,
$V(C)\subseteq V(A[ t/s], \Gamma _{1}, \Delta _{1}) \cap V(\Gamma _{2}, \Delta _{2})$
-
-
4.
$\langle (t=s, \Gamma _{1}:\Delta _{1});(A[ t/s], \Gamma _{2}:\Delta _{2} )\rangle $
, with the interpolant
$C\wedge t=s$
(similar to the previous case).
Lemma 3.49. Every interpolant can be reduced to either
$\top $
,
$\bot $
or one that contains no occurrence of either.
Proof. If
$V(C)\neq \emptyset $
(for any interpolant C), then it contains some n-ary predicate
$R^{n}$
, and each occurrence of
$\top $
and
$\bot $
can be replaced by
$(\exists {\mathcal T}_{\alpha },\ldots ,\alpha _{n})R^{n}\vee \neg (\alpha _{1},\ldots ,\alpha _{n}) R^{n}$
and
$(\exists {\mathcal T}_{\alpha },\ldots ,\alpha _{n})R^{n}\wedge \neg (\alpha _{1},\ldots ,\alpha _{n}) R^{n}$
, respectively.
Otherwise C contains no quantification. We then remove all anaphoric expressions by replacing any anaphora with its source and then apply the following transformations:
-
1.
$\top \rightarrow A \equiv A$
;
$\bot \rightarrow A \equiv \top $
;
$A \rightarrow \top \equiv \top $
;
$A \rightarrow \bot \equiv \neg A$
-
2.
$\top \wedge A\equiv A$
;
$\bot \wedge A\equiv \bot $
-
3.
$\top \vee A \equiv \top $
;
$\bot \vee A\equiv A$
-
4.
$\neg \top \equiv \bot $
;
$\neg \bot \equiv \top $
It is clear by induction on the weight of the formula C that the result will be either
$\top $
,
$\bot $
, or contain no occurrences of either.□
Acknowledgments
This paper was written with support of the Academy of Finland research project no. 1308664. This paper was written with support of the Deutsche Forschungsgemeinschaft (DFG) research project no. 390218268.
