[TYPES] Subject reduction

[Ansten Mørch Klev]

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