DROPS

Document

From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)

Authors: Ingo Blechschmidt, Hajime Ishihara, Peter M. Schuster, and Gabriele Buriola

Published in: Dagstuhl Reports, Volume 14, Issue 1 (2024)

Abstract

What is the computational content of proofs? This is one of the main topics in mathematical logic, especially proof theory, that is of relevance for computer science. The well-known foundational solutions aim at rebuilding mathematics constructively almost from scratch, and include Bishop-style constructive mathematics and Martin-Löf’s intuitionistic type theory, the latter most recently in the form of the so-called homotopy or univalent type theory put forward by Voevodsky. From a more practical angle, however, the question rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. Ideally, all this is done by manipulating proofs mechanically and/or by adequate metatheorems (proof translations, automated theorem proving, program extraction from proofs, proof mining, etc.). A crucial role for answering these questions is played by coherent and geometric theories and their generalizations: not only that they are fairly widespread in modern mathematics and non-classical logics (e.g., in abstract algebra, and in temporal and modal logics); those theories are also a priori amenable for constructivisation (see Barr’s Theorem, especially its proof-theoretic variants, and the numerous Glivenko–style theorems); last but not least, effective theorem-proving for coherent theories can be automated with relative ease and clarity in relation to resolution. Specific topics that substantially involve computer science research include categorical semantics for geometric theories up to the proof-theoretic presentation of sheaf models and higher toposes; extracting the computational content of proofs and dynamical methods in quadratic form theory; the interpretation of transfinite proof methods as latent computations; complexity issues of and algorithms for geometrization of theories; the use of geometric theories in constructive mathematics including finding algorithms, ideally with integrated developments; and coherent logic for obtaining automatically readable proofs.

Cite as

Ingo Blechschmidt, Hajime Ishihara, Peter M. Schuster, and Gabriele Buriola. From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021). In Dagstuhl Reports, Volume 14, Issue 1, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{blechschmidt_et_al:DagRep.14.1.1,
  author =	{Blechschmidt, Ingo and Ishihara, Hajime and Schuster, Peter M. and Buriola, Gabriele},
  title =	{{From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)}},
  pages =	{1--24},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{1},
  editor =	{Blechschmidt, Ingo and Ishihara, Hajime and Schuster, Peter M. and Buriola, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.1},
  URN =		{urn:nbn:de:0030-drops-204882},
  doi =		{10.4230/DagRep.14.1.1},
  annote =	{Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}

Document

DOI: 10.4230/LIPIcs.CSL.2024.16

A General Constructive Form of Higman’s Lemma

Authors: Stefano Berardi, Gabriele Buriola, and Peter Schuster

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

In logic and computer science one often needs to constructivize a theorem ∀ f ∃ g.P(f,g), stating that for every infinite sequence f there is an infinite sequence g such that P(f,g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of ∀ f ∃ g.P(f,g): for every f there is a "long enough" finite prefix g₀ of g such that P(f,g₀), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version. Our approach with bars generalises the approaches to Higman’s lemma undertaken by Coquand-Fridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman’s lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman’s lemma, our constructive proofs are closer to the original classical proofs.

Cite as

Stefano Berardi, Gabriele Buriola, and Peter Schuster. A General Constructive Form of Higman’s Lemma. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berardi_et_al:LIPIcs.CSL.2024.16,
  author =	{Berardi, Stefano and Buriola, Gabriele and Schuster, Peter},
  title =	{{A General Constructive Form of Higman’s Lemma}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.16},
  URN =		{urn:nbn:de:0030-drops-196599},
  doi =		{10.4230/LIPIcs.CSL.2024.16},
  annote =	{Keywords: intuitionistic logic, constructive mathematics, formal proof, inductive predicate, bar induction, well quasi-order, Higman’s lemma}
}

Search Results

Documents authored by Buriola, Gabriele

From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)

Abstract

Cite as

A General Constructive Form of Higman’s Lemma

Abstract

Cite as

Thanks for your feedback!

Could not send message