We take the closures of all the instances of the following as axioms:
Since λ-expressions in which the λ doesn't bind variables in encoding position in the matrix, we know that the following are axioms of quantificational logic:
The first says that the property being an individual that doesn't exemplify P exists; the second says that the property being an individual that exemplifies both P and Q exists; and the third says that the property being an individual that bears R to something exists.
So from these axioms, and the relevant instances of Axiom 1, we have the following as theorems:
In each equation, the λ-expressions flanking the identity signs denote the same property.
Using the same examples as before, we know that the following are axioms of quantificational logic:
So from these axioms, and the relevant instances of Axiom 2, we have the following as theorems:
The first asserts that b exemplifies being an individual that doesn't exemplify P if and only if b doesn't exemplify P; the second asserts that c exemplifies being an individual that exemplifies both P and Q if and only if c exemplifies both P and Q; the third says that d exemplifies being an individual that bears R to something if and only if d bears R to something.
Here is an instance of our quantificational logic that tells us that a binary λ-expression, in which none of the variables bound by the λ are in encoding position, has a denotation:
This asserts that the binary relation being individual x and y such that the x exemplifies P and the bears R to y exists. So for example, we might represent the relation that two numbers bear to one another just in case the first is odd and is less than the second, as follows:
[λxy Ox & x<y]↓
Since we know the property has a denotation, we can derive from Axiom 2 that:
This asserts that a and b exemplify the relation being individuals x and y such that x is odd and less than y if and only if a is odd and less than b.
Axiom 3 applies only to λ-expressions whose form is elementary, i.e., the matrix is always an exemplification formula with the arguments to the relation being pairwise-distinct free variables and the λ binds just all those variables, as in the following examples:
We can derive the following axiom schemata from Axiom 2:
In the unary case, we have:
In the 0-ary case, we have:
The proof of unary case is easy to see: Suppose F doesn't occur free in φ and x doesn't occur in encoding position somewhere in φ. Then [λx φ]↓, but quantification logic. So by Axiom 2, [λx φ]x ≡ φ. Then by GEN: ∀x([λx φ]x ≡ φ). So by RN, □∀x([λx φ]x ≡ φ). Existentially generalize on the λ-expression and we have ∃F□∀x(Fx ≡ φ), which is what we had to show.
Some examples that assert the existence of properties:
The first asserts that there is a property that, necessarily, is exemplified by all and only those objects that fail to exemplify P. And so on for the others.
And as an example of a theorem that asserts the existence of a binary relation:
Recall that there is a definition of identity for relations on the webpage The Language of the Theory. The first definition tells us that properties F and G are identical if and only if, necessarily, they encode the same properties. The second definition tells us that, for n>1, n-place relations F and G are identical iff for each way of plugging n−1 objects in the same order into F and G, the resulting 1-place properties are identical. The third definition tells us that propositions p and q are identical just in case the property being such that p ([λy p]) is identical to the property being such that q ([λy q]).
These definitions, together with the comprehension principle for relations, constitute a mathematically precise theory of relations and properties, for they are explicit existence and identity conditions for these entities.
Notice that these definitions allow us to consistently assert that there are properties and relations which are necessarily exemplified by the same objects but which are nevertheless distinct. For example, the properties being equiangular and being equilateral are distinct properties, and so it is natural to suppose, therefore, that the property being an equiangular Euclidean triangle is distinct from the property being an equilateral Euclidean triangle. However, these two complex properties are exemplified by the same objects at every possible world (it is necessarily the case that anything exemplifying the one exemplifies the other). This is a virtue of the theory—many theories and/or treatments of properties identify properties that are necessarily equivalent. We identify properties only when they are necessarily equivalent with respect to the objects that encode them, not when they are necessarily equivalent with respect to the objects that exemplify them. The intuition here is that abstract objects represent possible objects of thought. If properties F and G are distinct, then it is possible to conceive of an object having (i.e., encoding) F and not G (and vice versa). So the ‘encoding extensions’ of F and G are distinct when F and G are distinct. However, if F and G are not distinct properties, one couldn't conceive of an object having (i.e., encoding) F and not G. The encoding extensions of identical properties are the same.
Note that the following are axioms of quantificational logic:
The first asserts that (the proposition) that b doesn't exemplify Q exists. The second asserts that (the proposition) that-a-exemplifies-P-and-b-exemplifies-Q exists. And so on.
From these axioms, and the relevant 0-ary instances of Axiom 2, the following are provable as theorems:
We read the first as: (the proposition) that-b-doesn’t-exemplify-Q is true if and only if b doesn’t exemplify Q. The second asserts: (the proposition that-a-exemplifies-P-and-b-exemplifies-Q is true if and only if a exemplifies P and b exemplifies Q. The third asserts: (the proposition) that-a-bears-R-to-something is true if and only if a bears R to something. Notice that the notion of ‘exemplification’ has become the notion of ‘truth’ in the 0-ary case.
In general, since it is axiomatic that [λ φ]↓ for every φ, we can derive, as a theorem schema, that:
I.e., the proposition that-φ is true if and only if φ. It follows from this by the Rule of Necessitation and Existential Inroduction that:
This is the 0-ary case of the comprehension principle for relations, and it can be read as follows: for any condition φ in which p doesn't occur free, there exists proposition such that, necessarily, p is true if and only if φ. Here are some examples:
We may read the first example as follows: there exists a proposition p such that, necessarily, p is true if and only if b doesn’t exemplify Q. And so on for the other examples.
Here, too, it is important to recall the definition for the identity of propostions on the page The Language of the Theory. As noted above this definition tells us that propositions p and q are identical if and only if the properties being such that p ([λy p]) and being such that q ([λy q]) are identical. The conditions under which properties are identical has already been defined, and so propositional identity is hereby reduced to property identity. Consequently, we now have a precise theory of propositions: the comprehension axiom and the above definition give us explicit existence and identity conditions for propositions.
This definition also allows us to consistently assert that certain necessarily equivalent propositions are nevertheless distinct. For example, both of the following propositions are necessarily false: that Fido is a dog and it is not the case that Fido is a dog and that there is a barber who shaves only those people who don't shave themselves. In formal terms, these propositions would be denoted by the following complex 0-ary predicates:
Though the two propositions are necessarily equivalent (i.e., true in the same possible worlds), we may consistently assert that they are distinct. This stands in contrast to treatments of propositions on which necessarily equivalent propositions are identified, contrary to intuition.