How to Universally Close the Existential Rule

8 years 3 months ago
How to Universally Close the Existential Rule
This paper introduces a nested sequent system for predicate logic. The system features a structural universal quantifier and a universally closed existential rule. One nice consequence of this is that proofs of sentences cannot contain free variables. Another nice consequence is that the assumption of a non-empty domain is isolated in a single inference rule. This rule can be removed or added at will, leading to a system for free logic or classical predicate logic, respectively. The system for free logic is interesting because it has no need for an existence predicate. We see syntactic cut-elimination and completeness results for these two systems as well as two standard applications: Herbrand’s Theorem and interpolation. Table of Contents
Kai Brünnler
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LPAR
Authors Kai Brünnler
Comments (0)