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.

Elementary quotient completions, church’s thesis, and partitioned assemblies / M.E. Maietti, F. Pasquali, G. Rosolini. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - 15:2(2019 Jun), pp. 21.1-21.21. [10.23638/LMCS-15(2:21)2019]

Elementary quotient completions, church’s thesis, and partitioned assemblies

F. Pasquali
Secondo
Investigation
;
2019

Abstract

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.
And phrases: Realizability; Completion; Formal Church thesis; Lawvere hyperdoctrine
Settore MATH-01/A - Logica matematica
   Computing with Infinite Data
   CID
   European Commission
   Horizon 2020 Framework Programme
   731143

   Correctness by Construction
   CORCON
   European Commission
   SEVENTH FRAMEWORK PROGRAMME
   612638
giu-2019
Article (author)
File in questo prodotto:
File Dimensione Formato  
1802.06400.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Licenza: Creative commons
Dimensione 491.5 kB
Formato Adobe PDF
491.5 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/1158382
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
  • OpenAlex ND
social impact