A Tableaux Method for Term Logic

Abstract

In this contribution we present a full tableaux method for Term Functor Logic and we discuss its features. This goal should be of interest because the plus-minus calculus of Term Functor Logic features a peculiar algebra that, as of today, has not been used to produce a full tableaux method. To reach this goal we brie y present Term Functor Logic, then we introduce our contribution and, at the end, we discuss some of its features.

Keywords

• Term logic
• semantic tree
• syllogistic

Introduction

In this contribution we present a full tableaux method for Term Functor Logic [ 29,30,32,9,12,13 ] and we discuss its features. This goal should be of interest because the plus-minus calculus of Term Functor Logic features a peculiar algebra that, as of today, has not been used to produce a full tableaux method (cf. [ 8,26 ]).1 To reach this goal we brie y present Term Functor Logic (with special emphasis on syllogistic), then we introduce our contribution and, at the end, we discuss the features of the method. Syllogistic is a term logic that has its origins in Aristotle's Prior Analytics [ 1 ] and deals with the consequence relation 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 a rmative (is) or negative (is not ). These categorical propositions have a type denoted by a label (either a (universal a rmative, SaP), e (universal negative, SeP), i (particular a rmative, SiP), or o (particular negative, SoP)) that allows us to determine a mood. A categorical 1 [32, p.183 ] have already advanced a proposal, but its scope is limited to propositional logic. syllogism, then, is a sequence of three categorical propositions ordered in such a way that two propositions are premises and the last one is a conclusion. Within the premises there is a term that 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 last term, four gures can be set up in order to encode the valid syllogistic moods or patterns (Table 1).2

Term Functor Logic (TFL) is a plus-minus calculus, developed by Sommers [ 29,30,32 ] and Englebretsen [ 9,12,13 ], that deals with syllogistic by using terms rather than rst order language elements such as individual variables or quanti ers.3 According to this algebra, the four categorical propositions can be represented by the following syntax:4

SaP := S + P = S SeP := S P = S SiP := +S + P = +S SoP := +S P = +S ( P) = ( P) S = ( P) (+P) = P S = P (+S) ( P) = +P + S = +P ( S) (+P) = +( P) + S = +( P) (+S) ( S)

Given this algebraic representation, the plus-minus algebra o ers a simple method of decision for syllogistic: 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 [12, p.167]. Thus, for instance, if we consider a valid syllogism from gure 1, we can see how the application of this method produces the right conclusion (Table 2). 2 For sake of brevity, but without loss of generality, here we omit the syllogisms that require existential import. 3 That we can represent and perform inference without rst order language elements such as individual variables or quanti ers is not news (cf. [ 27,23,18 ]), but Sommers' logical project has a wider impact: that we can use a logic of terms instead of a rst order system has nothing to do with the mere syntactical fact, as it were, that we can reason without quanti ers or variables, but with the general view that natural language is a source of natural logic (cf. [ 30,31,20 ]). 4 We mainly focus on the presentation by [ 12 ]. 1. All dogs are animals. D + A 2. All German Shepherds are dogs. G + D ` All German Shepherds are animals. G + A

In the previous example we can clearly see how the method works: i) if we add up the premises we obtain the algebraic expression ( 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 quantity (zero in this case) is the same as the number of premises with particular quantity (zero in this case).

This algebraic approach is also capable of representing relational, singular, and compound propositions with ease and clarity while preserving its main idea, namely, that inference is a logical procedure between terms. For example, the following cases illustrate how to represent and perform inferences with relational (Table 3), singular5 (Table 4), or compound propositions6 (Table 5). 1. Some horses are faster than some dogs. +H1 + (+F12 + D2) 2. Dogs are faster than some men. D2 + (+F23 + M3) 3. The relation faster than is transitive. (+F12 + (+F23 + M3)) + (+F13 + M3) ` Some horses are faster than some men. +H1 + (+F13 + M3) 1. All men are mortal. M + L 2. Socrates is a man. +s + M ` Socrates is mortal. +s + L

Proposition TFL 1. If P then Q. [p] + [q] 2. P . [p] ` Q. [q] 5 Provided singular terms, such as Socrates, are represented by lowercase letters. 6 Given that compound propositions can be represented as follows, P := +[p], Q := +[q], :P := [ p], P ) Q := [p]+[q], P ^Q := +[p]+[q], and P _Q := [p] [q], the method of decision behaves like resolution (cf. [ 24 ]).

These examples are designed to show that TFL is capable of dealing with a wide range of inferences, namely, those classical rst order logic is capable to deal with. However, in certain sense, TFL is arguably more expressive than classical rst order logic in so far as it is capable of dealing with active-passive voice transformations, associative shifts, and polyadic simpli cations [9, p.172 ]: we will refer to these features later. 3

TFL tableaux

As we can see, the peculiar algebra of TFL has some interesting capacities (and inference rules); however, as of today, this algebra has not been exploited as to produce a full tableaux method (cf. [ 8,32,26 ]): so here we propose one in three steps. First, we start by o ering some rules; then we show how can we apply those rules in three di erent inferential contexts (basic syllogistic, relational syllogistic, and propositional logic); and nally, we o er some evidence to the e ect that the method is reliable.

As usual, and following [ 8,26 ], we say a tableau is an acyclic connected graph determined by nodes and vertices. 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:

A Ai

B Bi +A

B +Ai

Bi

Diagram 1.1: TFL tableaux rules

In Diagram 1.1, from left to right, the rst rule is the rule for a (e) type propositions, and the second rule is the rule for i (o) type propositions. Notice that, after applying the rule, we introduce some index i 2 f1; 2; 3; : : :g. 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 1. A tableau is closed if and only if every branch is closed; otherwise it is open. So, 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., [ f Ag ` ?).

