Intuitionistic completeness of first-order logic
From MaRDI portal
Publication:392280
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
completenessconstructive type theoryintuitionistic logicBHK semanticsevidence semanticsintersection type
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
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
