We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

math.CT

Change to browse by:

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Mathematics > Category Theory

Title: The Gödel Fibration

Abstract: 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 existence of a prenex normal form presentation for every logical formula. Building up from Hofstra's earlier fibrational characterization of the de Paiva's categorical Dialectica construction, we show that a fibration is an instance of the Dialectica construction if and only if it is a G\"odel fibration. This result establishes an internal presentation of the dialectica construction. Then we provide a deep structural analysis of the Dialectica construction producing a full description of which categorical structure behaves well with respect to this construction, focusing on (weak) finite products and coproducts. We conclude describing the applications we envisage for this generalized fibrational version of the Dialectica construction.
Comments: 39 pages
Subjects: Category Theory (math.CT); Logic (math.LO)
MSC classes: 18C10, 18C15, 18D05
Cite as: arXiv:2104.14021 [math.CT]
  (or arXiv:2104.14021v1 [math.CT] for this version)

Submission history

From: Matteo Spadetto [view email]
[v1] Wed, 28 Apr 2021 20:53:48 GMT (35kb)

Link back to: arXiv, form interface, contact.