Natural Term Logic

Our aim is to develop a formal logic which reflects the logical mechanisms of the grammar of natural language. In particular a formal logic which is not

tied in any way to extensionalism or standard interpretations of quantifiers and multiple generality. It is our conviction that the standard use of variables (in quantifier logic, lambda calculus and the constructivist version used in dependent type theory) while being useful and mathematically interesting, does not directly reflect the actual logical structure of natural language and its mechanisms for expressing 'quantitative' determiners and multiple generality (cf. the study of suppositio and syncategoremata in the middle ages. ). Our philosophical premise is that the conceiving, applying, checking and reasoning about Turing complete formal systems presupposes a priori a system of cognitive categories that are independent from and prior to standard quantifiers. Rather the most adequate type of formal system for logic would be in the style of Quine's paper 'Variables explained away' (this can be compared to our considerations on the philosophical significance of term-rewriting systems in our paper on Analyticity and the A Priori). The earlier work of Schönfinkel and Curry (combinatory logic) while also involving the elimination of bound variables is however structurally quite different. Quine himself also mentions the earlier work of Tarski on cylindric algebras. It is necessary to extend the combinatory approach to intensional logic and a main source of inspiration for our work is George Bealer's book 'Quality and Concept'.

Our work on Aristotle's Topics attempts not only a formalization of this work but argues for there being present in Aristotle a variant of a natural deduction calculus for an extension of second-order logic. However it does not deal directly with variable-free logic, being focused on inference rather than logical expression.

Our system of variable-free logic is called Natural Term Logic. The basic building blocks are called primitive terms and denoted by capital roman letters $M,N,P$. Each term is assigned a unique (predication) sort which is an integer $\geq 0$. The sort $0$ should be understood as indicating that the term cannot be used a a predicate (i.e. it is unsaturated) and this will include both abstract objects (like propositions) and concrete objects. We sometimes denote the sort of a term by $M^{(s)}$. Finally we have constructors, denoted by lower-case Greek letters $\alpha, \beta, \gamma$ to which are assigned a unique signature $(s_1, s_2,..., s_n) \rightarrow s$ where $s$ is sort and the $s_i$ are sorts. The classification into sorts can be compared to the saturated and unsaturared lekta of Stoic logic and there are also important comparisons that should be made with medieval and classical grammar (our terms are slightly more general than definite grammatical categories or 'flections'). Constructors take as arguments terms of specified sorts and yield a complex term of sort $s$.

Roughly speaking, sort 0 terms correspond to proper nouns or nominalized sentences (in particular the objects of propositional attitudes), sort 1 terms are those that can be used as monadic predicates, sort 2 terms correspond to relations, etc. At this stage the same term can be used for different kinds of supposition. Thus we have the sort 1 term 'man' which also doubles as a predicate 'being a man' when conjoined with the appropriate constructor.

Basic constructors include the family $\delta$ (for simplicity we denote these basic constructor families by a single letter) which diagonalizes terms (this corresponds in particular to reflexive constructions such as 'to love oneself') and $\sigma$ which corresponds to permutations (this includes the reciprocal of relations: the reciprocal of the relation of 'somebody to know something' corresponds to 'something to be known by somebody').

But the fundamental family of constructors are $\pi$ which correspond to predication (both simple and embedded - this will be explained further ahead). We sometimes omit the constructor and use simply the concatenation of terms such as $SM$ for the nominalized sentence 'Socrates is a man'. If $L$ is of sort 2 (a relation) then predication can create a term o sort 1 $LJ$ (to love John) and then a term of 0 sort $MLJ$ 'that Mary loves John' (where we use a form of concatenation mimicking the SVO construction). As we shall see, we have a certain freedom on how we define these simple forms of predication (when combined with the basic constructors above).

But what is embedded predication ? Consider the sort 1 term Happy and the sort 1 complex term 'known by John'. Then we can form the 1 sort complex term 'known to be happy by John'. The grammatical aspect here is doubtlessly complex and varied (related to dependency and verbal complements). What is clear is that this construction cannot be reduced to simple predication involving the terms 'know' and 'happy'. Let us explain in more detail embedded predication.

Consider the following related complex terms (we use variables for convenience):\\


1 sort: 'X knows (about the) love (relation)' (knowing about the love relation)

2 sort 'X knows (about property) loving W' (somebody knowing the property of loving somebody)

2 sort 'X knows (about property) being loved by Z'

1 sort 'X knows (about property) to love Mary'

1 sort 'X knows (about property) being loved by John'

3 sort 'X knows that Z loves W'

2 sort 'X knows that Z loves Mary'

2 sort 'X knows that John loves W'

1 sort 'X knows that John loves Mary'


Only the 1 sort complex terms are examples of non-embedded predication of the terms Knowledge and Love. In all other cases the predicative aspect of the predicate term is pulled up into the complex predication term itself.

We have two versions of the analogues of binary connectives for terms. For 2 sort terms $L$ (love) and $R$ (respect) we have $L\& R$ the relation of somebody loving and respecting somebody. But we can also combine terms into a juxtaposed conjunction relation $L\otimes R$ resulting in a degenerate complex term of sort 4. Negation applies to terms of all sorts. Thus we have 'not being the case that Mary loves John', 'not loving Mary', 'not loving', etc. The juxtaposed conjunction together with $\delta$ allow us to define the product of relations, for example 'someone being the father of someone who is the father of someone'. This can be given an alternative (perhaps preferable) presentation using the natural term logic versions of the Peano operator and its indefinite version (selector). For instance for a 1 sort $M$ we form 0-terms 'the M' and 'a M'. But there are also 'functional' versions for 2 sort term yielding 1 sort terms: for instance 'the father of somebody' and 'a father of somebody'. We can also venture into the quicksand of extensions of terms as well as mereology (which was already developed in the middle ages in the analysis of the syncategoremata totus and pars).

Finally let us come to quantifiers. Though this is not strictly necessary for a formal study of our system we make the philosophcial assumptions that all quantification is bounded in some form, even if only implicitly.

Let us consider 1 sort terms only. Then 'all M is N' will be expressed by a constructor $\kappa MN$ with obvious signature $(1, 1) \rightarrow 0$ and analogously for 'some'. We can wonder if (grammatically oriented) we could also conceive of $\kappa$ as being a constructor of signature $1 \rightarrow 1$ so that $(\kappa M)N$ could be read in the same way. Or what about Bobzien's proposal for a Stoic implicational reading ?

Of great importance is how $\delta$ combines with quantifier operators by entangling together different subterms thus allowing us to express multiple generality in a way formally similar to the mechanisms of natural language and in particular the use of anaphoric pronouns. Examples can be found for instance in Boethius' discussion of conditional propositions in \emph{De topicis differentiis} (1176B) in which what in modern notation would be written $\forall x S(x) \rightarrow R(x)$ is expressed "If it is spherical, it is revolvable.", the second occurrence of the pronoun 'it' being anaphoric. In Natural Term Logic this could correspond to first applying $\delta$ to the term corresponding to $\lambda x y S(x) \rightarrow R(y)$ (the relation of one thing being spherical implying that the other revolvable) and then applying an unbounded quantification operator.

We cannot discuss here 'judgement' vs. proposition nor the interesting possibilities of formalizing directly much of the medieval theory of obligations (much richer than the proposition vs. judgment distinction) as well as a even closer interpretation of the Topics and medieval developments inspired by this work..

Consider the sentence 'every man has a father and has somebody who gave that man a name'. Suppose 'John is a man' is accepted. Then we must be able to infer that 'John has a father and there is somebody who gave John a name' : can we devise a syntactical algorithm for tracking the 'free variable' 'that man' ? And things get even more complicated when we are in the presence of embedded predication (verbal complements, etc.).

And what about 1 sort terms built from $\kappa$ such as 'having every brother liking Winnie-the-Pooh' ? We will see further ahead how this is done.

And surely we need a determiner-constructor corresponding for instance to adjectival constructions and other determiners in noun sentences. How is the complex term 'rational animal' formed (this kind of juxtaposition of terms can be given, it seems, a conjunctive reading) ? It would be interesting to study the subtle problem of semantic differences in the order of longer strings of determiners as well as apposition. The Topics permit us to formulate a much more fine-grained theory of noun sentence determiners.

Our Natural Term Logic is typed but only in a very broad sense. It turns out that the above approach has some very interesting applications to standard type theories such as the simply typed lambda calculus and Girard's system F.

In this paper we shall see that we can give a variable-free equivalent presentation of the simply typed lambda calculus and furthermore that this approach can be internalized in system F.