1 The quantified argument calculus

The quantified argument calculus, or Quarc for short, is a system of first-order quantified logic, specific for utilization of quantified arguments, whereby quantifiers are bound by monadic predicates, in the argument position of predicates. In its current form it was first suggested by Ben-Yami [Reference Ben-Yami2]. It has been argued [Reference Ben-Yami1, Reference Ben-Yami4] that this syntactical restriction of quantification makes Quarc more similar to natural languages compared to the standard predicate calculus (PC).

As to their precise relation, it has been shown in [Reference Lanzet10] that an extended version of Quarc (enriched with a special predicate and adapted to a strong Kleene three-valued system) is at least as strong as PC. Conversely, PC extended with the principle of instantiation, which states unary predicates have instances and in effect precludes trivial truth of universal sentences (another feature, this time semantic, that has been argued makes Quarc more alike natural languages), was shown in [Reference Raab22] to be at least as strong as Quarc. Finally, in [Reference Pavlović and Gratzl21] a system of Quarc equivalent to PC was identified. It obviously contains no instantiation, and moreover includes a new, abstract, mode of quantification to account for the unrestricted quantification in PC. From this result, and given Quarc’s purported similarity to natural languages, that paper argues that PC utilizes an abstraction of natural language quantification.

Therefore, the debate so far places Quarc somewhere in between the abstract approach of PC and the ground-level of natural languages. While somewhat closer to the former, Quarc of course still contains considerable regimentation [Reference Ben-Yami2] and is closely related to other logical systems, notably free logic [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18]. In fact, it was the developments in proof theory of free logic [Reference Pavlović and Gratzl20] that motivated further developments in [Reference Pavlović and Gratzl21]. Moreover, Quarc has been shown to contain the fundamental properties of a good logic system, such as soundness in [Reference Ben-Yami2, Reference Pavlović and Gratzl21] and completeness in [Reference Pavlović17, Reference Pavlović and Gratzl21].

Another fundamental (but nonetheless less frequently attained) property of a logical system is decidability. This question has recently been raised for Quarc in [Reference Pascucci16], and the present paper offers several answers. Of course, it has been known for a very long time that the PC is undecidable [Reference Church6, Reference Church7, Reference Turing24], but given that the results so far show a complex relationship between PC and Quarc (features are both added and subtracted) they do not offer indications as to which fragments of Quarc are decidable. The goal of this paper is to use proof-theoretic methods to instead directly identify several subsystems of Quarc for which decidability can be demonstrated. The upside of using proof theory is that the end result will also provide us with an algorithm for finding proofs, although we will not here dwell much on the matters of their computational efficiency (on the face of it, it does not appear to be particularly high, and if so, optimization is left for future research).

A significant portion of the investigations into the logical properties of Quarc done so far has been proof-theoretic, specifically by utilizing sequent calculi in the style of [Reference Negri and von Plato15]—in addition to the already mentioned [Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18, Reference Pavlović and Gratzl21], they were also used in [Reference Pavlović and Gratzl19], and likewise constitute the bulk of research in [Reference Pavlović17]. In this paper we rely on those results, especially [Reference Pavlović and Gratzl21], to a considerable extent.

For the purpose of streamlining expressivity Quarc adopts several further devices akin to those used in natural languages, like the reordered predicates (corresponding to, among others, the passive constructions), different modes of predication (the one used in this paper will be that of negative predication), as well as anaphora. The first two were shown in [Reference Pavlović and Gratzl21] to be inessential in the presence of the last one, but due to modularity we retain them for simpler expressivity.

We find it to be a significant upside that we are able to retain many features of Quarc. In fact, the entire vocabulary is kept, with the modification in the first attempt happening only with respect to quantification, disallowing quantifier embedding. This is especially important when discussing the applicability of Quarc, where the straightforward connection of its expressive devices to their natural language counterparts is an additional bonus. Of course, losing quantifier embedding altogether significantly reduces the expressivity of our language, so subsequently we bring it back in a controlled manner, while making sure to steer clear of undecidability-generating combinations. This version is more involved, but the same result is obtained, and then extended to more complex forms of quantification first formally explored in [Reference Lanzet10], but in this version based on a later treatment as in [Reference Pavlović and Gratzl21].

Quarc has already seen a fair number of applications, both logical like in the aforementioned [Reference Lanzet10, Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18, Reference Pavlović and Gratzl21, Reference Raab22], as well as philosophical, starting with its first introduction in [Reference Ben-Yami1]. Since then it has been used to investigate necessary existence and the Barcan formulas [Reference Ben-Yami4], natural logic [Reference Ben-Yami3], as well as Aristotle’s syllogistic [Reference Pavlović17, Reference Raab23]. To demonstrate the utility of the present approach beyond, and in addition to, its pure logical interest, we will also refine and then extend the results of the last two papers to show that the system presented here allows for the proof of decidability of Aristotle’s assertoric syllogistic.

Plan of the paper: In the remainder of this introduction we lay out the language of Quarc and then proceed to briefly present the background sequent calculus and recollect that it contains the standard structural properties, including height-preserving admissibility of contraction and admissibility of cut. These are presented without proof and the reader is referred to previous literature on Quarc should they wish to check the details (they are in any case fairly routine). However, we dedicate slightly more space to subformula property, since it plays an important role in the main argument of the paper.

