FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Herbrand's Theorem as Higher-Order Recursion

Author: Graham Leigh

Paper Information

Title:Herbrand's Theorem as Higher-Order Recursion
Authors:Graham Leigh
Proceedings:CL&C Full papers and abstracts
Editor: Stefano Berardi
Keywords:Herbrand's Theorem, Classical sequent calculus, Reductive cut elimination, Higher order recursion schemes
Abstract:

ABSTRACT. Herbrand's Theorem, a fundamental result of classical logic, states that for every valid existential formula $\exists x F(x)$ there is a finite set of terms $T$ such that the quantifier-free disjunction $\bigvee_{t\in T} F(t)$ is a tautology. Herbrand disjunctions can be computed in a number of ways, such as via cut-elimination, re-interpretations of classical logic in intuitionistic logic and term calculi for classical natural deduction.

In this talk I will outline a language-theoretic representation of Herbrand's Theorem. Specifically, I will introduce a class of higher order recursion schemes (HORS) for computing Herbrand disjunctions from classical sequent calculus proofs. HORS are a generalisation of regular tree grammars to finite types which equate to the simply-typed $\lambda Y$-calculus with non-deterministic reductions. The representation interprets inference rules of proofs as non-terminals whose production rules operate compositionally to extract the term instantiations that result from reductive cut-elimination. Current limitations of the approach, as well as future directions, will be discussed.

Pages:1
Talk:Jul 07 14:45 (Session 28A)
Paper: