Related papers: Dialectica Principles via G\"odel Doctrines

G\"odel's Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent…

We introduce the notion of a G\"odel fibration, which is a fibration categorically embodying both the logical principle of traditional Skolemization (we can exchange the order of quantifiers paying the price of a functional) and the…

Grothendieck fibrations are fundamental in capturing the concept of dependency, notably in categorical semantics of type theory and programming languages. A relevant instance are Dialectica fibrations which generalise G\"odel's Dialectica…

G\"odel's Dialectica has been introduced and developed in the tradition of the so-called functional interpretations. Only recently has it been related with the a priori unrelated notion of differentiation, by taking a program-theoretic…

G\"odel's Dialectica interpretation is a fundamental tool for the extraction of computational content from proofs, and plays a central role in today's proof mining program. In the past decades, it has also been studied from the perspective…

Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples.…

We adapt our light Dialectica interpretation to usual and light modal formulas (with universal quantification on boolean and natural variables) and prove it sound for a non-standard modal arithmetic based on Goedel's T and classical S4. The…

We present two Dialectica-like constructions for models of intensional Martin-L\"of type theory based on G\"odel's original Dialectica interpretation and the Diller-Nahm variant, bringing dependent types to categorical proof theory. We set…

The categorical modeling of Petri nets has received much attention recently. The Dialectica construction has also had its fair share of attention. We revisit the use of the Dialectica construction as a categorical model for Petri nets…

This is the author's PhD thesis. It is a contribution to categorical logic, in particular to the theory of realizability toposes. While the tools of categorical logic have proven very successful in analyzing and organizing proof theoretic…

We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We…

Extending G\"odel's \emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite…

G\"odel's second incompleteness theorem is standardly understood as showing that no sufficiently strong, consistent theory of arithmetic can prove its own consistency, a result typically interpreted against a model-theoretic background in…

We use G\"{o}del's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erd\H{o}s and Rado. Our proof makes use of the product of selection functions, which forms an intuitive…

G{\"o}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula to the notion of provable formula.We survey a…

Recently, the second author, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of nonstandard arithmetic - including overspill, underspill, and…

This article surveys work done in the last six years on the unification of various functional interpretations including G\"odel's dialectica interpretation, its Diller-Nahm variant, Kreisel modified realizability, Stein's family of…

Hilbert's Entscheidungsproblem has given rise to a broad and productive line of research in mathematical logic, where the classification process of decidable classes of first-order sentences represent only one of the remarkable results.…

For Hilbert, the consistency of a formal theory T is an infinite series of statements "D is free of contradictions" for each derivation D and a consistency proof is i) an operation that, given D, yields a proof that D is free of…

We use G\"odel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable…