|Page 99 of 800||Search internet|
The universal quantifier of macro expands to . In , neither nor has a meaning of its own in . They only make sense in the combination where they represent a universal quantifier.
Implementing the universal quantifier this way allows to piggyback lambda calculus: A function for checking that a lambda variable does not occur free in a lambda term can be used directly for expressing side conditions in .
Furthermore, the scheme is flexible. It is easy to introduce a new quantifier which macro expands to without having to modify the code which implements side conditions.
The initial f in f.allfunc is a reference to . Other theories may have other quantifiers.
If one decides to implement ZFC on top of and if one decides ZFC should have a constructs like , then one can use the same trick and represent as something like .
|Page 99 of 800||Search logiweb.eu|