arXiv subjects

Victor Barroso-Nascimento

Publications and source records attributed to Victor Barroso-Nascimento.

7 recordsLinked to original sources

arXiv2026

Higher-order Kripke models for intuitionistic and non-classical modal logics

This paper introduces higher-order (``nested") Kripke models, a generalization of Kripke models that is remarkably close to Kripke's original idea -- both mathematically and conceptually. Standard models are now $0$-ary models, whereas $n$-ary models for $n > 0$ are models whose set of objects (``possible worlds'') contain only $(n-1)$-ary models. A key idea is the use of worlds as fixed points for modal definitions, in the sense that what is necessary or possible in a world of a frame depends only on what is true in the same world on the accessible frames. This paper mainly deals with the paradigmatic cases of intuitionistic modal logics $IK$ and $MK$, from which the generalisation to other non-classical logics arises naturally. The association between conditions on accessibility relations and modal axioms also carries over to this framework, so modal logics stronger than $K$ can be obtained by imposing requirements on the relations between frames. Just like Kripke models define a concept of ``alternative'' for classical models, the $n$-ary models (for $n > 0$) defines the same concept for any interpretation of the $(n-1)$-ary models.

cs.LO↗

arXiv2026

Bilateralism with incompatible proofs and refutations

Logical bilateralism challenges traditional concepts of logic by treating assertion and denial as independent yet opposed acts. While initially devised to justify classical logic, its constructive variants show that both acts admit intuitionistic interpretations. This paper presents a bilateral system where a formula cannot be both provable and refutable without contradiction, offering a framework for modelling epistemic entities, such as mathematical proofs and refutations, that exclude inconsistency. The logic is formalised through a bilateral natural deduction system with desirable proof-theoretic properties, including normalisation. We also introduce a base-extension semantics requiring explicit constructions of proofs and refutations while preventing them from being established for the same formula. The semantics is proven sound and complete with respect to the calculus. Finally, we show that our notion of refutation corresponds to David Nelson's constructive falsity, extending rather than revising intuitionistic logic and reinforcing the system's suitability for representing constructive epistemic reasoning.

cs.LO↗

arXiv2026

Glivenko's theorems from an ecumenical perspective

In this paper, we revisit Glivenko's theorems, foundational results relating classical and intuitionistic logic, from an ecumenical perspective. We begin by discussing the historical context and significance of Glivenko's original contributions, and then examine their extensions and reinterpretations within ecumenical logical frameworks. Our analysis focuses on three ecumenical systems: Prawitz's natural deduction system NE; the system NEK, closely related to one introduced by Krauss in an unpublished manuscript; and the ECI system proposed by Barroso-Nascimento.

cs.LO↗

arXiv2026

A Proof-Theoretic Approach to the Semantics of Classical Linear Logic

Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces). This work proposes a different perspective on assigning meaning to proofs by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support. Recent developments have shown that BeS is powerful enough to capture proof-theoretic notions in structurally rich logics such as intuitionistic linear logic. In this paper, we extend this framework to the classical case, presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic (MALL).

cs.LO↗

arXiv2025

Effects of the Strict-Tolerant Approach on Intuitionistic and Minimal Logic

This paper extends the literature on the strict-tolerant logical approach by applying its methods to intuitionistic and minimal logic. In short, the strict-tolerant approach modifies the usual notion of logical consequence by stipulating that, in order for an inference to be valid, from the truth of the premises must follow the non-falsity of the conclusion. This notion can also be generalized to define strict-tolerant metainferences, metametainferences and so on, which may or may not generate logics distinct from those obtained on the inferential level. It is already known that strict-tolerant definitions can make the notion of inference for non-classical logics collapse into the classical notion, but the strength of this effect is not yet fully known. This paper shows that intuitionistic strict-tolerant inferences also collapse into classical ones, but minimal ones do not. However, minimal strict-tolerant logic has the property that no inferences are valid (which is not carried over to the metainferential level). Additionally, it is shown that the logics obtained from intuitionistic, minimal and classical logic at the metainferential level are distinct from each other.

cs.LO↗

arXiv2025

A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)

We define base-extension semantics (Bes) using atomic systems based on sequent calculus rather than natural deduction. While traditional Bes aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a Bes framework more suited to classical semantics. The harmony in classical sequents leads to straightforward semantic clauses derived solely from right introduction rules. This framework enables a Sandqvist-style completeness proof that extracts a sequent calculus proof from any valid semantic consequence. Moreover, we show that the inclusion or omission of atomic cut rules meaningfully affects the semantics, yet completeness holds in both cases.

cs.LO↗

arXiv2025

Bilateral base-extension semantics

Bilateralism is the position according to which assertion and rejection are conceptually independent speech acts. Logical bilateralism demands that systems of logic provide conditions for assertion and rejection that are not reducible to each other, which often leads to independent definitions of proof rules (for assertion) and dual proof rules, also called refutation rules (for rejection). Since it provides a critical account of what it means for something to be a proof or a refutation, bilateralism is often studied in the context of proof-theoretic semantics, an approach that aims to elucidate both the meaning of proofs (and refutations) and what kinds of semantics can be given if proofs (and refutations) are considered as basic semantic notions. The recent literature on bilateral proof-theoretic semantics has only dealt with the semantics of proofs and refutations, whereas we deal with semantics in terms of proofs and refutations. In this paper we present a bilateral version of base-extension semantics - one of the most widely studied proof-theoretic semantics - by allowing atomic bases to contain both atomic proof rules and atomic refutation rules. The semantics is shown to be sound and complete with respect to the bilateral dual intuitionistic logic 2Int. Structural similarities between atomic proofs and refutations also allow us to define duality notions for atomic rules, deductions and bases, which may then be used for the proof of bilateral semantic harmony results. Aside from enabling embeddings between different fragments of the language, bilateral semantic harmony is shown to be a restatement of the syntactic horizontal inversion principle, whose meaning-conferring character may now be interpreted as the requirement of preservation of harmony notions already present at the core of the semantics by inferences.

math.LO↗