PRK, una lógica constructiva clásica

Mostrar todas las versiones(3)

Esta tesis presenta el sistema prk, un sistema lógico en el cual las nociones de prueba y refutación son duales. Este sistema extiende a la lógica clásica y es constructivo en el sentido de que se lo puede dotar de una interpretación computacional con buenas propiedades. Las fórmulas de prk se clasi...

Descripción completa

Detalles Bibliográficos
Autor principal: Freund, Teodoro
Formato: Tesis de Grado
Lenguaje:Español
Publicado: 2021
Materias:
LOGICA
CURRY-HOWARD
LOGICA CLASICA
PROPOSICIONES COMO TIPOS
LOGICA CONSTRUCTIVA
SEMANTICA DE KRIPKE
LOGIC
CLASSICAL LOGIC
PROPOSITION AS TYPES
CONSTRUCTIVE LOGIC
KRIPKE SEMANTICS
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:seminario_nCOM000486_Freund
record_format dspace
spelling todo:seminario_nCOM000486_Freund2023-10-03T16:48:50Z PRK, una lógica constructiva clásica PRK, a constructive classical logic Freund, Teodoro LOGICA CURRY-HOWARD LOGICA CLASICA PROPOSICIONES COMO TIPOS LOGICA CONSTRUCTIVA SEMANTICA DE KRIPKE LOGIC CURRY-HOWARD CLASSICAL LOGIC PROPOSITION AS TYPES CONSTRUCTIVE LOGIC KRIPKE SEMANTICS Esta tesis presenta el sistema prk, un sistema lógico en el cual las nociones de prueba y refutación son duales. Este sistema extiende a la lógica clásica y es constructivo en el sentido de que se lo puede dotar de una interpretación computacional con buenas propiedades. Las fórmulas de prk se clasifican a lo largo de dos ejes, dependiendo de su positividad (afirmación o negación) y su fuerza (fuerte o clásica). Las proposiciones fuertes se demuestran, canónicamente, con reglas de introducción, mientras que las proposiciones clásicas se demuestran por reducción al absurdo. El sistema prk resulta ser correcto y completo con respecto a una clase de modelos de Kripke, definida en este mismo trabajo. Siguiendo la correspondencia de Curry–Howard, se formaliza un cálculo asociado a prk, denominado λprk, cuyo sistema de tipos se corresponde con la lógica prk. Se establecen varias propiedades sobre λprk, incluyendo preservación de tipos, confluencia y una caracterización de las formas normales de las pruebas y refutaciones. La terminación fuerte del cálculo λprkse demuestra a través de una traducción a System F extendido con ecuaciones recursivas entre tipos, y apoyándose en un resultado de Mendler. Por último, se considera una extensión a segundo orden del sistema prk, junto con el cálculo correspondiente λ2prk. Se extienden a este marco los resultados anteriormente mencionados, exceptuando la terminación fuerte de λ2prk, que queda abierta como trabajo futuro. This thesis introduces prk, a constructive classical logic with dual proofs and refutations that refines classical logic and provides a well behaved computational interpretation for it. Formulas in prk can be classified along two axes, depending on their positivity (affirmation or denial) and their strength (strong or classical). Strong propositions are, canonically, proved with introduction rules, whereas the proof of a classical proposition always proceeds by contradiction. The system prk is shown to be sound and complete with respect to a particular kind of Kripke semantics, also defined in this work. A calculus for prk, dubbed λprk, is formalized. Its type system is in close correspondence with the logical rules of prk, in the sense of the propositions-as-types paradigm. A number of properties, including subject reduction, confluence, and a characterization of canonical proofs and refutations, are established. Strong normalization of this calculus is proved via a translation to System F with Mendlerstyle recursive type constraints. Finally, an extension of prk to second order logic is presented, including a corresponding calculus λ2prk. The aforementioned results are extended to this setting, except for strong normalization of λ2prk, which is left as future work. Fil: Freund, Teodoro. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2021 Tesis de Grado PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv Español
topic LOGICA
CURRY-HOWARD
LOGICA CLASICA
PROPOSICIONES COMO TIPOS
LOGICA CONSTRUCTIVA
SEMANTICA DE KRIPKE
LOGIC
CURRY-HOWARD
CLASSICAL LOGIC
PROPOSITION AS TYPES
CONSTRUCTIVE LOGIC
KRIPKE SEMANTICS
spellingShingle LOGICA
CURRY-HOWARD
LOGICA CLASICA
PROPOSICIONES COMO TIPOS
LOGICA CONSTRUCTIVA
SEMANTICA DE KRIPKE
LOGIC
CURRY-HOWARD
CLASSICAL LOGIC
PROPOSITION AS TYPES
CONSTRUCTIVE LOGIC
KRIPKE SEMANTICS
Freund, Teodoro
PRK, una lógica constructiva clásica
topic_facet LOGICA
CURRY-HOWARD
LOGICA CLASICA
PROPOSICIONES COMO TIPOS
LOGICA CONSTRUCTIVA
SEMANTICA DE KRIPKE
LOGIC
CURRY-HOWARD
CLASSICAL LOGIC
PROPOSITION AS TYPES
CONSTRUCTIVE LOGIC
KRIPKE SEMANTICS
description Esta tesis presenta el sistema prk, un sistema lógico en el cual las nociones de prueba y refutación son duales. Este sistema extiende a la lógica clásica y es constructivo en el sentido de que se lo puede dotar de una interpretación computacional con buenas propiedades. Las fórmulas de prk se clasifican a lo largo de dos ejes, dependiendo de su positividad (afirmación o negación) y su fuerza (fuerte o clásica). Las proposiciones fuertes se demuestran, canónicamente, con reglas de introducción, mientras que las proposiciones clásicas se demuestran por reducción al absurdo. El sistema prk resulta ser correcto y completo con respecto a una clase de modelos de Kripke, definida en este mismo trabajo. Siguiendo la correspondencia de Curry–Howard, se formaliza un cálculo asociado a prk, denominado λprk, cuyo sistema de tipos se corresponde con la lógica prk. Se establecen varias propiedades sobre λprk, incluyendo preservación de tipos, confluencia y una caracterización de las formas normales de las pruebas y refutaciones. La terminación fuerte del cálculo λprkse demuestra a través de una traducción a System F extendido con ecuaciones recursivas entre tipos, y apoyándose en un resultado de Mendler. Por último, se considera una extensión a segundo orden del sistema prk, junto con el cálculo correspondiente λ2prk. Se extienden a este marco los resultados anteriormente mencionados, exceptuando la terminación fuerte de λ2prk, que queda abierta como trabajo futuro.
format Tesis de Grado
author Freund, Teodoro
author_facet Freund, Teodoro
author_sort Freund, Teodoro
title PRK, una lógica constructiva clásica
title_short PRK, una lógica constructiva clásica
title_full PRK, una lógica constructiva clásica
title_fullStr PRK, una lógica constructiva clásica
title_full_unstemmed PRK, una lógica constructiva clásica
title_sort prk, una lógica constructiva clásica
publishDate 2021
url https://hdl.handle.net/20.500.12110/seminario_nCOM000486_Freund
work_keys_str_mv AT freundteodoro prkunalogicaconstructivaclasica
AT freundteodoro prkaconstructiveclassicallogic
_version_ 1807318075780890624

Ejemplares similares