We then move to the first of two central sections of the paper, in which we present a decidable fragment of Quarc, where all of the vocabulary of regular Quarc, as well as the rules, have been retained, but quantification has been restricted to what we label single-stack (not permitting quantifier embedding). This system is then shown to be decidable, as well as sound and complete with respect to the appropriate Quarc semantics, and the results then extended to its subsystems.

We next take a brief detour and show that Aristotle’s assertoric syllogistic is contained within (a subsystem of) this new version of Quarc, and thus that our central result reasserts that it is likewise decidable.

We then fully develop the single-stack system into what we label single-type quantification, where within the scope of universal quantification only universal (or, equivalently, negated particular) quantification is found, and analogously for particular. The decidability result for this system is likewise obtained, and then expanded to complex quantification (which only makes sense in the presence of embedded quantification). Finally, we highlight questions not answered in the present work and lay out further avenues of research in the concluding remarks.

1.1 Language of Quarc

We begin this preliminary exposition by presenting the vocabulary of Quarc. While in the later sections Quarc will be modified, for our present purposes this part will remain unaltered throughout the paper.

Definition 1.1 (Vocabulary of Quarc).

The vocabulary of Quarc consists of countable non-empty sets of:

1. (i) Singular arguments (SA): $a,b,c,\ldots $ .

2. (ii) Predicates: $P,Q,R,\ldots $ , each with fixed arity n indicated as $P^n$ .

Countable sets of:

1. (iii) Anaphors: $\alpha ,\beta ,\gamma ,\ldots $ .

2. (iv) Reordered n-ary predicates: $P^{\pi n},Q^{\pi n},R^{\pi n},\ldots $ , where $2\leq n$ .

As well as logical symbols:

1. (v) Connectives: $\neg , \wedge , \vee , \to $ .

2. (vi) Quantifiers: $\forall , \exists $ .

And finally auxiliary symbols:

1. (vii) Parentheses: (, ).

In the following t indicates a singular argument, $\pi n$ a permutation of n excluding identity-permutation, P without superscript a predicate or a reordered predicate of arity n, and M a unary predicate. Moreover $A[a]$ indicates the formula A which contains an occurrence of the argument a, the list $t_{1}\ldots t_{j}$ indicates j occurrences, left to right, of the singular argument t and $A[b/c]$ indicates the result of the substitution of an instance of an argument c by an argument (with subscript if indicated) or anaphor b in formula A. The language of Quarc, due to [Reference Ben-Yami2], then consists of the set of formulas given by the following BNF over the vocabulary in Definition 1.1.

Definition 1.2 (Formula of Quarc).

$$ \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)\circ (A)^{*}|\ \\ &A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}]^{**}\ |\ A[\mu M/t]^{***}, \end{align*} $$

where formulas of the form $(t_{1}\ldots t_{n})P^{n}$ are called basic, with parentheses omitted whenever possible and arity omitted when clear from context, $\circ \in \{\wedge , \vee , \to \}$ , $\mu \in \{\forall , \exists \}$ , subscript $\alpha $ is called the source of the anaphor and not considered part of the argument [Reference Ben-Yami2, p. 128], and moreover:

$^{*}$ 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[\mu M/t]$ is governed (definition below) by the displayed occurrence of the quantified argument (QA) $\mu M$ .

In the rest of the paper we will use $p,q,\ldots $ to indicate basic formulas. Note that since subscript $\alpha $ is not considered part of the argument, the substituting quantified argument $\mu M$ will be the source of the same anaphors as the substituted singular argument t.

Definition 1.3 (Governance).

An occurrence $ \mu M $ of a QA governs a formula A just in case $\mu M$ 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 $\mu M$ and all the anaphors of all the QAs in B.

The definition of governance will be familiar to those used to Quarc and probably arcane at first glance to those new to it, but we present it here in full since we will vary it somewhat in the rest of the paper.

With the formula of Quarc defined, its weight $\mathtt {w}$ is then the following.

Definition 1.4 (Weight of a formula, $\mathtt {w}$ ).

$$ \begin{align*} \begin{array}{lr} \displaystyle\mathtt{w}((t_{1}\ldots t_{n})P^{n})=0, &\displaystyle\mathtt{w}(A\circ B)=\mathtt{w}(A)+\mathtt{w}(B)+1,\\ \displaystyle\mathtt{w}((t_{1}\ldots t_{n})P^{\pi n})=1, &\displaystyle\mathtt{w}(A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}])=\\ \displaystyle\mathtt{w}((t_{1}\ldots t_{n})\neg P)=\mathtt{w}((t_{1}\ldots t_{n}) P)+1,\qquad &\hfill \displaystyle\mathtt{w}(A[t_1,\ldots,t_j])+1,\\ \displaystyle\mathtt{w}(\neg A)=\mathtt{w}(A)+1, &\displaystyle\mathtt{w}(A[\mu M/t])=\mathtt{w}(A[t])+1. \end{array} \end{align*} $$

1.2 Proof theory of Quarc

A handy summary of all the significant proof-theoretic properties of Quarc is provided in [Reference Pavlović and Gratzl21], and there the starting sequent calculus for this paper is likewise presented, namely G3Q (recapped in Figure 1).

Figure 1 G3Q.

