next up previous
Next: Possible Applications to Artificial Up: FIRST ORDER THEORIES OF Previous: More Philosophical Examples-Mostly Well

Propositions Expressing Quantification

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.

Thus

  equation361

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

  equation364

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

  equation367

is the concept of Mike's only child. tex2html_wrap_inline1401 is the proposition that the described child exists. We have

  equation374

but we may want the equality of the two propositions, i.e.

  equation381

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 tex2html_wrap_inline1403 such that

  equation385

is the possible world that is the same as the world tex2html_wrap_inline1405 except that the inner variable V has the value x instead of the value it has in tex2html_wrap_inline1405 . 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. gif

Let tex2html_wrap_inline1413 be the actual world. Let tex2html_wrap_inline1415 mean that the proposition P is true in the possible world tex2html_wrap_inline1405 . Then

  equation391

Let tex2html_wrap_inline1421 mean that X denotes x in tex2html_wrap_inline1405 , and let tex2html_wrap_inline1429 mean the denotation of X in tex2html_wrap_inline1405 when that is defined.

The truth condition for All(V,P) is then given by

  equation394

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 tex2html_wrap_inline1405 . Similarly

  equation397

The meaning of The(V,P) is given by

  equation400

and

  equation403

We also have the following syntactic rules governing propositions involving quantification:

  equation407

and

  equation410

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:

  equation413

  equation416

axioms similar to (92) for other conceptual functions,

  equation420

  equation423

  equation426

  equation429

  equation432

  equation435

axioms similar to (98) for other functions,

  equation439

  equation442

and corresponding axioms to (100) for Exist and The.

Along with these comes an axiom corresponding to tex2html_wrap_inline1403 -conversion,

  equation446

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 tex2html_wrap_inline1405 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

  equation449


next up previous
Next: Possible Applications to Artificial Up: FIRST ORDER THEORIES OF Previous: More Philosophical Examples-Mostly Well

John McCarthy
Sun Mar 10 22:57:10 PST 1996