8.2.2 Metaoperators

Page 305 of 800

Search internet

In addition to metavariables, check defines the following metaoperators:

If the premise is provable then the conclusion is provable.

If the side condition evaluates to then the conclusion is provable.

Both and are provable.

is provable for all terms .

Everything is provable. A theory is said to be inconsistent if it can prove the absurdity .

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,

means

Page 305 of 800

Search logiweb.eu