All rules consist of one sequent, written below the inference line, which is its conclusion, and one or more sequents above the line called its premises. All the displayed formulas (i.e., except those in $\Gamma $ and $\Delta $ ) are called active formulas of the rule if they occur in the premise(s) and principal if they occur in the conclusion of the rule. $\Gamma $ and $\Delta $ are called the context of the rule. A branch is a series of sequents (finite or infinite), starting with the endsequent, in which every element is a conclusion of a rule of which the following element is a premise. The height of a derivation is the length (number of consecutive applications of derivation rules) of its longest branch. We use ‘ $\vdash _n\!$ ’ to indicate derivability with height at most n.

The reader is directed to [Reference Pavlović and Gratzl21] for details (the proofs of relevant properties are in any case for the most part standard proof-theoretic fare), but here we just remind them of the following.

Observation 1.5. All the standard structural properties, namely height-preserving (hp) substitution, axiom generalization, hp-admissibility of weakening, hp-invertibility of all the rules, hp-admissibility of contraction and admissibility of cut, hold for G3Q.

As has been shown in [Reference Pavlović and Gratzl21], in the presence of anaphora this system is equivalent to one not containing reorder or negative predication, but as already mentioned we leave them here since they do not cause any issues going forward but make comparison with other systems of Quarc more legible.

2 A decidable fragment of Quarc

In the proof of completeness of G3Q (and thus Quarc) in [Reference Pavlović and Gratzl21], an algorithmic method of finding any valid derivation is presented—we start with the desired endsequent and work our way up, applying the rules bottom-up until we have reached an initial sequent along every branch. And since all derivations are finite, the whole procedure will take only a finite amount of steps. This does not, however, imply that the converse procedure, of finding a countermodel, will likewise terminate (and thus that we have an effective decision procedure).

Example 2.1. As an illustration, consider the following proof-search procedure for a sequent $aM\Rightarrow (\exists M,\forall M)R$ (in any system with instantiationFootnote ¹ the antecedent could also be empty):

Clearly, the proof search will continue indefinitely, as substitution instances of $(a,\forall M)R$ will occur along the branch, each triggering a generation of a fresh singular argument which then generates a new instance of the formula. Therefore, the countermodel generated will likewise be infinite.

To prevent this we restrict quantification and then show that in the resulting system we can define a procedure, taken from [Reference Negri11], that prunes the infinite branches of the proof search to finite length, in a syntactic counterpart of semantic filtration. This procedure has recently seen extensive use to obtain decidability results for a wide range of different logics (e.g., [Reference Girlando, Negri, Olivetti and Risch9, Reference Negri and Olivetti12–Reference Negri and Sbardolini14]).

We start by presenting a significantly restricted version of Quarc before again expanding it in Section 4. In this paper we continue the convention from [Reference Pavlović and Gratzl19, Reference Pavlović and Gratzl21] of indicating a limitation of the system via subscript and its extension with a superscript. Let Quarc $_{1}$ have the same vocabulary as Quarc in Definition 1.1 and consist of the set of formulas given by the following BNF:

Definition 2.2 (Formula of Quarc $_1$ ).

$$ \begin{align*} \begin{array}{ll} \displaystyle A::= &(t_1,\ldots,t_n)P^{n} |\ (t_{\pi 1},\ldots,t_{\pi n})P^{\pi n} |\ (t_1,\ldots,t_n)\neg P\ |\ \neg (A)^* \ |\ (A)\circ (A)^*|\ \\ &|\ A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}]^{**}\ |\ A[\mu M/t]^{***}, \end{array} \end{align*} $$

where $=\ \in P^2$ , $\circ \in \{\wedge , \vee , \to \}$ , and $\mu \in \{\forall , \exists \}$ and all the previous stipulations apply, except that:

$^{***}$ where A: (1) contains no quantified argument $\mu S$ , and (2) $A[\mu M/t]$ is governed by the displayed occurrence of the quantified argument $\mu M$ . This condition replaces the condition $(*\!*\!*)$ from Definition 1.2.

We here retain the standard definition of governance [Reference Ben-Yami2] from Definition 1.3 and simply add the condition (1), making the language a special case of that in Definition 1.2. So, all the quantified sentences of Quarc $_1$ are also sentences of Quarc and therefore Quarc $_1$ is a fragment of full Quarc in which quantified arguments govern only formulas where no other quantifiers occur. We label this type of quantification single-stack.

The calculus G3Q $_1$ is likewise obtained from G3Q by limiting the rules to the language of Quarc $_1$ —in effect, to $A[t/\mu M]$ not containing quantified arguments. Note that this simply means that the quantifier rules are now limited to single-stack quantification.

It is easy to see these rules would be admissible in G3Q. Specifically, in each case the quantified argument will govern the principal formula, so each of these is an instance of the corresponding rule in G3Q. Therefore, G3Q $_1$ is, like its Quarc $_1$ counterpart, a subsystem of G3Q. In fact, it is obvious that G3Q is a conservative extension of G3Q $_1$ (modulo single-stack quantification).

2.1 Structural properties

The structural properties of G3Q $_1$ will be of use going forward so they should be demonstrated. However, their proofs follow the (standard in the vein of [Reference Negri and von Plato15]) presentation of the same properties for G3Q in [Reference Pavlović and Gratzl21], so they will be presented only schematically here, focusing on the new cases.

Lemma 2.3 (Axiom generalization).

For any formula A, the sequent $A,\Gamma \Rightarrow \Delta , A$ is derivable.

Proof. By induction on the weight of formula A.

