Remarks on Herbrand normal forms and Herbrand realizations

[B] Beeson, M.J.: Goodman's theorem and beyond. Pac. J. Math.84, 1–16 (1979)

[G76] Goodman, N.: The theory of the Gödel functionals. J. Symb. Logic41, 574–582 (1976)

[G78] Goodman, N.: Relativized realizability in intuitionistic arithmetic of all finite types. J. Symb. Logic43, 23–44 (1978)

[K1] Kleene, S.C.: Introduction to metamathematics. Amsterdam: North-Holland 1952

[Kr51, 52] Kreisel, G.: On the interpretation of non-finitist proofs, I and II. J. Symb. Logic16, 241–267 (1951);17, 43–58 (1952)

[Kr52a] Kreisel, G.: On the concepts of completeness and interpretation of formal systems. Fundam. Math.39, 103–127 (1952).

[Kr82] Kreisel, G.: Finiteness theorems in arithmetic: an application of Herbrand's theorem forΣ 2-formulas. In: Stern, J. (ed.). Proc. of the Herbrand symposium (Marseille, 1981), pp. 39–55, Amsterdam: North-Holland 1982

[Kr-L] Kreisel, G., Levy, A.: Reflection principles and their use for establishing the complexity of axiomatic systems. Z. Math. Logik Grundlagen Math.14, 97–142 (1968)

[Lu73] Luckhardt, H.: Extensional Gödel functional interpretation. A consistency proof of classical analysis. Lect. Notes Math. vol. 306. Berlin Heidelberg New York: Springer 1973

[Lu89] Luckhardt, H.: Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken. J. Symb. Logic54, 234–263 (1989)

[P70] Parsons, C.: On a number-theoretic choice schema and its relation to induction. In: Kino, A., Myhill, J., Vessley, R.E. (eds.). Intuitionism and Proof Theory, pp. 459–473. Amsterdam: North-Holland 1970

[P71] Parsons, C.: On a number-theoretic choice schema II (abstract). J. Symb. Logic36, 587 (1971)

[P72] Parsons, C.: Onn-quantifier-induction. J. Symb. Logic37, 466–482 (1972)

[Sch] Schwichtenberg, H.: Proof theory: some applications of cut-elimination. In: Barwise, J. (ed.). Handbook of mathematical Logic, pp. 867–895. Amsterdam: North-Holland 1977

[Sh] Shoenfield, J.R.: Mathematical logic. New York: Addison-Wesley 1967

[Si85] Sieg, W.: Fragments of arithmetic. Ann. Pure Appl. Logic28, 33–71 (1985)

[Si87] Sieg, W.: Provably recursive functionals of theories with König's lemma. Rend. Semin. Mat. Torino. Faxicolo speciale 75–92 (1987)

[Si91] Sieg, W.: Herbrand analyses. Arch. Math. Logic30, 409–441 (1991)

[Ta] Tait, W.W.: Infinitely long terms of transfinite type. In: Crossley, J.N., Dummett, M.A.E. (eds.). Formal systems and recursive functions, pp. 176–185. Amsterdam: North-Holland 1965

[Tr] Troelstra, A. S.: Metamathematical investigation of intuitionistic arithmetic and analysis. (Lect. Notes Math., vol. 344). Berlin Heidelberg New York: Springer 1973