|Page 305 of 800||Search internet|
In addition to metavariables, check defines the following metaoperators:
The check page declares , , , , and to be metaoperators by defining their 'meta/kg' aspect to be 'infer', 'endorse', 'plus', 'all', and 'false', respectively. If you want to define some other notation and want to use e.g. for then you can use a macro definition:
Alternatively, you can directly declare as a metaoperator:
That allows to state e.g. generalization as
instead of .
The check page macro defines the quantifier such that it can quantify over a list of variables. As an example, is shorthand for .
and have the same charge and are post-associative. As an example, means .
Charges are opposite to those of first order predicate calculus: has greater charge than which in turn has greater charge than and . Thus,
|Page 305 of 800||Search logiweb.eu|