Related papers: Bicategories, Biequivalence, and Bi-Interpretabili…

Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula…

We provide a denotational semantics for first-order logic that captures the two-level view of the computation process typical for constraint programming. At one level we have the usual program execution. At the other level an automatic…

The Univalent Foundations requires a logic that allows us to define structures on homotopy types, similar to how first-order logic with equality ($\text{FOL}_=$) allows us to define structures on sets. We develop the syntax, semantics and…

Contemporary semantic description of logic is based on the ontology of all possible interpretations, an insufficiently clear metaphysical concept. In this article, logic is described as the internal organization of language. Logical…

Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent…

Logically constrained term rewriting is a rewriting framework that supports built-in data structures such as integers and bit vectors. Recently, constrained terms play a key role in various analyses and applications of logically constrained…

In this thesis, we develop the theory of bifibrations of polycategories. We start by studying how to express certain categorical structures as universal properties by generalising the shape of morphism. We call this phenomenon…

The category of models of any theory $T$ in any first-order language $L$ has the surprising property that any small category that is elementarily equivalent with it, already embeds in it. The proof uses an abstract argument via ultrapowers,…

We define the notion of 2-filtered 2-category and give an explicit construction of the bicolimit of a category valued 2-functor. A category considered as a trivial 2-category is 2-filtered if and only if it is a filtered category, and our…

From an inconsistent database non-trivial arguments may be constructed both for a proposition, and for the contrary of that proposition. Therefore, inconsistency in a logical database causes uncertainty about which conclusions to accept.…

Indexed symmetric monoidal categories are an important refinement of bicategories -- this structure underlies several familiar bicategories, including the homotopy bicategory of parametrized spectra, and its equivariant and fiberwise…

Traditional treatments of formal logic provide: 1. A syntax for formulas. 2. An inference relation between sets of formulas. 3. A rule for assigning meaning to formulas (semantics) that is sound with respect to the inference relation. First…

Syntax is a latent hierarchical structure which underpins the robust and compositional nature of human language. In this work, we explore the hypothesis that syntactic dependencies can be represented in language model attention…

The distributed representations currently used are dense and uninterpretable, leading to interpretations that themselves are relative, overcomplete, and hard to interpret. We propose a method that transforms these word vectors into reduced…

We introduce a novel semantics for a multi-agent epistemic operator of knowing how, based on an indistinguishability relation between plans. Our proposal is, arguably, closer to the standard presentation of knowing that modalities in…

Calculi of string diagrams are increasingly used to present the syntax and algebraic structure of various families of circuits, including signal flow graphs, electrical circuits and quantum processes. In many such approaches, the semantic…

We contemplate a higher-level bipolar abstract argumentation for non-elementary arguments such as: X argues against Ys sincerity with the fact that Y has presented his argument to draw a conclusion C, by omitting other facts which would not…

The cartesian structure possessed by relations, spans, profunctors, and other such morphisms is elegantly expressed by universal properties in double categories. Though cartesian double categories were inspired in part by the older program…

We relativise double categories of relations to stable orthogonal factorisation systems. Furthermore, we present the characterisation of the relative double categories of relations in two ways. The first utilises a generalised comprehension…

Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative…