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. Functional predicates are also sometimes called mappings , but that term has additional meanings in mathematics . In a model , a function symbol will be modelled by a function .
21-462: [REDACTED] Look up mapping in Wiktionary, the free dictionary. Mapping may refer to: Cartography , the process of making a map Mapping (mathematics) , a synonym for a mathematical function and its generalizations Mapping (logic) , a synonym for functional predicate Types of mapping [ edit ] Animated mapping ,
42-414: 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. Note that P will itself be
63-455: A map See also [ edit ] All pages with titles beginning with Mapping All pages with titles containing Mapping Mapping theorem (disambiguation) Mappings (poetry) Surveying , the field work of gathering map data Topics referred to by the same term [REDACTED] This disambiguation page lists articles associated with the title Mapping . If an internal link led you here, you may wish to change
84-434: 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
105-491: A practice of some religions Texture mapping , in computer graphics Web mapping , the use of the World Wide Web to depict spatial data on a map See also [ edit ] All pages with titles beginning with Mapping All pages with titles containing Mapping Mapping theorem (disambiguation) Mappings (poetry) Surveying , the field work of gathering map data Topics referred to by
126-404: 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: (Of course, this is the same proposition that had to be proven as a theorem before introducing
147-402: 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
168-464: A relational predicate involving both X and Y . So if there is such a predicate P and a theorem: then you can introduce a function symbol F of domain type T and codomain type U that satisfies: 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
189-443: 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
210-504: 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
231-496: Is different from Wikidata All article disambiguation pages All disambiguation pages Mapping (logic) Specifically, the symbol F in a 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 )
SECTION 10
#1732772953598252-746: 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: First, we must replace F ( C ) with some other variable D : Of course, this statement isn't correct; D must be quantified over just after C : We still must introduce P to guard this quantification: This
273-485: 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
294-460: The depiction of events over time on a map using sequential images representing each timeframe Brain mapping , the techniques used to study the brain Data mapping , data element mappings between two distinct data models Digital mapping , the use of a computer to depict spatial data on a map Gene mapping , the assignment of DNA fragments to chromosomes Mind mapping , the drawing of ideas and
315-425: The free dictionary. Mapping may refer to: Cartography , the process of making a map Mapping (mathematics) , a synonym for a mathematical function and its generalizations Mapping (logic) , a synonym for functional predicate Types of mapping [ edit ] Animated mapping , the depiction of events over time on a map using sequential images representing each timeframe Brain mapping ,
336-399: 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
357-448: The link to point directly to the intended article. Retrieved from " https://en.wikipedia.org/w/index.php?title=Mapping&oldid=1257757262 " Category : Disambiguation pages Hidden categories: Short description is different from Wikidata All article disambiguation pages All disambiguation pages mapping [REDACTED] Look up mapping in Wiktionary,
378-407: The relations among them Projection mapping , the projection of videos on the surface of objects with irregular shapes Robotic mapping , creation and use of maps by robots Satellite mapping , taking photos of Earth from space Spiritual mapping , a practice of some religions Texture mapping , in computer graphics Web mapping , the use of the World Wide Web to depict spatial data on
399-411: The same term [REDACTED] This disambiguation page lists articles associated with the title Mapping . If an internal link led you here, you may wish to change the link to point directly to the intended article. Retrieved from " https://en.wikipedia.org/w/index.php?title=Mapping&oldid=1257757262 " Category : Disambiguation pages Hidden categories: Short description
420-417: The set 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 ]. 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 ,
441-560: The techniques used to study the brain Data mapping , data element mappings between two distinct data models Digital mapping , the use of a computer to depict spatial data on a map Gene mapping , the assignment of DNA fragments to chromosomes Mind mapping , the drawing of ideas and the relations among them Projection mapping , the projection of videos on the surface of objects with irregular shapes Robotic mapping , creation and use of maps by robots Satellite mapping , taking photos of Earth from space Spiritual mapping ,
SECTION 20
#1732772953598#597402