Applied Proof Theory Workshop

To mark the end of the ARC Project Meaning in Action, there will be a workshop on the project themes on 5-6 November 2020 (AEST). Due to the situation with COVID-19, all the talks will be held online. If you would like to participate, please contact Shawn Standefer for details.

Speakers

Program

Titles and abstracts will be added closer to the date of the workshop. All times are listed in Melbourne local time (AEST). Find your local time.

5 November

10:00—11:30: Teresa Kouri Kissel, “Proof-Theoretic Pluralism, Harmony and Identity”
12:30—14:00: Shawn Standefer, “The Universal Generalization Problem and Informational Screening”
15:30—17:00: Rajeev Goré, “Bi-Intuitionistic Logics: a New Instance of an Old Problem”
18:00—19:30: Rosalie Iemhoff, “The Stability of Logical Inference”

6 November

10:00—11:30: Natalia Buacar, “Logical Agreements from a Proof Theoretical Perspective”
12:30—14:00: Greg Restall, “Natural Deduction with Alternatives”
15:30—17:00: Dave Ripley, “General Elimination and Catamorphisms”
18:00—19:30: Andrew Arana, “On the difficulty of discovering proofs”

Videos of talks will be available after the workshop on the Melbourne Logic Group Vimeo page.

Abstracts

Andrew Arana “On the difficulty of discovering proofs”

Abstract: An account of mathematical understanding should account for the differences between theorems whose proofs are easy to discover, and those whose proofs are difficult to discover. Though Hilbert seems to have created proof theory with the idea that it would address this kind of “discovermental complexity’’, much more attention has been paid to the lengths of proofs, a measure of the difficulty of verifying of a given formal object that it is a proof of a given formula in a given formal system. In this presentation we will shift attention back to discovermental complexity, by addressing a “topological” measure of proof complexity recently highlighted by Alessandra Carbone (2009). Though we will contend that Carbone’s measure fails as a measure of discovermental complexity, it forefronts numerous important formal and epistemological issues, including the structure of proofs and the question of whether impure proofs are systematically simpler than pure proofs. This is joint work with Will Stafford (Irvine).

Natalia Buacar “Logical Agreements from a Proof Theoretical Perspective”

Abstract: Since Quine sentenced “change of logic, change of subject” many efforts have been made to make sense of the possibility of genuine disagreement in logic and authentic rivalry between logics. This way of approaching the question can be associated with a very common mode of philosophical argumentation that is rooted in adversariality that emphasizes disagreements. Such an approach has been criticized from a feminist perspective. This perspective highlights the cooperative aspects of argumentation and conceives it as an attempt to identify the points of agreement between arguers, in a way that brings together their different points of view. In this talk, I adopt that perspective to track certain central agreements in the realm of logic. From this point of view, the challenge is to specify the scope of the agreement. Such agreement must not be  generalized as to dissolve the disagreement about logic, transforming it into mere verbal disputes that can be solved by simply specifying the use of words. However, it must be substantive enough to guarantee fluid communication between the defenders of rival logics. I propose to use Proof theory as a theoretical framework to visualize and understand some of these meeting points, hoping that setting a clear common ground will clarify the philosophical discussion and even the source and nature of the disagreements.

Rajeev Goré “Bi-Intuitionistic Logics: a New Instance of an Old Problem”

Abstract: As anyone who reads the literature on bi-intuitionistic logic will know, the numerous papers by Cecylia Rauszer are foundational but confusing.  For example: these papers claim and retract various versions of the deduction theorem for bi-intuitionistic logic; they erroneously claim that the calculus is complete with respect to rooted canonical models; and they erroneously claim the admissibility of cut in her sequent calculus for this logic. Worse, authors such as Crolard, have based some of their own foundational work on these confused and confusing results and proofs.

We trace this confusion to the axiomatic formalism of RBiInt in which Rauszer first characterized bi-intuitionistic logic and show that, as in modal logic, RBiInt can be interpreted as two different consequence relations. We remove this ambiguity by using generalized Hilbert calculi, which are tailored to capture consequence relations.

