A note on equality in finite-type arithmetic
| Authors |
|
| Publication date |
11-2017
|
| Journal |
Mathematical Logic Quarterly
|
| Volume | Issue number |
63 | 3-4
|
| Pages (from-to) |
282-288
|
| Organisations |
-
Faculty of Science (FNWI)
-
Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
|
| Abstract |
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.
|
| Document type |
Article
|
| Language |
English
|
| Published at |
https://doi.org/10.1002/malq.201600080
|
|
Permalink to this page
|
Back