Intuitionistic completeness of first-order logic

DOI10.1016/J.APAL.2013.07.009MaRDI QIDQ392280zbMATH OpenOpenAlexWikidataFDO

Authors Mark Bickford, Robert Constable

Publication date 13 January 2014

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1110.1614

zbMATH Keywords

completeness intuitionistic logic BHK semantics constructive type theory evidence semantics intersection type

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Intuitionistic mathematics (03F55)

Abstract: 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 �ot of mFOL. Our result resolves an open question posed by Beth in 1947.

Recommendations

Cites work

Cited in

(23)

Describes a project that uses

Uses Software

This page was built for publication: Intuitionistic completeness of first-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q392280)