As the examples of the previous sections have shown, admitting concepts as objects and introducing standard concept functions makes ``quantifying in'' rather easy. However, forming propositions and individual concepts by quantification requires new ideas and additional formalism. We are not very confident of the approach presented here.
We want to continue describing concepts within first order logic with no logical extensions. Therefore, in order to form new concepts by quantification and description, we introduce functions All, Exist, and The such that All(V,P) is (approximately) the proposition that ``for all values of V, P is true'', Exist(V,P) is the corresponding existential proposition, and The(V,P) is the concept of ``the V such that P''.
Since All is to be a function, V and P must be objects in the logic. However, V is semantically a variable in the formation of All(V,P), etc., and we will call such objects inner variables so as to distinguish them from variables in the logic. We will use V, sometimes with subscripts, for a logical variable ranging over inner variables. We also need some constant symbols for inner variables (got that?), and we will use doubled letters, sometimes with subscripts, for these. XX will be used for individual concepts, PP for persons, and QQ for propositions.
The second argument of All and friends is a ``proposition with variables in it'', but remember that these variables are inner variables which are constants in the logic. Got that? We won't introduce a special term for them, but will generally allow concepts to include inner variables. Thus concepts now include inner variables like XX and PP, and concept forming functions like Telephone and Know take as arguments concepts containing internal variables in addition to the usual concepts.
is a proposition with the inner variable PP in it to the effect that if PP is a child of Mike, then his telephone number is the same as Mike's, and
is the proposition that all Mike's children have the same telephone number as Mike. Existential propositions are formed similarly to universal ones, but the function Exist introduced here should not be confused with the function Exists applied to individual concepts introduced earlier.
In forming individual concepts by the description function The, it doesn't matter whether the object described exists. Thus
is the concept of Mike's only child. is the proposition that the described child exists. We have
but we may want the equality of the two propositions, i.e.
This is part of general problem of when two logically equivalent concepts are to be regarded as the same.
In order to discuss the truth of propositions and the denotation of descriptions, we introduce possible worlds reluctantly and with an important difference from the usual treatment. We need them to give values to the inner variables, and we can also use them for axiomatizing the modal operators, knowledge, belief and tense. However, for axiomatizing quantification, we also need a function such that
is the possible world that is the same as the world except that the inner variable V has the value x instead of the value it has in . In this respect our possible worlds resemble the state vectors or environments of computer science more than the possible worlds of the Kripke treatment of modal logic. This Cartesian product structure on the space of possible worlds can also be used to treat counterfactual conditional sentences.
Let be the actual world. Let mean that the proposition P is true in the possible world . Then
Let mean that X denotes x in , and let mean the denotation of X in when that is defined.
The truth condition for All(V,P) is then given by
Here V ranges over inner variables, P ranges over propositions, and x ranges over things. There seems to be no harm in making the domain of x depend on . Similarly
The meaning of The(V,P) is given by
We also have the following syntactic rules governing propositions involving quantification:
where absent(V,X) means that the variable V is not present in the concept X, and Subst(X,V,Y) is the concept that results from substituting the concept X for the variable V in the concept Y. absent and Subst are characterized by the following axioms:
axioms similar to (92) for other conceptual functions,
axioms similar to (98) for other functions,
and corresponding axioms to (100) for Exist and The.
Along with these comes an axiom corresponding to -conversion,
The functions absent and Subst play a ``syntactic'' role in describing the rules of reasoning and don't appear in the concepts themselves. It seems likely that this is harmless until we want to form concepts of the laws of reasoning.
We used the Greek letter for possible worlds, because we did not want to consider a possible world as a thing and introduce concepts of possible worlds. Reasoning about reasoning may require such concepts or else a formulation that doesn't use possible worlds.
Martin Davis (in conversation) pointed out the advantages of an alternate treatment avoiding possible worlds in case there is a single domain of individuals each of which has a standard concept. Then we can write