In proof-theoretic semantics it is assumed that the meaning of logical connectives is given by the rules of inference governing them in some underlying proof system. A bilateralist take on this can be understood as demanding of a proof system to display not only rules giving the connectives’ provability conditions but also their refutability conditions. Thus, with such an approach the bilateralism is implemented on the level of derivability, i.e., our proof system is bilateral by displaying two derivability relations, one for proving and one for refuting. While in natural deduction this seems rather straightforwardly feasible by dualizing proof rules (see, e.g., [1]), in a sequent calculus this does not seem trivially realizable. After all, here two derivability relations are inherent: one within sequents expressed by the sequent sign and one between sequents expressed by the horizontal lines. So, it seems that if we are serious about having a bilateral sequent calculus, both relations need to be dualized.

I will show, however, that in such a setting an apparent asymmetry between the notions of proof and refutation arises, which means we achieve the opposite of our original aim - to establish more bilaterality. The reasons for this are related to deeper issues that we need to think about, such as our notion of refutation and our understanding of derivability in natural deduction and in sequent calculus. Therefore, I will argue, either we accept that there are limits as to how bilateral we can design a sequent calculus or we need to give up certain prima facie intuitive background assumptions concerning derivability.

Bibliography

1. Heinrich Wansing,A more general general proof theory,Journal of Applied Logic,vol. 25 (2017), pp.23–46.

Authors: Barteld Kooi and Allard Tamminga

Within the context of Gentzen-calculi for classical propositional logic we present an algorithm that constructs a left rule from a right rule (and vice versa). First, we show that the algorithm is correct. Second, we use our algorithm to analyse the relation between proof-theoretical semantics (the meaning of an operator is given by its inference rules) and model-theoretical semantic (the meaning of an operator is given by its truth- and falsity-conditions). Third, we use our algorithm to study the concept of harmony and show what is wrong with Prior’s pair of rules for tonk.

In Gentzen-calculi for classical logic every operator has a left rule and a right rule. Bearing Prior’s challenge in mind, it has often been noted (first by Gentzen himself) that left rules and right rules are dependent, but as yet it is still under debate how this relation must be understood. In the context of natural deduction systems, Prawitz proposes his “Inversion Principle” to make this relation more precise. Crudely speaking, his principle says that an introduction rule followed by an elimination rule can never lead to anything beyond the original premises.