Basic case. If A is basic, then $A,\Gamma \Rightarrow \Delta , A$ is an initial sequent.

Inductive case. Straightforward, and we illustrate on the example of $\forall $ :

It should be obvious that in any other case this will likewise be an application of a right rule followed by a left one (or vice versa), and then the inductive hypothesis.

Lemma 2.4 (Substitution).

If $\vdash _{n}\Gamma \Rightarrow \Delta $ holds in G3Q $_{1}$ , then it likewise holds that $\vdash _{n}\Gamma [s/t] \Rightarrow \Delta [s/t]$ .

Proof. Routine by induction on the height of the derivation, simplified from the corresponding proof in [Reference Pavlović and Gratzl21].

Lemma 2.5 (Weakening).

Weakening is height-preserving admissible in G3Q $_{1}$ , namely if $\vdash _{n}\Gamma \Rightarrow \Delta $ holds in G3Q $_1$ , then for any A likewise $\vdash _{n}A, \Gamma \Rightarrow \Delta $ and $\vdash _{n}\Gamma \Rightarrow \Delta , A$ hold.

Proof. Routine by induction on the height of the derivation.

Lemma 2.6 (Rule invertibility).

All the rules of G3Q $_1$ are height-preserving invertible, namely if for a conclusion of the rule $\vdash _{n} \Gamma \Rightarrow \Delta $ holds, then for its premise(s) $\vdash _{n} \Gamma ^\prime \Rightarrow \Delta ^\prime $ (and possibly $\vdash _{n} \Gamma ^{\prime \prime } \Rightarrow \Delta ^{\prime \prime }$ ) likewise hold.

Proof. Routine by induction on the height of the derivation for each of the cases.

Lemma 2.7 (Contraction).

Contraction is height-preserving admissible in G3Q $_{1}$ , namely if $\vdash _{n}A, A, \Gamma \Rightarrow \Delta $ holds then $\vdash _{n}A, \Gamma \Rightarrow \Delta $ likewise holds, and similarly if $\vdash _{n} \Gamma \Rightarrow \Delta , A, A$ then $\vdash _{n} \Gamma \Rightarrow \Delta , A$ .

Proof. Routine by simultaneous induction on the height of the derivation.

Theorem 2.8 (Cut).

The rule of Cut:

is admissible in G3Q $_{1}$ .

Proof. Routine by primary induction on the weight of the cut formula A with a subinduction on the sum of heights of premises of cut, adapted and simplified from [Reference Pavlović and Gratzl21]. We illustrate on the example of $\forall $ when the cut formula is principal in both premises of the cut. Then the derivation has the following form:

This is transformed into:

Where the upper cut is of lesser height, while the lower is of lesser weight.

2.4 Semantics

With decidability established, we now continue to demonstrate further meta-theoretic properties, namely soundness and completeness. But of course, in order to do so, we here first need to recap (and slightly adapt) the standard semantics [Reference Ben-Yami2, Reference Ben-Yami, Pavlović, Berčić, Golubović and Trobok5, Reference Pavlović17, Reference Yin and Ben-Yami26] for Quarc, from its presentation in [Reference Pavlović and Gratzl21].

Definition 2.20 (Value assignment $\mathcal V$ ).

1. 1. $\mathcal V(t=t)=1$ .

2. 2. $\mathcal V(s=t)\in \{0,1\}$ .

3. 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. 4. $\mathcal V((t_{\pi 1},\ldots ,t_{\pi n})P^{\pi n})=\mathcal V((t_{1},\ldots ,t_{n})P^{n})$ .

5. 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. 6. $\mathcal V((t_{1},\ldots ,t_{n})\neg P)=\mathcal V(\neg (t_{1},\ldots ,t_{n})P)$ .

7. 7. $\mathcal V(A[ t_{\alpha }/t_{1}, \alpha /t_{2},\ldots ,\alpha /t_{n}] )=\mathcal V(A[t_1,\ldots ,t_n])$ .

8. 8. $\mathcal V(A [ \forall M] )=1$ iff for every SA t for which $\mathcal V(tM)=1$ , $\mathcal V(A [ t/\forall M])=1$ .

9. 9. $\mathcal V(A [ \exists M] )=1$ iff for some SA t for which $\mathcal V(tM)=1$ , $\mathcal V(A [ t/\exists M])=1$ .

10. 10. For any unary predicate M there is an SA t such that $\mathcal V(tM)=1$ .

Definition 2.21 (Validity).

A formula A is valid under $\mathcal V$ if $\mathcal V(A)=1$ . A sequent $\Gamma \Rightarrow \Delta $ is valid under an appropriateFootnote ² 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 appropriate assignment.

We can now show the following.

Theorem 2.22 (Soundness of G3Q $_1$ ).

G3Q $_1$ is sound. Namely, if a sequent $\Gamma \Rightarrow \Delta $ is derivable in G3Q $_1$ , then it is valid.

Proof. By induction on the height of $\Gamma \Rightarrow \Delta $ . The proof is a special case of the proof in [Reference Pavlović and Gratzl21], with a limitation on the quantifier rules. We illustrate on the example of $\forall $ .

If the last step was L $\forall $ then it has the form

Assume $tM, A[\forall M], \Gamma $ are all valid. Then, by Definition 2.20.8, so is $A[t/\forall M]$ . So, all of $tM, A[t/\forall M], A[\forall M], \Gamma $ are valid, and therefore by the inductive hypothesis so is some formula in $\Delta $ .

