http://hdl.handle.net/11089/48059 2026-04-06T22:49:24Z 2026-04-06T22:49:24Z Gheorghiu, Alexander V. Pym, David J. http://hdl.handle.net/11089/48072 2023-10-13T01:27:46Z 2023-07-18T00:00:00Z

Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic Gheorghiu, Alexander V.; Pym, David J. 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.

2023-07-18T00:00:00Z Ayhan, Sara Wansing, Heinrich http://hdl.handle.net/11089/48071 2023-10-13T01:27:54Z 2023-07-18T00:00:00Z

On Synonymy in Proof-Theoretic Semantics: The Case of \(\mathtt{2Int}\) Ayhan, Sara; Wansing, Heinrich 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.

2023-07-18T00:00:00Z van Dijk, Emma Ripley, David Gutierrez, Julian http://hdl.handle.net/11089/48070 2023-10-13T01:27:56Z 2023-08-16T00:00:00Z

Core Type Theory van Dijk, Emma; Ripley, David; Gutierrez, Julian 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.

2023-08-16T00:00:00Z Restall, Greg http://hdl.handle.net/11089/48069 2023-10-13T01:27:51Z 2023-06-25T00:00:00Z

Structural Rules in Natural Deduction with Alternatives Restall, Greg 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.

2023-06-25T00:00:00Z