A note on arithmetic in finite types

TL;DR

This paper develops a comprehensive arithmetic framework for all finite types, enabling higher-type equality, internal proof of Dialectica interpretation soundness, and supporting both intensional and extensional models.

Contribution

It introduces a novel arithmetic system for finite types with derivable congruences, internal soundness proofs, and compatibility with multiple model types.

Findings

Higher-type equality can be defined with all congruences derivable.

Dialectica interpretation's soundness is provable within the system.

Supports both intensional and extensional models.

Abstract

We present a version of arithmetic in all finite types which allows for a definition of equality at higher types for which all congruence are derivable, for which the soundness of the Dialectica interpretation is provable inside the system itself, which allows for both intensional and extensional models and for which the deduction theorem holds.