Accordingly, up next we show the method works for syllogistic by proving the four basic syllogisms of the rst gure, namely, moods aaa, eae, aii, and eio (Diag. 1.2). Also, as expected, this method can also be used with relational propositions. Consider the tableau in Diagram 1.3 corresponding to the example given in Table 6 (in the following tableaux we omit the subscript indexes since there is no ambiguity). Also, in compliance with the tenets of TFL, the method preserves the expressive power of TFL with respect to active-passive voice transformations, associative shifts, and polyadic simpli cations as shown in Table 7 and Diagram 1.4.

M + P

S + M ` S + P ( S + P) +S P +S1

P1

M P

S + M ` S P ( S P) +S + P +S1 +P1

M + P +S + M ` +S + P (+S + P)

S P +S1 +M1

M P +S + M ` +S P (+S P)

S + P +S1 +M1 S1 ?

+M1 M1 ? +P1 ?

S1 ?

+M1 M1 ?

P1 ?

M1 ?

+P1 S1 ?

P1 ?

M1 ?

S1 ?

P1 +P1 ?

Diagram 1.2: TFL proofs Table 6: Relational syllogistic example (adapted from [12, p.172])

+M1 +F1 ?

F1

A1 ? (+A + M)1

A M1

M1 ?

Diagram 1.3: Relational syllogistic tableau +M + (+L + M) ` +W + (+L + M) (+W + (+L + M))

W (+L + M) +M1 +L1 +W1 W1 ? (+L + M)1

L M1 L1 ?

M1 ? +M + (+L + W) ` +(+M + L) + W (+(+M + L) + W) (+M + L) W +M1 +L1 +W1

M1 ? W1 ? (+M + L)1

M L1

L1 ? +M + (+L + W) ` +L + M (+L + M)

L M +M1 +L1 +W1 L1 ?

M1 ? Diagram 1.4: Active-passive voice transformation, associative shift, and polyadic simpli cation

Finally, we produce some evidence to the fact that this method is reliable in the sense that what can be proven using the inference rules (say, TFLrvualleids) can be proven using the tableaux method (say, TFLtvaablildeaux), and vice versa. Proposition 1. If an inference is TFLrvualleids, it is TFLtvaablildeaux.

Proof. We proceed by cases. We check each mediate inference rule of TFL (vide Appendix) is TFLtvaablildeaux. For the rule DON we only need to retort to Section 2: in there we can observe the four possible ocurrences of DON and how they are TFLtvaablildeaux. For the rule Simp we can build the next tableaux and observe they are all valid: +(+X + Y) + Z ` +X + Y (+X + Y)

X Y +X1 +Y1 +Z1 X1 ?

Y1 ? +(+X + Y) ` +X + Y (+X + Y)

X Y

Z +X1 +Y1

Z1

Y1 ? X1 ? +(+X + Y) + Z ` +X + Z (+X + Z)

X Z +X1 +Y1 +Z1 X1 ?

Z1 ? +(+X + Y) ` +Y (+X

X + Z

Z Z) X1 ? +Z1 ?

A

B ` +( A) + ( B) (+( A) + ( B))

( A) ( B) ( A)

A ? ( B)

B ? Finally, for the rule Add we can build the next tableaux: +(+X + Y) + Z ` +Y + Z (+Y + Z)

Y Z +X1 +Y1 +Z1 Y1 ?

Z1 ? +(+X + Y) ` +Y (+Y

Y + Z

Z Z) +X1 +Y1

Z1 Y1 ? +Z1

? X + Y

