+++ title = "Predicate with integer evaluation" author = "Yann Herklotz" tags = [] categories = [] backlinks = ["2e1b3c2", "2e1b3c"] forwardlinks = ["2e1b3b", "2e1b3c2"] zettelid = "2e1b3c1" +++ The first possibility is to extend the notion of predicates with two arguments ([\#2e1b3b]), to having multiple arguments. This can be done by having a predicate that evaluates to a natural number, which is then used to select the right variable. However, this has multiple downsides, one being that the predicate basically becomes a function that is opaque to the outside definitions. It would therefore have to carry around many proofs about properties that need to hold for the function, such as it being injective and getting the right property. It being a function would also make it difficult to analyse from the outside, and it would then also be difficult to do symbolic analysis on the predicates. Having a syntactic representation of this kind of function would also be quite complex, and would come with it's own problems. The predicate would have to be quite complex, reducing the amount of analysis that one can do. [\#2e1b3b]: /zettel/2e1b3b