The treatment given here should be compared with that in (Church 1951b) and in (Morgan 1976). Church introduces what might be called a two-dimensional type structure. One dimension permits higher order functions and predicates as in the usual higher order logics. The second dimension permits concepts of concepts, etc. No examples or applications are given. It seems to me that concepts of concepts will be eventually required, but this can still be done within first order logic.
Morgan's motivation is to use first order logic theorem proving programs to treat modal logic. He gives two approaches. The syntactic approach--which he applies only to systems without quantifiers--uses operations like our And to form compound propositions from elementary ones. Provability is then axiomatized in the outer logic. His semantic approach uses axiomatizations of the Kripke accessibility relation between possible worlds. It seems to me that our treatment can be used to combine both of Morgan's methods, and has two further advantages. First, concepts and individuals can be separately quantified. Second, functions from things to concepts of them permit relations between concepts of things that could not otherwise be expressed.
Although the formalism leads in almost the opposite direction, the present paper is much in the spirit of (Carnap 1956). We appeal to his ontological tolerance in introducing concepts as objects, and his section on intensions for robots expresses just the attitude required for artificial intelligence applications.
We have not yet investigated the matter, but plausible axioms for necessity or knowledge expressed in terms of concepts may lead to the paradoxes discussed in (Kaplan and Montague 1960) and (Montague 1963). Our intuition is that the paradoxes can be avoided by restricting the axioms concerning knowledge of facts about knowledge and necessity of statements about necessity. The restrictions will be somewhat unintuitive as are the restrictions necessary to avoid the paradoxes of naive set theory.
Chee K. Yap (1977) proposes virtual semantics for intensional logics as a generalization of Carnap's individual concepts. Apart from the fact that Yap does not stay within conventional first order logic, we don't yet know the relation between his work and that described here.
I am indebted to Lewis Creary, Patrick Hayes, Donald Michie, Barbara Partee and Peter Suzman for discussion of a draft of this paper. Creary in particular has shown the inadequacy of the formalism for expressing all readings of the ambiguous sentence ``Pat knows that Mike knows what Joan last asserted''. There has not been time to modify the formalism to fix this inadequacy, but it seems likely that concepts of concepts are required for an adequate treatment.