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
Publicado: 2017
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:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v27_n4_p1023_Steren
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 paper:paper_0955792X_v27_n4_p1023_Steren
record_format dspace
spelling paper:paper_0955792X_v27_n4_p1023_Steren2023-06-08T15:55:56Z The first-order hypothetical logic of proofs 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. 2017 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v27_n4_p1023_Steren 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
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.
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
publishDate 2017
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_0955792X_v27_n4_p1023_Steren
http://hdl.handle.net/20.500.12110/paper_0955792X_v27_n4_p1023_Steren
_version_ 1768542995739574272

Ejemplares similares