Intuitionistic completeness of first-order logic

DOI10.1016/J.APAL.2013.07.009zbMath1345.03114arXiv1110.1614OpenAlexW1999807931WikidataQ55967618 ScholiaQ55967618MaRDI QIDQ392280

Mark Bickford, Robert L. 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

completenessconstructive type theoryintuitionistic logicBHK semanticsevidence semanticsintersection type

Mathematics Subject Classification ID

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

Related Items (6)

Innovations in computational type theory using Nuprl ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ Trace-based verification of imperative programs with I/O ⋮ Lindenbaum’s Lemma via Open Induction ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ Higher order functions and Brouwer’s thesis

Uses Software

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

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Intuitionism. An introduction
• Combinatory logic. With two sections by William Craig.
• The foundations of mathematics. A study in the philosophy of science
• Innovations in computational type theory using Nuprl
• Lectures on the Curry-Howard isomorphism
• Do-it-yourself type theory
• The calculus of constructions
• Constructivism in mathematics. An introduction. Volume II
• LCF considered as a programming language
• Zur Deutung der intuitionistischen Logik
• Edinburgh LCF. A mechanized logic of computation
• 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
• Syntactic translations and provably recursive functions
• A framework for defining logics
• An intuitiomstic completeness theorem for intuitionistic predicate logic
• An intuitionistically plausible interpretation of intuitionistic logic
• An application of constructive completeness
• Completeness and incompleteness for intuitionistic logic
• Intensional interpretations of functionals of finite type I
• On weak completeness of intuitionistic predicate logic
• On the interpretation of intuitionistic number theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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