Functional predicate: Difference between revisions

Revision as of 23:30, 26 January 2003

Revision as of 23:41, 26 January 2003

Line 1:

In [[formal logic]], theand termrelated "mapping"branches isof sometimes[[mathematics]], distinguisheda from'''functional "function"predicate''', inor that'''function a mappingsymbol''', is a logical symbol, whereasthat amay functionbe isapplied ato [[modelobject (logic)|model]]term ofto suchproduce aanother symbolobject in [[set theory]]term.

Functional predicates are also sometimes called ''mappings'', but that term has other meanings as well.

Formally, the symbol <i>F</i> in a [[formal language]] is a ''mapping'' if, [[given any]] symbol <i>X</i> representing an object in the language, <i>F</i>(<i>X</i>) is again a symbol representing an object in that language.

In a [[model (logic)|model]], a function symbol will be modelled by a [[function]].

In [[typed logic]], <i>F</i> is a mapping with ''___domain'' type <b>T</b> and ''codomain'' type <b>U</b> if, given any symbol <i>X</i> representing an object of type <b>T</b>, <i>F</i>(<i>X</i>) is a symbol representing an object of type <b>U</b>.

One can similarly define mappings of more than one variable, analogous to functions of more than one variable.

FormallySpecifically, the symbol <i>F</i> in a [[formal language]] is a ''mapping''functional symbol if, [[given any]] symbol <i>X</i> representing an object in the language, <i>F</i>(<i>X</i>) is again a symbol representing an object in that language.

A mapping in zero variables is simply a [[constant]] symbol.

In [[typed logic]], <i>F</i> is a mappingfunctional symbol with ''___domain'' type <b>T</b> and ''codomain'' type <b>U</b> if, given any symbol <i>X</i> representing an object of type <b>T</b>, <i>F</i>(<i>X</i>) is a symbol representing an object of type <b>U</b>.

One can similarly define mappings of more than one variable, analogous to functions of more than one variable; a mapping in [[zero]] variables is simply a [[constant]] symbol.

Now consider a model of the formal language, with the types <b>T</b> and <b>U</b> modelled by [[set]]s [<b>T</b>] and [<b>U</b>] and each symbol <i>X</i> of type <b>T</b> modelled by an element [<i>X</i>] in [<b>T</b>].

Line 11 ⟶ 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>].

One can replace a mappingfunctional predicate with aan ordinary [[predicate (logic)|predicate]] in two variables (or replace a mappingfunctional predicate in <i>n</i> variables with aan ordinary predicate in <i>n</i> + 1 variables), along with ana [[axiomproposition (logic)|proposition]].

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 statment, 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 axiomproposition:

: [[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>).

Conversely, given any predicate <i>P</i> satisfying that axiomproposition, you get a definedfunctional mappingpredicate <i>F</i>, where <i>F</i>(<i>X</i>) is the unique <i>Y</i> such that <i>P</i>(<i>X</i>,<i>Y</i>) holds.

For this reason, many treatments of formal logic do not deal explicitly with mappingsfunction symbols but instead use only relation symbols (ordinary predicates); alternatively, one can treat a functional predicate as a ''special kind of'' predicate, specifically one that satisfies the proposition above.