Function symbol: Difference between revisions

Revision as of 00:12, 18 September 2009

Latest revision as of 22:33, 2 September 2025

(28 intermediate revisions by 19 users not shown)

Line 1:

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

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.

{{About|the generalization of "function" in mathematical logic|symbols and notation used for functions|Function (mathematics)#Notation}}

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

{{Unreferenced|date=December 2009}}

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

In [[mathematical logic]] particularly [[model theory]], a '''function symbol''' is a [[non-logical symbol]] which represents a [[Function (mathematics)|function]] or [[Map (mathematics)|mapping]] on the [[___domain of discourse]], though, formally, does not need to represent anything at all. Function symbols are a basic component in [[formal languages]] to form [[Term (logic)|terms]]. Specifically, if the symbol <math>F</math> is a function symbol if, then given any constant symbol <math>X</math> representing an object in the language, <math>F(X)</math> also represents an object in the language. Similarly, if <math>T</math> is some term in the language, <math>F(T)</math> is also a term. As such, the interpretation of a function symbol must be defined over the whole ___domain of discourse. Function symbols are a [[primitive notion]], and are therefore not defined in terms of other, more basic concepts.

Specifically, the symbol ''F'' in a [[Formal language (logic)|formal language]] is a functional symbol if, [[given any]] symbol ''X'' representing an object in the language, ''F''(''X'') is again a symbol representing an object in that language.

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

One can similarly define function symbols of more than one variable, analogous to functions of more than one variable; a function symbol in [[0 (number)|zero]] variables is simply a [[constant]] symbol.

Now consider a model of the formal language, with the types '''T''' and '''U''' modelled by [[Set (mathematics)|sets]] ['''T'''] and ['''U'''] and each symbol ''X'' of type '''T''' modelled by an element [''X''] in ['''T'''].

Then ''F'' can be modelled by the set

:<math>[F]:=\big\{([X],[F(X)]):[X]\in[\mathbf{T}]\big\},</math>

which is simply a [[function (mathematics)|function]] with ___domain ['''T'''] and codomain ['''U''']. It is a requirement of a consistent model that [''F''(''X'')] = [''F''(''Y'')] whenever [''X''] = [''Y''].

It is a requirement of a consistent model that [''F''(''X'')] = [''F''(''Y'')] whenever [''X''] = [''Y''].

== Introducing new function symbols ==

IntroducingIn a treatment of [[predicate logic]] that allows one to introduce new functionpredicate symbols, fromone oldwill also want to be able to introduce new function symbols. isGiven easy; giventhe function symbols ''F'' and ''G'', thereone iscan introduce a new function symbol ''F'' o∘ ''G'', the ''[[function composition|composition]]'' of ''F'' and ''G'', satisfying (''F'' o∘ ''G'')(''X'') = ''F''(''G''(''X'')), [[for all]] ''X''.

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 ''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 ⟶ 19:

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. This is called an [[extension by definition]]. Note that ''P'' will itself be a relational [[predicate (logic)|predicate]] involving both ''X'' and ''Y''.

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:

: For all ''X'' of type '''T''', for some unique ''Y'' of type '''U''', ''P''(''X'',''Y''),

Line 33 ⟶ 29:

: For all ''X'' of type '''T''', for all ''Y'' of type '''U''', ''P''(''X'',''Y'') [[if and only if]] ''Y'' = ''F''(''X'').

== 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 [[Gödel'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 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 50 ⟶ 45:

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 ⟶ 61:

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.

== SeeUninterpreted alsofunctions ==

An '''uninterpreted function'''<ref>{{Cite book |last1=Bryant |first1=Randal E. |title=Computer Aided Verification |last2=Lahiri |first2=Shuvendu K. |last3=Seshia |first3=Sanjit A. |year=2002 |isbn=978-3-540-43997-4 |series=Lecture Notes in Computer Science |volume=2404 |pages=78–92 |chapter=Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions |doi=10.1007/3-540-45657-0_7 |chapter-url=https://link.springer.com/content/pdf/10.1007/3-540-45657-0_7.pdf |s2cid=9471360}}</ref> is one that has no other property than its name and ''[[Arity|n-ary]]'' form. The theory of uninterpreted functions is also sometimes called the free theory, because it is freely generated, and thus a [[free object]], or the empty theory, being the [[Theory (mathematical logic)|theory]] having an empty set of [[Sentence (mathematical logic)|sentences]] (in analogy to an [[initial algebra]]). Theories with a non-empty set of equations are known as [[Equational theory|equational theories]]. The [[satisfiability]] problem for free theories is solved by [[syntactic unification]]; algorithms for the latter are used by interpreters for various computer languages, such as [[Prolog]]. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see [[Unification (computer science)]].

=== Example ===

As an example of uninterpreted functions for [[SMT-LIB]], if this input is given to an [[Satisfiability modulo theories|SMT solver]]:<syntaxhighlight lang="text" line="1">

(declare-fun f (Int) Int)

(assert (= (f 10) 1))

</syntaxhighlight>the SMT solver would return "This input is satisfiable". That happens because <code>f</code> is an uninterpreted function (i.e., all that is known about <code>f</code> is its [[Signature (logic)|signature]]), so it is possible that <code>f(10) = 1</code>. But by applying the input below:<syntaxhighlight lang="text" line="1">

(declare-fun f (Int) Int)

(assert (= (f 10) 1))

(assert (= (f 10) 42))

</syntaxhighlight>the SMT solver would return "This input is unsatisfiable". That happens because <code>f</code>, being a function, can never return different values for the same input.

=== Discussion ===

The [[decision problem]] for free theories is particularly important, because many theories can be reduced by it.<ref>{{cite book |last1=de Moura |first1=Leonardo |url=https://leodemoura.github.io/files/sbmf09.pdf |title=Formal methods : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers |last2=Bjørner |first2=Nikolaj |date=2009 |publisher=Springer |isbn=978-3-642-10452-7 |___location=Berlin}}</ref>

Free theories can be solved by searching for [[Common subexpression|common subexpressions]] to form the [[congruence closure]].{{clarify|reason=Indicate about solving which problem in free theories the sentence is supposed to speak. E.g. to solve the satisfiability problem of conjunctions of equations, the Martelli-Montanari syntactic unification algorithm suffices, neither common subexpressions nor congruence closures are needed. Maybe, satisfiability of arbitrary Boolean combinations of equations is meant?|date=May 2014}} Solvers include [[satisfiability modulo theories]] solvers.

==See also==

*[[Algebraic data type]]

*[[Initial algebra]]

*[[Logical connective]]

*[[Logical constant]]

* [[Term algebra]]

* [[Theory of pure equality]]

== References ==

{{reflist}}{{Mathematical logic}}

{{DEFAULTSORT:Functional Predicate}}

[[Category:Model theory]]

[[Category:Articles lacking sources (Erik9bot)]]

[[pl:Symbol funkcyjny]]

[[zh:泛函谓词]]