BORIS Theses

BORIS Theses
Bern Open Repository and Information System

Axiomatizing One-Variable Fragments of First-Order Logics

Tokuda, Naomi (2024). Axiomatizing One-Variable Fragments of First-Order Logics. (Thesis). Universität Bern, Bern

[img]
Preview
Text
24tokuda_n.pdf - Thesis
Available under License Creative Commons: Attribution-Noncommercial (CC-BY-NC 4.0).

Download (572kB) | Preview

Abstract

First-order logics are much more expressive than their propositional counterparts, but often lack decidability. To remedy this problem while still maintaining some of the expressivity of first-order logics, we consider one-variable fragments of first-order logics. The one-variable fragment of a first-order logic consists of consequences in the logic constructed using one distinguished variable x, unary predicates, propositional operations, and the quantifiers (∀x) and (∃x). We define a semantics for a first-order logic based on a class of L-lattices, which induces a semantics for its one-variable fragment. However, finding an axiomatization of this fragment is generally not trivial. A Hilbert-style axiomatization of a first-order logic does not yield a Hilbert-style axiomatization of its one-variable fragment, since derivations of one-variable formulas may introduce new variables. Consequence in one-variable first-order logics can be translated into consequence in a class of algebras with modalities. Therefore, the challenge of finding axiomatizations for one-variable fragments may be interpreted as the challenge of finding an equational basis for the corresponding classes of algebras. Despite axiomatization results for certain fragments, a general approach has been missing. In this thesis, we take a first step towards overcoming this challenge, by proving that the class of algebras corresponding to the one-variable fragment of a first-order logic based on a variety of L-lattices that has the superamalgamation property admits an axiomatization by “S5-like” equations. This is achieved through both algebraic and proof-theoretic approaches.

Item Type: Thesis
Dissertation Type: Single
Date of Defense: 29 August 2024
Subjects: 500 Science > 510 Mathematics
Institute / Center: 08 Faculty of Science > Department of Mathematics and Statistics > Institute of Mathematics
Depositing User: Hammer Igor
Date Deposited: 01 Oct 2024 15:45
Last Modified: 01 Oct 2024 15:45
URI: https://boristheses.unibe.ch/id/eprint/5470

Actions (login required)

View Item View Item