Classical Logic with Partial Functions

Abstract. We introduce a semantics for classical logic with partial functions. We believe that the semantics is natural. When a formula contains a subterm in which a function is applied outside of its domain, our semantics ensures that the formula has no truth-value, so that it cannot be used for reasoning. The semantics relies on order of formulas. In this way, it is able to ensure that functions and predicates are properly declared before they are used. We define a sequent calculus for the semantics, and prove that this calculus is sound and complete for the semantics.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Hans de Nivelle
• Keywords: CADE 2010, Classical Logic, Logical Reasoning, Semantics, We Believe