Functional predicate: Difference between revisions

Revision as of 10:12, 12 March 2013

Revision as of 16:05, 25 September 2014

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 ''composition'' of ''F'' and ''G'', satisfying (''F'' o ''G'')(''X'') = ''F''(''G''(''X'')), [[for all]] ''X''.

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.