Functional predicate: Difference between revisions

Revision as of 06:02, 17 December 2009

Latest revision as of 18:49, 14 July 2025

(16 intermediate revisions by 14 users not shown)

Line 1:

{{Short description|Symbol representing a mathematical concept}}

{{Unreferenced|date=December 2009}}

In [[formal logic]] and related branches of [[mathematics]], a '''functional predicate''',{{cn|reason=This seems to me a particularly unusual naming.|date=July 2025}} 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[[Mapping (mathematics)|additional meanings asin wellmathematics]].

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

Line 15 ⟶ 16:

==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. Given the function symbols ''F'' and ''G'', one can introduce a new function symbol ''F'' ∘ ''G'', the ''[[function composition|composition]]'' of ''F'' and ''G'', satisfying (''F'' ∘ ''G'')(''X'') = ''F''(''G''(''X'')), [[for all]] ''X''.

Introducing new function symbols from old function symbols is easy; given function symbols ''F'' and ''G'', there is a new function symbol ''F'' o ''G'', the ''composition'' of ''F'' and ''G'', satisfying (''F'' o ''G'')(''X'') = ''F''(''G''(''X'')), [[for all]] ''X''.

Of course, the right side of this equation doesn't make sense in typed logic unless the ___domain type of ''F'' matches the codomain type of ''G'', so this is required for the composition to be defined.

Line 22:

In untyped logic, there is an ''identity predicate'' id that satisfies id(''X'') = ''X'' for all ''X''.

In typed logic, given any type '''T''', there is an identity predicate id_'''T''' with ___domain and codomain type '''T'''; it satisfies id_'''T'''(''X'') = ''X'' for all ''X'' of type '''T'''.

Similarly, if '''T''' is a [[Subtyping|subtype]] of '''U''', then there is an inclusion predicate of ___domain type '''T''' and codomain type '''U''' 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 ''X'' (or every ''X'' of a certain type), [[there exists]] a [[unique (mathematics)|unique]] ''Y'' satisfying some condition ''P'', then you can introduce a function symbol ''F'' to indicate this.

Note that ''P'' will itself be a relational [[predicate (logic)|predicate]] involving both ''X'' and ''Y''.

So if there is such a predicate ''P'' and a theorem:

Line 38:

But there is a method of replacing functional symbols with relational symbols wherever the former may occur; furthermore, this is algorithmic and thus suitable for applying most metalogical theorems to the result.

Specifically, if ''F'' has ___domain type '''T''' and [[codomain]] type '''U''', then it can be replaced with a predicate ''P'' of type ('''T''','''U''').

Intuitively, ''P''(''X'',''Y'') means ''F''(''X'') = ''Y''.

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

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

: [[For all]] ''X'' of type '''T''', for some [[unique (mathematics)|unique]] ''Y'' of type '''U''', ''P''(''X'',''Y'').

(Of course, this is the same proposition that had to be provedproven as a theorem before introducing a new function symbol in the previous section.)

Because the elimination of functional predicates is both convenient for some purposes and possible, many treatments of formal logic do not deal explicitly with function symbols but instead use only relation symbols; another way to think of this is that a functional predicate is a ''special kind of'' predicate, specifically one that satisfies the proposition above.

Line 49:

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

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

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

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

(This example uses [[mathematical symbols]].)

This schema states (in one form), for any functional predicate ''F'' in one variable:

Line 66:

==See also==

*[[Function symbol (logic)]]

*[[Logical connective]]

*[[Logical constant]]

{{Mathematical logic}}

{{DEFAULTSORT:Functional Predicate}}

[[Category:Model theory]]

[[plCategory:SymbolModel funkcyjnytheory]]

[[zh:泛函谓词]]