Seminars

Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms.

This dissertation concerns the properties of and relationship between positive truth and fixpoints over intuitionistic arithmetic in three respects: the strength of these theories relative to the arithmetic base theories, relationships between theories of strictly positive fixpoints and compositional and disquotational truth for strictly truth-positive sentences, and a comparison with the classical case.

Opponent: Gerhard Jäger, Professor Emiratus University of Bern

Natural languages vary in their quantity expressions, but the variation seems to be constrained by general properties, so-called universals. Explanations thereof have been sought among constraints of human cognition, communication, complexity, and pragmatics. In this work, we examine whether perceptual constraints and coordination dynamics contribute to the development of two universals: monotonicity and convexity. Using a state-of-the-art multi-agent language coordination model (originally applied to colour terms) we evolve communicatively usable quantity terminologies. We compare the degrees of convexity and monotonicity of languages evolving in populations of agents with and without approximate number sense (ANS). The results suggest that ANS supports the development of monotonicity and, to a lesser extent, convexity. We relate our results to some classical observations about generalised quantifiers in mathematical logic and to the research on conceptual spaces.

This is joint work with Dariusz Kalociński, Franek Rakowski and Jakub Uszyński.

Let M be the weak set theory obtained from ZF by removing the Collection Scheme, restricting the Separation Scheme to bounded formulae, and adding an axiom asserting that every set is contained transitive set. In this talk I will consider two formulations of the set-theoretic Collection Scheme restricted formulae that are Π_n in the Levy hierarchy: Π_n-Collection and Strong Π_n-Collection. It is known that, over M, Strong Π_n-Collection is equivalent to Π_n-Collection plus Σ_n+1-Separation, and Strong Π_n-Collection proves the consistency of M + Π_n-Collection. In this talk I will show that for all n > 0, every well-founded model of M + Π_n-Collection satisfies Strong Π_n-Collection. In particular, for n > 0, M + Strong Π_n-Collection does not prove the existence of a transitive model of M + Π_n-Collection. And, for n > 0, the minimum model of M + Strong Π_n-Collection and M + Π_n-Collection coincide. If time permits, I will indicate how the assumption that that the model is well-founded can be replaced with the assumption that the model instead satisfies a fragment of Foundation. This reveals new equivalences between subsystems of ZF that include the Powerset axiom.

We explain some of the connections between two research areas: cyclic proof theory and proof assistants. This talk is based on joint work-in-progress with Lide Grotenhuis.

In cyclic proof theory, we replace induction axioms with circular reasoning. By carefully placing restrictions on cycles, we can make sure that we do not prove more than with induction. Such cyclic proofs can be interpreted as programs using the Curry-Howard correspondence: cycles correspond to recursive calls, while the restrictions make sure that the program always terminates. Using this perspective, we show how the type theory implemented by proof assistants can be seen as a cyclic proof system: one where programs/proofs are defined using (co)pattern matching. We show some of the difficulties that come up specifically in dependent type theory: why unification becomes important, and how one can translate cyclic proofs to inductive proofs while preserving computational behavior. In addition, we show how some of the techniques from cyclic proof theory might be used to extend proof assistants.

Voting on two alternatives appears unproblematic compared to voting on three (or more). When faced with only two alternatives, many arguments show that Majority Rule distinguishes itself from all other ways of making a group decision. For three or more alternatives, one faces the so-called “Paradox of Voting”: there may be elections with a majority cycle in which a majority of voters prefer A to B, a majority of voters prefer B to C, and a majority of voters prefer C to A. In this talk, I will explain a series of results that axiomatically characterize rules for resolving majority cycles in elections. These rules avoid the “Strong No Show Paradox” by responding properly to the addition of new voters to an election and mitigate spoiler effects by responding properly to the addition of new candidates to an election.

This talk is based on joint work with Wes Holliday.

The 2024 Annual European Meeting of the Association for Symbolic Logic, also known as the Logic Colloquium, will be held in Gothenburg on 24-28 June, 2024 and hosted by the Faculty of Humanities at the University of Gothenburg. The colloquium comprises 3 tutorials, 7 plenary lectures and 6 special sessions as well as contributed talks. In addition, the 2024 Gödel Lecture was delivered at the meeting.

See lc2024.se for full information.