Research Projects
The Master of Logic allows students to earn up to 24 EC via research projects. These are the research projects I have worked on so far.
Formal Analysis of Material Dialogues for FOL
This project was supervised by Dominik Kirst from Saarland University. It can be viewed as me carrying out one of the ideas mentioned in the “future work” section of my Bachelor’s thesis. Dialogical logic, originally put forward by Paul Lorenzen, captures the notion of first-order validity in terms of games modeled after a debate. Material dialogues, the variant we examine in this project, has a distinctly model-theoretic flavor compared to the formal dialogues usually considered in the literature. Arguably, it also is closer to Lorenzen’s original formulation of dialogical logic.
In the course of the project, I gave a novel formalization of material dialogues, using insights from my Bachelor’s thesis. I examined the thereby arising semantics for first-order logic in the calculus of inductive constructions, with special attention paid to the constructivity of completeness proofs with regards to them. I obtained the following results:
- Classical material dialogues admit a soundness proof with regards to a cut-free sequent calculus. Their induced notion of validity entails exploding classical Tarski validity, a constructively stricter notion than the usual Tarski validity. This yields a constructive completeness proof with regards to a natural deduction system.
- Intuitionistic material dialogues admit no completeness proof without additional assumptions, as their induced notion of validity is entailed by the standard Tarski validity over a non-trivial fragment of first-order logic. This means intuitionistic material dialogues “inherit” parts of the meta-logic, thus requiring axioms fixing the strength of the meta-logic to prove completeness.
- I give a novel variant of material dialogues for intuitionistic logic, called Kripke material dialogues, arising from the idea of “dialogues played over the canonical notion of model”. Similarly to classical material dialogues for classical first-order logic, these admit a soundness proof with regards to a cut-free sequent calculus and a constructive completeness proof with regards to a natural deduction system, both for intuitionistic first-order logic. However, the completeness proof is restricted to the ∀,→,⊥-fragment.
We are currently in the process of turning the project’s results into a paper which we hope to present at a conference.
Links
- The project report: pdf
References
- Lorenzen. Logik und Agon
- Lorenzen. Ein dialogisches Konstruktivitätskriterium
- Lorenz. Arithmetik und Logik als Spiele
- Forster, Kirst, Wehr. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory
Aczel’s Type-Theoretic Interpretation of CZF
This project was supervised by Robert Passmann. It can be viewed as a culmination of the set theory lectures which I took during the Master of Logic and my background in type theory. I read Peter Aczel’s three seminal papers on his interpretation of constructive Zeremelo-Fraenkel set theory into Martin Löf’s dependent type theory and summarized them in a manner accessible to anyone with a little knowledge about axiomatic set theory and no background in type theory.
The summary was published as part of the ILLC technical report series. I also gave a talk on the subject at the Mathematische Logik research seminar at Hamburg university on the 21. January 2021.
Links
- The summary: pdf
References
- Aczel. The Type Theoretic Interpretation of Constructive Set Theory
- Aczel. The Type Theoretic Interpretation of Constructive Set Theory: Choice Principles
- Aczel. The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions
Categorical Normalization by Evaluation
This project was supervised by Benno van den Berg. We read papers on normalization by evaluation, a semantic technique for normalizing the terms of a type theory. The focus was on papers which made use of categorical semantics (see the references below). To close the project, I combined the insights gleamed from the reading to try to transfer a technique for handling certain additional constants, introduced in the seminal paper on NBE by Berger and Schwichtenberg, to the categorical setting of the reduction free normalization proof of Altenkirch et. al. I succeeded in adapting the categorical normalization interpretation from Altenkirch et. al. to admit Schwichtenberg’s and Berger’s inductive correctness proof of the normalization theorem with the added constants. However, I did not manage to extend the categorical proof of the normalization theorem, given by Altenkirch et. al., to cover generic constants with similar conditions.
Links
- The project report: pdf
References
- Berger, Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus
- Altenkirch, Hofmann, Streicher. Categorical reconstruction of a reduction free normalization proof
- Altenkirch, Dybjer, Hofmann, Scott. Normalization by evaluation for typed lambda calculus with coproducts
- Altenkirch, Hofmann, Streicher. Reduction-free normalisation for system F
- Altenkirch, Kaposi. Normalization by Evaluation for Type Theory, in Type Theory