Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice

DOI10.1007/s00153-018-0612-9OpenAlexW2787206234WikidataQ114018307 ScholiaQ114018307MaRDI QIDQ1756495

Hajime Ishihara, Maria Emilia Maietti, Samuele Maschio, Thomas Streicher

Publication date: 14 January 2019

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-018-0612-9

zbMATH Keywords

realizabilitytype theoryformal Church's thesis

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25)

Related Items (9)

On Church’s thesis in cubical assemblies ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ Parametric Church's thesis: synthetic computability without choice ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ Unnamed Item ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ A categorical reading of the numerical existence property in constructive foundations

Cites Work

• Quotient completion for the foundation of constructive mathematics
• Realizability. An introduction to its categorical side
• A minimalist two-level foundation for constructive mathematics
• Classical recursion theory. The theory of functions and sets of natural numbers
• Constructivism in mathematics. An introduction. Volume II
• Sheaves in geometry and logic: a first introduction to topos theory
• Independence of the induction principle and the axiom of choice in the pure calculus of constructions
• Unifying exact completions
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Elementary quotient completion
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Tripos theory
• Setoids in type theory
• Extensional Constructs in Intensional Type Theory
• Why topology in the minimalist foundation must be pointfree
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice