Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Herbrand schemes to functional interpretation

Sebastian Enqvist-Pyk

Abstract

Herbrand schemes are a method to extract Herband disjunctions directly from sequent calculus proofs, without appealing to cut elimination, using a formal grammar known as a higher-order recursion scheme. In this note, we show that the core ideas of Herbrand schemes can be reformulated as a functional interpretation of classical sequent calculus, similar to the functional interpretation of classical logic due to Gerhardy and Kohlenbach.

From Herbrand schemes to functional interpretation

Abstract

Herbrand schemes are a method to extract Herband disjunctions directly from sequent calculus proofs, without appealing to cut elimination, using a formal grammar known as a higher-order recursion scheme. In this note, we show that the core ideas of Herbrand schemes can be reformulated as a functional interpretation of classical sequent calculus, similar to the functional interpretation of classical logic due to Gerhardy and Kohlenbach.
Paper Structure (27 sections, 7 theorems, 140 equations, 4 figures)

This paper contains 27 sections, 7 theorems, 140 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Types and terms
  3. Sequent calculus
  4. Two-sided sequent calculus
  5. One-sided sequent calculus
  6. Formulas as types, proofs as terms
  7. Formulas as types
  8. Proofs as terms
  9. Case $\mathsf{lem}$:
  10. Case $\mathsf{w}$:
  11. Case $\mathsf{cut}$:
  12. Case $\mathsf{c}$:
  13. Case $\exists$:
  14. Case $\neg \exists$:
  15. Case $\vee$:
  16. ...and 12 more sections

Key Result

Proposition 1

Every type is inhabited by some closed term.

Theorems & Definitions (10)

  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Proposition 3
  • Proposition 4
  • Definition 1
  • Proposition 5
  • Theorem 1
  • Theorem 2: Herbrand's Theorem