In bilateral logic formulas are signed by + and –, indicating the speech acts assertion and denial. I argue that making an assumption is also speech act. Speech acts cannot be embedded within other speech acts. Hence we cannot make sense of the notion of making an assumption in bilateral logic. Attempts to solve this problem are considered and rejected.

Proof-theoretic semantics is an inferentialist theory of meaning originally developed in a unilateral framework. Its extension to bilateral systems opens both opportunities and problems. The problems are caused especially by Coordination Principles (a kind of rule that is not present in unilateral systems) and mismatches between rules for assertion and rules for rejection. In this paper, a solution is proposed for two major issues: the availability of a reduction procedure for tonk and the existence of harmonious rules for the paradoxical (...) zero-ary connective \(\bullet\). The solution is based on a reinterpretation of bilateral rules as complex rules, that is, rules that introduce or eliminate connectives in a subordinate position. Looking at bilateral rules from this perspective, the problems faced by bilateralism can be seen as special cases of general problems of complex systems, which have been already analyzed in the literature. In the end, a comparison with other proposed solutions underlines the need for further investigation in order to complete the picture of bilateral proof-theoretic semantics. (shrink)

In a recent paper, under the auspices of an unorthodox variety of bilateralism, we introduced a new kind of proof-theoretic semantics for the base modal logic \(\mathbf{K}\), whose values lie in the closed interval \([0,1]\) of rational numbers [14]. In this paper, after clarifying our conception of bilateralism – dubbed “soft bilateralism” – we generalize the fractional method to encompass extensions and weakenings of \(\mathbf{K}\). Specifically, we introduce well-behaved hypersequent calculi for the deontic logic \(\mathbf{D}\) and the non-normal modal logics (...) \(\mathbf{E}\) and \(\mathbf{M}\) and thoroughly investigate their structural properties. (shrink)

In a recent paper del Valle-Inclan and Schlöder argue that bilateral calculi call for their own notion of proof-theoretic harmony, distinct from the usual (or ‘unilateral’) ones. They then put forward a specifically bilateral criterion of harmony, and present a harmonious bilateral calculus for classical logic. In this paper, I show how del Valle-Inclan and Schlöder’s criterion of harmony suggests a notion of normal form for bilateral systems, and prove normalisation for two (harmonious) bilateral calculi for classical logic, HB1 and (...) HB2. The resulting normal derivations have the usual desirable features, like the separation and subformula properties. HB1-normal form turns out to be strictly stronger that the notion of normal form proposed by Nils Kürbis, and HB2-normal form is neither stronger nor weaker than a similar proposal by Marcello D’Agostino, Dov Gabbay, and Sanjay Modgyl. (shrink)

We consider an approach to propositional synonymy in proof-theoretic semantics that is defined with respect to a bilateral G3-style sequent calculus \(\mathtt{SC2Int}\) for the bi-intuitionistic logic \(\mathtt{2Int}\). A distinctive feature of \(\mathtt{SC2Int}\) is that it makes use of two kind of sequents, one representing proofs, the other representing refutations. The structural rules of \(\mathtt{SC2Int}\), in particular its cut rules, are shown to be admissible. Next, interaction rules are defined that allow transitions from proofs to refutations, and vice versa, mediated through (...) two different negation connectives, the well-known implies-falsity negation and the less well-known coimplies-truth negation of \(\mathtt{2Int}\). By assuming that the interaction rules have no impact on the identity of derivations, the concept of inherited identity between derivations in \(\mathtt{SC2Int}\) is introduced and the notions of positive and negative synonymy of formulas are defined. Several examples are given of distinct formulas that are either positively or negatively synonymous. It is conjectured that the two conditions cannot be satisfied simultaneously. (shrink)

Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use (...) the operational view of them as provided by uniform proof-search—the proof-theoretic foundation of logic programming (LP)—to establish the completeness of IPL for the B-eS. This perspective allows negation, a subtle issue in P-tS, to be understood in terms of the negation-as-failure protocol in LP. Specifically, while the denial of a proposition is traditionally understood as the assertion of its negation, in B-eS we may understand the denial of a proposition as the failure to find a proof of it. In this way, assertion and denial are both prime concepts in P-tS. (shrink)

