Introducing New Function Symbols
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.
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 idT with domain and codomain type T; it satisfies idT(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. 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).
Read more about this topic: Functional Predicate
Famous quotes containing the words introducing, function and/or symbols:
“The beginner’s well-known propensity for obtruding upon his own privacy, by introducing himself, or a vicar, into his first novel, owes less to the attraction of a ready theme than to the relief of getting rid of oneself, before going on to better things.”
—Vladimir Nabokov (1899–1977)
“The information links are like nerves that pervade and help to animate the human organism. The sensors and monitors are analogous to the human senses that put us in touch with the world. Data bases correspond to memory; the information processors perform the function of human reasoning and comprehension. Once the postmodern infrastructure is reasonably integrated, it will greatly exceed human intelligence in reach, acuity, capacity, and precision.”
—Albert Borgman, U.S. educator, author. Crossing the Postmodern Divide, ch. 4, University of Chicago Press (1992)
“Many older wealthy families have learned to instill a sense of public service in their offspring. But newly affluent middle-class parents have not acquired this skill. We are using our children as symbols of leisure-class standing without building in safeguards against an overweening sense of entitlement—a sense of entitlement that may incline some young people more toward the good life than toward the hard work that, for most of us, makes the good life possible.”
—David Elkind (20th century)