-
Normalization and cut-elimination theorems for some logics of evidence and truth
Authors:
Marcelo E. Coniglio,
Martín Figallo,
Abilio Rodrigues
Abstract:
In this paper, we investigate proof-theoretic aspects of the logics of evidence and truth LETJ and LETF. These logics extend, respectively, Nelson's logic N and the logic of first-degree entailment FDE, also known as Belnap-Dunn four-valued logic, with a classicality operator that recovers classical logic for formulas in its scope. We will present natural deduction and sequent systems for LETJ and…
▽ More
In this paper, we investigate proof-theoretic aspects of the logics of evidence and truth LETJ and LETF. These logics extend, respectively, Nelson's logic N and the logic of first-degree entailment FDE, also known as Belnap-Dunn four-valued logic, with a classicality operator that recovers classical logic for formulas in its scope. We will present natural deduction and sequent systems for LETJ and LETF, together with proofs of normalization and cut-elimination theorems, respectively. As a corollary, we obtain decidability for both logics.
△ Less
Submitted 31 May, 2024;
originally announced May 2024.
-
Tense distributive lattices: algebra, logic and topology
Authors:
Aldo Victorio Figallo,
Jonathan Sarmiento,
Martín Figallo
Abstract:
Tense logic was introduced by Arthur Prior in the late 1950s as a result of his interest in the relationship between tense and modality. Prior's idea was to add four primitive modal-like unary connectives to the base language today widely known as Prior's tense operators. Since then, Prior's operators have been considered in many contexts by different authors, in particular, in the context of alge…
▽ More
Tense logic was introduced by Arthur Prior in the late 1950s as a result of his interest in the relationship between tense and modality. Prior's idea was to add four primitive modal-like unary connectives to the base language today widely known as Prior's tense operators. Since then, Prior's operators have been considered in many contexts by different authors, in particular, in the context of algebraic logic.
Here, we consider the category tdlat of bounded distributive lattices equipped with Prior's tense operators. We establish categorical dualities for tdlat in terms of certain categories of Kripke frames and Priestley spaces, respectively. As an application, we characterize the congruence lattice of any tense distributive lattice as well as the subdirectly irreducible members of this category. Finally, we define the logic that preserves degrees of truth with respect to tdlat-algebras and precise the relation between particular sub-classes of tdlat and know tense logics found in the literature.
△ Less
Submitted 9 September, 2023;
originally announced September 2023.
-
Normal proofs and tableaux for the Font-Rius tetravalent modal logic
Authors:
Marcelo Coniglio,
Martín Figallo
Abstract:
Tetravalent modal logic (T ML) was introduced by Font and Rius in 2000; and it is an expansion of the Belnap-Dunn four{valued logic FOUR, a logical system that is well{known for the many applications it has been found in several fields. Besides, T ML is the logic that preserve degrees of truth with respect to Monteiro's tetravalent modal algebras. Among other things, Font and Rius showed that T ML…
▽ More
Tetravalent modal logic (T ML) was introduced by Font and Rius in 2000; and it is an expansion of the Belnap-Dunn four{valued logic FOUR, a logical system that is well{known for the many applications it has been found in several fields. Besides, T ML is the logic that preserve degrees of truth with respect to Monteiro's tetravalent modal algebras. Among other things, Font and Rius showed that T ML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in [16], it was presented a sequent system for T ML with the cut{elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present work, we continue with the study of T ML under a proof-theoretic perspective. In first place, we show that the natural deduction system given in [16] admits a normalization theorem. In second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced in [17], we define a decidable tableau system adequate to check validity in the logic T ML. Finally, we provide a sound and complete tableau system for T ML in the original language.These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras.
△ Less
Submitted 28 April, 2023;
originally announced May 2023.
-
On the logic that preserves degrees of truth associated to involutive Stone algebras
Authors:
Liliana M. Cantú,
Martín Figallo
Abstract:
Involutive Stone algebras (or {\bf S}--algebras) were introduced by R. Cignoli and M. Sagastume in connection to the theory of $n$-valued Łukasiewicz--Moisil algebras.
In this work we focus on the logic that preserves degrees of truth associated to involutive Stone algebras, named {\bf \em Six}. This follows a very general pattern that can be considered for any class of truth structure endowed w…
▽ More
Involutive Stone algebras (or {\bf S}--algebras) were introduced by R. Cignoli and M. Sagastume in connection to the theory of $n$-valued Łukasiewicz--Moisil algebras.
In this work we focus on the logic that preserves degrees of truth associated to involutive Stone algebras, named {\bf \em Six}. This follows a very general pattern that can be considered for any class of truth structure endowed with an ordering relation, and which intends to exploit many--valuedness focusing on the notion of inference that results from preserving lower bounds of truth values, and hence not only preserving the value $1$.
Among other things, we prove that {\bf \em Six} is a many--valued logic (with six truth values) that can be determined by a finite number of matrices (four matrices). Besides, we show that {\bf \em Six} is a paraconsistent logic. Moreover, we prove that it is a genuine LFI (Logic of Formal Inconsistency) with a consistency operator that can be defined in terms of the original set of connectives. Finally, we study the proof theory of {\bf \em Six} providing a Gentzen calculus for it, which is sound and complete with respect to the logic.
△ Less
Submitted 23 April, 2023;
originally announced April 2023.
-
Cut-free sequent-style systems for a logic associated to involutive Stone algebras
Authors:
Liliana M. Cantú,
Martín Figallo
Abstract:
In \cite{LC, LCMF}, it was introduced a logic (called \Six ) associated to a class of algebraic structures known as {\em involutive Stone algebras}. This class of algebras, denoted by \Sto , was considered by the first time in \cite{CS1} as a tool for the study of certain problems connected to the theory of finite--valued Łukasiewicz--Moisil algebras. In fact, \Six\ is the logic that preserves deg…
▽ More
In \cite{LC, LCMF}, it was introduced a logic (called \Six ) associated to a class of algebraic structures known as {\em involutive Stone algebras}. This class of algebras, denoted by \Sto , was considered by the first time in \cite{CS1} as a tool for the study of certain problems connected to the theory of finite--valued Łukasiewicz--Moisil algebras. In fact, \Six\ is the logic that preserves degrees of truth with respect to the class \Sto .
Among other things, it was proved that \Six\ is a 6--valued logic that is a {\em Logic of Formal Inconsistency} (\LFI ); moreover, it is possible to define a consistency operator in terms of the original set of connectives. A Gentzen-style system (which does not enjoy the cut--elimination property) for \Six\ was given. Besides, in \cite{LCMF}, it was shown that \Six\ is matrix logic that is determined by a finite number of matrices; more precisely, four matrices. However, this result was further sharpened in \cite{SMUR} proving that just one of these four matrices determine \Six , that is, \Six\ can be determined by a single 6--element logic matrix.
In this work, taking advantage of this last result, we apply a method due to Avron, Ben-Naim and Konikowska \cite{Avron02} to present different Gentzen systems for \Six\ enjoying the cut--elimination property. This allows us to draw some conclusions about the method as well as to propose additional tools for the streamlining process. Finally, we present a decision procedure for \Six\ based in one of these systems.
△ Less
Submitted 23 April, 2023;
originally announced April 2023.
-
Proof-theoretic aspects of paraconsistency with strong consistency operator
Authors:
Victoria Arce Pistone,
Martín Figallo
Abstract:
In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (LFI) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such LFI's. In our work, we intend make a first step in that direction. On the other hand, the logic Ciore was d…
▽ More
In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (LFI) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such LFI's. In our work, we intend make a first step in that direction. On the other hand, the logic Ciore was developed to provide new logical systems in the study of inconsistent databases from the point of view of LFI. An interesting fact about Ciore is that it has a strong consistency operator, that is, a consistency operator which (forward/backward) propagates inconsistency. Also, it turns out to be an algebraizable logic (in the sense of Blok and Pigozzi) that can be characterized by means of a 3-valued logical matrix. Recently, a first-order version of Ciore, namely QCiore, was defined preserving the spirit of Ciore, that is, without introducing unexpected relations between the quantifiers. Besides, some important model-theoretic results were obtained for this logic.
In this paper we study some proof--theoretic aspects of both Ciore and QCiore respectively. In first place, we introduce a two-sided sequent system for Ciore. Later, we prove that this system enjoys the cut-elimination property and apply it to derive some interesting properties. Later, we extend the above-mentioned system to first-order languages and prove completeness and cut-elimination property using the well-known Shütte's technique.
△ Less
Submitted 22 April, 2023;
originally announced April 2023.
-
On a four-valued logic of formal inconsistency and formal underterminedness
Authors:
Marcelo E. Coniglio,
G. T. Gomez-Pereira,
Martín Figallo
Abstract:
Belnap-Dunn's relevance logic, BD, was designed seeking a suitable logical device for dealing with multiple information sources which sometimes may provide inconsistent and/or incomplete pieces of information. BD is a four-valued logic which is both paraconsistent and paracomplete. On the other hand, De and Omori while investigating what classical negation amounts to in a paracomplete and paracons…
▽ More
Belnap-Dunn's relevance logic, BD, was designed seeking a suitable logical device for dealing with multiple information sources which sometimes may provide inconsistent and/or incomplete pieces of information. BD is a four-valued logic which is both paraconsistent and paracomplete. On the other hand, De and Omori while investigating what classical negation amounts to in a paracomplete and paraconsistent four-valued setting, proposed the expansion BD2 of the four valued Belnap-Dunn logic by a classical negation.
In this paper, we reintroduce the logic BD2 by means of a primitive weak consistency operator $©$. This approach allows us to state in a direct way that this is not only a Logic of Formal Inconsistency (LFI) but also a Logic of Formal Underterminedness (LFU). After presenting a natural Hilbert-style characterization of BD2 obtained by means of twist-structures semantics, we propose a first-order version of BD2 called QBD2, with semantics based on an appropriate notion of partial structures. We show that in QBD2, $\exists$ and $\forall$ are interdefinable in terms of the paracomplete and paraconsistent negation, and not by means of the the classical negation. Finally, a Hilbert-style calculus for QBD2 is presented, proving the corresponding and soundness and completeness theorems.
△ Less
Submitted 3 December, 2022;
originally announced December 2022.
-
Super-Łukasiewicz logics expanded by $Δ$
Authors:
Aldo V. Figallo,
Aldo Figallo-Orellano,
Martín Figallo
Abstract:
Baaz's operator $Δ$ was introduced (by Baaz) in order to extend Gödel logics, after that this operator was used to expand fuzzy logics by Hájek in his celebrated book. These logics were called $Δ$-fuzzy logics. On the other hand, possibility operators were studied in the setting of Łukasiewicz-Moisil algebras; curiously, one of these operators coincide with the Baaz's one. In this paper, we study…
▽ More
Baaz's operator $Δ$ was introduced (by Baaz) in order to extend Gödel logics, after that this operator was used to expand fuzzy logics by Hájek in his celebrated book. These logics were called $Δ$-fuzzy logics. On the other hand, possibility operators were studied in the setting of Łukasiewicz-Moisil algebras; curiously, one of these operators coincide with the Baaz's one. In this paper, we study the $Δ$ operator in the context of ($n$-valued) Super-Łukasiewicz logics. An algebraic study of these logics is presented and the cardinality of Lindembaun-Tarski algebra with a finite number of variables is given. Finally, as a by-product, we present an alternative axiomatization of Hájek's Łukasiwicz logic expanded with $Δ$.
△ Less
Submitted 4 November, 2022;
originally announced November 2022.
-
Cut--free sequent calculus and natural deduction for the tetravalent modal logic
Authors:
Martín Figallo
Abstract:
The {\em tetravalent modal logic} ($\cal TML$) is one of the two logics defined by Font and Rius (\cite{FR2}) (the other is the {\em normal tetravalent modal logic} ${\cal TML}^N$) in connection with Monteiro's tetravalent modal algebras. These logics are expansions of the well--known {\em Belnap--Dunn's four--valued logic} that combine a many-valued character (tetravalence) with a modal character…
▽ More
The {\em tetravalent modal logic} ($\cal TML$) is one of the two logics defined by Font and Rius (\cite{FR2}) (the other is the {\em normal tetravalent modal logic} ${\cal TML}^N$) in connection with Monteiro's tetravalent modal algebras. These logics are expansions of the well--known {\em Belnap--Dunn's four--valued logic} that combine a many-valued character (tetravalence) with a modal character. In fact, $\cal TML$ is the logic that preserve degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $\cal TML$ and the algebras is not so good as in ${\cal TML}^N$, but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus (see \cite{FR2}). In this work, we prove that the sequent calculus given by Font and Rius does not enjoy the cut--elimination property. Then, using a general method proposed by Avron, Ben-Naim and Konikowska (\cite{Avron02}), we provide a sequent calculus for $\cal TML$ with the cut--elimination property. Finally, inspired by the latter, we present a {\em natural deduction} system, sound and complete with respect to the tetravalent modal logic.
△ Less
Submitted 24 January, 2021;
originally announced January 2021.
-
Some model-theoretic results on the 3-valued paraconsistent first-order logic QCiore
Authors:
Marcelo E. Coniglio,
Tadeo G. Gomez,
Martin Figallo
Abstract:
In this paper the 3-valued paraconsistent first-order logic QCiore is studied from the point of view of Model Theory. The semantics for QCiore is given by partial structures, which are first-order structures in which each n-ary predicate R is interpreted as a triple of paiwise disjoint sets of n-uples representing, respectively, the set of tuples which actually belong to R, the set of tuples which…
▽ More
In this paper the 3-valued paraconsistent first-order logic QCiore is studied from the point of view of Model Theory. The semantics for QCiore is given by partial structures, which are first-order structures in which each n-ary predicate R is interpreted as a triple of paiwise disjoint sets of n-uples representing, respectively, the set of tuples which actually belong to R, the set of tuples which actually do not belong to R, and the set of tuples whose status is dubious or contradictory. Partial structures were proposed in 1986 by I. Mikenberg, N. da Costa and R. Chuaqui for the theory of quasi-truth (or pragmatic truth). In 2014, partial structures were studied by M. Coniglio and L. Silvestrini for a 3-valued paraconsistent first-order logic called LPT1, whose 3-valued propositional fragment is equivalent to da Costa-D'Otaviano's logic J3. This approach is adapted in this paper to QCiore, and some important results of classical Model Theory such as Robinson's joint consistency theorem, amalgamation and interpolation are obtained. Although we focus on QCiore, this framework can be adapted to other 3-valued first-order logics.
△ Less
Submitted 23 August, 2018; v1 submitted 15 July, 2018;
originally announced July 2018.
-
Free algebras in varieties of Hilbert algebras with supremum generated by finite chains
Authors:
Aldo V. Figallo,
Elda Pick,
Susana Saad,
Martin Figallo
Abstract:
Hilbert algebras with supremum, i.e., Hilbert algebras where the associated order is a join-semilattice were first considered by A.V. Figallo, G. Ramon and S. Saad in [11], and independently by S. Celani and D. Montangie in [7].
On the other hand, L. Monteiro introduced the notion of n-valued Hilbert algebras (see [12]). In this work, we investigate the class of n-valued Hilbert algebras with su…
▽ More
Hilbert algebras with supremum, i.e., Hilbert algebras where the associated order is a join-semilattice were first considered by A.V. Figallo, G. Ramon and S. Saad in [11], and independently by S. Celani and D. Montangie in [7].
On the other hand, L. Monteiro introduced the notion of n-valued Hilbert algebras (see [12]). In this work, we investigate the class of n-valued Hilbert algebras with supremum, denoted Hn, i.e., n-valued Hilbert algebras where the associated order is a join-semilattice. The varieties Hn are generated by finite chains. The free Hn-algebra Freen+1(r) with r generators is studied. In particular, we determine an upper bound to the cardinal of the finitely generated free algebra Freen+1(r).
△ Less
Submitted 30 July, 2013;
originally announced July 2013.