Using our correspondence analysis for proof systems and truth- and falsity-conditions, we note that left rules correspond to falsity-conditions and that right rules correspond to truth-conditions. This observation lies at the basis of our algorithm that constructs left rules from right rules (and vice versa). Accordingly, we offer a novel perspective on harmony, the balance between left rules and right rules (or within the context of natural deduction systems, between introduction and elimination rules). We say that a left rule \(L\) and a right rule \(R\) are harmonious if and only if our algorithm applied to \(L\) constructs a right rule \(R'\) that is inferentially equivalent to \(R\) (and vice versa).

Authors: Victor Nascimento, Luiz Carlos Pereira and Elaine Pimentel

Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of logical proofs as one of the main points of controversy. The intuitionist advocates for a strict notion of constructive proof, while the classical logician advocates for a notion which allows non-construtive proofs through reductio ad absurdum. A great deal of controversy still subsists to this day on the matter, as there is no agreement between disputants on the precise standing of non-constructive methods.

Two very distinct approaches to logic are currently providing interesting contributions to this debate. The first, oftentimes called logical ecumenism [1], aims to provide a unified framework in which two “rival” logics may peacefully coexist, thus providing some sort of neutral ground for the contestants. The second, proof-theoretic semantics [2], aims not only to elucidate the meaning of a logical proof, but also to provide means for its use as a basic concept of semantic analysis. Logical ecumenism thus provides a medium in which meaningful interactions may occur between classical and intuitionistic logic, whilst proof-theoretic semantics provides a way of clarifying what is at stake when one accepts or denies reductio ad absurdum as a meaningful proof method.

In this paper we show how to coherently combine both approaches by providing not only a medium in which classical and intuitionistic logics may coexist, but also one in which classical and intuitionistic notions of proof may coexist.

Bibliography

1. Dag Prawitz. Natural deduction: A proof-theoretical study. Dover Publications, 2006.
2. Peter Schroeder-Heister. A natural extension of natural deduction. Journal of Symbolic Logic, 49:1284–1300, 1984.

Keywords: proof-theoretic validity, classical logic, sequent calculus

Proof-theoretic validity offers a non-referential semantics for certain logics. Currently it has been developed for intuitionistic logic (e.g. [2]; [4]), certain intermediate logics (e.g. [3]; [5], and certain substructural logics (e.g. [1]). This has been done by using a natural deduction calculus. However, there are many logics that are more naturally represented in the sequence calculus, including, for the purposes of proof-theoretic validity, classical logic. This paper develops the beginnings of a notion of proof-theoretic validity for the sequent calculus and applies it to classical logic to show that in this setting the left rules for classical logic are valid given the right rules. We then address certain philosophical questions about this move including how we should interpret the sequence and whether this is a form of bilateralism.

Bibliography

1. Gheorghiu, Alexander V., Tao Gu, and David J. Pym,Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic,Automated Reasoning with Analytic Tableaux and Related Methods(Prague),(Revantha Ramanayake and Josef Urban, editors),vol. 14278,Springer,2023,pp. 367–-385.
2. Goldfarb, Warren,On Dummett’s ‘Proof-Theoretic Justifications of Logical Laws,Advances in Proof-Theoretic Semantics(Thomas Piecha and Peter Schroeder-Heister, editors),Springer,Cham,2016,pp. 195–210.
3. Piecha, Thomas, Wagner de Campos Sanz, and Peter Schroeder-Heister,Failure of Completeness in Proof-Theoretic Semantics,Journal of Philosophical Logic,vol. 44 (2015), no. 3 pp. 321–-335.
4. Stafford, Will and Victor Nascimento,Following all the rules: Intuitionistic completeness for generalized proof-theoretic validity,Analysis,vol. 83 (2023), no. 3, pp. 507–-516.
5. Stafford, Will,Proof-Theoretic Semantics and Inquisitive Logic,Journal of Philosophical Logic,vol. 50 (2021), no. 5, pp. 1199-–1229.

Prawitz’s proof-theoretic semantics evaluates validity of proofs \(\models^{\texttt{P}}\) over atomic bases \(\mathfrak{B}\) and detour reductions. In current approaches, proofs and reductions are left out, and consequence \(\models\) is defined outright; a variant \(\models^{\texttt{S}}\), due to Sandqvist, deals with disjunction in an elimination-like way. \(\models^{\texttt{P}}\), \(\models\) and \(\models^{\texttt{S}}\) can be given in a monotonic or non-monotonic format, according to whether extensions of \(\mathfrak{B}\) are brought in when defining, by closure, consequence under assumptions. Completeness results have been proved on non-monotonic and monotonic \(\models\), and monotonic \(\models^{\texttt{S}}\) [2]. In the monotonic framework, these results adapt to \(\models^{\texttt{P}}\) modulo conditions for equivalence and completeness on \(\models^{\texttt{P}}\) [1]. I show that similar results hold in the non-monotonic approach too, via the following:

• \(\Gamma \models_\mathfrak{B} A \Leftrightarrow \Gamma \models^{\texttt{P}}_{\mathfrak{B}} A\),
• \(\Gamma \models A \Leftrightarrow \Gamma \models^{\texttt{P}} A\),
• \((\Gamma \models^{\texttt{S}}_{\mathfrak{B}} A \Rightarrow \Gamma \models^{\texttt{P}}_{\mathfrak{B}} A) \Rightarrow (\Gamma \models^{\texttt{P}}_{\mathfrak{B}} A \Rightarrow \Gamma \models^{\texttt{S}}_{\mathfrak{B}} A)\),
• \(\Sigma\) is \(\mathfrak{B}\)-complete (\(\mathfrak{B}\)-sound) on \(\Vdash\) iff \(\Gamma \Vdash_{\mathfrak{B}} A \Rightarrow \Gamma \vdash_{\Sigma \cup \mathfrak{B}} A\) (\(\Gamma \vdash_{\Sigma \cup \mathfrak{B}} A \Rightarrow \Gamma \Vdash_{\mathfrak{B}} A\)). Then, \(\Sigma\) \(\mathfrak{B}\)-complete on \(\models^{\texttt{S}} A\) and \(\mathfrak{B}\)-sound on \(\models^{\texttt{P}} \Rightarrow (\Gamma \models^{\texttt{S}} A \Leftrightarrow \Gamma \models^{\texttt{P}} A\) and \(\Sigma\) complete over \(\models^{\texttt{P}})\)
• \(\Sigma\) satisfies the export principle [2] \(\Rightarrow\) \(\Sigma\) not \(\mathfrak{B}\)-complete on \(\Vdash\).

1 also holds with classical meta-logic and a strict \(\models^{\texttt{P}}\) where closure is necessary but not sufficient for validity when \(\Gamma \neq \emptyset\). 3 also holds with \(\models\) and strict \(\models^{\texttt{P}}\).

Bibliography

1. Antonio Piccolomini d’Aragona,Inversion and \(\mathfrak{B}\)-Completeness in Monotonic PTS,Forthcoming.
2. Peter Schroeder-Heister,Proof-Theoretic Semantics,The Stanford Encyclopedia of Philosophy,(Edward N. Zalta, Uri Nodelman, editors).