One-Variable Fragments of First-Order Many-Valued Logics
In this thesis we study one-variable fragments of first-order logics. Such a one-variable fragment consists of those first-order formulas that contain only unary predicates and a single variable. These fragments can be viewed from a modal perspective by replacing the universal and existential quantifier with a box and diamond modality, respectively, and the unary predicates with corresponding propositional variables. Under this correspondence, the one-variable fragment of first-order classical logic famously corresponds to the modal logic S5.
This thesis explores some such correspondences between first-order and modal logics. Firstly, we study first-order intuitionistic logics based on linear intuitionistic Kripke frames. We show that their one-variable fragments correspond to particular modal Gödel logics, defined over many-valued S5-Kripke frames. For a large class of these logics, we prove the validity problem to be decidable, even co-NP-complete. Secondly, we investigate the one-variable fragment of first-order Abelian logic, i.e., the first-order logic based on the ordered additive group of the reals. We provide two completeness results with respect to Hilbert-style axiomatizations: one for the one-variable fragment, and one for the one-variable fragment that does not contain any lattice connectives. Both these fragments are proved to be decidable. Finally, we launch a much broader algebraic investigation into one-variable fragments. We turn to the setting of first-order substructural logics (with the rule of exchange). Inspired by work on, among others, monadic Boolean algebras and monadic Heyting algebras, we define monadic commutative pointed residuated lattices as a first (algebraic) investigation into one-variable fragments of this large class of first-order logics. We prove a number of properties for these newly defined algebras, including a characterization in terms of relatively complete subalgebras as well as a characterization of their congruences.