Despite the successes of the Predicate Calculus, based on Frege’s Begriffsschrift (1879), there have been recurrent attempts to develop different logic systems, closer in various respects to natural language. Strawson’s (1950, 1952) and Sommers’ (1982) are two such familiar earlier ones.

More recently, Lawrence Moss has published a series of works, some co-authored with Pratt-Hartmann, which engage in the similar project of Natural Logic (Pratt-Hartmann and Moss 2009; Moss 2010b, 2010c, 2010a, 2011, 2015). Natural Logic has several aims. One main aim is to “construct a system [whose] syntax is closer to that of a natural language than is first-order logic” and give “logical systems in which one can carry out as much simple reasoning in language as possible” (Moss 2010b, 538–539). Moss’s works “attempt to make a comprehensive study of the entailment relation in fragments of language,” “to go beyond truth conditions and examples, important as they are, and to aim for more global characterizations” (2010b, 561). “The subject of natural logic,” Moss writes, “might be defined as ‘logic for natural language, logic in natural language.’ By this, we aim,” he clarifies, “to find logical systems that deal with inference in natural language, or something close to it” (2015, 563). Moss has tried to faithfully represent in his systems standard quantifiers, passive-active voice relations, comparative adjectives, and more.

A different system with similar aspirations which has also been recently developed is the Quantified Argument Calculus, or Quarc.¹ Quarc is a powerful formal logic system, first introduced in Ben-Yami’s “The Quantified Argument Calculus” (2014), based on work published by Ben-Yami in the preceding decade (primarily 2004) and closely related to the calculus introduced in Lanzet and Ben-Yami (2004). It is closer in its syntax than is the Predicate Calculus to natural language, sheds light on the logical role of some of the latter’s features which it incorporates (such as copular structure, converse relation terms and anaphora), and it is also closer to natural language in the logical relations it validates. Ben-Yami (2014) contains a Lemmon-style natural deduction system for Quarc and a truth-valuational, substitutional semantics; this system has been shown to be sound and complete (Ben-Yami 2014; Ben-Yami and Pavlović 2022). Quarc has since been extended into a sound and complete three-valued system with defining clauses, using model-theoretic semantics (Lanzet 2017). In this latter version it was shown to contain a semantically isomorphic image of the Predicate Calculus. Thus, Quarc has been shown to be at least as strong as the first-order Predicate Calculus, and moreover, the proofs in these papers shed light on the nature of quantification in the Predicate Calculus (see there for details). In other works (Pavlović 2017; Pavlović and Gratz 2019), a sequent calculus has been developed for several versions of Quarc and various properties of the system, such as cut-elimination, subformula property and consistency were proved. Quarc has also been used to investigate Aristotelian logic, both assertoric and modal, in works mentioned above as well as in Raab (2018). Raab concludes that the Quarc-reconstruction he provides of Aristotle’s logic is “much closer to Aristotle’s original text than other such reconstructions brought forward up to now” (abstract).

It would be interesting to compare what Natural Logic has achieved with what has or can be achieved by Quarc. The present paper embarks on this inquiry. Only embarks, for limitations of space and time force us to leave out a comparative study of some central questions of the Natural Logic project. An important issue for Moss is that of decidability. He would like to determine whether the logic systems he constructs to incorporate reasoning in natural language, systems which are more limited in their expressive power than the first-order Predicate Calculus, are decidable. Moss and Pratt-Hartmann write:

From a computational point of view […] expressive power is a double-edged sword: roughly speaking, the more expressive a language is, the harder it is to compute with. In the last decade, this trade-off has led to renewed interest in inexpressive logics, in which the problem of determining entailments is algorithmically decidable with (in ideal cases) low complexity. The logical fragments subjected to this sort of complexity-theoretic analysis have naturally enough tended to be those which owe their salience to the syntax of first-order logic, for example: the two-variable fragment, the guarded fragment, and various quantifier-prefix fragments. But of course it is equally reasonable to consider instead logics defined in terms of the syntax of natural languages. (2009, 647–648)

Moss also thinks that decidable systems with less expressive power might represent more faithfully actual human reasoning (2015, 563). Interesting and important as decidability questions are, they will not be addressed in this paper but be left for future work.

The primary concern of this paper is Quarc’s capacity to incorporate the natural language inferences studied by Natural Logic. Natural Logic’s starting point is a variety of inferences in natural language, all apparently formally valid. Formal systems are then built to incorporate some of these inferences. I shall examine whether Quarc can incorporate these inferences or how it should be extended to accomplish this. I shall also discuss the soundness and completeness of the systems I consider.

Quarc is introduced in the next section; I develop it there only to the extent needed for its application later in the paper. In the section following it, I first present several arguments which Moss considers, and then address each of them in a separate subsection. Along the way I also consider whether, with Moss, we should allow nouns to be negated. I end with a short conclusion, which also includes directions for future work.

1 Introduction to Quarc

By now, Quarc has been presented in several works and in several versions (Ben-Yami 2014; Lanzet 2017; Pavlović and Gratz 2019; Ben-Yami and Pavlović 2022) and there is therefore no need for an additional detailed exposition. Moreover, for our purposes below we do not need to employ the full version of Quarc that was introduced in Ben-Yami (2014). Accordingly, although I shall first informally introduce the full Quarc language of that paper, the following formal introduction will be of a reduced version (but with the addition of identity), one which we shall then continue to use.

1.1 Informal Introduction of the System

Consider a simple subject–predicate or argument–predicate sentence:

1. Alice is polite.

Its grammatical form can be represented by

2. (Alice) is polite

with the argument in parenthesis, followed by the copula and then the predicate. In the Predicate Calculus, we formalise this sentence by

3. \(P(a)\)

Quarc does not depart from this formalisation, apart from a typographical change: the arguments, in Quarc, are written to the left of the predicate:

4. \((a)P\)

Similarly,

5. Alice loves Bob.

is formalised, in Quarc, as

6. \((a,b)L\)

Consider next the quantified sentence,

7. Every student is polite.

Its grammatical form can be represented by

8. (every student) is polite

Here, grammatically, the argument is the noun phrase “every student.” In it, the quantifier “every” attaches to the one-place predicate “student,” and together they form a quantified argument. This is the way quantification is incorporated in Quarc:

9. \((\forall S)P\)

Namely, quantifiers are not sentential operators. Rather, they attach to one-place predicates to form quantified arguments. Some other examples:

10. Some students are polite.
11. Every girl loves Bob.
12. Every girl loves some boy.

are formalised (respectively; likewise below) by,

13. \((\exists S)P\)
14. \((\forall G,b)L\)
15. \((\forall G,\exists B)L\)

This basic departure in the treatment of quantification requires a few additional ones. One is the need to reintroduce the copular structure and, with it, modes of predication, as in Aristotelian logic. In natural language, we can negate sentence (1), “Alice is polite,” in two ways:

16. It’s not the case that Alice is polite.
17. Alice isn’t polite.

The Predicate Calculus allows only the first mode of negation—the one rarer and somewhat artificial in natural language—namely, sentential negation. Quarc, however, also allows the negation symbol to be written between the argument or arguments and the predicate, signifying negative predication, by contrast to affirmative one. These two sentences are thus formalised, respectively, by

18. \(\lnot((a)P)\)
19. \((a)\lnot P\)

Parentheses can be omitted without ambiguity in these formulas, and they can be written as \(\lnot aP\) and \(a\lnot P\). Since the argument is singular, these two formulas are equivalent, and they shall be defined as such both in the proof system and in the semantics below. However, the equivalence does not hold when the argument is quantified:

20. It’s not the case that some students are polite.
21. Some students aren’t polite.

