6.7.13 Representation of object quantifiers

Page 99 of 800

Search internet

The universal quantifier all x : A of FOL macro expands to $f.allfunc \ x . A$ . In FOL , neither f.allfunc z nor $\ x . A$ has a meaning of its own in FOL . They only make sense in the $f.allfunc \ x . A$ combination where they represent a universal quantifier.

Implementing the universal quantifier this way allows FOL 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 FOL .

Furthermore, the scheme is flexible. It is easy to introduce a new quantifier exist x : A which macro expands to $f.existfunc \ x . A$ without having to modify the code which implements side conditions.

The initial f in f.allfunc is a reference to FOL . Other theories may have other quantifiers.

If one decides to implement ZFC on top of FOL and if one decides ZFC should have a constructs like $"\{ x \in S | p \}"$ , then one can use the same trick and represent $"\{ x \in S | p \}"$ as something like $"comprehension ( "[ S ]" , "[ \ x . P ]")"$ .

Page 99 of 800

Search logiweb.eu