Variables in Formulae of the First Order Language 1
Grzegorz Bancerek · 1990
The articles [7], [5], [9], [8], [3], [4], [2], [6], and [1] provide the notation and terminology for this paper. For simplicity, we adopt the following convention: i, j, k denote natural numbers, x denotes a bound variable, a denotes a free variable, p, q denote elements of WFF, l denotes a finite sequence of elements of Var, P denotes a predicate symbol, and V denotes a non empty subset of Var. In this article we present several logical schemes. The scheme QC Func Uniq deals with a non empty set A , a function B from WFF into A , a function C from WFF into A , an element D of A , a unary functor F yielding an element of A , a unary functor G yielding an element of A , a binary functor H yielding an element of A , and a binary functor I yielding an element of A , and states that: B = C provided the following conditions are met: • Let given p and d1, d2 be elements of A . Then (i) if p = VERUM, then B(p) = D, (ii) if p is atomic, then B(p) = F (p), (iii) if p is negative and d1 = B(Arg(p)), then B(p) = G(d1), (iv) if p is conjunctive and d1 = B(LeftArg(p)) and d2 = B(RightArg(p)), then B(p) = H (d1,d2), and (v) if p is universal and d1 = B(Scope(p)), then B(p) = I (p,d1), and • Let given p and d1, d2 be elements of A . Then (i) if p = VERUM, then C (p) = D, (ii) if p is atomic, then C (p) = F (p), (iii) if p is negative and d1 = C (Arg(p)), then C (p) = G(d1), (iv) if p is conjunctive and d1 = C (LeftArg(p)) and d2 = C (RightArg(p)), then C (p) = H (d1,d2), and (v) if p is universal and d1 = C (Scope(p)), then C (p) = I (p,d1). The scheme QC Def D deals with a non empty set A , an element B of A , an element C of WFF, a unary functor F yielding an element of A , a unary functor G yielding an element of A , a binary