The first-order hypothetical logic of proofs

The Propositional Logic of Proofs (LP) is a modal logic in which the modality □A is revisited as [[t]]A, t being an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness, can realize all S4 theorems and is capable of reflecting its own proofs (⊢A impli...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Steren, G., Bonelli, E.
Formato:	JOUR
Materias:	Curry howard isomorphism First-order logic of proofs Lambda calculus Natural deduction Calculations Computer circuits Differentiation (calculus) Semantics Curry-Howard correspondence Curry-Howard isomorphism First order logic Provability semantics Soundness and completeness Strong normalization Formal logic
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_0955792X_v27_n4_p1023_Steren
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_0955792X_v27_n4_p1023_Steren
record_format	dspace
spelling	todo:paper_0955792X_v27_n4_p1023_Steren2023-10-03T15:51:51Z The first-order hypothetical logic of proofs Steren, G. Bonelli, E. Curry howard isomorphism First-order logic of proofs Lambda calculus Natural deduction Calculations Computer circuits Differentiation (calculus) Semantics Curry-Howard correspondence Curry-Howard isomorphism First order logic Lambda calculus Natural deduction Provability semantics Soundness and completeness Strong normalization Formal logic The Propositional Logic of Proofs (LP) is a modal logic in which the modality □A is revisited as [[t]]A, t being an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness, can realize all S4 theorems and is capable of reflecting its own proofs (⊢A implies ⊢[[t]]A, for some t). A presentation of first-order LP has recently been proposed, FOLP, which enjoys arithmetical soundness and has an exact provability semantics. A key notion in this presentation is how free variables are dealt with in a formula of the form [[t]]A(i). We revisit this notion in the setting of a Natural Deduction presentation and propose a Curry-Howard correspondence for FOLP. A term assignment is provided and a proof of strong normalization is given. © The Author, 2016. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_0955792X_v27_n4_p1023_Steren
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Curry howard isomorphism First-order logic of proofs Lambda calculus Natural deduction Calculations Computer circuits Differentiation (calculus) Semantics Curry-Howard correspondence Curry-Howard isomorphism First order logic Lambda calculus Natural deduction Provability semantics Soundness and completeness Strong normalization Formal logic
spellingShingle	Curry howard isomorphism First-order logic of proofs Lambda calculus Natural deduction Calculations Computer circuits Differentiation (calculus) Semantics Curry-Howard correspondence Curry-Howard isomorphism First order logic Lambda calculus Natural deduction Provability semantics Soundness and completeness Strong normalization Formal logic Steren, G. Bonelli, E. The first-order hypothetical logic of proofs
topic_facet	Curry howard isomorphism First-order logic of proofs Lambda calculus Natural deduction Calculations Computer circuits Differentiation (calculus) Semantics Curry-Howard correspondence Curry-Howard isomorphism First order logic Lambda calculus Natural deduction Provability semantics Soundness and completeness Strong normalization Formal logic
description	The Propositional Logic of Proofs (LP) is a modal logic in which the modality □A is revisited as [[t]]A, t being an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness, can realize all S4 theorems and is capable of reflecting its own proofs (⊢A implies ⊢[[t]]A, for some t). A presentation of first-order LP has recently been proposed, FOLP, which enjoys arithmetical soundness and has an exact provability semantics. A key notion in this presentation is how free variables are dealt with in a formula of the form [[t]]A(i). We revisit this notion in the setting of a Natural Deduction presentation and propose a Curry-Howard correspondence for FOLP. A term assignment is provided and a proof of strong normalization is given. © The Author, 2016.
format	JOUR
author	Steren, G. Bonelli, E.
author_facet	Steren, G. Bonelli, E.
author_sort	Steren, G.
title	The first-order hypothetical logic of proofs
title_short	The first-order hypothetical logic of proofs
title_full	The first-order hypothetical logic of proofs
title_fullStr	The first-order hypothetical logic of proofs
title_full_unstemmed	The first-order hypothetical logic of proofs
title_sort	first-order hypothetical logic of proofs
url	http://hdl.handle.net/20.500.12110/paper_0955792X_v27_n4_p1023_Steren
work_keys_str_mv	AT stereng thefirstorderhypotheticallogicofproofs AT bonellie thefirstorderhypotheticallogicofproofs AT stereng firstorderhypotheticallogicofproofs AT bonellie firstorderhypotheticallogicofproofs
_version_	1807321046732242944

The first-order hypothetical logic of proofs

Ejemplares similares