Natural deduction with alternatives extends Gentzen–Prawitz-style natural deduction with a single structural addition: negatively signed assumptions, called alternatives. It is a mildly bilateralist, single-conclusion natural deduction proof system in which the connective rules are unmodi_ed from the usual Prawitz introduction and elimination rules — the extension is purely structural. This framework is general: it can be used for (1) classical logic, (2) relevant logic without distribution, (3) affine logic, and (4) linear logic, keeping the connective rules fixed, and varying purely (...) structural rules. The key result of this paper is that the two principles that introduce kinds of irrelevance to natural deduction proofs: (a) the rule of explosion (from a contradiction, anything follows); and (b) the structural rule of vacuous discharge; are shown to be two sides of a single coin, in the same way that they correspond to the structural rule of weakening in the sequent calculus. The paper also includes a discussion of assumption classes, and how they can play a role in treating additive connectives in substructural natural deduction. (shrink)

Neil Tennant’s core logic is a type of bilateralist natural deduction system based on proofs and refutations. We present a proof system for propositional core logic, explain its connections to bilateralism, and explore the possibility of using it as a type theory, in the same kind of way intuitionistic logic is often used as a type theory. Our proof system is not Tennant’s own, but it is very closely related, and determines the same consequence relation. The difference, however, matters for (...) our purposes, and we discuss this. We then turn to the question of strong normalization, showing that although Tennant’s proof system for core logic is not strongly normalizing, our modified system is. (shrink)

In this paper, we introduce the notion of intuitionistic fuzzy PMS-subalgebras under homomorphism and Cartesian product and investigate several properties. We study the homomorphic image and inverse image of the intuitionistic fuzzy PMS-subalgebras of a PMS-algebra, which are also intuitionistic fuzzy PMS-subalgebras of a PMS-algebra, and find some other interesting results. Furthermore, we also prove that the Cartesian product of intuitionistic fuzzy PMS-subalgebras is again an intuitionistic fuzzy PMS-subalgebra and characterize it in terms of its level sets. Finally, we consider (...) the strongest intuitionistic fuzzy PMS-relations on an intuitionistic fuzzy set in a PMS-algebra and demonstrate that an intuitionistic fuzzy PMS-relation on an intuitionistic fuzzy set in a PMS-algebra is an intuitionistic fuzzy PMS-subalgebra if and only if the corresponding intuitionistic fuzzy set in a PMS-algebra is an intuitionistic fuzzy PMS-subalgebra of a PMS-algebra. (shrink)

In this paper we introduce the modelwise interpolation property of a logic that states that whenever \(\models\phi\to\psi\) holds for two formulas \(\phi\) and \(\psi\), then for every model \(\mathfrak{M}\) there is an interpolant formula \(\chi\) formulated in the intersection of the vocabularies of \(\phi\) and \(\psi\), such that \(\mathfrak{M}\models\phi\to\chi\) and \(\mathfrak{M}\models\chi\to\psi\), that is, the interpolant formula in Craig interpolation may vary from model to model. We compare the modelwise interpolation property with the standard Craig interpolation and with the local interpolation (...) property by discussing examples, most notably the finite variable fragments of first order logic, and difference logic. As an application we connect the modelwise interpolation property with the local Beth definability, and we prove that the modelwise interpolation property of an algebraizable logic can be characterized by a weak form of the superamalgamation property of the class of algebras corresponding to the models of the logic. (shrink)

One takes advantage of some basic properties of every homotopic \(\lambda\)-model (e.g. extensional Kan complex) to explore the higher \(\beta\eta\)-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher \(\lambda\)-terms, whose equality rules would be contained in the theory of any \(\lambda\)-homotopic model.

Rough set theory is an excellent mathematical tool for the analysis of a vague description of actions in decision problems. Now, in this paper by considering the notion of an equality algebra, the notion of the lower and the upper approximations are introduced and some properties of them are given. Moreover, it is proved that the lower and the upper approximations define an interior operator and a closure operator, respectively. Also, using D-lower and D-upper approximation, conditions for a nonempty subset (...) to be definable are provided and investigated that under which condition D-lower and D-upper approximation can be filter. (shrink)

An algebraic type of structure is shown forth which is such that if it is a characteristic matrix for a logic, then that logic satisfies Meyer's weak variable sharing property. As a corollary, it is shown that RM and all its odd-valued extensions \(\mathbf{RM}_{2n\mathord{-}1}\) satisfy the weak variable sharing property. It is also shown that a proof to the effect that the "fuzzy" version of the relevant logic R satisfies the property is incorrect.