[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear types-list, Here is some more information regarding the interesting question raised by Peter Selinger. This use of ‘subject’ and ‘predicate’ appears indeed already in the first volume (1958) of Curry & Feys, page 272. I could not find it in Curry’s ‘Functionality in combinatory logic’ (1934). The reason why this terminology was chosen may have been the following. We all know the terms ‘subject’ and ‘predicate’ from school grammar. These terms go back to Aristotle’s ‘hypokeimenon’ and ‘kategoroumenon’ and are a staple of traditional logic. One of Frege’s main inventions in his *Begriffsschrift* (1879) was to replace these terms with the mathematical terms ‘function’ and ‘argument’. The analysis of propositions into function and argument(s) naturally leads to the idea of a type hierarchy, as first hinted at in Frege’s *Grundgesetze* (1893), and, concomitantly, to the idea that any component of a proposition belongs to a type in such a hierarchy. In a typing judgement, a : A, we are saying that a is an object of type A. Is this judgement itself (or its content) to be analyzed as: function applied to argument(s)? That does not seem quite right, certainly not in Curry’s context, where a is always a function. The traditional terminology therefore presents itself as a natural alternative: a : A is to be analyzed as subject—copula—predicate. The philologically inclined may be interested in ch. 2 of Jonathan Barnes's *Truth, etc.* (Oxford, 2007). The philosophically inclined may perhaps see that the question of the logical form of typing judgements is closely related to the so-called 'concept horse problem' first raised by Frege. Best wishes, Ansten
