Functional predicate: Difference between revisions

Revision as of 22:48, 1 June 2004

Revision as of 01:20, 18 June 2004

Line 42:

Specifically, if <i>F</i> has ___domain type <b>T</b> and codomain type <b>U</b>, then it can be replaced with a predicate <i>P</i> of type (<b>T</b>,<b>U</b>).

Intuitively, <i>P</i>(<i>X</i>,<i>Y</i>) means <i>F</i>(<i>X</i>) = <i>Y</i>.

Then whenever <i>F</i>(<i>X</i>) would appear in a statmentstatement, you can replace it with a new symbol <i>Y</i> of type <b>U</b> and include another statement <i>P</i>(<i>X</i>,<i>Y</i>).

To be able to make the same deductions, you need an additional proposition:

: [[For all]] <i>X</i> of type <b>T</b>, for some [[unique]] <i>Y</i> of type <b>U</b>, <i>P</i>(<i>X</i>,<i>Y</i>).

Line 50:

This may seem to be a problem if you wish to specify a proposition [[schema (logic)|schema]] that applies only to functional predicates <i>F</i>; how do you know ahead of time whether it satisfies that condition?

To get an equivalent formulation of the schema, first replace anything of the form <i>F</i>(<i>X</i>) with a new variable <i>Y</i>.

Then [[universally quantify]] over each <i>Y</i> immediately after the corresponding <i>X</i> is introduced (that is, after <i>X</i> is quantified over, or at the beginning of the statmentstatement if <i>X</i> is free), and guard the quantification with <i>P</i>(<i>X</i>,<i>Y</i>).

Finally, make the entire statmentstatement a [[material implication|material consequence]] of the uniqueness condition for a functional predicate above.

Let us take as an example the [[axiom schema of replacement]] in [[Zermelo-Fraenkel set theory]].

Line 59:

First, we must replace <i>F</i>(<i>C</i>) with some other variable <i>D</i>:

: &forall; <i>A</i>, &exist; <i>B</i>, &forall; <i>C</i>, <i>C</i> &isin; <i>A</i> &rarr; <i>D</i> &isin; <i>B</i>.

Of course, this statmentstatement isn't correct; <i>D</i> must be quantified over just after <i>C</i>:

: &forall; <i>A</i>, &exist; <i>B</i>, &forall; <i>C</i>, &forall; <i>D</i>, <i>C</i> &isin; <i>A</i> &rarr; <i>D</i> &isin; <i>B</i>.

We still must introduce <i>P</i> to guard this quantification: