A Compact [0,1]-valued First-order Lukasiewicz Logic with Identity on Hilbert Space
Daniele Mundici · Journal of Logic and Computation · 2009
By an MV-set, we understand a pair (E,X) where X is a set of unit vectors in a Hilbert space E such that the linear span of X is dense in E, and 〈v,w〉 ≥ 0 for all v,w ∈ X. The scalar product 〈v,w〉 ∈ [0,1] is the identity degree of v and w. Building on MV-sets and continuous functions and relations defined on them, we construct a compact [0,1]-valued first-order Łukasiewicz logic, whose set of unsatisfiable formulas is recursively enumerable. In the particular case when X is an orthonormal basis of E we recover classical Skolem first-order logic with identity, constants, functions and relations. Our main tools are the Kolmogorov dilation theorem for positive semidefinite kernels, and the Tarski–Seidenberg decision method for elementary algebra and geometry.