Autumn Semester HS2022

Unless stated otherwise, all talks will take place in room A97 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.

Schedule

Abstracts

In standard proof theory a proof is a finite tree whose nodes are labelled by sequents and which is generated by a finite set of rules. One such rule is the cut rule, which is a sequent calculus analogue of the well-known modus ponens rule. As the cut rule introduces new formulas into a proof, it makes proofs non-analytic. Therefore, much effort is devoted to show that the cut rule can be eliminated from a given calculus without changing the set of derivable sequents. Such a cut-elimination theorem is established by showing how instances of the cut rule in a given proof can be pushed upwards until the premises of the instances are axioms. One then shows that in this case the instances of cut can be eliminated from the proof. However, this standard strategy does not work when one considers so-called non-wellfounded proofs, which are proofs in which some branches are allowed to be infinitely long. Clearly, in such a setting it is not enough to simply push instances of cut upwards, as a leaf might never be reached. In this talk I will present ongoing research on cut-elimination for non-wellfounded proofs for a fragment of the modal mu-calculus. I will discuss the basic idea how to construct a cut-free proof from a given non-wellfounded proof and present some of the current problems of my method.

Dyadic Deontic Logic is an extension of Monadic Deontic Logic that employs a weaker conditional. We consider two equivalent systems of Alethic-Deontic logic and Pure Deontic logic and present justification counterparts for them. Soundness and completeness of Alethic-Deontic system with respect to preference models is proved.

4-valued logic plays a certain role in Indian philosophy, in particular in connection with the so-called Catuskoti. I will begin this talk with looking at 3- and 4-valued logics from a rather general perspective and then turn to (more specific) Gentzen systems 3K and 4B for prominent such logics. The last part is dedicated to the question whether it is possible to make sense of Catuskoti on the basis of more traditional (Western) logics. An extension of 4B will play a central role in this enterprise.

In this talk, I will describe a moduli-theoretic approach to problems in computational complexity theory. By simulating Turing machines with polynomial maps, we may describe Turing machine computations as algebraic maps between ind-varieties. This leads to ’moduli spaces’ of polynomial time (non)deterministic Turing machines, as well as spaces parametrizing (non)deterministic polynomial time problems. I will explain how one can explicitly write down polynomial equations defining these spaces. This gives a framework for studying various problems in computational complexity, such as P vs NP.

A rule is passive for a logic L if there is no substitution making its premises a theorem for L, and L is said to be passively structurally complete if all of its passive rules are derivable in the logic. Since a rule is passive exactly when its premises are not unifiable, the study of passive structural completeness (or PSC) also has connections to the study of unification problems for the logic, or equivalently for its equivalent algebraic semantics, by Ghilardi's algebraic approach to unification. In ongoing joint work with Aglianò, we show a new characterization for the PSC of quasivarieties, which has an interesting interpretation in quasivarieties of residuated lattices. Moreover, as a result of our investigation, we also show new results about the unification type of some relevant fuzzy logics, such as product logic and nilpotent minimum logic.

D. Shoesmith and T. Smiley (1978) introduced a generalization of traditional Hilbert-style systems in which rules of inference may have multiple formulas in their conclusions and derivations are trees labelled with sets of formulas. These modifications created the possibility of generating (finite) analytic Hilbert-style systems for a very inclusive class of logics determined by (finite) non-deterministic matrices (C. Caleiro and S. Marcelino, 2019). The analyticity of these systems ensures that, when searching for a proof, we only need to consider formulas in a set that is completely determined by the subformulas of the statement of interest. This contrasts with usual traditional Hilbert-style systems (for classical and intuitionistic logics, for example) lacking analyticity results. In this talk, we will present how the above notions and result may be generalized to the context of two-dimensional logics and two-dimensional non-deterministic matrices (in the sense of C. Blasio, J. Marcos and H. Wansing, 2017). We will also see that logics failing to be finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics. We will illustrate this fact with the well-known logic of formal inconsistency called mCi, first showing that it fails to be finitely axiomatizable in one dimension and then presenting a finite and analytic two-dimensional Hilbert-style system for it.

In the field of formal language theory it is a natural question to ask about the closure properties of language families represented by automata. The complementation of Büchi automata is a long-standing venture that started in the 1960's with the seminal research by J. R. Büchi. After many decades, a complementation algorithm efficient enough to be used in practice is still to be found. Many constructions have reached the worst-case lower bound of (0.76n)n , but most of them behave badly on practical cases. In his PhD thesis, Joel Allred from the University of Fribourg studied the complementation of Büchi automata and comupted the complexity of a specific complementation algorithm, which will be presented in the seminar session.

The complexity class BQP, short for Bounded-Error Quantum Polynomial Time, describes the class of problems, that can be solved by a quantum Turing machine in polynomial time. It is the quantum analog to the classical complexity class BPP and shares similar properties. Namely, that P is contained in BQP and BQP is low to itself. The goal of this thesis is to give a brief overview of the complexity class BQP and some closely related concepts such as the qubit and quantum gates. I will also introduce quantum Turing machines and quantum circuits and use these two models of computation to present two equivalent definitions of BQP. I will then take a closer look at the relationships the class BQP shares with other classes e.g. EXP, PSPACE, BPP and P.

The film MY PHANTOM follows the intimate and honest journey of Dutch alpinist Line van den Berg questioning what a means to be a woman in the climbing community. For years, Line has been searching for the 'perfect' female climbing partner to share the passion for mountains, but also the struggles of being an athlete in a male-dominated sports. But is this search really about finding this one partner, or is it about finding her own place in society?
MY PHANTOM portraits Line climbing hard mixed routes throughout the Alps, with the highpoint being the First Female Ascent of the Phantom Direct on the south face of the Grandes Jorasses with Fay Manners, established in January 2022.
Premiere: 6 November 2022, Dutch Mountain Film Festival
Director & Writer: Line van den Berg
Producer: Scenarios4
Teaser on youtube