6.7.13 Representation of object quantifiers

Prev Up Next 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 ]")".

Prev Up Next Page 99 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05