1.1. 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.
1.1.1. 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”