eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/24398
Title:  Intuitionistic Completeness of FirstOrder Logic 
Authors:  Constable, Robert Bickford, Mark 
Keywords:  logic completeness semantics polymorphic 
Issue Date:  7Oct2011 
Abstract:  We establish completeness for intuitionistic firstorder logic, iFOL, showing that is a formula is provable if and only if it is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform evidence into a formal firstorder proof. We have implemented Prf . Uniform validity is defined using the intersection operator as a universal quantifier over the domain of discourse and atomic predicates. Formulas of iFOL that are uniformly valid are also intuitionistically valid, but not conversely. Our strongest result requires the Fan Theorem; it can also be proved classically by showing that Prf terminates using K¨onig’s Theorem.
The fundamental idea behind our completeness theorem is that a single evidence term evd witnesses the uniform validity of a minimal logic formula F. Finding even one uniform realizer guarantees validity because Prf (F, evd) builds a firstorder proof of F, establishing its uniform validity and providing a purely logical normalized realizer.
We establish completeness for iFOL as follows. Friedman showed that iFOL can be embedded in minimal logic (mFOL). By his transformation, mapping formula A to F r(A). If A is uniformly valid, then so is F r(A), and by our Basic Completeness result, we can find a proof of F r(A) in minimal logic. Then we prove A from F r(A) in intuitionistic logic by a proof procedure fixed in advance. Our result resolves an open question posed by Beth in 1947. 
URI:  http://hdl.handle.net/1813/24398 
Appears in Collections:  Computing and Information Science Technical Reports

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
