Functional predicate: Difference between revisions

Revision as of 10:43, 26 February 2021

Latest revision as of 18:49, 14 July 2025

(4 intermediate revisions by 4 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 [[Mapping (mathematics)|additional meanings in mathematics]].

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

*[[Logical constant]]

{{Mathematical logic}}

{{DEFAULTSORT:Functional Predicate}}

[[Category:Model theory]]