Premium
A note on equality in finite‐type arithmetic
Author(s) -
Berg Benno
Publication year - 2017
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201600080
Subject(s) - soundness , mathematics , observational equivalence , extensional definition , equivalence (formal languages) , interpretation (philosophy) , type (biology) , algebra over a field , arithmetic , calculus (dental) , discrete mathematics , pure mathematics , computer science , programming language , statistics , medicine , paleontology , ecology , dentistry , biology , tectonics
We present a version of arithmetic in all finite types based on a systematic use of an internally definable notion of observational equivalence for dealing with equalities at higher types. For this system both intensional and extensional models are possible, the deduction theorem holds and the soundness of the Dialectica interpretation is provable inside the system itself.