×

Functional interpretation and inductive definitions. (English) Zbl 1193.03082

The authors describe in detail a Dialectica interpretation of the classical theory \(\text{ID}_1\) in a language of higher-type functionals allowing primitive recursion on natural numbers as well as a schema of recursion along well-founded trees. A natural extension to \(n\) times iterated inductive definitions is outlined, and hence \(\Pi^1_1\)-comprehension is covered. A variant of Shoenfield’s interpretation, which incorporates also an idea due to J. Diller and W. Nahm [Arch. Math. Logik Grundlagenforsch. 16, 49–66 (1974; Zbl 0277.02006)] (and hence similar to one used by W. Burr [Arch. Math. Logic 39, No. 8, 599–604 (2000; Zbl 0968.03066)] for \(\text{KP}\omega\)), is used. An important feature of the language of well-founded trees is a possibility to collect a sequence of trees into one tree. The paper solves a problem posed in [J. Avigad and S. Feferman, Stud. Logic Found. Math. 137, 337–405 (1998; Zbl 0913.03053)]. Proofs are given in detail and are well motivated.

MSC:

03F10 Functionals in proof theory
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] DOI: 10.1007/BF02011878 · Zbl 0411.03051
[2] DOI: 10.1002/malq.200610038 · Zbl 1154.03036
[3] Theories for admissible sets: A unifying approach to proof theory (1986) · Zbl 0638.03052
[4] A system of abstract constructive ordinals 37 pp 355– (1972) · Zbl 0264.02026
[5] Compositio Mathematica 20 pp 107– (1968)
[6] Collected works II (1990)
[7] DOI: 10.1111/j.1746-8361.1958.tb01464.x · Zbl 0090.01003
[8] DOI: 10.1007/BFb0103100
[9] DOI: 10.1016/j.apal.2004.11.001 · Zbl 1095.03060
[10] DOI: 10.1007/BF02025118 · Zbl 0277.02006
[11] DOI: 10.1007/s001530050167 · Zbl 0968.03066
[12] Mathematical logic (2001) · Zbl 0965.03001
[13] Handbook of mathematical logic pp 867– (1977)
[14] DOI: 10.1007/BFb0079558
[15] Trudy Matematicheskogo Instituia Imeni V. A. Steklova 242 pp 147– (2003)
[16] Applied proof theory: Proof interpretations and their use in mathematics · Zbl 1158.03002
[17] DOI: 10.1090/S0002-9904-1955-09896-3 · Zbl 0066.25901
[18] DOI: 10.1090/S0002-9947-1955-0070594-4
[19] Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies 897 (1981) · Zbl 0489.03022
[20] Handbook of proof theory pp 337– (1998)
[21] DOI: 10.1007/BFb0066745
[22] Interpreting classical theories in constructive ones 65 pp 1785– (2000) · Zbl 0981.03061
[23] DOI: 10.1016/S0168-0072(97)00045-6 · Zbl 0945.03084
[24] Intuition and proof theory pp 475– (1970)
[25] A variant of the double-negation translation
[26] DOI: 10.1090/S0002-9947-04-03515-9 · Zbl 1079.03046
[27] Logic Colloquium ’77 pp 55– (1978)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.