Content deleted Content added
Toby Bartels (talk | contribs) m Missed a couple. |
Toby Bartels (talk | contribs) Further explanation of the relationship to relational predicates; using a slightly different version of Replacement for an example to better bring out the ideas involved. |
||
Line 1:
In [[formal logic]] and related branches of [[mathematics]], a '''functional predicate''', or '''function symbol''', is a logical symbol that may be applied to an object term to produce another object term.
Functional predicates are also sometimes called ''mappings'', but that term has other meanings as well.
In a [[model (logic)|model]], a function symbol will be modelled by a [[function]].
Line 13:
It is a requirement of a consistent model that [<i>F</i>(<i>X</i>)] = [<i>F</i>(<i>Y</i>)] whenever [<i>X</i>] = [<i>Y</i>].
== Introducing new function symbols ==
In a treatment of predicate logic that allows one to introduce new predicate symbols, one will also want to be able to introduce new function symbols.
Introducing new function symbols from old function symbols is easy; given function symbols <i>F</i> and <i>G</i>, there is a new function symbol <i>F</i> o <i>G</i>, the ''composition'' of <i>F</i> and <i>G</i>, satisfying (<i>F</i> o <i>G</i>)(<i>X</i>) = <i>F</i>(<i>G</i>(<i>X</i>)), [[for all]] <i>X</i>.
Of course, the right side of this equation doesn't make sense in typed logic unless the ___domain type of <i>F</i> matches the codomain type of <i>G</i>, so this is required for the composition to be defined.
One also gets certain function symbols automatically.
Given any type <b>T</b>, there is an ''identity predicate'' id<sub><b>T</b></sub> with ___domain and codomain type <b>T</b>; it satisfies id<sub><b>T</b></sub>(<i>X</i>) = <i>X</i> for all <i>X</i> of type <b>T</b>.
Similarly, if <b>T</b> is a [[subtype]] of <b>U</b>, then there is an inclusion predicate of ___domain type <b>T</b> and codomain type <b>U</b> that satisfies the same equation; there are additional function symbols associated with other ways of constructing new types out of old ones.
Additionally, one can define functional predicates after proving an appropriate [[theorem]].
(If you're working in a formal system that doesn't allow you to introduce new symbols after proving theorems, then you will have to use relation symbols to get around this, as in the next section.)
Specifically, if you can prove that for every <i>X</i> (or every <i>X</i> of a certain type), there exists a [[unique]] <i>Y</i> satisfying some condition <i>P</i>, then you can introduce a function symbol <i>F</i> to indicate this.
Note that <i>P</i> will itself be a relational [[predicate (logic)|predicate]] involving both <i>X</i> and <i>Y</i>.
So if there is such a predicate <i>P</i> and a theorem:
: 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>),
then you can introduce a function symbol <i>F</i> of ___domain type <b>T</b> and codomain type <b>U</b> that satisfies:
: For all <i>X</i> of type <b>T</b>, for all <i>Y</i> of type <b>U</b>, <i>P</i>(<i>X</i>,<i>Y</i>) [[if and only if]] <i>Y</i> = <i>F</i>(<i>X</i>).
== Doing without functional predicates ==
Many treatments of predicate logic don't allow functional predicates, only relational [[predicate (logic)|predicate]]s.
This is useful, for example, in the context of proving [[metalogic]]al theorems (such as [[Goedel's incompleteness theorem]]s), where one doesn't want to allow the introduction of new functional symbols (nor any other new symbols, for that matter).
But there is a method of replacing functional symbols with relational sybmols wherever the former may occur; furthermore, this is algorithmic and thus suitable for applying most metalogical theorems to the result.
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>.
Line 19 ⟶ 43:
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>).
(Of course, this is the same proposition that had to be proved as a theorem before introducing a new function symbol in the previous section.)
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 statment if <i>X</i> is free), and guard the quantification with <i>P</i>(<i>X</i>,<i>Y</i>).
Finally, make the entire statment 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]].
This schema states (in one form), for any functional predicate <i>F</i> in one variable:
:∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, <i>C</i> ∈ <i>A</i> → <i>F</i>(<i>C</i>) ∈ <i>B</i>.
First, we must replace <i>F</i>(<i>C</i>) with some other variable <i>D</i>:
:∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, <i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>.
Of course, this statment isn't correct; <i>D</i> must be quantified over just after <i>C</i>:
:∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, ∀ <i>D</i>, <i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>.
We still must introduce <i>P</i> to guard this quantification:
:∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, ∀ <i>D</i>, <i>P</i>(<i>C</i>,<i>D</i>) → (<i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>).
This is almost correct, but it applying to too many predicates; what we actually want is:
:(∀ <i>X</i>, ∃! <i>Y</i>, <i>P</i>(<i>X</i>,<i>Y</i>)) → (∀ <i>A</i>, ∃ <i>B</i>, ∀ <i>C</i>, ∀ <i>D</i>, <i>P</i>(<i>C</i>,<i>D</i>) → (<i>C</i> ∈ <i>A</i> → <i>D</i> ∈ <i>B</i>)).
This version of the axiom schema of replacement is now suitable for use in a formal language that doesn't allow the introduction of new function symbols.
Alternatively, one may interpret the original statement as a statement in such a formal language; it was merely an abbreviation for the statement produced at the end.
| |||