=Paper=
{{Paper
|id=Vol-2585/paper1
|storemode=property
|title=Tableaux for Murphree's numerical term logic
|pdfUrl=https://ceur-ws.org/Vol-2585/paper1.pdf
|volume=Vol-2585
|authors=J.-Martín Castro-Manzano
|dblpUrl=https://dblp.org/rec/conf/lanmr/Castro-Manzano19
}}
==Tableaux for Murphree's numerical term logic==
https://ceur-ws.org/Vol-2585/paper1.pdf
Tableaux for Murphree’s numerical term logic
J.-Martı́n Castro-Manzano
Faculty of Philosophy, UPAEP University
21 sur 1103, Puebla, Mexico
josemartin.castro@upaep.mx
Abstract. Murphree’s Numerical Term Logic is a logic capable of repre-
senting and performing inference with numerical quantifiers by modifying
Sommers Term Functor Logic: in this contribution we offer a tableaux
method for it.
Keywords: Semantic trees, term logic, numerical term logic.
1 Introduction
In other places we have developed tableaux for Sommers’ Term Functor Logic
[19,8,21], Intermediate Term Functor Logic à la Thompson [23], and Englebret-
sen’s Modal Term Logic [7]. In this contribution we continue our exploration into
the realm of term logics and, by using Murphree’s Numerical Term Logic [13],
we present tableaux for a family of term logics comprising Term Functor Logic,
Intermediate Term Functor Logic, and Numerical Term Logic. Hence, for a more
detailed exposition of Term Functor Logic and its tableaux, we refer the reader
to our previous work [4]. Meanwhile, in order to achieve our present goal, we first
provide a summary of some preliminary concepts (syllogistic, term functor logic,
and term functor logic tableaux), then we explain the basics of Murphree’s logic
(namely, its syntax and rules) and, finally, we develop tableaux for it (including
some metalogical results).
2 Preliminaries
2.1 Syllogistic
Syllogistic is a term logic that has its origins in Aristotle’s Prior Analytics [1] and
deals with inference between categorical propositions. A categorical proposition
is a proposition composed by two terms, a quantity, and a quality. The subject
and the predicate of a proposition are called terms: the term-schema S denotes
the subject term of the proposition and the term-schema P denotes the predicate.
The quantity may be either universal (All ) or particular (Some) and the quality
may be either affirmative (is) or negative (is not). These categorical propositions
have a type denoted by a label (either a (universal affirmative, SaP), e (universal
negative, SeP), i (particular affirmative, SiP), or o (particular negative, SoP))
Copyright © 2019 for this paper by its authors. Use permitted under Creative Commons License
Attribution 4.0 International (CC BY 4.0)
1
that allows us to determine a mood, that is, a sequence of three categorical
propositions ordered in such a way that two propositions are premises and the
last one is a conclusion. A categorical syllogism, then, is a mood with three terms
one of which appears in both premises but not in the conclusion. This particular
term, usually denoted with the term-schema M, works as a link between the
remaining terms and is known as the middle term. According to the position of
this middle term, four figures can be set up in order to encode the valid syllogistic
moods (Table 1).1
First Second Third Fourth
figure figure figure Figure
aaa eae iai aee
eae aee aii iai
aii eio oao eio
eio aoo eio
Table 1: Valid syllogistic moods
2.2 Term Functor Logic
Term Functor Logic (TFL) [18,19,21,6,8,9] is basically a plus-minus algebra that
employs terms rather than first order language elements such as individual vari-
ables or quantifiers (cf. [17,14,10,19,20,11]). According to this algebra, the four
categorical propositions can be represented by the following syntax [8]:
a. SaP := −S + P
b. SeP := −S − P
c. SiP := +S + P
d. SoP := +S − P
Given this representation, this plus-minus algebra provides a simple rule for
syllogistic inference: a conclusion follows validly from a set of premises if and
only if i) the sum of the premises is algebraically equal to the conclusion and
ii) the number of conclusions with particular quantity (viz., zero or one) is the
same as the number of premises with particular quantity [8, p.167]. Thus, for
instance, if we consider a valid syllogism, say the mood aaa from the first figure
(i.e. aaa-1), we can see how the application of this method produces the right
conclusion (Table 2).
In the previous example we can clearly see how the method works:
i) if we add up the premises we obtain the algebraic expression
1
For sake of brevity, but without loss of generality, here we omit the syllogisms that
require existential import.
2
Proposition TFL
1. All dogs are animals. −D + A
2. All German Shepherds are dogs. −G + D
` All German Shepherds are animals. −G + A
Table 2: A valid syllogism: aaa-1
(−D + A) + (−G + D) = −D + A − G + D = −G + A, so that the sum of the
premises is algebraically equal to the conclusion and the conclusion is −G + A,
rather than +A − G, because ii) the number of conclusions with particular quan-
tity (zero in this case) is the same as the number of premises with particular
quantity (zero in this case).
2.3 TFL tableaux
As in [4], we say a tableau is an acyclic connected graph determined by nodes
and vertices [5,16]. The node at the top is called root. The nodes at the bottom
are called tips. Any path from the root down a series of vertices is a branch. To
test an inference for validity we construct a tableau which begins with a single
branch at whose nodes occur the premises and the rejection of the conclusion:
this is the initial list. We then apply the rules that allow us to extend the initial
list (Diagram 1.1).
−A ± B +A ± B
−Ai ±Bi +Ai
±Bi
Diagram 1.1: TFL tableaux rules
In Diagram 1.1, from left to right, the first rule is the rule for a (e) propo-
sitions, and the second rule is the rule for i (o) propositions. Notice that, after
applying a rule, we introduce some index i ∈ {1, 2, 3, . . .}. For propositions a and
e, the index may be any number; for propositions i and o, the index has to be a
new number if they do not already have an index. Also, following TFL tenets,
we assume the followings rules of rejection: −(±A) = ∓A, −(±A ± B) = ∓A ∓ B,
and −(− − A − −A) = +(−A) + (−A).
As usual, a tableau is complete if and only if every rule that can be applied
has been applied. A branch is closed if and only if there are terms of the form ±Ai
and ∓Ai on two of its nodes; otherwise it is open. A closed branch is indicated
by writing a ⊥ at the end of it; an open branch is indicated by writing ∞. A
tableau is closed if and only if every branch is closed; otherwise it is open. So,
3
again as usual, A is a logical consequence of the set of terms Γ (i.e. Γ ` A) if and
only if there is a complete closed tableau whose initial list includes the terms of
Γ and the rejection of A (i.e. Γ ∪ {−A} ` ⊥). Accordingly, up next we provide
some examples for basic syllogistic (Diagram 1.2).
−M + P −M + P
−S + M +S + M
` −S + P ` +S + P
−(−S + P) −(+S + P)
+S − P −S − P
+S1 +S1
−P1 +M1
−S1 +M1 −M1 +P1
⊥ ⊥
−M1 +P1 −S1 −P1
⊥ ⊥ ⊥ ⊥
−M − P −M − P
−S + M +S + M
` −S − P ` +S − P
−(−S − P) −(+S − P)
+S + P −S + P
+S1 +S1
+P1 +M1
−S1 +M1 −M1 −P1
⊥ ⊥
−M1 −P1 −S1 +P1
⊥ ⊥ ⊥ ⊥
Diagram 1.2: Moods aaa-1, eae-1, aii-1, and eio-1
3 Murphree’s Numerical Term Logic
In Szabolcsi’s view [22, p.3], quantification within first order logic systems is
“extremist” in the sense that it is limited to represent two extremes: either ev-
erything or something.2 Indeed, it is usual to find logical treatments that assume
that intermediate or subjective quantifiers [22, p.26ff] such as “many”, “most”,
2
This is not completely true because, for example, we have the proposals developed
by [12,24] (however, since these are not part of first order logic prima facie and
4
or “few” (cf. [15,23]) have to be treated as simple cases of existential quantifiers,
and numerical or objetive quantifiers usually suffer the same fate. However, such
a treatment is far from being justified. There are several reasons to support this
claim, but in the interest of time, consider that reasoning in natural language
includes more quantifiers than the usual “all” or “some”. For instance, regard
that both “most” and “some” are particular (i.e. non-universal) quantifiers, but
they do not express the same meaning: the former implies the latter, but the
converse is false; and the same occurs when reasoning with numerical quantifiers.
Given this situation, Murphree [13], and Szabolcsi [22] developed numerical ex-
tensions of Sommers’ Term Functor Logic: in this work, however, we focus only
on Murphree’s [13].
Murphree’s Numerical Term Logic (NTL) is a term logic capable of repre-
senting and performing inference with numerical quantifiers by modifying TFL’s
syntax and rule of inference. Thus, NTL offers the following syntax for numeri-
cally quantified propositions:
e. All but n S are P := −n S + P
f. At most n S are P := −n S − P
g. At least n S are P := +n S + P
h. At least n S are not P := +n S − P
To better explain this representation, consider the next examples:
1. At least 15 Americans are republicans := +15 A + R
2. All but 120 students understand logic := −120 S + U
3. At most 150,000 Europeans are male := −150,000 E − A
4. There are at least 33 mathematicians := +33 M + M
5. At least 66 logicians are not democrats := +66 L − D
Now, at this point it is important to notice that when n = 0 (n = 1), the
traditional universal (particular) categorical propositions are included within
NTL:
6. All S is P = All but 0 S are P := −0 S + P
7. No S is P = At most 0 S are P := −0 S − P
8. Some S are P = At least 1 S is P := +1 S + P
9. Some S are not P = At least 1 S is not P := +1 S − P
Also, by adapting some ideas by Szabolcsi, in NTL we can represent exact
(10), fractionary (12), and subjective (13) quantifiers. This last example shows
in what sense the intermediate propositions of Intermediate Term Functor Logic
(TFL+ ) are included within NTL:
10. Exactly n S are P := +(+n−1 S + P) + (−n S − P)
11. At most r/q of S are P := −r/q S − P
they are developed by and for first order languages, we omit their treatment in this
contribution) and, in all fairness, we can charge TFL with the same offense.
5
12. Many S are P := +m S + P
Given these syntactical tweaks, NTL modifies TFL’s rule of inference as
follows: a conclusion follows validly from a set of premises if and only if i) the
sum of the premises is algebraically equal to the conclusion, ii) the number of
conclusions with particular quantity (viz., zero or one) is the same as the number
of premises with particular quantity, and iii) either (a) the value of a universal
conclusion is equal to the sum of the values of the universal premises, or (b)
the value of a particular conclusion is equal to the difference of the universal
premise minus the particular.3 Hence, TFL and TFL+ are sublogics of NTL. To
exemplify NTL, let us consider some valid inferences (Tables 3-6).
Proposition NTL
1. All but 6 philosophers are logical. −6 P + L
2. All but 20 smart people are philosophers. −20 S + P
` All but 26 smart people are logical. −26 S + L
Table 3: A valid numerical syllogism (adapted from [13])
Before we move on, and in order to reach our goal, we need to make a little
syntax modification that will come in handy in due time: we add the predicate
term of a proposition an arbitrary natural number e > n for any other natural
n. This results in the following syntax for NTL:
e’. All but n S are P := −n S +e P
f’. At most n S are P := −n S −e P
g’. At least n S are P := +n S +e P
h’. At least n S are not P := +n S −e P
Proposition NTL
1. All but 11 anarchists are logicians. −11 A +e L
2. At least 30 Mexicans are anarchists. +30 M +e A
` At least 19 Mexicans are logicians. +19 M +e L
Table 4: A valid numerical syllogism (adapted from [13])
3
This last condition is different from Szabolcsi’s, who considers that the value of the
premises need be equal or greater than the value of the conclusion (cf. [22, p.45].
6
Proposition NTL
1. Most guys are friendly. −m G +e F
2. All those who are friendly are tolerant. −0 F +e T
` Most guys are tolerant. −m G +e T
Table 5: A valid numerical syllogism (adapted from [22, p.53])
Proposition NTL
1. All but 3 teachers gave 4 books to all but 5 students. −3 T + (+(+e G +4 B) −5 S)
2. All but 2 teachers are underpaid persons. −2 T +e U
3. Every book is expensive −0 B +e E
4. All but 7 students are ingrates. −7 S +e I
5. There are at least 50 students. +50 S +e S
6. There are at least 10 teachers. +10 T +e T
` At least 5 underpaid persons gave 4 expensive +5 U + (+(+e G +4 E) +38 I)
things to 38 ingrates.
Table 6: A valid numerical syllogism (adapted from [13])
With these elements, we now introduce the tableaux rules for NTL in Dia-
gram 1.3: from left to right, the first rule is for universal propositions, the second
rule is for particular propositions. Notice that after applying a rule we introduce
some index i ∈ {1, 2, 3, . . .} just as in TFL tableaux; but also, notice that after
applying a rule we create a vector v by keeping track of the numerical value n
of the proposition. The third diagram, on the other hand, is a rule for ordering
atomic terms with a “+” attached. Now, given these rules, we say A is a logi-
cal consequence of the set of terms Γ if and only if there is a complete closed
tableau whose initial list includes the terms of Γ and the rejection of A, and
v = 0. Accordingly, up next we show some examples of valid inferences (Dia-
grams 1.4 and 1.5) and then we argue that a valid inference in NTL produces a
closed complete tree with v = 0 and vice versa.
−n A ±e B +n A ±e B +n A
− n A i ± e Bi +n Ai +k≤n A
v=n
±e Bi
v=n
Diagram 1.3: NTL tableux rules
7
−6 C +e L −11 A +e L −m G +e F
−20 S +e C +30 M +e A −0 F +e T
` −26 S +e L ` +19 M +e L ` − m G +e T
−(−26 S +e L) −(+19 M +e L) −(−m G +e T)
+26 S −e L −19 M −e L +m G −e T
+26 S1 +30 M1 +m G1
− e L1 +e A1 −e T1
+20 S1 +19 M1 −m G1 +e F1
⊥
−20 S1 +e C 1 −19 M1 −e L1 +0 F1
⊥ ⊥
+6 C1 +11 A1 −0 F1 +e T1
⊥ ⊥
−6 C 1 +e L1 −11 A1 +e L1 v = +m − m − 0 = 0
⊥ ⊥ ⊥ ⊥
v = +26 − 20 − 6 = 0 v = +30 − 19 − 11 = 0
Diagram 1.4: From left to right, tableaux for Tables 3, 4, and 5
Proposition 1 A valid inference in NTL is a closed complete tree with v = 0.
Proof. Consider that a valid inference in NTL may be of two basic general forms
(Table 7).
Form 1 Form 2
1. −n X ±e Y −n X ±e Y
2. −m Z ±e X +m+n Z ±e X
` −n+m Z ±e Y +m Z ±e Y
Table 7: Basic general forms of a valid inference in NTL
Now, besides these two general forms, we must consider two cases. For the
base case let us consider each basic form. For form 1, take n = m = 0, and for
form 2 take n = 0 and m = 1. Hence, NTL collapses with TFL, in which case
we just obtain closed complete trees in TFL. For the inductive case, take n = k
and m = j. Such a replacement yields a valid inference in NTL, since all the
conditions of a valid inference in NTL are preserved. Now, suppose that each
form is also valid in NTL for n = k + 1 and m = j + 1 for k, j > 0, then the trees
would look as follows:
8
−3 T + (+(+e G +4 B) −5 S)
−2 T +e U
−0 B +e E
−7 S +e I
+50 S +e S
+10 T +e T
` +5 U + (+(+e G +4 E) +38 I
−(+5 U + (+(+e G +4 E) +38 I)
−5 U − (+(+e G +4 E) +38 I
+50 S1
+ e S1
+10 T2
+e T2
+2 T2
−2 T2 +e U2
⊥
+7 S1
−7 S1 +e I1
⊥
+38 I1
+3 T2
−3 T2 +(+e G +4 B) −5 S2
⊥
+e G2
+4 B2
− 5 S2
+0 B2
−0 B2 +e E2
⊥
+ 4 E2
+5 U 2
−5 U2 −(+(+e G +4 E) +38 I2
⊥ −(+e G +4 E) −38 I2
−38 I1 −(+e G +4 E)1
⊥ − e G − 4 E1
−e G2 −4 E2
⊥ ⊥
v = +50 + 10 − 2 − 7 − 3 + 4 − 5 − 0 − 5 − 38 − 4 = 0
Diagram 1.5: Tableau for Table 6
9
−k+1 X ±e Y −k+1 X ±e Y
−j+1 Z +e X +k+j+2 Z +e X
` −k+j+2 Z ±e Y ` +j+1 Z ±e Y
−(−k+j+2 Z ±e Y) −(+j+1 Z ±e Y)
+k+j+2 Z ∓e Y −j+1 Z ∓e Y
+k+j+2 Z1 +k+j+2 Z1
∓e Y1 +e X1
+k+j+2>j+1,∀k,j>0 Z1 +k+j+2>j+1,∀k,j>0 Z1
−j+1 Z1 +e X1 −j+1 Z1 ∓e Y 1
⊥ ⊥
+e>k+1,∀k X1 +e>k+1,∀k X1
−k+1 X1 ±e Y1 −k+1 X1 ±e Y 1
⊥ ⊥ ⊥ ⊥
v = +k + j + 2 − (j + 1) − (k + 1) = 0 v = +k + j + 2 − (j + 1) − (k + 1) = 0
Proposition 2 A closed complete tree with v = 0 is a valid inference in NTL.
Proof. Suppose there is a closed complete tree with v = 0 that is not a valid
inference in NTL. Then there is a closed complete tree whose initial list includes
a set of terms Γ , the rejection of the conclusion and v = 0, but from Γ we cannot
develop a proof of the conclusion by following the rules of NTL. Without loss of
generality, consider the trees corresponding to the valid basic forms of Table 7.
Then we have two alternatives whose conclusions are, respectively, −n+m X ±e Y,
and +m X ±e Y. Now, since each tree is complete, the rules for generating the
trees have been applied; and since each tree is closed, each tree has to have the
following forms:
Γ Γ
` −n+m X ±e Y ` +m X ±e Y
−(−n+m X ±e Y) −(+m X ±e Y)
+n+m X ∓e Y −m X ∓e Y
+n+m Xi +n+m Xi ∈ Γ
∓e Y i ±e Y i ∈ Γ
. +m Xi
.
.
.
.
.
−n+m Xi ∈ Γ ±e Y i ∈ Γ
−m Xi ∓e Yi
⊥ ⊥
⊥ ⊥
10
Suppose, then, that we have an instance of the first tree but that the re-
sulting proof is not valid, that is to say, where Γ + = Γ ∪ {+n+m X ∓e Y},
Γ + ` ⊥, but the application of the rule of inference to Γ does not allow us
to produce −n+m X ±e Y. Now, since the tree of the diagram is complete, all the
tips are closed, hence the previous nodes have to include something of the form
−m+n X ±e Y or −m Z ±e Y and −n X +e Z, that is to say, Γ = {−m+n X ±e Y}
or Γ = {. . . , −m Z ±e Y, −n X +e Z, . . .}. But then, in any case, if we apply con-
dition i) to Γ we obtain something of the form −X ±e Y, and not the other
way around due to condition ii); and last, by condition iii)(a), the conclusion
has to be of the form −m+n X ±e Y. But that contradicts the assumption that
we cannot develop a proof of such conclusion by using the rule of NTL. The
same occurs, mutatis mutandis, for the second tree. Thus, Γ = {+m X ±e Y} or
Γ = {. . . , −n Z ±e Y, +m+n X +e Z, . . .}. In any case, if we apply condition i) to
Γ we obtain something of the form +m X ±e Y, and not the other way around
due to condition ii); and last, by the condition iii)(b), the conclusion has to be
something of the form +m X ±e Y. But that contradicts the assumption that we
cannot develop a proof of such conclusion.
4 Conclusions
In this contribution we have attempted to offer a tableaux method for a family of
term logics comprising Term Functor Logic, Intermediate Term Functor Logic,
and Numerical Term Logic by using and adapting Murphree’s system. This is
possible because TFL and TFL+ are sublogics of NTL and so, in some sense,
the method we have developed for NTL represents this family of Sommersian
term logics. Now, we have to mention that for the purposes of this paper we
have focused only on the terministic features of NTL, but further comparison
is required with the algebraic proof systems introduced by [3,2]; and alterna-
tive term logics like Szabolcsi’s [22], for they may have more or less the same
motivation but not the same rules.
Acknowledgments
We would like to thank the anonymous reviewers for their precise corrections
and useful comments. Financial support given by UPAEP Research Grant.
References
1. Aristotle. Prior Analytics. Hackett Classics Series. Hackett, 1989.
2. Walter A. Carnielli. Polynomial ring calculus for many-valued logics. In 35th
International Symposium on Multiple-Valued Logic (ISMVL’05), pages 20–25, May
2005.
3. Walter A. Carnielli. A polynomial proof system for lukasiewicz logics. In Second
Principia International Symposium, August 6-10, 2001.
11
4. J.-Martı́n Castro-Manzano and Paniel-O. Reyes-Cárdenas. Term functor logic
tableaux. South American Journal of Logic, 4(1):1–22, 2018.
5. Marcello D’Agostino, Dov M. Gabbay, Reiner Hähnle, and Joachim Posegga. Hand-
book of Tableau Methods. Springer, 1999.
6. George Englebretsen. The New Syllogistic. 05. P. Lang, 1987.
7. George Englebretsen. Preliminary notes on a new modal syllogistic. Notre Dame
J. Formal Logic, 29(3):381–395, 06 1988.
8. George Englebretsen. Something to Reckon with: The Logic of Terms. Canadian
electronic library: Books collection. University of Ottawa Press, 1996.
9. George Englebretsen and Charles Sayward. Philosophical Logic: An Introduction
to Advanced Topics. Bloomsbury Academic, 2011.
10. Steven T. Kuhn. An axiomatization of predicate functor logic. Notre Dame J.
Formal Logic, 24(2):233–241, 04 1983.
11. Larry Moss. Natural logic. In S. Lappin and C. Fox, editors, The Handbook of
Contemporary Semantic Theory. John Wiley & Sons, 2015.
12. Andrzej Mostowski. On a generalization of quantifiers. Fundamenta Mathematicae,
44(2):12–36, 1957.
13. Wallace A. Murphree. Numerical term logic. Notre Dame J. Formal Logic,
39(3):346–362, 07 1998.
14. Aris Noah. Predicate-functors and the limits of decidability in logic. Notre Dame
J. Formal Logic, 21(4):701–707, 10 1980.
15. Philip L. Peterson. On the logic of “few”, “many”, and “most”. Notre Dame J.
Formal Logic, 20(1):155–179, 01 1979.
16. Graham Priest. An Introduction to Non-Classical Logic: From If to Is. Cambridge
Introductions to Philosophy. Cambridge University Press, 2008.
17. Willard Van Orman Quine. Predicate functor logic. In J E Fenstad, editor, Pro-
ceedings of the Second Scandinavian Logic Symposium. North-Holland, 1971.
18. Fred Sommers. On a fregean dogma. In Imre Lakatos, editor, Problems in the
Philosophy of Mathematics, volume 47 of Studies in Logic and the Foundations of
Mathematics, pages 47 – 81. Elsevier, 1967.
19. Fred Sommers. The Logic of Natural Language. Clarendon Library of Logic and
Philosophy. Clarendon Press; Oxford: New York: Oxford University Press, 1982.
20. Fred Sommers. Intelectual autobiography. In David S. Oderberg, editor, The Old
New Logic: Essays on the Philosophy of Fred Sommers, pages 1 – 24. Bradford
book, 2005.
21. Fred Sommers and George Englebretsen. An Invitation to Formal Reasoning: The
Logic of Terms. Ashgate, 2000.
22. L. Szabolcsi and G. Englebretsen. Numerical Term Logic. Edwin Mellen Press,
2008.
23. Bruce Thompson. Syllogisms using “few”, “many”, and “most”. Notre Dame J.
Formal Logic, 23(1):75–84, 01 1982.
24. Dag Westerståhl. Aristotelian syllogisms and generalized quantifiers. Studia Logica,
48(4):577–585, Dec 1989.
12