If the last step was R $\forall $ then it has the form

Assume all formulas in $\Gamma $ are valid. By Lemma 2.4, for every s such that $sM$ holdsFootnote ³ , the sequent $sM, \Gamma \Rightarrow \Delta , A[s/\forall M] $ is derivable with the same height. Hence, and since all the formulas in $sM, \Gamma $ are valid, by the inductive hypothesis either $A[s/\forall M]$ or some formula in $\Delta $ is valid. In the latter case we are done, and otherwise for every $sM$ it is valid that $A[s/\forall M]$ , and so by Definition 2.20.8 $A[\forall M]$ is valid.

3 Interlude: Assertoric syllogistic

It has been shown in [Reference Raab23] that Quarc accommodates Aristotle’s assertoric syllogistic. We first refine this result by showing this already holds for the weaker system Quarc $_1$ . But in fact, since the syllogistic deals only with properties, and not relations, it should be clear that this will also be the case for just Quarc $_{1.13}$ (the monadic fragment of Quarc $_1$ ). Notice however, that due to the proofs of contraries and A-I conversion below, Quarc $_{1.1B}$ would not suffice. Obviously, the addition of instantiation is required, but this is not done ad hoc, since the motivation for its addition is rooted in reasons unconnected to Aristotle [Reference Ben-Yami1, Reference Pavlović, Gratzl, Mras, Weingartner and Ritter18].

To do this, given Theorem 2.8 it will be enough to show the following.

Proof. We first demonstrate the syllogisms. Only the proofs for the syllogisms with negative sentences need to be shown, because, as explained below, the proofs of their affirmative counterparts can be recovered by simply omitting the negation symbol.

Celarent (Barbara):

The top sequent holds by Lemma 2.3. The proof of Barbara is identical, with ‘ $\neg $ ’ removed (and no use of lemma required since then the top sequent is initial).

Ferio (Darii):

Again the top sequent holds by Lemma 2.3, and the proof of Darii is identical, with ‘ $\neg $ ’ removed.

We now move to the relations of the square of oppositions, starting with contrariety.

Contraries: $\forall MP, \forall M\neg P\Rightarrow $

Contradictories: $\Rightarrow \forall M P,\exists M\neg P $ ; $\forall M P,\exists M\neg P \Rightarrow $ ; $\Rightarrow \forall M \neg P,\exists M P $ ; $\forall M \neg P,\exists M P \Rightarrow $

Very similar for the remaining contradictories. Remaining relations of the square of oppositions follow from these two using Theorem 2.8. As an illustration:

Where the conclusion of the lower cut gives subcontaries, while the conclusion of the upper cut one subalternation pair (superalternation is simple from here). We now move to the conversions.

E-conversion: $\forall M \neg P \vdash \forall P \neg M$

We can now show the following.

Proof. The demonstration of the remainder of the syllogistic in G3Q $_1$ follows the standard presentation, here using Theorem 2.8. As an illustration we offer two examples, one of a direct and one of an indirect proof.

Cesare: $\forall P \neg M, \forall S M\Rightarrow \forall S \neg P$

Baroco: $ \forall P M,\exists S\neg M\Rightarrow \exists S\neg P$

So the syllogistic is derivable in G3Q $_1$ and therefore, given Theorems 2.22 and 2.26, valid in Quarc $_1$ .

A consequence of this is an alternative derivation of a familiar result [Reference von Plato25], that:

Going further, not only is Quarc $_{1.13}$ sufficient to accommodate Aristotle’s assertoric syllogistic, but for the traditional syllogistic we can likewise omit all connectives except for negation in negative predication and literals. Therefore, the language required for the syllogistic is

$$ \begin{align*} A::=(t)P |\ (t)\neg P\ |\ (\mu M) P \ |\ (\mu M) \neg P\ |\ \neg A. \end{align*} $$

We still keep to the form and present the formulas of the language in BNF, but a recursive definition is required only for negation. It is moreover easy to see that, in the absence of binary (or higher) connectives and predicates, we no longer require anaphora. Therefore, the sequent calculus now consists only of the rules for negation (now for literals), quantifiers, negative predication and instantiation. That the structural rules and decidability will hold for the resulting system is straightforward as in Propositions 2.27 and 2.28.

No rule of this system contains any branching. Therefore, the proof search will terminate in polynomial time (bound by the weight of the endsequent, the number of singular arguments, and the number of predicates therein). The class of those endsequents that contain two quantified formulas in the antecedent and one in the succedent will exhaust the original assertoric syllogistic.

4 Embedded quantification: Quarc $_t$ and beyond

Coming back to Quarc proper, in our search for its decidable subsystems it was important to retain the entirety of what makes Quarc what it is, and we have managed to do so in terms of keeping its entire vocabulary, as well as derivation rules. But to achieve this, we substantially diminished its expressive power to avoid the kind of vicious loops proof search can enter with embedded quantification.

In the present section we try to keep what worked to ensure decidability of the resulting system, but alleviate some of the cost we have so far paid to achieve it, by reintroducing the embedding of quantified arguments in a controlled manner to obtain the central system of this paper. The crucial observation here is that the problematic type of embedding is that which includes a quantified argument of one type (universal/particular) governed by a quantified argument of the other type.

