Intuitionistic completeness of first-order logic

DOI10.1016/J.APAL.2013.07.009zbMATH Open1345.03114arXiv1110.1614OpenAlexW1999807931WikidataQ55967618 ScholiaQ55967618MaRDI QIDQ392280FDOQ392280

Authors: Mark Bickford, Robert Constable 

Publication date: 13 January 2014

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

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.

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

Recommendations

• Intuitionistic completeness for first order classical logic
• scientific article; zbMATH DE number 1169382
• Completeness and incompleteness for intuitionistic logic
• Intuitionistic completeness and classical logic
• First-order intensional logic
• Strong conceptual completeness for first-order logic
• scientific article; zbMATH DE number 5000990
• First-order predicate logic and Gödel's completeness theorem
• Intuitionistic computability logic
• Publication:3027002

zbMATH Keywords

completenessintuitionistic logicBHK semanticsconstructive type theoryevidence semanticsintersection type

Mathematics Subject Classification ID

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

Cites Work

• Innovations in computational type theory using Nuprl
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• LCF considered as a programming language
• Title not available (Why is that?)
• Title not available (Why is that?)
• A framework for defining logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On weak completeness of intuitionistic predicate logic
• Intuitionism. An introduction
• Combinatory logic. With two sections by William Craig.
• Lectures on the Curry-Howard isomorphism
• On the interpretation of intuitionistic number theory
• Title not available (Why is that?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Title not available (Why is that?)
• Completeness and incompleteness for intuitionistic logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Zur Deutung der intuitionistischen Logik
• Types and programing languages
• Title not available (Why is that?)
• The calculus of constructions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The foundations of mathematics. A study in the philosophy of science
• Title not available (Why is that?)
• Intensional interpretations of functionals of finite type I
• Undecidability and intuitionistic incompleteness
• Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
• Continuation-passing style models complete for intuitionistic logic
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Syntactic translations and provably recursive functions
• Title not available (Why is that?)
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• An intuitionistically plausible interpretation of intuitionistic logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An application of constructive completeness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Do-it-yourself type theory

Cited In (22)

• Intuitionistic ancestral logic as a dependently typed abstract programming language
• Simple proof of the completeness theorem for second-order classical and intuitionistic logic by reduction to first-order mono-sorted logic
• Verified completeness in Henkin-style for intuitionistic propositional logic
• An intuitionistic completeness theorem for classical predicate logic
• Title not available (Why is that?)
• Semantical completeness of first-order predicate logic and the weak fan theorem
• Title not available (Why is that?)
• Failure of completeness in proof-theoretic semantics
• Title not available (Why is that?)
• Lindenbaum's lemma via open induction
• Trace-based verification of imperative programs with I/O
• Completeness theorems for first-order logic analysed in constructive type theory
• Title not available (Why is that?)
• THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC
• Validating Brouwer's continuity principle for numbers using named exceptions
• Innovations in computational type theory using Nuprl
• Title not available (Why is that?)
• Title not available (Why is that?)
• UNIFICATION IN INTERMEDIATE LOGICS
• Intuitionistic completeness for first order classical logic
• Higher order functions and Brouwer's thesis
• Title not available (Why is that?)

Uses Software

• Coq
• MetaPRL
• Nuprl
• Twelf
• Automath
• LCF
• Agda

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)