Content deleted Content added
disambiguate |
→Introducing new function symbols: func comp |
||
Line 15:
==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. Given the function symbols ''F'' and ''G'', one can introduce a new function symbol ''F'' ∘ ''G'', the ''[[function composition|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.
| |||