Computer Science – Logic in Computer Science
Scientific paper
2011-10-07
Computer Science
Logic in Computer Science
2011-10-17: Abstract updated to match 10/14 version. 2011-10-14: Edited version posted
Scientific paper
We establish completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable if and only if its embedding into minimal logic, mFOL, is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL and mFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform minimal evidence into a formal first-order 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 Konig'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 intuitionistic validity because Prf(F, evd) builds a first-order proof of F, establishing its intuitionistic 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 A-transformation, mapping formula F to FA. If F is uniformly valid, then so is FA, and by our completeness theorem, we can find a proof of FA in minimal logic. Then we intuitionistically prove F from FFalse, i.e. by taking False for A and for \bot of mFOL. Our result resolves an open question posed by Beth in 1947.
Bickford Mark
Constable Robert
No associations
LandOfFree
Intuitionistic Completeness of First-Order Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Intuitionistic Completeness of First-Order Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Intuitionistic Completeness of First-Order Logic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-133681