Contributed Talks 23
Chair: Sebastian G.W. Speitel
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
16:30 
Sara Ayhan, Obstacles of a truly bilateral sequent calculus 
In prooftheoretic 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


16:55 
Barteld Kooi, Constructing Harmony 
Authors: Barteld Kooi and Allard Tamminga Within the context of Gentzencalculi 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 prooftheoretical semantics (the meaning of an operator is given by its inference rules) and modeltheoretical semantic (the meaning of an operator is given by its truth and falsityconditions). 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 Gentzencalculi 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 falsityconditions, we note that left rules correspond to falsityconditions and that right rules correspond to truthconditions. 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). 

17:20 
Luiz Carlos Pereira, An ecumenical view of prooftheoretic semantics 
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 nonconstrutive 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 nonconstructive 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, prooftheoretic 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 prooftheoretic 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


17:45 
Will Stafford, Prooftheoretic validity for sequents 
Keywords: prooftheoretic validity, classical logic, sequent calculus Prooftheoretic validity offers a nonreferential 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 prooftheoretic validity, classical logic. This paper develops the beginnings of a notion of prooftheoretic 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


18:10 
Antonio Piccolomini d'Aragona, Inversion in nonmonotonic PTS 
Prawitz’s prooftheoretic 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 eliminationlike way. \(\models^{\texttt{P}}\), \(\models\) and \(\models^{\texttt{S}}\) can be given in a monotonic or nonmonotonic format, according to whether extensions of \(\mathfrak{B}\) are brought in when defining, by closure, consequence under assumptions. Completeness results have been proved on nonmonotonic 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 nonmonotonic approach too, via the following:
1 also holds with classical metalogic 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