X + Z ` X + (+Y + Z) ( X + (+Y + Z)) +X (+Y + Z)

+X1 (+Y + Z)1

Y Z1 X1 ?

X1 ? +Y1

Y1 ? +Z1

Z1 ? Proposition 2. If an inference is TFLtvaablildeaux, it is TFLrvualleids.

Proof. We proceed by reductio. Suppose we pick an arbitrary inference that is TFLtvaablildeaux but is not TFLrvualleids. Then there is a complete closed tableau whose initial list includes the set of terms (possibly empty) and the rejection of the conclusion (say, + = [ f ( A)g); but from alone we cannot construct a proof of the conclusion by using any of the rules of mediate inference. There are ve general cases using the tableaux rules: a complete closed tableau whose conclusion is A + B, A B, +A + B, +A B, or A + A when is empty. Since in each case the tableau is complete, the corresponding rules have been applied; and since each tableau is closed, each tableau must be of one of the following general forms:

B B)

B

Bi . .

.

Ai 2 ?

Bi 2 ? ` +A (+A

A +Ai 2

Bi 2 . .

.

Ai ?

B B) B

Bi ? ` A + A ( A + A) +A A +Ai

Ai ?

So, suppose we have an instance of the rst general form but the corresponding inference is not TFLrvualleids, i.e., where + = [ f+A Bg, + ` ?, but from any application of DON, Simp, and Add to , the conclusion A B does not obtain. Now, by following the paths of the tableau of the rst general form, we observe that, at the bottom, the tableau has a couple of closed branches. Hence, at some previous nodes the tableau has to include something of the form

A + X; X B, that is to say, we need = f: : : ; A + X; X B; : : :g. But if so, by applying DON, we obtain A B from , which contradicts the assumption. Similarly, suppose we have an instance of the second general form but the corresponding inference is not TFLrvualleids, i.e., where + = [ f A Bg, + ` ?, but from any application of DON, Simp, and Add to , the conclusion +A B does not obtain. By following the paths of the tableau of the second general form, we observe that, at the bottom, the tableau has a couple of closed branches, and for those branches to be closed, we need something of the form +A; B or something of the form +(+A + X) B at some previous nodes of the tableau, that is to say, we need either = f: : : ; +A; B; : : :g or = f: : : ; +(+A + X) B; : : :g. But if so, in either case, by applying Add, we obtain +A B from ; and by applying Simp, we obtain +A B from , which contradicts the assumption. Finally, assume we have an instance of the third general form. In that case, the path of the tableau consists only of + = f+A Ag, and so, trivially, + ` ?. But since is empty, A + A has to be a tautology (i.e., All A is A) (cf. [12, p.168]). 4

Concluding remarks

In this contribution we have attempted to o er a full tableaux method for Term Functor Logic. Here are some remarks we can extract from this attempt: a) the tableaux method we have o ered avoids condition ii) of the method of decision for syllogistic (namely, that the number of particular premises has to be equal to the number of particular conclusions), thus allowing its general application for any number of premisses. b) The method preserves the power of TFL with respect to relational inferences, passive-active voice transformations, associative shifts, and polyadic simpli cations, which is something that gives this method a competitive advantage over classical rst order logic (tableaux). c) As a particular case, when no superscript index is used, we just obtain a tableaux method for propositional logic.7 d) Due to the peculiar algebra of TFL, we have no use for quanti cation rules nor skolemization, which could be useful in relation to resolution and logic programming. e) The number of inference rules (cf. [12, p.168-170]) gets drastically reduced to a shorter, simpler, and uniform set of tableaux rules that preserves the capacity of TFL to perform inference in di erent inferential contexts (basic syllogistic, relational syllogistic, and propositional logic). f ) Also, we have to mention that for the purposes of this paper we have focused only on the terministic features of TFL, but further comparison is required with the algebraic proof systems introduced in the 2000s by [ 6,4 ], since these systems allow us to reconstruct Boole's analysis of syllogistic logic by employing polynomial formatted proofs [ 5 ] and can also be extended to several other logics, like modal logic [ 2,7 ]. g) Finally, we need to add that, due to reasons of space, we are unable to introduce the modal [ 10,28,19 ], intermediate [ 25,33 ] or numerical [ 22 ] extensions of the method that allow us to represent and reason with modal propositions or non-classical quanti ers; however, we need to stress that the inferential and representative powers of term logics go far beyond the limits of the traditional or rst order logic frontiers (cf. [ 20 ]).

