Interpretation and Satisfiability in the First Order Logic
Edmund Woronowicz · 1990
The articles [6], [3], [1], [5], [4], [2], and [7] provide the notation and terminology for this paper. In the sequel i, k are natural numbers and A, D are non-empty sets. Let us consider A. The functor V(A) yields a non-empty set of functions and is defined by: V(A) = ABoundVar. The following propositions are true: (1) V(A) = ABoundVar. (2) For an arbitrary x such that x is an element of V(A) holds x is a function from BoundVar into A. Let us consider A. Then V(A) is a non-empty set of functions from BoundVar to A. In the sequel x, y will be bound variables and v, v1 will be elements of V(A). Let us consider A, v, x. Then v(x) is an element of A. We now define two new functors. Let us consider A, and let p be an element of Boolean. The functor ¬p yields an element of Boolean and is defined by: for every element x of A holds (¬p)(x) = ¬(p(x)). Let q be an element of Boolean. The functor p ∧ q yielding an element of Boolean is defined as follows: for every element x of A holds (p ∧ q)(x) = (p(x)) ∧ (q(x)). We now state two propositions: