Melbourne Logic Day

There will be a Logic Day workshop at the University of Melbourne on Friday, December 9. The tentative schedule is below. Additional talk titles and abstracts to come.

11-12:15 -- Greg Restall (Melbourne) Proof Terms as Invariants

12:15-1:30 -- Lloyd Humberstone (Monash) Dependency and Disjunction

1:30-2:30 -- Lunch 

2:30-3:45 -- Hiroakira Ono (JAIST) An algebraic approach to cut elimination for modal logics

3:45-5 -- Tomasz Kowalski (La Trobe) Algebraic cut elimination and completions of lattices. 

Restall Abstract: In this talk, I will explain how proof terms for derivations in classical propositional logic are invariants for derivations under a natural class of permutations of rules. The result is two independent characterisations of one underlying notion of proof identity.

Humberstone Abstract: We ponder the anomalous behaviour of disjunction in what in Valentin Goranko and Antti Kuusisto, 'Logics for Propositional Determinacy and Independence' (arXiv:1609.07398v1 [math.LO], September 2016) is called the logic of propositional dependence; see esp. pp. 10 and 16--19. As the authors make clear in other parts of their discussion, this logic, we well as another logic they suggest is superior in avoiding the anomalies in question, is quite closely connected with the topics of noncontingency and supervenience.

Ono Abstract: Based on the idea by S. Maehara in his paper in 1991, we will give a simple algebraic proof of cut elimination for modal logics. First, we introduce the notion of “approximate mappings” for assignments on modal algebras, and show a key lemma on them. Taking a sequent system GS4 for modal logic S4 as an example, we show how to apply our key lemma for proving cut elimination. Then, we will explain relations between our approximate mappings and quasi-embeddings which was introduced in my joint paper in 2004 with F. Belardinelli and P. Jipsen.  

Kowalsi Abstract: We will present a simple example of an algebraic method of showing cut elimination. The example is a sequent system for lattices devised by Matsumoto. It has an unusual feature of being "fully classical" in the sense of all structural rules being present, yet it is an adequate proof system for arbitrary lattices. The method is very similar to the one from (Belardinelli, Jipsen, Ono 2004), but it can acocmmodate (some) rules with context restrictions, and it is (perhaps) neater. (This is joint work with Hiroakira Ono.)