For all these reasons, we believe this proof procedure is not only novel, but also promising, not just as yet another critical thinking tool or didactic contraption, but as a research device for probabilistic and numerical reasoning (in so far as it could be used to represent probabilistic (cf. [ 34 ]) or numerical reasoning (cf. [ 22 ])), diagrammatic reasoning (as it nds its natural home in a project of visual reasoning (cf. [ 11,32 ])), psychology (as it could be used to approximate a richer psychological account of syllogistic reasoning (cf. [ 17,16 ])) , arti cial intelligence (as it could be used to develop tweaked inferential engines for Aristotelian databases (cf. [ 21 ])), and of course, philosophy of logic (as it promotes the revision and revival of term logic (cf. [ 35,30,12,13 ]) as a tool that might be more interesting and powerful than once it seemed (cf. [ 3,14,15 ])). We are currently working on some of these issues.

Acknowledgments

We would like to thank the anonymous reviewers for their precise corrections and useful comments. Financial support given by UPAEP Research Grant. 7 The tableaux method can be used for propositional logic. Recall the propositional logic to TFL transcription is as follows: P := +[p], Q := +[q], :P := [p], P ) Q :=[p] + [q], P ^ Q := +[p] + [q], and P _ Q := [p] [q]; and notice that for the propositional case we need not use the superscript indexes. Appendix. Rules of inference for TFL In this Appendix we expound the rules of inference for TFL as they appear in [12, p.168-170].

Rules of immediate inference 1. Premise (P ): Any premise or tautology can be entered as a line in proof. (Tautologies that repeat the corresponding conditional of the inference are excluded. The corresponding conditional of an inference is simply a conditional sentence whose antecedent is the conjunction of the premises and whose consequent is the conclusion.) 2. Double Negation (DN ): Pairs of unary minuses can be added or deleted from a formula (i.e., X = X). 3. External Negation (EN ): An external unary minus can be distributed into or out of any phrase (i.e., ( X Y ) = X Y ). 4. Internal Negation (IN ): A negative quali er can be distributed into or out of any predicate-term (i.e., X ( Y ) = X + ( Y )). 5. Commutation (Com): The binary plus is symmetric (i.e., +X+Y = +Y +X). 6. Association (Assoc): The binary plus is associative (i.e., +X + (+Y + Z) = +(+X + Y ) + Z). 7. Contraposition (Contrap): The subject- and predicate-terms of a universal a rmation can be negated and can exchange places (i.e., X +Y = ( Y )+ ( X)). 8. Predicate Distribution (PD ): A universal subject can be distributed into or out of a conjunctive predicate (i.e., X + (+Y + Z) = +( X + Y ) + ( X + Z)) and a particular subject can be distributed into or out of a disjunctive predicate (i.e., +X + ( ( Y ) ( Z)) = (+X + Y ) (+X + Z)). 9. Iteration (It ): The conjunction of any term with itself is equivalent to that term (i.e., +X + X = X).

Rules of mediate inference 1. (DON ): If a term, M , occurs universally quanti ed in a formula and either M occurs not universally quanti ed or its logical contrary occurs universally quanti ed in another formula, deduce a new formula that is exactly like the second except that M has been replaced at least once by the rst formula minus its universally quanti ed M . 2. Simpli cation (Simp): Either conjunct can be deduced from a conjunctive formula; from a particularly quanti ed formula with a conjunctive subjectterm, deduce either the statement form of the subject-term or a new statement just like the original but without one of the conjuncts of the subjectterm (i.e., from +(+X +Y ) Z deduce any of the following: +X +Y , +X Z, or +Y Z), and from a universally quanti ed formula with a conjunctive predicate- term deduce a new statement just like the original but without one of the conjuncts of the predicate-term (i.e., from X (+Y + Z) deduce either X Y or X Z). 3. Addition (Add ): Any two previous formulae in a sequence can be conjoined to yield a new formula, and from any pair of previous formulae that are both universal a rmations and share a common subject-term a new formula can be derived that is a universal a rmation, has the subject-term of the previous formulae, and has the conjunction of the predicate- terms of the previous formulae as its predicate-term (i.e., from X + Y and X + Z deduce X + (+Y + Z)).

References

1. Aristotle . Prior Analytics. Hackett Classics Series. Hackett, 1989 .