formalised by:

22. \(\lnot (\exists SP)\)
23. \((\exists S)\lnot P\)

These formulas will not be equivalent either in the proof system or in the semantics.

Some adjectives have a corresponding negative form: polite and impolite, for instance. Yet even if “Alice isn’t polite” means the same as “Alice is impolite,” this is not the case with all such pairs of adjectives. Often, the negative form designates not the contradictory but the contrary of the positive one: while “reverent” means, feeling or showing deep and solemn respect, “irreverent” means, showing a lack of respect for people or things that are generally taken seriously (Oxford definitions); one’s attitude towards, say, religion can be neither reverent nor irreverent. Moreover, many adjectives have no negative form: tall, asleep, red; and relation words usually don’t—e.g. “loves” or “teacher of.” For these and other reasons (see below on negative nouns), the work done by negative predication cannot generally be accomplished by negative predicates.

All natural languages have the means of reordering the noun-phrases in relational sentences without changing, if the arguments are all singular, what is said by the sentences. Different languages achieve this by different means. English often accomplishes it by changing from active- to passive-voice:

24. Alice loves Bob.
25. Bob is loved by Alice.

In the singular case, the two are logically equivalent. But again, this is not generally the case when the arguments are quantified:

26. Every girl loves some boy.
27. Some boy is loved by every girl.

Quarc incorporates this reordering by having an \(n\)-place predicate written with a permutation of the \(1, 2, \ldots, n\) sequence as superscripts to its right. Sentences (24) to (27) are then formalised by,

28. \((a,b)L\)
29. \((b,a)L^{2,1}\)
30. \((\forall G, \exists B)L\)
31. \((\exists B, \forall G)L^{2,1}\)

As with negation, the formulas with singular arguments alone are defined as equivalent in both proof system and semantics, while this equivalence will not generally hold for sentences with quantified arguments.

The last additional feature of Quarc is its use of anaphora. Consider the two sentences,

32. John loves John.

33. John loves himself.

The former is rarely used, although one of its uses is to explain the use of the reflexive pronoun “himself” in the latter. The reflexive pronoun “himself” in (33) is anaphoric on the earlier occurrence of “John,” its source, in the sense that it can be replaced by its source and the sentence will have the same meaning. This eliminable anaphor is what Geach called pronoun of laziness (1962, sec. 76). Quarc incorporates it by using a Greek letter for the anaphor, also written as a subscript to the right of its source. Accordingly, it formalises (32) and (33) by:

34. \((j,j)L\)

35. \((j_{\alpha}, \alpha)L\)

The formalisation of quantified sentences in which quantified arguments have anaphors is similar:

36. Every man loves himself.

37. \((\forall M_{\alpha},\alpha)L\)

As with negation and reordering, if all arguments are singular, then a Quarc formula with an anaphor and the formula with that anaphor replaced by its source are defined as equivalent in both proof system and semantics. However, the anaphor is no longer generally replaceable by its source when the latter is quantified, neither in natural language nor in Quarc.

With this I conclude the informal introduction of Quarc and turn to the more rigorous introduction of the formal system. However, for the purposes of the discussion below, we don’t need to use formulas with anaphora. I therefore introduce a reduced version of Quarc, in this respect, which will make it easier to follow and focus on the main argument of this paper. The interested reader is referred to the works mentioned above to see how anaphora is incorporated in the full version of Quarc.

1.2 Vocabulary of Quarc

The language of Quarc contains the following symbols:

38. (Vocabulary)

    • Predicates: \(P, Q, R, \ldots\), denumerably many and each with a fixed number of places, including the two-place predicate \(=\).

    • Singular arguments (SAs): \(a, b, c, \ldots\), denumerably many.

    • Sentential operators: \(\lnot, \land, \lor, \rightarrow, \leftrightarrow\).

    • Quantifiers: \(\forall, \exists\).

    • Numerals used as indices, comma, parentheses.

If \(P\) is a one-place predicate, then \(\forall P\) and \(\exists P\) will be called quantified arguments (QAs). An argument is a singular argument or a quantified one. For every \(n\)-place predicate \(R\), \(n > 1\), apart from \(=\), \(R^{\pi}\), where \(\pi\) is any permutation of \(1, \ldots, n\) (including the identity permutation), is called a reordered form of \(R\); \(R^{\pi}\) is also an \(n\)‑place predicate.

1.3 Formulas of Quarc

The following rules specify all the ways in which formulas can be generated.

39. (Formulas)

    1. (Basic formula) If \(P\) is a non-reordered \(n\)-place predicate and \(c_1, \ldots, c_n\) singular arguments (SAs), then \((c_1, \ldots, c_n)P\) is a formula, called a basic formula.

    2. (Reorder) If \(P\) is a reordered \(n\)-place predicate, \(n > 1\), and \(c_1, \ldots, c_n\) SAs, then \((c_1, \ldots, c_n)P\) is a formula.

    3. (Negative predication) If \(P\) is an \(n\)-place predicate and \(c_1, \ldots, c_n\) SAs, then \((c_1, \ldots, c_n)\lnot P\) is a formula.

    4. (Identity) If \(c_1\) and \(c_2\) are SAs then \(c_1 = c_2\) is a formula. \(c_1 = c_2\) is an alternative way of writing \((c_1, c_2)=\).

    5. (Sentential operators) If \(\phi\) and \(\psi\) are formulas, so are \(\lnot (\phi)\), \((\phi)\land(\psi)\), \((\phi)\lor(\psi)\), \((\phi)\rightarrow(\psi)\) and \((\phi)\leftrightarrow(\psi)\). The parentheses surrounding formulas are called sentential parentheses.

    6. (Quantification) If \(\phi\) is a formula containing an occurrence of an SA \(c\), and substituting the quantified argument \(qP\) (i.e. \(\forall P\) or \(\exists P\)) for \(c\) will result in \(qP\) governing \(\phi\) (see definition below), then \(\phi [qP/c]\) is a formula. (\(\phi [qP/c]\) is the formula in which \(qP\) replaced the occurrence of \(c\).)

Formulas of the form, \((c_1, \ldots, c_n)P\), in which \(P\) is a reordered predicate are not considered basic formulas, as this simplifies the semantic definitions below.

The notion of governance, which is related to that of scope in the Predicate Calculus, is defined as follows:

