Logiweb(TM)

8.2.2 Metaoperators

Prev Up Next Page 305 of 800 Search internet


In addition to metavariables, check defines the following metaoperators:

x infer y
If the premise x is provable then the conclusion y is provable.
x endorse y
If the side condition x evaluates to true then the conclusion y is provable.
x oplus y
Both x and y are provable.
All x : y
y is provable for all terms x.
False
Everything is provable. A theory is said to be inconsistent if it can prove the absurdity False.

The check page declares x infer y, x endorse y, x oplus y, All x : y, and False 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. x infer2 y for x infer y then you can use a macro definition:

macro define x infer2 y as x infer y end define

Alternatively, you can directly declare x infer2 y as a metaoperator:

meta define x infer2 y as "infer" end define

That allows to state e.g. generalization as

#a infer2 all #x : #a

instead of #a infer all #x : #a.

The check page macro defines the quantifier such that it can quantify over a list of variables. As an example, All x ,, y : z is shorthand for All x : All y : z.

x infer y and x endorse y have the same charge and are post-associative. As an example, x infer y infer z means x infer ( y infer z ).

Charges are opposite to those of first order predicate calculus: x oplus y has greater charge than All x : y which in turn has greater charge than x infer y and x endorse y. Thus,

All #x ,, #y : #x imply #y infer #x infer #y oplus All #u ,, #x : #x infer all #u : #x

means

( All #x ,, #y : ( ( #x imply #y ) infer ( #x infer #y ) ) ) oplus ( All #u ,, #x : ( #x infer all #u : #x ) )

Prev Up Next Page 305 of 800 Search logiweb.eu

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