We show that RBiInt leads to two logics, wBIL and sBIL, with different extensional and meta-level properties, and that they are, respectively, sound and strongly complete with respect to the Kripkean local and global semantic consequence relations of bi-intuitionistic logic. Finally, we explain where they were conflated by Rauszer. This is joint work with Ian Shillito.

Rosalie Iemhoff “The Stability of Logical Inference”

Abstract: It is well-known that extending a theory by nonlogical axioms may result in a theory in which besides the new axioms even some new logical principles become valid. One of the most salient examples of this phenomenon is intuitionistic set theory, which derives the law of excluded middle once the Axiom of Choice is added to it. Less well-known is the fact that also the logical inferences of a theory are not always preserved under the addition of axioms, even in case the logical principles do remain equal. In this talk I will discuss some recent results on the (un)stability of logical inference under extensions and provide many examples.

Teresa Kouri Kissel “Proof-Theoretic Pluralism, Harmony and Identity”

Abstract: Ferrari and Orlandelli (2019) propose that an admissibility condition on a proof-theoretic logical pluralism be that the logics in question must be harmonious, in the sense of Dummett. This allows them to develop an innovative pluralism, which shows variance on two levels. On one level, we have a pluralism which makes sense of that proposed in Restall (2014): the connectives remain fixed across all admissible logics, since they share the same operational rules. But, thanks to their system, we can also admit some logics which do not share connective meanings, and hence have different operational rules. This allows for us to have a pluralism at two levels: the level of validity and the level of connective meanings.

This system is proposed as a refi nement to that of Restall (2014) in response to objections proposed by Kouri (2016). In the spirit of the Kouri (2016) objections, I argue here that there are some logics we want to admit to our system which are not harmonious. I show how this leads to a possible three-level logical pluralism, where we have pluralism at the level of validity, connective meanings, and in what makes a logic admissible.

Greg Restall “Natural Deduction with Alternatives”

Abstract: In this talk, I will introduce natural deduction with alternatives, explaining how this framework can provide a simple well-behaved single conclusion natural deduction system for a range of logical systems, including classical logic, (classical) linear logic, relevant logic and affine logic, by varying the policy for managing discharging of assumptions and retrieval of alternatives. Along the way, the talk will touch on (1) the connection between normalisation of a natural deduction proof and cut elimination in a corresponding sequent calculus; (2) the separation between the operational rules governing the connectives and the “antecedently given context of deducibility”, to borrow a phrase from Nuel Belnap’s essay, “Tonk, Plonk and Plink” (1962); and (3) the sense in which the operational rules for a connective might be understood as providing a definition of that connective.

Dave Ripley “General elimination harmony and catamorphisms”

Abstract: `General elimination harmony’ is one attempt to articulate a notion of coherence between introduction and elimination rules for a connective, following on an idea of Gentzen. A very similar idea arises in the theory of functional programming, under the name `catamorphisms’. Indeed, this talk will show that the two ideas amount to the same thing for many cases of common concern, such as conjunctions/pair types or disjunctions/sum types.

However, the two ideas are not the same across the board. The difference is revealed when we look at recursive types. This talk will explore the differences that recursive types reveal, and argue that catamorphisms provide a better precisification of Gentzen’s idea than general elimination harmony does.

Shawn Standefer “The Universal Generalization Problem and Informational Screening”

Abstract: The rule of inference introducing a universal quantifier proceeds from a premiss involving a singular term to a conclusion with a universal quantifier. What entitles one to pass from the apparently particular premise to the general conclusion? One option, defended by Kit Fine, involves the use of arbitrary objects. Another option, defended by Breckinridge and Magidor is that it involves arbitrary reference. A third option, defended by Carlo Cellucci, involves the use of substitution. In this talk, I will set out the Problem of Universal Generalization and provide some background on the views of Fine and Cellucci. I will argue that these views miss out on some related devices of generalization, such as modal operators. I will present an alternative account that uses the notion of informational screening. I will explain this notion, provide examples of how it works, and argue that it can accommodate Cellucci’s proposal while also applying more broadly. Finally, I will close by considering some objections to the proposal.