Sobre la representación de S4.3

En 1935 Gerhard Gentzen introdujo un formalismo sintáctico para representar lógicas llamado Cálculo de Secuentes. El mismo es adecuado para analizar propiedades de la lógica, facilita un conocimiento más profundo del comportamiento individual de cada uno de los operadores de la misma y en muchos cas...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Bonelli, Eduardo, Menni, Matías
Otros Autores:	Meré, María Claudia
Formato:	Tesis Tesis de grado
Lenguaje:	Español
Publicado:	1996
Materias:	Ciencias Informáticas Representations (procedural and rule-based) lógica modal formalismos reglas
Acceso en línea:	http://sedici.unlp.edu.ar/handle/10915/2143
Aporte de:	SEDICI (UNLP) de Universidad Nacional de La Plata

id	I19-R120-10915-2143
record_format	dspace
institution	Universidad Nacional de La Plata
institution_str	I-19
repository_str	R-120
collection	SEDICI (UNLP)
language	Español
topic	Ciencias Informáticas Representations (procedural and rule-based) lógica modal formalismos reglas
spellingShingle	Ciencias Informáticas Representations (procedural and rule-based) lógica modal formalismos reglas Bonelli, Eduardo Menni, Matías Sobre la representación de S4.3
topic_facet	Ciencias Informáticas Representations (procedural and rule-based) lógica modal formalismos reglas
description	En 1935 Gerhard Gentzen introdujo un formalismo sintáctico para representar lógicas llamado Cálculo de Secuentes. El mismo es adecuado para analizar propiedades de la lógica, facilita un conocimiento más profundo del comportamiento individual de cada uno de los operadores de la misma y en muchos casos se puede usar para implementar un demostrador de teoremas para la misma, todo esto a través del estudio de las pruebas que en ese sistema deductivo pueden construirse. Una de las reglas de inferencia del Cálculo de Secuentes es de particular importancia en el estudio de propiedades metalógicas, la regla de Corte. Esta incorpora dentro del cálculo el uso de lemas. Los lemas son útiles para demostrar nuevos teoremas rápidamente, pero desde un punto de vista metalógico estamos interesados en estudiar pruebas sin elementos redundantes. Es fundamental entonces que un cálculo permita la construcción de una prueba sin aplicaciones de la regla de Corte para cada teorema. Esta propiedad se conoce como Propiedad de Eliminación de la Regla de Corte y trae como corolario propiedades tan importantes como consistencia, decidibilidad, interpolación, etc. Así, cualquier estudio relativo a una lógica tiene en cuenta la formulación de un Cálculo de Secuentes asociado como metodología básica para la comprensión de la misma. Las lógicas modales no constituyen una excepción. En este trabajo analizamos el Cálculo de Secuentes de S4.3, una lógica modal particular. Esta lógica también es una lógica temporal en el sentido que puede usarse para razonar sobre aserciones basadas en el tiempo, lineal y continuo. En la literatura encontramos un solo Cálculo de Secuentes (al estilo Gentzen, o a la Gentzen) para S4.3. Este cálculo presenta ciertas diferencias significativas respecto a aquellos formulados originalmente por Gentzen (llámense representaciones standard). Específicamente, una de las reglas de inferencia correspondiente al operador necesidad es complicada y su escritura en el formalismo resulta intrincada. Sin embargo, es importante destacar que esta representación goza de la Propiedad de Elimi- nación de la Regla de Corte. Surge entonces la siguiente pregunta. ¿ Habrá una representación standard para S4.3 que goce de la Propiedad de Eliminación de la Regla de Corte ? Formalizando la noción de representación standard dentro de las representaciones a la Gentzen, veremos que si aceptamos cierta conjetura que se expone en el capítulo 3, tal cálculo es imposible de obtener. Esto nos lleva a estudiar un formalismo alternativo para representar lógicas modales que altera la definición de secuente en el sentido que incorpora la noción de verdad relativa dentro de las reglas. Este formalismo fue originalmente definido para representar lógicas modales intuicionistas de modo que debemos alterar las definiciones básicas de forma de poder trabajar en un marco clásico. Usando este formalismo obtenemos un cálculo para S4.3 que goza de la Propiedad de Eliminación de la Regla de Corte y cuyas reglas son intuitivamente sencillas. Es importante notar que la demostración de la Propiedad de eliminación de la Regla de Corte es sintáctica. Además, el formalismo tiene otras ventajas. El uso del cálculo es ameno y natural, en numerosos ejemplos se verá que la construcción de pruebas en el cálculo es muy sencilla e intuitiva. Además se logra una independencia de las reglas de introducción de los operadores modales. De hecho, de el cálculo para S4.3 se puede extraer un cálculo para S4 sin modificar las reglas de introducción para los operadores modales. Sencillamente se quita del cálculo una regla que "exige" la propiedad de conexión sobre la relación de accesibilidad de los modelos de Kripke de la lógica.
author2	Meré, María Claudia
author_facet	Meré, María Claudia Bonelli, Eduardo Menni, Matías
format	Tesis Tesis de grado
author	Bonelli, Eduardo Menni, Matías
author_sort	Bonelli, Eduardo
title	Sobre la representación de S4.3
title_short	Sobre la representación de S4.3
title_full	Sobre la representación de S4.3
title_fullStr	Sobre la representación de S4.3
title_full_unstemmed	Sobre la representación de S4.3
title_sort	sobre la representación de s4.3
publishDate	1996
url	http://sedici.unlp.edu.ar/handle/10915/2143
work_keys_str_mv	AT bonellieduardo sobrelarepresentaciondes43 AT mennimatias sobrelarepresentaciondes43
bdutipo_str	Repositorios
_version_	1764820464523280384

Sobre la representación de S4.3

Ejemplares similares