Bilateral base-extension semantics

Victor Barroso-Nascimento; Maria Osório

Home/Archive/arXiv

arXiv · 2505.01593

Bilateral base-extension semantics

Victor Barroso-Nascimento·Maria Osório

View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

math.LO cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Victor Barroso-Nascimento, Maria Osório. 2025-05-02. Bilateral base-extension semantics. https://arxiv.org/abs/2505.01593

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Loops, Inverse Limits and Non-Determinism

We introduce an operator on problems in Weihrauch complexity, which we call the infinite loop or inverse limit, and which corresponds to an infinite compositional product. This operation arises naturally whenever one implements algorithms that produce a sequence of results in an infinite loop, using some fixed subroutine. We prove that the corresponding operator is monotone with respect to (strong) Weihrauch reducibility but that it is not a closure operator. One of our findings is that weak Kőnig's lemma is closed under infinite loops, which implies that the class of non-deterministically computable problems is also closed under this operation. Consequently, this class allows for a high degree of flexibility in programming. As our main technical tools, we present an injective version of the recursion theorem and an infinitary version of the so-called independent choice theorem. We also show that, in general, the infinite loop operator is more powerful than the composition of the diamond operator followed by the parallelization operator. However, in many practical scenarios, these compositions yield a result, which coincides with the application of the infinite loop operator. Finally, we discuss the special situation of loops for single-valued problems and for problems on Turing degrees.

math.LO↗

arXiv2026

Scott topologies on meet-continuous domains

We study Scott products and sobriety of countable meet-continuous domains, meaning meet-continuous dcpos without any additional continuity or least-element assumption. Using the complete-lattice test-family theorem of Xu and Ji, we prove finite-product equality for those domains that are $L$-dcpos, and for the weaker class whose principal ideals have suprema of all nonempty subsets. For an arbitrary family of nonempty countable meet-continuous $L$-dcpos, we prove that the Scott topology on the order product equals the product of the factor Scott topologies if and only if only finitely many factors lack a least element. We also establish sobriety under bounded completeness and under additional common-upper-bound conditions. Assuming square-product equality, sobriety is characterized by Scott closedness of common-upper-bound sections associated with irreducible Scott-closed sets, with an equivalent sequential formulation in the countable case. Two extraction lemmas extend to meet-semilattice dcpos. The finite-product and sobriety questions for general countable meet-continuous domains remain unresolved here.

math.LO↗

arXiv2026

Randomized Borel $(2d+1)$-coloring of digraphs

Let $G$ be a Borel digraph with maximum out-degree $d \in \mathbb{N}$. We show that $G$ admits a random Borel $(2d+1)$-coloring for which every edge is almost surely not monochromatic. This gives a simpler proof of a recent result of Pelayo-Gómez: such a graph $G$ admits a measurable proper $(2d+1)$-coloring with respect to any Borel probability measure on $V(G)$. Our proof is an adaptation of Pelayo-Gómez's proof to the randomized Borel setting.

math.LO↗