English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

"Church's thesis" ($\mathsf{CT}$) as an axiom in constructive logic statesthat every total function of type $\mathbb{N} \to \mathbb{N}$ is computable,i.e. definable in a model of computation. $\mathsf{CT}$ is inconsistent in bothclassical mathematics and in Brouwer's intuitionism since it contradicts WeakK\"onig's Lemma and the fan theorem, respectively. Recently, $\mathsf{CT}$ wasproved consistent for (univalent) constructive type theory.  Since neither Weak K\"onig's Lemma nor the fan theorem are a consequence ofjust logical axioms or just choice-like axioms assumed in constructive logic,it seems likely that $\mathsf{CT}$ is inconsistent only with a combination ofclassical logic and choice axioms. We study consequences of $\mathsf{CT}$ andits relation to several classes of axioms in Coq's type theory, a constructivetype theory with a universe of propositions which does neither prove classicallogical axioms nor strong choice axioms.  We thereby provide a partial answer to the question which axioms may preservecomputational intuitions inherent to type theory, and which certainly do not.The paper can also be read as a broad survey of axioms in type theory, with allresults mechanised in the Coq proof assistant.

Church's thesis and related axioms in Coq's type theory