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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

We investigate how much type theory is able to prove about the naturalnumbers. A classical result in this area shows that dependent type theorywithout any universes is conservative over Heyting Arithmetic (HA). We build onthis result by showing that type theories with one level of universes areconservative over Higher-order Heyting Arithmetic (HAH). Although this clearlydepends on the specific type theory, we show that the interpretation of logicalso plays a major role. For proof-irrelevant interpretations, we will see thatstrong versions of type theory prove exactly the same higher-order arithmeticalformulas as HAH. Conversely, proof-relevant interpretations prove strictly moresecond-order arithmetical formulas than HAH, however they still prove exactlythe same first-order arithmetical formulas. Along the way, we investigate thedifferent interpretations of logic in type theory, and to what extent dependenttype theories can be seen as extensions of higher-order logic. We apply ourresults by proving De Jongh's theorem for type theory.

Conservativity of Type Theory over Higher-order Arithmetic