Hypothetical Logic of Proofs

&
Logica Universalis 8 (1):103-140 (2014)
  Copy   BIBTEX

Abstract

The logic of proofs is a refinement of modal logic introduced by Artemov in 1995 in which the modality ◻A is revisited as ⟦t⟧A where t is an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness and is capable of reflecting its own proofs . We develop the Hypothetical Logic of Proofs, a reformulation of LP based on judgemental reasoning

Categories

Keywords

Reprint years

DOI

10.1007/s11787-014-0098-0

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.
Proofs are Programs: 19th Century Logic and 21st Century Computing.Philip Wadler - manuscript
A short introduction to intuitionistic logic.G. E. Mint︠s︡ - 2000 - New York: Kluwer Academic / Plenum Publishers.
$lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
On proof terms and embeddings of classical substructural logics.Ken-Etsu Fujita - 1998 - Studia Logica 61 (2):199-221.
Lambda Calculus and Intuitionistic Linear Logic.Simona Ronchi Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
Derivation and computation: taking the Curry-Howard correspondence seriously.Harold Simmons - 2000 - New York: Cambridge University Press.
A lambda proof of the p-w theorem.Sachio Hirokawa, Yuichi Komori & Misao Nagayama - 2000 - Journal of Symbolic Logic 65 (4):1841-1849.
Recursion theory and the lambda-calculus.Robert E. Byerly - 1982 - Journal of Symbolic Logic 47 (1):67-83.
Typed lambda-calculus in classical Zermelo-Frænkel set theory.Jean-Louis Krivine - 2001 - Archive for Mathematical Logic 40 (3):189-205.
The Proofs of $alpha rightarrow alpha$ in $P - W$.Sachio Hirokawa - 1996 - Journal of Symbolic Logic 61 (1):195-211.
Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.

Analytics

Added to PP
2014-03-04

Downloads
20 (#747,345)

6 months
5 (#629,136)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
The Basic Intuitionistic Logic of Proofs.Sergei Artemov & Rosalie Iemhoff - 2007 - Journal of Symbolic Logic 72 (2):439 - 451.

Add more references