The tableaux method applied to a quasi-modulated logic for the quantifier "few"
Logics of formal inconsistency with replacement: An algebraic and proof-theoreti...
Genericity in the context of theorem proving: a cloud based proof assistant for fl...
| Full text | |
| Author(s): |
Coniglio, Marcelo E.
;
Figallo, Martin
Total Authors: 2
|
| Document type: | Journal article |
| Source: | LOGIC AND LOGICAL PHILOSOPHY; v. 33, n. 2, p. 33-pg., 2024-01-26. |
| Abstract | |
Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four -valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro's tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut -elimination property. However, in a previous work we presented a sequent system for TML 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 article we continue with the study of TML under a proof -theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof -theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (AU) | |
| FAPESP's process: | 22/03862-2 - Proof-theoretical methods for LFIs and other non-classical logics: decidability and applications |
| Grantee: | Marcelo Esteban Coniglio |
| Support Opportunities: | Research Grants - Visiting Researcher Grant - International |
| FAPESP's process: | 20/16353-3 - Rationality, logic, and probability: RatioLog |
| Grantee: | Marcelo Esteban Coniglio |
| Support Opportunities: | Research Projects - Thematic Grants |