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

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Kai Brünnler
• Keywords: Automated Reasoning, Free Logic, Logic, LPAR 2010, Nice Consequence