We now carefully reintroduce more quantification, making sure that it stacks only in single-type (indicated by a single t in the subscript)—within a formula governed by a universal one, only universal quantified arguments occur (or, which is effectively the same, particular within the scope of an odd number of negations), and likewise for the particular quantification.

Since tracking the number of (explicit or implicit) negations within which a QA occurs now becomes a crucial task, before defining the language itself we define the polarity of an occurrence of a quantified argument.

It is clear that in effect, the polarity tracks the number of negations (explicit, or implicit in the case of implication) that a QA occurs under, with positive polarity indicating an even (including zero), and negative polarity an odd number of negations.

With this at hand we can now expand the definition of a formula:

Definition 4.2 (Formula of Quarc $_{t}$ ).

$$ \begin{align*} \begin{array}{ll} \displaystyle A::= &\displaystyle(t_1,\ldots,t_n)P^{n} |\ (t_{\pi 1},\ldots,t_{\pi n})P^{\pi n} |\ (t_1,\ldots,t_n)\neg P\ |\ \neg (A) \ |\ (A)\circ (A)|\ \\ &\displaystyle|\ A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}]\ |\ A[\forall M/t]^{*}\ |\ A[\exists M/t]^{**}, \end{array} \end{align*} $$

where $=\ \in P^2$ , $\circ \in \{\wedge , \vee , \to \}$ and all the stipulations from Definition 2.2 apply, except that:

$^{*}$ $A[t]$ contains no $\underline {\exists S}$ / $\overline {\forall S}$ .

$^{**}$ $A[t]$ contains no $\underline {\forall S}$ / $\overline {\exists S}$ .

These two conditions replace point (2) of the condition $(*\!*\!*)$ from Definition 2.2.

Notice that all formulas of Quarc $_1$ remain formulas of the new language, since they contain no other occurrences of QAs within a scope of $\mu M$ , and therefore the polarity conditions are met. However, new formulas can now be generated, e.g.,

(1) $$ \begin{align} (\forall M_{\alpha}, \exists Y)O\supset \alpha R \end{align} $$

with the illustrative reading of “Every man who owns a yacht is rich”, used as an example in [Reference Lanzet10, Reference Pavlović and Gratzl21]. Note that here the occurrence of the universal argument is positive (given that it governs the formula), and the occurrence of the particular is negative (in the antecedent of an implication). We will offer more insight into this sentence in Section 4.1 of this paper.

The sequent calculus of Quarc $_t$ , G3Q $_t$ is the same as G3Q $_1$ (and by extension also G3Q), modulo being defined for the formulas of Quarc $_t$ . In effect, this means that only the application conditions for the quantifier rules will change, where $A[t/\forall M]$ contains no $\underline {\exists S}/\overline {\forall S}$ , $A[t/\exists S]$ contains no $\underline {\forall S}/\overline {\exists S}$ .

Now that the possibility of embedded quantification has been reintroduced, we also offer a method of tracking how deep the embedding goes, which will be of use from Lemma 4.9 onward.

Definition 4.4 (Quantifier depth, $\mathtt {qd}$ ).

For every formula A s.t. $\mathtt {qr}(A)=0$ , also $\mathtt {qd}(A)=0$ , and otherwise:

$$ \begin{align*} &\mathtt{qd}(\neg A)=\mathtt{qd}(A),\\ &\mathtt{qd}(A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}])=\mathtt{qd}(A),\\ &\mathtt{qd}(A\circ B)=max(\mathtt{qd}(A),\mathtt{qd}(B)),\\ &\mathtt{qd}(A[\mu M])=\mathtt{qd} (A[t/\mu M])+1. \end{align*} $$

We continue our discussion by noting that polarity is crucially sensitive to changes of the side of the sequent. Before proceeding we make this notion precise in the lemma below.

We now offer yet another useful piece of terminology before finally moving on to a key lemma.

In effect, the derived subformula is the transitive closure of the relation between the (main) active formula and its principal formula. It is easy to see (cf. weak subformula property) that every derived subformula of D is a subformula of D.

We are finally able to show the following.

We can also proceed to show the following.

4.1 Decidability of complex quantification

The natural language sentence “Every man who owns a yacht is rich” can be transposed into Quarc more faithfully to its surface syntax, by employing complex quantification, as was done in [Reference Lanzet10, Reference Pavlović and Gratzl21]. However, this translation is equivalent to (1) above, when using the system from the latter paper:

Observation 4.13. $(\forall s (s_{\alpha }M\wedge (\alpha ,\exists Y )O))R\Leftrightarrow (\forall M_{\alpha }, \exists Y)O\supset \alpha R.$

See Appendix 1 for a (large, but not difficult) proof of this claim. In fact, at this point there is no reason to doubt that complex quantification could be fully reduced to a combination of simple quantification, anaphora and connectives, as was done for negative predication and reorder in [Reference Pavlović and Gratzl21].

However, with that reduction the weight of the translation skyrocketed, and the added expressive device not only holds the complexity of formulas in check, but also provides a more apparent connection to its natural language counterparts. While we conjecture that such a reduction would be possible, and therefore that this result is not stronger than the one just established (hence the present investigation does not warrant a separate section), the exploration of that result would take us too far afield. In any case, on the face of it Quarc $^C$ offers more methods of embedding quantification (some redundant if the conjecture turns out true). We will in this section show that Theorem 4.10 can be extended to it with appropriate modifications, first and foremost of which is to the notion of polarity used in the definition of the language below.

