Maria Emilia Maietti ; Fabio Pasquali ; Giuseppe Rosolini - Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies

lmcs:4302 - Logical Methods in Computer Science, June 25, 2019, Volume 15, Issue 2 - https://doi.org/10.23638/LMCS-15(2:21)2019
Elementary Quotient Completions, Church's Thesis, and Partioned AssembliesArticle

Authors: Maria Emilia Maietti ; Fabio Pasquali ; Giuseppe Rosolini

Hyland's effective topos offers an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also contains a boolean full sub-quasitopos of "assemblies" where only a restricted form of Church's Thesis survives. In the present paper we compare the effective topos and the quasitopos of assemblies each as the elementary quotient completions of a Lawvere doctrine based on the partitioned assemblies. In that way we can explain why the two forms of Church's Thesis each category satisfies differ by the way each is inherited from specific properties of the doctrine which determines the elementary quotient completion.


Volume: Volume 15, Issue 2
Secondary volumes: Selected Papers of the Conference "Continuity, Computability, Constructivity: From Logic to Algorithms" (CCC 2017)
Published on: June 25, 2019
Accepted on: May 23, 2019
Submitted on: February 20, 2018
Keywords: Mathematics - Logic
Funding:
    Source : OpenAIRE Graph
  • Computing with Infinite Data; Funder: European Commission; Code: 731143
  • Correctness by Construction; Funder: European Commission; Code: 612638

Consultation statistics

This page has been seen 3189 times.
This article's PDF has been downloaded 1134 times.