## 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: |