Functional predicate: Difference between revisions

Revision as of 15:36, 9 March 2020

Latest revision as of 18:49, 14 July 2025

(6 intermediate revisions by 6 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 21 ⟶ 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]].

Line 42 ⟶ 43:

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 69 ⟶ 70:

*[[Logical constant]]

{{Mathematical logic}}

{{DEFAULTSORT:Functional Predicate}}

[[Category:Model theory]]