Before proceeding, a note on the terminology of complex quantification in [Reference Pavlović and Gratzl21]—there complex analogues of quantified arguments are called quantified clauses, while quantified arguments and clauses are jointly called quantified expressions.

Definition 4.14 (Formula of Quarc $_{t}^C$ ).

$$ \begin{align*} \begin{array}{ll} \displaystyle A::= &\displaystyle (t_1,\ldots,t_n)P^{n} |\ (t_{\pi 1},\ldots,t_{\pi n})P^{\pi n} |\ (t_1,\ldots,t_n)\neg P\ |\ \neg (A) \ |\ (A)\circ (A)\ |\ \\ &\displaystyle |\ A[t_{\alpha}/t_{1},\alpha/t_{i},\ldots, \alpha/t_{j}] \ |\ A[\forall M/t]^* \ |\ A[\exists M/t]^{**}\ |\ \\ &\displaystyle A[\forall s (A)^{***}/t]\ |\ A[\exists s (A)^{****}/t], \end{array} \end{align*} $$

where all the stipulations from Definition 4.2 apply, and additionally:

$^{*}$ $A[t]$ contains no $\underline {\exists rB}$ / $\overline {\forall rB}$ .

$^{**}$ $A[t]$ contains no $\underline {\forall rB}$ / $\overline {\exists rB}$ .

$^{***}$ $A[t]$ is not a basic formula with a unary predicate and contains no instances of $\underline {\exists S}$ , $\underline {\exists r B}$ / $\overline {\forall S}$ , $\overline {\forall r B}$ , while $(A)$ in $\forall s(A)$ contains no instances of $\overline {\exists S}$ , $\overline {\exists r B}$ / $\underline {\forall S}$ , $\underline {\forall r B}$ .

$^{****}$ $A[t]$ is not a basic formula with a unary predicate and contains no instances of $\underline {\forall S}$ , $\underline {\forall r B}$ / $\overline {\exists S}$ , $\overline {\exists r B}$ , and $(A)$ in $\exists s (A)$ contains no instances of $\underline {\forall S}$ , $\underline {\forall r B}$ / $\overline {\exists S}$ , $\overline {\exists r B}$ .

Note that condition (***) stands apart from the others. To make full sense of this definition, we expand the definition of polarity.

Definition 4.15 (Polarity in complex quantification).

An occurrence of a quantified expression in a formula is either positive or negative.

An occurrence of a (simple) quantified argument $\mu P$ is always positive in any formula $A[\mu P]$ it governs.

An occurrence of a (complex) quantified clause $\mu s B$ is always positive in any formula $A[\mu s B]$ it governs.

If a quantified expression occurs positive (negative) in B, then it occurs positive (negative) in $B\vee C$ , $C\vee B$ , $B \wedge C$ , $C\wedge B$ , $C\supset B$ , $B[t_{\alpha }/t_1,\ldots ,\alpha /t_n]$ , $B[\mu S]$ , $B[\forall s C]$ , $B[\exists s C]$ and $C[\exists s B]$ (where the quantified expression in brackets governs the formula),

and negative (positive) in $\neg B$ , $B\supset C$ and $C[\forall s B]$ .

As before, we mark a positive occurrence of a quantified clause $\mu s B$ as $\underline {\mu s B}$ and a negative one as $\overline {\mu s B}$ .

The definition of polarity in complex quantification is the same as for the simple case, except that any occurrence that appears within a universal quantified clause switches its polarity. This is due to the fact that those implicitly occur, like in Observation 4.13, in an antecedent of an implication.

Consequently, in the case of universal complex quantification, the polarity condition in the quantified clause (the complex construction mirroring quantified arguments) is reverse to all the others. The utility of this is easy to read off Figure 2, since there all the quantifiers within the quantified clause $\forall s B$ change the sides of the sequent in the bottom-up application of the complex universal rules.

Figure 2 G3Q $_t^C.$

It is not particularly difficult to see the following.

Theorem 4.16 (Structural properties G3Q $_t^C$ ).

All the standard structural properties, namely axiom generalization, height-preserving (hp) substitution, hp-admissibility of weakening, hp-invertibility of all the rules, hp-admissibility of contraction and admissibility of cut, all hold for G3Q $_t^C$ .

Proof. Parallel to the case of Theorem 4.3, these proofs extend those for the same properties from [Reference Pavlović and Gratzl21].

We now move to extending the proof of decidability to complex quantification. The only piece of terminology still required is an extension to the definition of quantifier depth. While any quantified argument only adds 1 to the depth of a formula it governs, a quantified clause adds its own depth to it.

Definition 4.17 (Quantifier depth $\mathtt {qd}$ in Quarc $_t^C$ ).

Quantifier depth of Definition 4.4 is extended with the following conditions:

$$ \begin{align*} \mathtt{qd}(A[\forall s (B)/t])&=\mathtt{qd} (B)+\mathtt{qd}(A[t])+1,\\ \mathtt{qd}(A[\exists s (B)/t])&=\mathtt{qd} (B)+\mathtt{qd}(A[t])+1. \end{align*} $$

We can now likewise show the following.

Theorem 4.18. G3Q $_t^C$ is decidable.