2. Agudelo Juan C. and Walter A. Carnielli . Polynomial ring calculus for modal logics: A new semantics and proof method for modalities . The Review of Symbolic Logic , 4 ( 1 ): 150 { 170 , 2011 .

3. Rudolf Carnap . Die alte und die neue logik . Erkenntnis , 1 : 12 { 26 , 1930 .

4. 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 .

5. Walter A. Carnielli . Polynomizing: Logic inference in polynomial format and the legacy of boole . In Model-Based Reasoning in Science, Technology, and Medicine , 2007 .

6. Walter A. Carnielli . A polynomial proof system for lukasiewicz logics . In Second Principia International Symposium, August 6 - 10 , 2001 .

7. Walter A. Carnielli and Mariana Matulovic . Non-deterministic semantics in polynomial format . Electronic Notes in Theoretical Computer Science , 305 : 19 { 34 , 2014 . Proceedings of the 8th Workshop on Logical and Semantic Frameworks (LSFA).

8. Marcello D'Agostino , Dov M. Gabbay , Reiner Hahnle, and Joachim Posegga. Handbook of Tableau Methods . Springer, 1999 .

9. George Englebretsen . The New Syllogistic . 05. P. Lang, 1987 .

10. George Englebretsen . Preliminary notes on a new modal syllogistic . Notre Dame J. Formal Logic , 29 ( 3 ): 381 { 395 , 06 1988 .

11. George Englebretsen . Linear diagrams for syllogisms (with relationals) . Notre Dame J. Formal Logic , 33 ( 1 ): 37 { 69 , 12 1991 .

12. George Englebretsen . Something to Reckon with: The Logic of Terms. Canadian electronic library: Books collection . University of Ottawa Press, 1996 .

13. George Englebretsen and Charles Sayward . Philosophical Logic: An Introduction to Advanced Topics . Bloomsbury Academic, 2011 .

14. Peter T. Geach . Reference and Generality: An Examination of Some Medieval and Modern Theories . Contemporary Philosophy / Cornell University. Cornell University Press, 1962 .

15. Peter T. Geach. Logic Matters . Campus (University of California Press). University of California Press, 1980 .

16. Frank C. Keil . Exploring boundary conditions on the structure of knowledge: Some nonobvious in uences of philosophy on psychology . In David S. Oderberg, editor, The Old New Logic: Essays on the Philosophy of Fred Sommers , pages 67 { 84 . Bradford book , 2005 .

17. Sangeet Khemlani and Philip N. Johnson-Laird . Theories of the syllogism: a metaanalysis . Psychological Bulletin , pages 427 { 457 , 2012 .

18. Steven T. Kuhn . An axiomatization of predicate functor logic . Notre Dame J. Formal Logic , 24 ( 2 ): 233 { 241 , 04 1983 .

19. M. Malink . Aristotle's Modal Syllogistic . Harvard University Press, 2013 .

20. Larry Moss . Natural logic . In S. Lappin and C. Fox, editors, The Handbook of Contemporary Semantic Theory . John Wiley & Sons, 2015 .

21. Eyal Mozes . A deductive database based on aristotelian logic . Journal of Symbolic Computation , 7 ( 5 ): 487 { 507 , 1989 .

22. Wallace A. Murphree . Numerical term logic . Notre Dame J. Formal Logic , 39 ( 3 ): 346 { 362 , 07 1998 .

23. Aris Noah . Predicate-functors and the limits of decidability in logic . Notre Dame J. Formal Logic , 21 ( 4 ): 701 { 707 , 10 1980 .

24. Aris Noah . Sommers's cancellation technique and the method of resolution . In David S. Oderberg, editor, The Old New Logic: Essays on the Philosophy of Fred Sommers , pages 169 { 182 . Bradford , 2005 .

25. Philip L. Peterson . On the logic of \few", \many", and \most" . Notre Dame J. Formal Logic , 20 ( 1 ): 155 { 179 , 01 1979 .

26. Graham Priest . An Introduction to Non-Classical Logic: From If to Is . Cambridge Introductions to Philosophy. Cambridge University Press, 2008 .

27. Willard Van Orman Quine . Predicate functor logic . In J E Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium . North-Holland, 1971 .

28. Adriane A. Rini . Is there a modal syllogistic? Notre Dame J . Formal Logic , 39 ( 4 ): 554 { 572 , 10 1998 .

29. 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 .

30. Fred Sommers . The Logic of Natural Language. Clarendon Library of Logic and Philosophy . Clarendon Press; Oxford: New York: Oxford University Press, 1982 .

31. 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 .

32. Fred Sommers and George Englebretsen . An Invitation to Formal Reasoning: The Logic of Terms . Ashgate, 2000 .

33. Bruce Thompson . Syllogisms using \few", \many", and \most" . Notre Dame J. Formal Logic , 23 ( 1 ): 75 { 84 , 01 1982 .

34. Bruce Thompson . Syllogisms with statistical quanti ers . Notre Dame J. Formal Logic , 27 ( 1 ): 93 { 103 , 01 1986 .

35. Henry Babcock Veatch. Intentional logic: a logic based on philosophical realism . Archon Books , 1970 .