Notation

Quantification of formulae are defined using de Bruijn index, but we can write terms and formulae by usual binder notation using macro.

variables x y z is just an example and can take any number of idents. e is an expression of term/formula.

Binder Notation

Binder notation of term takes either form:

Term: ‘x y z. e’, Formula: “x y z. e”
- x y z is the symbol for the bound variables, k:num-variables denotes the terms in Semiterm L ξ (n + $k)/Semiformula L ξ (n + $k). (n can be variable)
Term: ‘x y z | e’, Formula: “x y z | e”
- x y z is the symbol for the free variables, k:num-variables denotes the terms in Semiterm L ξ n/Semiformula L ξ n. (n can be variable)
Term: ‘e’, Formula: “e”
- An abbreviation of ‘ . e’/“ . e”