Meta tags:
Headings (most frequently used words):
function, symbol, contents, introducing, new, symbols, doing, without, functional, predicates, uninterpreted, functions, see, also, references, example, discussion,
Text of the page (most frequently used words):
the (62), function (37), for (30), type (29), and (28), this (26), #symbol (23), that (21), symbols (21), theory (20), logic (19), #predicate (18), with (16), new (14), one (14), forall (14), formal (13), functional (13), can (12), you (11), theories (11), logical (11), edit (11), displaystyle (11), all (10), set (10), domain (10), statement (9), variable (9), free (9), functions (9), uninterpreted (9), then (9), wikipedia (8), model (8), theorem (8), language (8), codomain (8), also (8), rightarrow (8), predicates (8), non (7), from (7), mathematical (7), problem (7), schema (7), list (7), example (7), other (7), exists (7), introduce (7), there (7), may (6), object (6), tarski (6), theorems (6), are (6), some (6), satisfies (6), additional (5), page (5), mathematics (5), truth (5), proof (5), systems (5), order (5), axiom (5), many (5), proposition (5), form (5), because (5), input (5), given (5), such (5), after (5), any (5), article (5), languages (4), contents (4), search (4), about (4), terms (4), use (4), articles (4), references (4), category (4), history (4), proving (4), recursive (4), calculus (4), satisfiability (4), term (4), constant (4), propositional (4), relation (4), gödel (4), empty (4), first (4), algebra (4), computer (4), see (4), smt (4), same (4), int (4), but (4), doesn (4), allow (4), must (4), over (4), only (4), specifically (4), representing (4), more (4), hide (4), move (4), sidebar (4), toggle (3), view (3), was (3), 2025 (3), needing (3), sets (3), primitive (3), arithmetic (3), finite (3), equivalence (3), atomic (3), consequence (3), boolean (3), foundations (3), general (3), types (3), paradox (3), 2009 (3), pdf (3), solver (3), would (3), return (3), assert (3), than (3), used (3), unification (3), certain (3), want (3), course (3), replace (3), not (3), condition (3), get (3), make (3), introducing (3), unique (3), relational (3), will (3), typed (3), similarly (3), defined (3), modelled (3), tools (3), main (3), table (2), contact (2), privacy (2), policy (2), using (2), clarification (2), september (2), short (2), description (2), different (2), wikidata (2), portal (2), abstract (2), algebraic (2), related (2), turing (2), lambda (2), decision (2), computable (2), church (2), validity (2), kripke (2), semantics (2), complete (2), elementary (2), diagram (2), standard (2), spectrum (2), interpretation (2), verifying (2), ordinal (2), hilbert (2), axiomatic (2), rule (2), inference (2), euclidean (2), skolem (2), second (2), signature (2), connective (2), ground (2), formula (2), definition (2), extension (2), von (2), neumann (2), grothendieck (2), zermelo (2), fraenkel (2), number (2), cardinality (2), element (2), monadic (2), argument (2), incompleteness (2), information (2), 978 (2), isbn (2), methods (2), science (2), 540 (2), initial (2), solved (2), solvers (2), include (2), particularly (2), discussion (2), happens (2), being (2), declare (2), fun (2), known (2), its (2), possible (2), applying (2), has (2), called (2), thus (2), algorithms (2), syntactic (2), equational (2), version (2), replacement (2), now (2), suitable (2), introduction (2), correct (2), applies (2), what (2), guard (2), quantification (2), quantified (2), both (2), treatments (2), another (2), above (2), how (2), anything (2), each (2), material (2), special (2), section (2), whenever (2), able (2), need (2), metalogical (2), doing (2), without (2), define (2), every (2), satisfying (2), identity (2), equation (2), composition (2), which (2), simply (2), big (2), represents (2), basic (2), discourse (2), learn (2), help (2), sources (2), citations (2), notation (2), appearance (2), upload (2), file (2), changes (2), links (2), read (2), log (2), create (2), account (2), donate (2), menu (2), add, topic, mobile, cookie, statistics, developers, code, conduct, legal, safety, contacts, disclaimers, text, available, under, apply, site, agree, registered, trademark, profit, organization, wikimedia, foundation, inc, creative, commons, attribution, sharealike, license, rendered, parsoid, last, edited, october, utc, hidden, categories, 2014, retrieved, https, org, index, php, title, function_symbol, oldid, 1315877491, uninterpreted_functions, supertask, philosophy, logicism, timeline, concrete, automated, machine, recursion, kolmogorov, complexity, versus, undecidable, decidable, computably, enumerable, thesis, encoding, computability, ultraproduct, value, transfer, principle, semantic, strength, categorical, submodel, saturated, prime, models, self, reverse, analysis, impossibility, zfc, independence, deductive, sequent, natural, deduction, principia, mathematica, elements, geometry, minimal, axioms, canonical, algebras, axiomatization, real, numbers, robinson, peano, true, substitution, string, sentence, rank, quantifier, metalanguage, bound, open, closed, grammar, formation, conservative, expression, automata, arity, alphabet, syntax, constructive, ackermann, bernays, naive, morse, kelley, platek, continuum, hypothesis, choice, binary, operation, aleph, inaccessible, large, cardinal, enumeration, numbering, isomorphism, schröder, bernstein, jection, sur, image, map, maps, constructible, universe, universal, fuzzy, ultrafilter, transitive, infinite, singleton, inhabited, uncountable, countable, operations, identities, power, cartesian, product, complement, union, intersection, partition, forcing, extensionality, class, hereditary, quantifiers, fixed, point, higher, valued, tables, connectives, venn, square, opposition, syllogism, soundness, equiconsistency, consistency, tautology, classical, traditional, logics, russell, löwenheim, lindström, halting, compactness, diagonal, cantor, banach, undefinability, completeness, paradoxes, lemma, moura, leonardo, bjørner, nikolaj, berlin, springer, 642, 10452, applications, 12th, brazilian, symposium, sbmf, gramado, brazil, august, revised, selected, papers, bryant, randal, lahiri, shuvendu, seshia, sanjit, 2002, lecture, notes, vol, 2404, 9471360, s2cid, 43997, 1007, 45657, 0_7, doi, aided, verification, modeling, counter, expressions, pure, equality, data, searching, modulo, needed, congruence, closure, common, subexpressions, important, reduced, unsatisfiable, never, values, satisfiable, below, lib, property, name, sometimes, freely, generated, having, analogy, equations, latter, interpreters, various, prolog, sentences, ary, alternatively, interpret, original, merely, abbreviation, produced, end, almost, too, actually, still, isn, just, let, take, uses, states, elimination, convenient, purposes, deal, explicitly, instead, way, think, seem, wish, specify, know, ahead, time, whether, equivalent, formulation, immediately, corresponding, introduced, beginning, finally, entire, uniqueness, universally, quantify, kind, had, proven, before, previous, replaced, intuitively, means, appear, deductions, don, useful, context, where, nor, matter, method, replacing, wherever, former, occur, furthermore, algorithmic, most, result, additionally, appropriate, working, have, around, next, prove, indicate, note, itself, involving, system, gets, automatically, untyped, inclusion, associated, ways, constructing, out, old, ones, subtype, treatment, allows, right, side, sense, unless, matches, required, requirement, consistent, mathbf, consider, analogous, zero, variables, though, formally, does, represent, component, whole, therefore, concepts, notion, mapping, when, remove, message, please, unsourced, challenged, jstor, scholar, books, newspapers, news, find, removed, adding, reliable, improve, needs, generalization, concept, redirected, encyclopedia, item, projects, printable, download, print, export, switch, legacy, parser, shortened, url, cite, permanent, link, here, actions, english, talk, polski, 日本語, italiano, subsection, top, personal, pages, recent, community, contribute, random, current, events, navigation, jump, content,
Text of the page (random words):
function symbol wikipedia jump to content main menu main menu move to sidebar hide navigation main page contents current events random article about wikipedia contact us contribute help learn to edit community portal recent changes upload file special pages search search appearance donate create account log in personal tools donate create account log in contents move to sidebar hide top 1 introducing new function symbols 2 doing without functional predicates 3 uninterpreted functions toggle uninterpreted functions subsection 3 1 example 3 2 discussion 4 see also 5 references toggle the table of contents function symbol 4 languages italiano 日本語 polski 中文 edit links article talk english read edit view history tools tools move to sidebar hide actions read edit view history general what links here related changes upload file permanent link page information cite this page get shortened url switch to legacy parser print export download as pdf printable version in other projects wikidata item appearance move to sidebar hide from wikipedia the free encyclopedia redirected from uninterpreted function symbol representing a mathematical concept this article is about the generalization of function in mathematical logic for symbols and notation used for functions see function mathematics notation this article needs more citations please help improve this article by adding citations to reliable sources unsourced material may be challenged and removed find sources function symbol news newspapers books scholar jstor september 2025 learn how and when to remove this message in formal systems particularly mathematical logic a function symbol is a non logical symbol which represents a function or 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 terms specifically if the symbol f displaystyle f is a function symbol then given any constant symbol x displaystyle x representing an object in the language f x displaystyle f x also represents an object in the language similarly if t displaystyle t is some term in the language f t displaystyle f t 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 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 zero variables is simply a constant symbol now consider a model of the formal language with the types t and u modelled by 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 f x f x x t displaystyle f big x f x x in mathbf t big which is simply a function with domain t and codomain u it is a requirement of a consistent model that f x f y whenever x y introducing new function symbols edit 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 composition of f and g satisfying f 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 one also gets certain function symbols automatically 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 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 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 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 then you can introduce a function symbol f of domain type t and codomain type u that satisfies 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 edit many treatments of predicate logic don t allow functional predicates only relational predicates this is useful for example in the context of proving metalogical theorems such as gödel s incompleteness theorems 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 y of type u p x y of course this is the same proposition that had to be proven 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 this may seem to be a problem if you wish to specify a proposition schema that applies only to functional predicates f how do you know ahead of time whether it satisfies that condition 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 consequence of the uniqueness condition for a functional predicate above let us take as an example the axiom schema of replacement in zermelo fraenkel set theory this example uses mathematical symbols this schema states in one form for any functional predicate f in one variable a b c c a f c b displaystyle forall a exists b forall c c in a rightarrow f c in b first we must replace f c with some other variable d a b c c a d b displaystyle forall a exists b forall c c in a rightarrow d in b of course this statement isn t correct d must be quantified over just after c a b c d c a d b displaystyle forall a exists b forall c forall d c in a rightarrow d in b we still must introduce p to guard this quantification a b c d p c d c a d b displaystyle forall a exists b forall c forall d p c d rightarrow c in a rightarrow d in b this is almost correct but it applies to too many predicates what we actually want is x y p x y a b c d p c d c a d b displaystyle forall x exists y p x y rightarrow forall a exists b forall c forall d p c d rightarrow c in a rightarrow d in b 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 uninterpreted functions edit an uninterpreted function 1 is one that has no other property than its name and 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 having an empty set of sentences in analogy to an initial algebra theories with a non empty set of equations are known as 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 edit as an example of uninterpreted functions for smt lib if this input is given to an smt solver declare fun f int int assert f 10 1 the smt solver would return this input is satisfiable that happens because f is an uninterpreted function i e all that is known about f is its signature so it is possible that f 10 1 but by applying the input below declare fun f int int assert f 10 1 assert f 10 42 the smt solver would return this input is unsatisfiable that happens because f being a function can never return different values for the same input discussion edit the decision problem for free theories is particularly important because many theories can be reduced by it 2 free theories can be solved by searching for common subexpressions to form the congruence closure clarification needed solvers include satisfiability modulo theories solvers see also edit algebraic data type initial algebra logical connective logical constant term algebra theory of pure equality references edit bryant randal e lahiri shuvendu k seshia sanjit a 2002 modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions pdf computer aided verification lecture notes in computer science vol 2404 pp 78 92 doi 10 1007 3 540 45657 0_7 isbn 978 3 540 43997 4 s2cid 9471360 de moura leonardo bjørner nikolaj 2009 formal methods foundations and applications 12th brazilian symposium on formal methods sbmf 2009 gramado brazil august 19 21 2009 revised selected papers pdf berlin springer isbn 978 3 642 10452 7 v t e mathematical logic general axiom list cardinality first order logic formal proof formal semantics foundations of mathematics information theory lemma logical consequence model theorem theory type theory theorems list paradoxes gödel s completeness incompleteness theorems tarski s undefinability banach tarski paradox cantor s theorem paradox diagonal argument compactness halting problem lindström s löwenheim skolem russell s paradox logics traditional classical logic logical truth tautology proposition inference logical equivalence consistency equiconsistency argument soundness validity syllogism square of opposition venn diagram propositional boolean algebra boolean functions logical connectives propositional calculus propositional formula truth tables many valued logic 3 finite predicate first order list second order monadic higher order fixed point free quantifiers predicate monadic predicate calculus set theory set hereditary class ur element ordinal number extensionality forcing relation equivalence partition set operations intersection union complement cartesian product power set identities types of sets countable uncountable empty inhabited singleton finite infinite transitive ultrafilter recursive fuzzy universal universe constructible grothendieck von neumann maps cardinality function map domain codomain image in sur bi jection schröder bernstein theorem isomorphism gödel numbering enumeration large cardinal inaccessible aleph number operation binary theories zermelo fraenkel axiom of choice continuum hypothesis general kripke platek morse kelley naive new foundations tarski grothendieck von neumann bernays gödel ackermann constructive formal systems list language syntax alphabet arity automata axiom schema expression ground extension by definition conservative relation formation rule grammar formula atomic closed ground open free bound variable language metalanguage logical connective predicate functional variable propositional variable proof quantifier rank sentence atomic spectrum signature string substitution symbol function logical constant non logical variable term theory list example axiomatic systems list of true arithmetic peano second order elementary function primitive recursive robinson skolem of the real numbers tarski s axiomatization of boolean algebras canonical minimal axioms of geometry euclidean elements hilbert s tarski s non euclidean principia mathematica proof theory formal proof natural deduction logical consequence rule of inference sequent calculus theorem systems axiomatic deductive hilbert list complete theory independence from zfc proof of impossibility ordinal analysis reverse mathematics self verifying theories model theory interpretation function of models model atomic equivalence finite prime saturated spectrum submodel non standard model of non standard arithmetic diagram elementary categorical theory model complete theory satisfiability semantics of logic strength theories of truth semantic tarski s kripke s t schema transfer principle truth predicate truth value type ultraproduct validity computability theory church encoding church turing thesis computably enumerable computable function computable set decision problem decidable undecidable p np p versus np problem kolmogorov complexity lambda calculus primitive recursive function recursion recursive set turing machine type theory related abstract logic algebraic logic automated theorem proving category theory concrete abstract category category of sets history of logic history of mathematical logic timeline logicism mathematical object philosophy of mathematics supertask mathematics portal retrieved from https en wikipedia org w index php title function_symbol oldid 1315877491 uninterpreted_functions category model theory hidden categories articles with short description short description is different from wikidata articles needing additional references from september 2025 all articles needing additional references wikipedia articles needing clarification from may 2014 this page was last edited on 9 october 2025 at 05 05 utc page was rendered with parsoid text is available under the creative commons attribution sharealike 4 0 license additional terms may apply by using this site you...
|