Proof. Tedious, but same, mutatis mutandis, as Lemma 4.5–Theorem 4.10, extended for the cases of complex quantification, noting that we need to extend Definition 4.7, whereby instantiated quantified clauses also count as derived subformulas, and in Lemmas 4.8 and 4.9 we need to add “ $L \forall c$ ” after $L \forall $ , and the same for the other three quantified rules whenever appropriate. The complex quantifier rules will behave in the same way as their simple counterparts.

In particular, in the extension of the Lemma 4.5, all the quantified arguments within a universal quantified clause will change polarity, as well as the side of the sequent, from $\forall s B$ to $B[t/s]$ .

Consequently, in Lemma 4.8, if a formula in a derivation is principal in L $\forall $ , L $\forall c$ , R $\exists $ or R $\exists c$ , then no derived subformula of it can be principal in R $\forall $ , R $\forall c$ , L $\exists $ or L $\exists c$ (and vice versa).

To show that further meta-theoretical properties hold, we need to extend the definition of value assignment with those for complex quantification from [Reference Pavlović and Gratzl21]:

Definition 4.19 (Value assignment $\mathcal V^C$ ).

Value assignment $\mathcal V^C$ extends the Definition 2.20 with the following clauses for formulas of Quarc $^C_t$ :

1. 11. $\mathcal V(A [ \forall s(B)] )\!=\!1$ iff for every SA t for which $\mathcal V(B[t/s])\!=\!1$ , ${\mathcal V(A [ t/\forall s(B)])\!=\!1}$ .

2. 12. $\mathcal V(A [ \exists s(B)] )\!=\!1$ iff for some SA t for which $\mathcal V(B[t/s])\!=\!1$ , ${\mathcal V(A [ t/\exists s(B)])\!=\!1}$ .

We can then also proceed to show the following.

Theorem 4.20 (Soundness of G3Q $^C_t$ ).

G3Q $^C_t$ is sound. Namely, if a sequent $\Gamma \Rightarrow \Delta $ is derivable in G3Q $^C_t$ , then it is valid in Quarc $^C_t$ .

Theorem 4.21 (Completeness of G3Q $^C_t$ ).

G3Q $^C_t$ is complete. Namely, if a sequent $\Gamma \Rightarrow \Delta $ is valid in Quarc $^C_t$ , then it is derivable in G3Q $^C_t$ .

Proof. Again tedious but the same, modulo the limited language, to the corresponding proofs in [Reference Pavlović and Gratzl21]. In effect, the proofs of Theorem 2.22 and Lemma 2.25 are simply extended with the new cases from Definition 4.19.

5 Conclusions and future work

In this paper we have extended the proof-theoretic investigations into Quarc by presenting and analyzing a series of its decidable subsystems, all of which retained the entire vocabulary of Quarc. The decidability result was reached via a restriction on quantification. First restriction was to what we have labeled single-stack—no quantified argument can appear within the scope of (or, in the parlance of Quarc, in a formula governed by) another quantified argument. On the other hand the second, demonstrably stronger, system restricted what type of quantification can be embedded—within universal only universal quantification is allowed, and likewise for particular.

In both cases the proof of decidability was then provided by imposing saturation criteria, which in effect limit the number of times a rule is applied to a formula (understood, as is common in proof theory, as a bottom-up application) to a minimum. This number can in turn be shown to be finite, thus finalizing the whole proof-search tree in a finite number of steps. As mentioned in the introduction, a significant upside to this approach is that it provides a ready-made algorithm for finding proofs. Moreover, this proof-search procedure can easily be rolled over into the proof of other meta-theoretic properties, especially completeness, as we have also seen in this paper.

To show this result is of interest that is not merely theoretic, we have made an interlude in which we refined the previous results on the connection of Quarc and Aristotle’s assertoric syllogistic, and this has allowed us to offer a new take on the proof of the latter’s decidability.

One avenue of research not pursued here was the computational efficiency of the systems and ways of improving it (as it stands, it is clear from numerous branching rules that it will not be very high), but that exploration is left for future work.

At the conclusion of present work several other extensive avenues of research still remain open and waiting to be explored. On the more practical side, embedding of Aristotle’s modal syllogistic into Quarc has been suggested [Reference Pavlović17, Reference Raab23] but still remains to be explored to its full potential. Of course, the complicating factor here is that, in contrast to the assertoric, the modal part of the syllogistic is nowhere near as clear-cut (nor generally accepted as correct). Its expansiveness, as well as the need to first extend Quarc with modalities (done only partially in [Reference Ben-Yami2, Reference Ben-Yami4, Reference Pavlović17]) means that this topic exceeded the confines of this paper, but is nonetheless a worthwhile future project.

Moreover, on the more theoretical side, while we have presented systems of increasing strength (for some the decision is pending, conditional upon a proof or refutation of a conjecture), we have of course not argued here that the systems could not be strengthened further. It remains to be seen how much restrictions on quantification (which constitute the only difference with the original Quarc) can be loosened while the property is retained, as well what would be plausible interpretations and applications of the resulting systems. And of course, it will be worthwhile to see how these systems relate to PC. These investigations could potentially be quite informative not only of Quarc, but likewise of natural language quantification, and will therefore hopefully be revisited in future work on Quarc. Moreover, other methods of obtaining decidability, fundamentally different and potentially incommensurate, are possible. Therefore, the present contribution is hopefully a start to a fruitful body of research into various means of answering the question of decidability of Quarc, rather than its end.