Content deleted Content added
m remove Erik9bot category,outdated, tag and general fixes |
→Doing without functional predicates: Added link. |
||
Line 38:
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'').
| |||