40. (Governance) An occurrence \(qP\) of a QA governs a string of symbols \(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 displayed parentheses are a pair of sentential parentheses, such that \(B\) contains \(qP\).

Once anaphors are introduced, the notion of governance becomes non-trivial and its definition needs elaboration. Since they are not introduced in this formal part, determining whether a quantified argument governs a formula is straightforward. For instance, \(\exists S\) governs the formulas \((\exists S)P\), \((\exists S)\lnot P\), \((a,\exists S)L\), \((\exists S, \forall P)L\) and \((\exists S, \forall P)L^{1,2}\) – the last two because it is to the left of \(\forall P\). By contrast, \(\exists S\) does not govern \(\lnot((\exists S)P)\), since it is contained in \(((\exists S)P)\); nor \(((\exists S)P)\land(aQ)\), as it is contained in \(((\exists S)P)\); nor \((\forall Q, \exists S)L\), since \(\forall Q\) is to its left. For the reduced Quarc language of this paper, a somewhat simpler definition of governance could be provided, practically listing the schemas of formulas governed by a QA; I prefer to use this definition in order to facilitate the transition to fuller Quarc languages. We shall often omit parentheses where no ambiguity arises.

1.4 Truth-Valuational, Substitutional Semantics

As in Ben-Yami (2014), I use here a truth-valuational, substitutional semantics for Quarc. Justification of the approach and answers to some common or possible objections, neither specific to Quarc but as a general semantic approach, can be found in Ben-Yami (2014) and Ben-Yami and Pavlović (2022). The results below do not depend on the use of this semantics: a model-theoretic semantics for Quarc can and has been developed. A precursor of Quarc with model-theoretic semantics is found in Lanzet and Ben-Yami (2004) and a three-valued version of Quarc with model-theoretic semantics is found in Lanzet (2017).

41. (Truth-Value Assignments) The following holds for any truth-value assignment, or valuation:

    1. (Basic formula) Every basic formula is assigned the truth-value of true or false, but not both.

    2. (Reorder) Let \(P\) be a non-reordered \(n\)-place predicate, \(n > 1\), and \(\pi = \pi 1, \ldots, \pi n\) a permutation of \(1,2,\ldots,n\). Then, the truth-value assigned to \((c_{\pi 1}, \ldots, c_{\pi n})P^{\pi}\) is that assigned to \((c_1, \ldots, c_n)P\).

    3. (Law of Identity) Every formula of the form \(c = c\) is true.

    4. (Indiscernibility of Identicals) If \(t = c\) is true and the formula \(\phi [t_1,\ldots,t_n]\) is a basic formula containing the instances \(t_1,\ldots,t_n\) of an SA \(t\), then \(\phi [c/t_1,\ldots,c/t_n]\) is true if \(\phi [t_1,\ldots,t_n]\) is true.

    5. (Instantiation) For every one-place predicate \(P\) there is some SA \(c\) such that \((c)P\) is true.

    6. (Sentential operators) Let \(\phi\) and \(\psi\) be formulas. Then, \(\lnot (\phi)\) is true just in case \(\phi\) is false, etc.

    7. (Negative predication) Let \(P\) be an \(n\)-place predicate and \(c_1, \ldots, c_n\) SAs. The truth-value of \((c_1, \ldots, c_n)\lnot P\) is that of \(\lnot (c_1, \ldots, c_n)P\).

    8. (Quantification) Let \(\phi[\forall P]\) (\(\phi [\exists P]\)) be a formula governed by an occurrence of \(\forall P\) (\(\exists P\)). If for every (some) SA \(c\) for which \((c)P\) is true, \(\phi[c/\forall P]\) (\(\phi[c/\exists P]\)) is true, then \(\phi[\forall P]\) (\(\phi [\exists P]\)) is true. If for some (every) \(c\) for which \((c)P\) is true \(\phi[c/\forall P]\) (\(\phi[c/\exists P]\)) is false, then \(\phi[\forall P]\) (\(\phi [\exists P]\)) is false.

42. (Validity) An argument whose premises are all and only the formulas in the set of formulas \(\mathfrak{S}\) and whose conclusion is the formula \(\phi\) is valid, written \(\mathfrak{S} \models \phi\), just in case every valuation that makes all the formulas in \(\mathfrak{S}\) true also makes \(\phi\) true, even if we add or eliminate singular arguments from our language (of course, only singular arguments not occurring in \(\mathfrak{S}\) or \(\phi\) can be eliminated). We also say that \(\mathfrak{S}\) entails \(\phi\).

For a discussion of these definitions, see Ben-Yami (2014).

1.5 Proof System

The proof system used here is based on that found in Ben-Yami (2014) and Ben-Yami and Pavlović (2022), with the omission of the rules for anaphora. I use a Lemmon-style natural deduction system, based on the one introduced in Jaśkowski (1934) and further developed and streamlined in Fitch (1952), Lemmon (1965) and elsewhere. Proofs are written as follows:

43. (Proof) A proof is a sequence of lines of the form \(\langle L, (i), \phi, R \rangle\), where \(L\) is a possibly empty list of line numbers; \((i)\) the line number in parenthesis; \(\phi\) a formula; and \(R\) the justification, a name of a derivation rule possibly followed by line numbers, written according to one of the derivation rules specified below. \(\phi\) is said to depend on the formulas listed in \(L\). The line numbers in \(L\) are written without repetitions and in ascending order. The formula in the last line of the proof is its conclusion. If there is a proof with the formula \(\phi\) as conclusion, depending only of formulas from the set \(\mathfrak{S}\), then \(\phi\) is provable from \(\mathfrak{S}\), or \(\mathfrak{S} \vdash \phi\).

I next list the derivation rules of the system.

44. (Derivation rules)

    1. (Premise) As any line of a proof, any formula can be written, depending on itself, its justification being Premise:

    \(i\) (\(i\))

    \(\phi\)

    Premise

    2. (Propositional Calculus Rules, PCR) We allow the usual derivation rules of the Propositional Calculus.

    3. (Identity Introduction, \(=\)I) As any line of the proof a formula of the form \(c = c\) can be written, depending on no premises, with its justification being \(=\)I.

       (\(i\))

       \(c = c\)

       \(=\)I

    4. (Identity Elimination, =E) (This and the following rules specify how to add a line to a proof which contains preceding lines of the specified forms.) Let \(\phi\) be a basic formula containing occurrences \(t_1,\ldots,t_n\) of the singular argument \(t\) (\(\phi\) may also contain additional occurrences of \(t\)).

       \(L_1\)	(\(i\))	\(\phi\)
       \(L_2\)	(\(j\))	\(t = c\)
       \(L_1, L_2\)	(\(k\))	\(\phi[c/t_1, \ldots, c/t_n]\)	\(=\)E \(i, j\)

       Where \(L_1, L_2\) is the list of numbers occurring either in \(L_1\) or in \(L_2\).

    5. (Sentence negation to Predication negation, SP) Let P be an \(n\)‑place predicate and \(c_1, \ldots, c_n\) singular arguments.

    \(L\) (\(i\))	\(\lnot(c_1, \ldots, c_n)P\)
    \(L\) (\(j\))	\((c_1, \ldots, c_n)\lnot P\)	SP \(i\)

    6. (Predication negation to Sentence negation, PS) Let \(P\) be an \(n\)‑place predicate and \(c_1, \ldots, c_n\) singular arguments.

       \(L\)	(\(i\))	\((c_1, \ldots, c_n)\lnot P\)
       \(L\)	(\(j\))	\(\lnot(c_1, \ldots, c_n)P\)	PS \(i\)

    7. (Reorder, R) Let \(P\) be an \(n\)-place predicate, \(n > 1\), and \(\pi = \pi{1}, \ldots \pi{n}\) and \(\rho = \rho{1}, \ldots \rho{n}\) two permutations of \(1,2,\ldots,n\) (the identity permutation included).

    \(L\) (\(i\))	\((c_{\pi{1}}, \ldots, c_{\pi{n}})P^\pi\)
    \(L\) (\(j\))	\((c_{\rho{1}}, \ldots, c_{\rho{n}})P^\rho\)	R \(i\)

    8. (Universal Introduction, \(\forall\)I) Let \(\phi[\forall P]\) be a formula governed by \(\forall P\). Assume that neither \(\phi[\forall P]\) nor the formulas in lines \(L\) apart from \((c)P\) in line \(i\) contain any occurrence of the singular argument \(c\).

       \(i\)	(\(i\))	\((c)P\)	Premise
       \(L\)	(\(j\))	\(\phi[c/\forall P]\)
       \(L-i\)	(\(k\))	\(\phi[\forall P]\)	\(\forall\)I \(i, j\)

       Where \(L-i\) is the possibly empty list of numbers occurring in \(L\) apart from \(i\).

    9. (Universal Elimination, \(\forall\)E) Let \(\phi[\forall P]\) be a formula governed by \(\forall\)P.

       \(L_1\)	(\(i\))	\(\phi[\forall P]\)
       \(L_2\)	(\(j\))	\((c)P\)
       \(L_1, L_2\)	(\(k\))	\(\phi[c/\forall P]\)	\(\forall\)E \(i, j\)

    10. (Particular² Introduction, \(\exists\)I) Let \(\phi[\exists P]\) be a formula governed by \(\exists P\).

        \(L_1\)	(\(i\))	\(\phi[c/\exists P]\)
        \(L_2\)	(\(j\))	\((c)P\)
        \(L_1, L_2\)	(\(k\))	\(\phi[\exists P]\)	\(\exists\)I \(i, j\)

    11. (Instantial Import, Imp)³ Let \(q\) stand for either \(\exists\) or \(\forall\), and \(\phi[qP]\) be governed by \(qP\). Assume \(c\) does not occur in \(\phi[qP]\), \(\psi\) or any of the formulas \(L_1\), and in no formula \(L_2\) apart from \(j\) and \(k\).

        \(L_1\)	(\(i\))	\(\phi[qP]\)
        \(j\)	(\(j\))	\((c)P\)	Premise
        \(k\)	(\(k\))	\(\phi[c/qP]\)	Premise
        \(L_2\)	(\(l\))	\(\psi\)
        \(L_1, L_2-j-k\)	(\(m\))	\(\psi\)	Imp \(i, j, k, l\)

As examples, I provide three proofs, which between them demonstrate all the derivation rules apart from the rules for identity, which are not special to Quarc, and Reorder, which is used later. First, \((\forall S)P \vdash (\exists S)P\):

This inference, being part of the Aristotelian Square of Opposition, is invalid on the standard translation of these sentences to the Predicate Calculus. Quarc is closer in this respect to Aristotelian Logic; for discussion, see Ben-Yami (2004, 2014), Lanzet (2017), Raab (2018).

Secondly, the Aristotelian Barbara, i.e. \((\forall S)M, (\forall M)P \vdash (\forall S)P\):

And lastly, an Aristotelian conversion: “No \(P\) is \(S\)” follows from “No \(S\) is \(P\).” Instead of introducing into Quarc a negative quantifier translating “no”—something that can be done—these sentences are translated here as synonymous with “Every/any \(S\) is not \(P\)” or \((\forall S)\lnot P\), and \((\forall P)\lnot S\), and we show that \((\forall S)\lnot P \vdash (\forall P)\lnot S\):

For additional examples, see Ben-Yami (2014) and Ben-Yami and Pavlović (2022).

2 Incorporation in Quarc of the Inferences Motivating the Natural Logic Project

2.1 The Inferences to be Considered

In different works, Moss provides different examples of the kinds of inference he discusses in the context of his Natural Logic project. I shall use here, as our point of departure, the inferences he lists in his “Natural Logic” (Moss 2015, 561–562). This list is more detailed and more recent than those found elsewhere in his writings.⁴

1. Passive voice

   Some dog sees some cat.

   ∴ Some cat is seen by some dog.

2. Conjunctive predicates

   Bao is seen and heard by every student.

   Amina is a student.

   ∴ Amina sees Bao.

3. Comparative adjectives

   Every giraffe is taller than every gnu.

   Some gnu is taller than every lion.

   Some lion is taller than some zebra.

   ∴ Every giraffe is taller than some zebra.

4. Defining clauses

   All skunks are mammals.

   ∴ All who fear all who respect all skunks fear all who respect all mammals.

5. Comparative quantifiers

   More students than professors run.

   More professors than deans run.

   ∴ More students than deans run.

I shall examine the incorporation of inferences of these kinds in Quarc, each in a separate subsection. But before turning to them, I address a different feature which some of Moss’s systems contain: negative nouns.

2.2 Negative Nouns

Some of Moss’s formal systems contain devices intended to represent “negated nouns such as ‘non-man’ or ‘non-animal’” (Pratt-Hartmann and Moss 2009, 648). Moss thinks that “this is rather unnatural in standard speech but it would be exemplified in sentences like Every non-dog runs” (2015, 567–568). Other examples Moss provides there are All non-apples on the table are blue and Bernadette knew all non-students at the party (Pratt-Hartmann and Moss 2009, 564).

But when such sentences are used, which I suspect is rarely, they are surely used as elliptical for sentences like, “All fruits on the table which aren’t apples are blue” or “Bernadette knew all non-student guests at the party.” There were also breadcrumbs on the table, but we didn’t mean to say that they were blue; and there were also drinks and finger food at the party.

This ellipsis understanding is also shared by Moss. In his (2010b, 539–540), we find an introductory dialogue between A, Moss’s mouthpiece, and a Questioning Q. Q requests “an example of some non-trivial inference carried out in natural language,” to which A responds by mentioning an inference containing the premise, Every non-pineapple is bigger than every unripe fruit. Q immediately remonstrates: “‘non-pineapple’?! I thought this was supposed to be natural language”; and A excuses himself with, “Take it as a shorthand for ‘piece of fruit which is not a pineapple’.” Regrettably, Q acquiesces: “Ok, I get it.”

Yet if, instead of Q, A would have encountered Critical C, she might have retorted, “So why not stay with ‘fruits which aren’t pineapples’? Should Logic turn a shorthand into a formal syntactic feature?! And you anyway intend to incorporate defining clauses in your system, for instance when formalising ‘all who respect all skunks,’ so you shall have the resources for ‘fruits which aren’t pineapples.’ If your goal is, as you stated, ‘logic for natural language, logic in natural language,’ then try avoiding non-men, non-dogs and other non-natural creatures.”

C’s point is supported by an observation due to Aristotle. In his Categories (~BC330), when discussing primary, individual substances—an individual man or horse, for instance—and secondary substances, like “man” and “animal” as species and genera, he notes: “Another mark of substance is that it has no contrary. What could be the contrary of any primary substance, such as the individual man or animal? It has none. Nor can the species or the genus have a contrary” (Cat. 5, 3b24). Since there is no contrary to man or animal, “non-man” and “non-animal” cannot function, on their own, as noun phrases.

The actual natural language sentences which Moss formalises by means of formal negative nouns, designated by a bar (\(\overline{q}\) for non-\(q\)’s), are sentences like, “Some \(p\) aren’t \(q\)” and “Some \(p\) don’t \(r\) any \(q\),” formalised by \(\exists(p, \overline{q})\) and \(\exists(p, \forall(q,\overline{r}))\) (2015, 573). (We don’t need to go into the details of Moss’s syntax, since for our purposes the idea is sufficiently clear from these examples.) These two sentences are formalised in Quarc by \((\exists P)\lnot Q\) and \((\exists P,\forall Q)\lnot R\). Accordingly, Quarc can formalise these sentences without recourse to negative nouns but by using negation as a mode of predication, as it is indeed used in natural language.

I think that finding the idea of negative nouns acceptable is influenced by the semantic idea of a domain of discourse. If, when quantifying, the plurality over which we quantify is that of a domain of discourse, then we can single out a part of it either as containing all items to which a predicate \(p\) applies, or all those to which it does not apply. Indeed, when Moss develops a semantics for languages that include negative nouns, his model or structure \(\mathfrak{U}\) contains a non-empty set \(A\) which functions as the domain, and if \(p^{\mathfrak{U}} \subseteq A\), then \({\overline{p}}^{\mathfrak{U}}=A \backslash p^{\mathfrak{U}}\) (Pratt-Hartmann and Moss 2009, 651). However, a domain of discourse, in the technical sense in which the idea is employed in semantics, is an artefact of Fregean Logic, whose quantified sentences contain no expression specifying the plurality over which they quantify. For this reason, the semantics must introduce an otherwise implicit domain. Natural language sentences, by contrast, do specify the plurality over which they quantify: when I say, “All your students came to class,” I specify your students as the relevant plurality. Quarc follows natural language in this respect, and needs no domain of discourse or of quantification (Ben-Yami 2004, 59–60; Lanzet 2017). Once the domain is eliminated, “non-man” and “non-animal” have nothing to designate and should be eliminated as well.

For these reasons, I think that negative nouns are not needed and should not be included in a logic which aspires to be a logic for natural language. As argued above, the rare sentences which apparently use them are better seen as elliptical: as such they can be formalised in Quarc, which therefore does not need to contain negative nouns.

2.3 Passive Voice

45. Some dog sees some cat.

    ∴ Some cat is seen by some dog.

Quarc was developed to incorporate reordering devices such as the active–passive voice distinction. If “\(a\) sees \(b\)” is formalised, “\((a,b)S\),” then “\(b\) is seen by \(a\)” is formalised, “\((b,a)S^{2,1}\).” We show that,

46. \((\exists D, \exists C)S \vdash (\exists C, \exists D)S^{2,1}\)

Quarc with truth-valuational semantics has been shown to be sound and complete in Ben-Yami (2014) and Ben-Yami and Pavlović (2022); a model-theoretic version of this result is found, for an earlier version of the system and for a three-valued version of it, in Lanzet and Ben-Yami (2004) and Lanzet (2017). Accordingly, Quarc is a sound and complete formal system, with a syntax modelled on natural language’s, which incorporates inferences like (45).

2.4 Conjunctive Predicates

47. Bao is seen and heard by every student.

    Amina is a student.

    ∴ Amina sees Bao.

The new element in this inference is the conjunctive verb, or more generally conjunctive predicate, “see and hear.” We shall extend Quarc to incorporate it.

We take our cue for the incorporation of conjunctive predicates in Quarc from the way negative predication, reordering and anaphora were incorporated in it. Namely, we shall define valuation- and derivation rules for the case in which all arguments are singular terms, and show that these together with the other rules which have already been defined provide us with desirable results for the more complex cases as well.

2.4.1 Vocabulary

We do not extend the basic vocabulary of Quarc but define,

48. (Conjunctive predicates) If \(P\) and \(Q\) are \(n\)‑place predicates, so is \((P)\land(Q)\), which is called a conjunctive predicate.

Conjunction of predicates can be iterated. Assuming \(P\), \(Q\) and \(R\) are \(n\)‑place predicates, so are \(((P)\land (Q))\land(R)\), \((P)\land ((Q)\land (R))\), \(((P)\land (Q))\land ((R)\land (P))\), and so on. However, as can be proved, formulas with the same predicates ordered and grouped in whichever way, with or without repetition, are equivalent both semantically and proof-theoretically. This allows us to omit parentheses for some conjunctive predicates: both \(((P)\land (Q))\land (R)\) and \((P)\land ((Q)\land (R))\) can be written as \(P\land Q\land R\).

Notice that many-place conjunctive predicates can be reordered like any other many-place predicate.

2.4.2 Formulas

No new rules. If \(P\) and \(Q\) are one-place predicates, then \((a)(P)\land (Q)\) is a formula. Similarly for any \(n\)‑place predicates and any arguments.

2.4.3 Semantics

49. (Conjunctive Predication). Let \(P\) and \(Q\) be \(n\)-place predicates, and \(c_1, \ldots, c_n\) singular arguments. The truth-value assigned to \((c_1, \ldots, c_n)(P)\land (Q)\) on a valuation is that assigned to \((c_1, \ldots, c_n)P\land (c_1, \ldots, c_n)Q\).

Examples. If, on a given valuation, \(aP\), \(aQ\) and \(aR\) are true, then so are, according to our definition, \(a(P)\land (Q)\), \(a(Q)\land (R)\) and \(a(R)\land (P)\). Accordingly, so are \(a((P)\land (Q))\land (R)\), \(a(P)\land ((Q)\land (R))\) and \(a((P)\land (Q))\land ((R)\land (P))\). If \(aP\) is false, then so are \(a(P)\land (Q)\), \(a(P)\land ((Q)\land (R))\) and \(a(R)\land (P)\); and so on.

This rule yields the desirable results for the two different sentences,

50. Every linguist knows and admires some philosopher.

formalised as,

51. \((\forall L,\exists P)(K)\land (A)\)

and

52. Every linguist knows some philosopher and every linguist admires some philosopher.

Formalised as,

53. \((\forall L,\exists P)K\land (\forall L,\exists P)A\)

According to Universal Quantification, (51) is true on a valuation just in case so are all formulas of the form, \((l,\exists P)(K)\land (A)\), where for \(l\) the formula \(lL\) is true. The formula \((l,\exists P)(K)\land (A)\) is true, according to Particular Quantification, just in case so is some formula of the form, \((l, p)(K)\land (A)\), where for \(p\) the formula \(pP\) is true. Next, according to Conjunctive Predication, \((l,p)(K)\land (A)\) is true just in case so is \((l,p)K\land (l,p)A\). Namely, (51) is true iff every linguist knows some philosopher and admires the same philosopher. By contrast, since (53) is true just in case so is each of its conjuncts, we shall not get that every linguist need admire a philosopher he knows.

2.4.4 Proofs

We add an introduction and an elimination rules for conjunctive predicates:

54. (Conjunctive Predication Introduction, CP‑I) Let \(P\) and \(Q\) be \(n\)‑place predicates, \(c_1, \ldots, c_n\) singular arguments.

    \(L\)	(\(i\))	\((c_1, \ldots, c_n)P \land (c_1, \ldots, c_n)Q\)
    \(L\)	(\(j\))	\((c_1, \ldots, c_n)(P)\land (Q)\)	CP‑I \(i\)

55. (Conjunctive Predication Elimination, CP‑E) Let P and Q be \(n\)‑place predicates, \(c_1, \ldots, c_n\) singular arguments.

    \(L\)	(\(i\))	\((c_1, \ldots, c_n)(P)\land (Q)\)
    \(L\)	(\(j\))	\((c_1, \ldots, c_n)P \land (c_1, \ldots, c_n)Q\)	CP‑E \(i\)

It is straightforward to see that soundness is preserved.

The completeness of Quarc on the truth-valuational approach is proved in Ben-Yami and Pavlović (2022) by adapting Henkin’s proof (1949). We won’t provide here the complete proof but only specify its features that are relevant for proving that the completeness of the system is preserved with the additional structures introduced in this paper. As part of the proof, a “Henkin Theory” is specified, consisting of all formulas falling under certain schemas. It is then shown that any valuation that respects the truth-value assignment rules for the connectives of the propositional calculus while making all the formulas of the Henkin Theory true, respects all the truth-value assignment rules of Quarc as well. Later, some of the formulas of the Henkin Theory are shown to be theorems of Quarc.

To prove that completeness is preserved, we should add to the Henkin theory the axiom schema,

56. \((c_1, \ldots, c_n)(P)\land (Q) \leftrightarrow ((c_1, \ldots, c_n)P \land (c_1, \ldots, c_n)Q)\)

Any valuation that respects the truth-value assignment rule for the connective \(\leftrightarrow\) while making all the formulas of this form true, clearly respects Conjunctive Predication (49) as well. And, given CP-I and CP-E, this is a schema of theorems of Quarc. See Henkin (1949) and Ben-Yami and Pavlović (2022) for further details.

We can now turn to a proof of the argument opening this subsection. We formalise it as follows:

We show that,

57. \((b, \forall S)(C \land H)^{2,1}, aS \vdash (a, b)C\)

2.5 Comparative Adjectives

58. Every giraffe is taller than every gnu.

    Some gnu is taller than every lion.

    Some lion is taller than some zebra.

    ∴ Every giraffe is taller than some zebra.

Most comparative adjectives are transitive: if Alice is younger than Bob, and Bob younger than Charlie, then Alice is younger than Charlie. It might thus seem that this transitivity is built into language as a formal rule, for any comparative adjective of the form, \(\phi\)‑er. There are, however, exceptions, as we learn from Rock–Paper–Scissors: in this game, paper is stronger or better than rock, rock is stronger than scissors, yet scissors is stronger than paper.

Such exceptions notwithstanding, we shall treat in this subsection comparative adjectives of the form \(\phi\)‑er as transitive. I do not think that the transitivity of adjectives of the \(\phi\)‑er structure is merely a frequent albeit contingent fact. Rather, we have here a rule of grammar which allows exceptions. That the past tense of “go” is “went” does not show it not to be a rule that the past tense of verbs is formed by adding “ed.” With comparative adjectives we have a different kind of rule and exception, concerning not syntax but meaning; yet this does not affect the fact that transitivity is a rule for the use of comparative adjectives, to be overridden only if the exception is explicitly introduced.

2.5.1 Vocabulary and formulas

We add to the language denumerably many two-place comparative predicates, \(P_\mathrm{er}\), \(Q_\mathrm{er}\), \(R_\mathrm{er}\)… No new formula rules.

2.5.2 Semantics

59. (Comparative Adjective Transitivity). Let \(P_\mathrm{er}\) be a comparative predicate, and \(c_1\), \(c_2\) and \(c_3\) singular arguments. If the truth-value assigned to \((c_1, c_2)P_\mathrm{er}\) and \((c_2, c_3)P_\mathrm{er}\) on a valuation is true, then that assigned to \((c_1, c_3)P_\mathrm{er}\) is also true.

2.5.3 Proofs

60. (Comparative Adjective Transitivity, CAT) Let \(P_\mathrm{er}\) be a comparative predicate, \(c_1\), \(c_2\) and \(c_3\) singular arguments.

Soundness is again immediate. Completeness is proved by adding to the Henkin theory all the formulas which fall under the schema,

61. \((c_1,c_2)P_\mathrm{er} \land (c_2,c_3)P_\mathrm{er} \rightarrow (c_1,c_3)P_\mathrm{er}\)

Any valuation that respects the truth-value assignment rules for the connectives \(\land\) and \(\rightarrow\) while making all the formulas of this form true, respects (59) as well. All formulas of this form are theorems of Quarc, provable from CAT. See again Ben-Yami and Pavlović (2022) for further details.

The proof of (58) is quite tedious and adds no interesting element to what we learn from proofs of simpler inferences. I shall therefore formalise and prove instead the following:

62. Every giraffe is taller than every wildebeest: \((\forall G,\forall W)T_\mathrm{er}\)

    Some wildebeest is taller than every lion: \((\exists W,\forall L)T_\mathrm{er}\)

    ∴ Every giraffe is taller than every lion: \((\forall G,\forall L)T_\mathrm{er}\)

We show that:

63. \((\forall G,\forall W)T_\mathrm{er}, (\exists W,\forall L)T_\mathrm{er} \vdash (\forall G,\forall L)T_\mathrm{er}\)

2.5.4 Asymmetry

Another property of comparative adjectives is asymmetry. If Alice is younger than Bob, then Bob isn’t younger than Alice. Unlike transitivity, asymmetry seems to have no exception for comparative adjectives.

This property can also be straightforwardly incorporated in Quarc. Nothing needs to be added to either vocabulary or formula rules. In the semantics, the rule should be that if \((c_1, c_2)P_\mathrm{er}\) is true on a valuation, then \((c_2, c_1)P_\mathrm{er}\) is false on it. And the rule of inference should allow the inference \((c_1,c_2)P_\mathrm{er} \vdash \lnot(c_2, c_1)P_\mathrm{er}\). We shall not develop this further here.

2.6 Defining Clauses

64. All skunks are mammals.

    ∴ All who fear all who respect all skunks fear all who respect all mammals.

Those who respect the skunks and mammals, as well as those who fear the former, are presumably not respectful triangles or fearful ideas, say. Which respectful and fearful “things” are referred to would depend on context, but something more specific does seem to be meant. We shall assume here that the conclusion is about creatures generally, and consider it as elliptical for,

65. All creatures who fear all creatures who respect all skunks fear all creatures who respect all mammals.

This will enable us to treat inference (64) by means of the extended, three-valued Quarc system developed in Lanzet (2017), which has the syntactic and semantic resources to represent defining clauses and can straightforwardly translate sentences such as (65).

One might object and claim that the conclusion of (64) is about absolutely everything. Triangles and ideas, so might one continue, also fall within its purview, only they happen not to fear or respect anything, ipso facto skunks and mammals. I find this approach unconvincing when applied to natural language, whose logic both Natural Logic and Quarc aim to represent. However, the issue need not be decided for the purpose of formalising inference (64) in Quarc: the means for representing absolute generality are provided in both Lanzet and Ben-Yami (2004) and Lanzet (2017), in each somewhat differently, by the introduction of a special predicate, Thing or \(T\). Very roughly, the idea is that everything is a Thing: for every constant \(c\), \(cT\) is true. (This special predicate also helps explore the relations between Quarc and the Predicate Calculus.) We shall not develop this idea further here, though, but continue with the assumption that a predicate with narrower application is assumed, and use creature as in (65).

The three-valued Quarc system of Lanzet (2017) is too complex to be fully presented in this paper. I shall therefore introduce only some of its features, which will enable us to get an idea of how sentence (65) and consequently inference (64) are handled by it. The reader is referred to Lanzet (2017) for a full exposition. Since we are not inquiring into decidability in this paper but leaving it as a subject for future work, neither shall we inquire whether a restricted, simpler yet complete and decidable version of that system suffices for the formalisation of the relevant arguments.

2.6.1 Compound Predicates

Consider the sentence,

66. Alice is a woman who knows Bob.

It is logically equivalent to,

67. Alice is a woman and Alice knows Bob.

While (67) is formalised in Quarc as,

68. \(aW \land (a,b)K\)

we shall formalise (66) by:

69. \(aW_x{:}(x,b)K\)

The chain of symbols, \(W_x{:}(x,b)K\), is considered a compound predicate.

More generally, if \(\phi [a]\) is a formula and \(P\) a one-place predicate, then \(P_x{:}\phi [x]\) is a compound predicate, which is also a one-place predicate. \(\phi [a]\) contains no occurrence of \(x\) (to avoid ambiguity), and \(x\) replaced some or all occurrences of \(a\) in \(\phi [a]\). \(P_x{:}\phi [x]\) can be read, \(P\) which is \(\phi\). \((b)P_x{:}\phi [x]\) is true on a valuation just in case \(bP\) and \(\phi [b/x]\) are true on that valuation.

With this in place, we can formalise the following compound predicates:

And we can now formalise sentence (65) as well, “All creatures who fear all creatures who respect all skunks fear all creatures who respect all mammals”:

70. \((\forall C_x{:}(x,\forall C_y{:}(y,\forall S)R)F,\forall C_y{:}(y,\forall M)R)F\)

2.6.2 Proofs

Lanzet (2017) develops a three-valued system, allowing for some formulas to lack a truth value. “All my children work in the coal mines” is neither true nor false when uttered by a childless person. Similarly, \(\exists SP\) and \(\forall SP\) will lack a truth value when \(S\) has no instances. If our conception of validity in a three-valued system is that truth entails truth, and this is Lanzet’s conception, then this three-valued framework complicates the proof system. The classical Negation Introduction rule, for instance, cannot be employed. In addition, some of the rules for quantifiers should be modified, because in some cases we should guarantee that the predicate occurring in the argument position, say \(P\), has instances. This can be done in several ways, one of them by having \((\exists P)P\) among our premises: this formula is true if and only if P has instances. For these two reasons, the \(\forall\)‑Introduction rule is replaced by two rules. Lanzet uses a proof system which operates on sequents, although resembling a natural deduction system in its inference rules. Adapting his rules to the system used in this paper, his \(\forall\)I1 rule will be:

Where \(\forall P\) governs \(\phi [\forall P]\) and \(c\) does not occur in \(L_1\) apart from \(i\), in \(L_2\) or in \(\phi [\forall P]\).

Returning to the inference with which we opened this subsection, on the conception of validity as truth entails truth, sentence (65), “All creatures who fear all creatures who respect all skunks fear all creatures who respect all mammals,” follows from “All skunks are mammals” only if we assume that the compound predicates in the conclusion’s argument positions, “creatures who fear all creatures who respect all skunks,” and “creatures who respect all mammals” have instances. Otherwise, if no one respected mammals, say, there would be no one to fear in the conclusion, and a true premise would have a conclusion which is neither true nor false.—We can develop a different conception of validity for three-valued systems, in which, instead of truth leading to truth, an argument is valid just in case, if its premises are not false, then its conclusion isn’t false either (Halldén 1949). Another option is to define validity for a three-valued system as, if the premises are true then the conclusion isn’t false (strict-to-tolerant validity, Cobreros et al. 2013). On either conception, a valid argument with true premises may have a conclusion which has no truth-value, and no additional premise should be added to (64). Both options are worth exploring, but here we shall limit ourselves to the option Lanzet adopts and take validity to mean, truth entails truth.

We should, therefore, add to (64) the two premises,

71. \((\exists C_x{:}(x,\forall C_y{:}(y,\forall S)R)F)C_x{:}(x,\forall C_y{:}(y,\forall S)R)F\)

72. \((\exists C_y{:}(y,\forall M)R)C_y{:}(y,\forall M)R\)

and show the following:

73. \(\forall SM\),
    \((\exists C_x{:}(x, \forall C_y{:}(y, \forall S)R)F)C_x{:}(x, \forall C_y{:}(y, \forall S)R)F\),
    \((\exists C_y{:}(y, \forall M)R)C_y{:}(y, \forall M)R\)   \(\vdash\)
    \((\forall C_x{:}(x, \forall C_y{:}(y, \forall S)R)F, \forall C_y{:}(y, \forall M)R)F\)

The proof is long and requires familiarity with the rules of Lanzet (2017), so instead of providing it we shall show that the inference is valid. Since the system of that paper was proved there to be complete, it follows that the inference can be proved.

We see that inference (64) can be incorporated in an existing powerful version of Quarc. Moreover, in the process, Quarc has brought to light two features of Moss’s original formulation which needed to be addressed: completion of an ellipsis and making two presuppositions explicit. We therefore proved here a revised inference, (73).

2.7 Comparative Quantifiers

74. More students than professors run.

    More professors than deans run.

    ∴ More students than deans run.

The four kinds of inference we discussed above did not pose serious issues for their incorporation in Quarc, syntactically, semantically, or proof-theoretically. The active–passive-voice distinction and defining clauses were already incorporated in Quarc, the latter in a three-valued version of it; and conjunctive predicates and comparative adjectives required rather straightforward extensions for their incorporation. Comparative quantifiers, however, pose several challenges, only some of which will be met in this paper.

The quantifiers of Quarc, \(\exists\) and \(\forall\), translate natural language’s “some,” “a,” “all,” “any” and “every” in various of their uses. All these quantifiers are unary determiners: they attach to one general noun to form a noun phrase. “Some boys,” “a girl,” “all men,” “any woman” and “every person” are a few examples. This is also true of some other natural language quantifiers, for instance three, at least seven, infinitely many, most and many. Translating these quantifiers in Quarc will require additional vocabulary but not additional syntactic roles.

By contrast, comparative quantifiers, in their use exemplified in (74), are binary determiners: they attach to two general nouns to form a noun-phrase. As, for instance, in “more students than professors” and “more professors than deans” (Ben-Yami 2009). Translating them into Quarc will therefore necessitate an additional syntactic role: a quantifier which attaches to an ordered pair of one-place predicates to form a quantified argument.

2.7.1 Vocabulary and Formulas

We add a new binary quantifier, \(\Pi\), read “more.” If \(P\) and \(Q\) are one-place predicates, then \(\Pi (P,Q)\) is a binary quantified argument.

2.7.2 Semantics

To capture the truth-conditions of “more” within a truth-valuational substitutional semantics, as well as those of many other, unary quantifiers—e.g. “three,” “at least seven,” “many” and “most”—we should overcome a difficulty related to the fact that several names might name the same thing (Lewis 1985). Suppose we defined “Two men married Olivia Langdon” as true if there are two different substitution instances of names for “two men,” each verifying “\(x\) is a man,” which yield a true sentence of the form, “\(x\) married Olivia Langdon.” We would then get that the sentence is true, since both “Mark Twain is a man” and “Samuel Clemens is a man” are true, as are “Mark Twain married Olivia Langdon” and “Samuel Clemens married Olivia Langdon.” Yet Mark Twain is Samuel Clemens, and only this single man married Olivia Langdon.

To overcome this difficulty, we first define for each one-place predicate \(P\) on each valuation \(\mathfrak{V}\) a maximal substitution set \(\mathfrak{S}\). This is a set for which,

• only names \(a\) for which \(aP\) is true on \(\mathfrak{V}\) are in \(\mathfrak{S}\).

• for any different \(a\) and \(b\) in \(\mathfrak{S}\), \(a=b\) is false on \(\mathfrak{V}\)

• for any \(c\) for which \(cP\) is true on \(\mathfrak{V}\), \(a=c\) is true on \(\mathfrak{V}\) for some \(a\) in \(\mathfrak{S}\), possibly \(c\) itself.

In this way we make sure that every \(P\) is counted exactly once, so to say, by the names in \(P\)’s maximal substitution set. It is easy to show that on each valuation, all maximal substitution sets of a given predicate have the same number of members, or cardinality.

We can now define the truth value of a formula \(\phi [\Pi(P,Q)]\), governed by \(\Pi(P,Q)\), on a valuation \(\mathfrak{V}\). We consider two maximal substitution sets \(\mathfrak{S}_P\) and \(\mathfrak{S}_Q\). \(\phi [\Pi(P,Q)]\) is true on \(\mathfrak{V}\) just in case more substitution cases of the form, \(\phi [a/\Pi(P,Q)]\) with \(a \in \mathfrak{S}_P\) are true on \(\mathfrak{V}\) than such substitution instances with \(a \in \mathfrak{S}_Q\).

Turning to inference (74), we can formalise it and show the validity of the formalisation in Quarc. Its formalisation will be,

75. \((\Pi(S,P))R, (\Pi(P,D))R \models (\Pi(S,D))R\)

We have to show that if both premises are true on a valuation \(\mathfrak{V}\), then so is the conclusion. We choose three maximal substitution sets on \(\mathfrak{V}\), \(\mathfrak{S}_S\), \(\mathfrak{S}_P\) and \(\mathfrak{S}_D\). If \((\Pi(S,P))R\) is true on \(\mathfrak{V}\), then there are more members \(a\) in \(\mathfrak{S}_S\) for which \(aR\) is true on \(\mathfrak{V}\) than members \(b\) in \(\mathfrak{S}_P\) for which \(bR\) is true on \(\mathfrak{V}\); and similarly, there are more such members \(b\) than members \(c\) of \(\mathfrak{S}_D\) for which \(cR\) is true on \(\mathfrak{V}\). So there are more members \(a\) in \(\mathfrak{S}_S\) for which \(aR\) is true on \(\mathfrak{V}\) than members \(c\) in \(\mathfrak{S}_D\) for which \(cR\) is true on \(\mathfrak{V}\). Accordingly, \((\Pi(S,D))R\) is true on \(\mathfrak{V}\).

2.7.3 Proofs

This is the part of the challenge comparative quantifiers pose which will not be met in this work. How is it possible to reflect the logic of the quantifier \(\Pi\) in a proof system, is a question we shall here leave unanswered. In fact, even the more basic question, whether it is possible to capture content by form for \(\Pi\) in argument–predicate sentences, will not be addressed here either.

To the best of my knowledge, Moss does not try to incorporate inference (74) or the quantifier “more,” as used in argument–predicate sentences, in his Natural Logic systems (but see below on the use of this quantifier in ‘existential’ sentences). In Moss (2015), he mentions inference (74) in order to show the apparent inadequacy of first-order logic as a means of representing the logic of natural language:

[In] the first-order language with one-place relations student(\(x\)), professor(\(x\)), and run(\(x\)), there is no first-order sentence \(\phi\) with the property that for all (finite) models \(M\), \(\phi\) is true in \(M\) if and only if “More students than professors run” is true in \(M\) in the obvious sense. This failure already suggests that first-order logic might not be the best “host logical system” for natural language inference. (2015, 563)

I agree with Moss on what he takes this inability to suggest. (See also Ben-Yami 2009 for a discussion of generalised quantifiers and comparative quantifiers.) What we managed to show in this paper is that Quarc does not have this shortcoming as a system for representing the logic of natural language. Quarc can incorporate natural language’s comparative quantifiers as binary quantifiers, imitating their natural language syntax, and it does that by providing the correct truth conditions for these sentences. We saw this being done for “more” with a truth-valuational substitutional semantics; the way to generalise this approach to other comparative quantifiers (e.g. “at least as many”) or construct a model-theoretic semantics for them is straightforward. Accordingly, we have managed to show an advantage of Quarc over the Predicate Calculus in this respect.

2.7.4 Comparative Quantifiers in “Existential” Sentences

In more recent work, Moss and Topal extended Natural Logic and applied it to sentences of the form, “There are at least as many \(p\) as \(q\)” and “There are more \(p\) than \(q\)” (2016; 2020) (see fn. 4). They have developed sound and complete proof systems for cardinality comparisons, for both finite (Moss 2016) and infinite sets (Moss and Topal 2020). This is impressive work, and it would be interesting to inquire whether Quarc can deliver anything comparable. This, however, will not be attempted in this paper, for several reasons.

There are obvious space considerations. For instance, the proof system of Moss (2016) contains 24 rules, of which 16 involve his formalisations of “at least as many” and “more”; the corresponding numbers for the proof system of Moss and Topal (2020) are 21 and 12. Accordingly, a Quarc system formalising these inferences might involve significantly more additions than the extended systems considered above. Similarly, a completeness proof for this extended system would not be established by minor additions to the one provided in Ben-Yami and Pavlović (2022). This is a topic for a separate paper.

Moreover, a Quarc treatment of sentences of the form, “There are at least as many \(p\) as \(q\)” and “There are more \(p\) than \(q\),” will depart from Moss’s in some important fundamental respects. Moss formalises these sentences by sentences similar in form to those formalising “All/some \(p\) are/aren’t \(q\).” For instance, “Some \(p\) are \(q\)” is formalised by \(\exists(p,q)\), and “There are more \(p\) than \(q\)” by \(\exists^{>}(p,q)\). Namely, apart from the different quantifier, no syntactic distinction is drawn between the argument–predicate sentence, “Some \(p\) are \(q\),” in which the argument is “some \(p\),” and the so-called existential sentence, “There are \(x\),” in which \(x\) is a noun phrase formed by a comparative quantifier, “more \(p\) than \(q\).” However, the existential sentence, “There are more \(p\) than \(q\)” is no argument–predicate one. A sentence similar to it in form using the quantifier “some” will be, “There are some \(p\),” and not, “Some \(p\) are \(q\).” An argument–predicate sentence with the quantifier “more” would have the form of the sentence considered above, “More students than professors run.” As mentioned earlier, Moss hasn’t developed a proof system for these sentences.

The distinction between existential sentences and argument–predicate sentences seems to be a linguistic universal. Moreover, existential sentences show important differences from quantified argument–predicate ones (Ben-Yami 2004, sec. 6.5; Francez, I. 2009; McNally 2011). Accordingly, a system that aims to be a logic for natural language informed by the latter’s syntax should formalise existential sentences differently than it does argument–predicate ones. It should distinguish the two constructions and explore the logical relations between them. As part of such a general treatment of existential sentences, those with a noun-phrase of the form “more \(p\) than \(q\)” as their pivot (see Francez, I. 2009; McNally 2011 for the terminology) can also be introduced and discussed, as well as those with other comparative quantifiers. A general inquiry into the logic and formalisation of existential sentences has not been attempted by Moss and shall not be attempted here either.

3 Conclusions and Future Work

This paper tried to assess the ability of Quarc, in its current or extended versions, to represent the kinds of inference which have served as the basis of Moss’s constructions of Natural Logic systems. We have shown how Quarc can incorporate, sometimes with some extensions, passive–active voice distinctions, conjunctive predicates (see and hear), comparative adjectives (taller), and defining clauses (who respect all mammals). All these were incorporated within sound and complete systems. We have also shown how Quarc can be syntactically extended to incorporate comparative quantifiers (more … than …) and provided a semantics but not a proof system for this extension.

All this was done by using a language with a syntax close to that of natural language. In this respect we followed Moss’s dictum for his Natural Logic project, “logic for natural language, logic in natural language” (2015, 563). I believe that in some respects we improved on Natural Logic, for instance by not using negative nouns.

The process also helped shed light on some of the inferences we discussed. The constraints of the formal system brought us to recognise an ellipsis and presuppositions involved in the conclusion of inference (64), “All who fear all who respect all skunks fear all who respect all mammals.”

A main aim of the Natural Logic project which we did not address here was the question of decidability. Apart from the theoretical interest, this is relevant to questions of the applicability of computer programmes for determining validity. I hope this question will be addressed in future work, by myself or others.

Another topic which was not addressed in this paper but which has engaged Natural Logic is that of monotonicity (Moss 2015, sec. 4). Moss’s work is based on van Benthem’s (1986, 1991), which generated additional inquiries as well (see van Benthem 2008 for a historical survey). Whether and how can Quarc analyse the phenomena of monotonicity is again left for future work.

The last topic mentioned as subject for future work is the formalisation of the so-called existential sentences—“There are \(x\)”—in Quarc. Once this is done, existential sentences with comparative quantifiers—“There are more \(p\) than \(q\)” and “There are at least as many \(p\) as \(q\)”—can also be formalised, and Moss’s work on these last sentences can be comparatively studied.

So, there is still work to be done. Yet hopefully, we have shown that in addition to the earlier successes in its application to the analysis of the logic of natural language, Quarc can also represent the inferences that motivated Moss’s Natural Logic.