Rencontre, 17 octobre 2024
Programme
- 10:30 – 12:00
-
Dominik Kirst (IRIF - Université Paris Cité)
Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ1-propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent definitions of decidable predicates and thus Σ1-propositions in constructive foundations, leading to non-equivalent Markov's principles. While this fact is well-reported in the literature, it is often overlooked, leading to wrong claims in standard references and published papers.
In this talk, I will illustrate the status of three natural variants of MP in Martin-Löf's constructive type theory (MLTT), by first giving respective equivalence proofs to different formulations of Post's theorem, stability of termination of computations, completeness of various proof systems w.r.t. some model-theoretic semantics for Σ1-theories, and finiteness principles for both extended natural numbers and trees. Afterwards, I describe how these three variants of MP can be separated using effectful models of MLTT, adapting Kreisel’s original proof strategy using free choice sequences to Cohen and Rahli’s framework of stateful type theories.
- 13:45 – 14:45
-
Jonas Frey (LIPN, Université Sorbonne Paris-Nord)Invited talk: The shape of contexts
Contexts x_1:A_1,...,x_n:A_n in simple type theory can be viewed as “flat”, since the variable declarations don’t depend on each other and can be permuted.
In dependent type theory, the general form of contexts is (x_1:A_1, x_2:A_2(x_1), ...,x_n:A_n(x_1,...,x_{n-1})) with a linear dependency chain between the variable declarations: However, the specific contexts occuring in practice are not always totally ordered. For example, in the context (x y:O, f:A(x,y)) the first two variables are not interdependent.
So maybe we should allow finite posets as shapes of contexts? It turns out to be better to use an even more general class of structures: finite direct categories, i.e. finite categories which have no nontrivial isomorphisms and endomorphisms.
FDCs were introduced by Makkai [1] as part of his notion of “First order logic with dependent sorts”, but the perspective on FDCs proposed in this talk is somewhat different since FDCs are not used to represent dependency structures of theories, but of contexts.
In the talk I will explain why FDCs seem to provide a good abstract notion of “shape” for contexts, that the category of FDCs and discrete fibrations forms a coclan, and how to derive a notion of dependent algebraic theory from these ideas which is very close to Chaitanya Leena Subramaniam’s “dependently typed theories”.
[1] https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
- 15:15 – 16:15
-
Pierre-Marie Pédrot (Galinette, INRIA)Invited talk: Upon This Quote I Will Build My Church Thesis
The internal Church thesis (CT) is a logical principle stating that any function f : N → N is computed by a concrete program in some Turing-complete language. CT has been widely used in constructive mathematics, most specifically in the Russian tradition. On the other side of the iron curtain, Martin-Loef Type Theory (MLTT) was designed as the modern embodiment of Bishop-style neutral mathematics. It should come as a surprise that the natural type-theoretic equivalent of CT was conjectured to be inconsistent with MLTT. In this talk, we will prove that this conjecture is false, by introducing “MLTT”, a consistent extension of MLTT with quoting primitives that implements CT in a computational way.
