Reglas de introducción y eliminación de la deducción natural para cuantificadores modales

He leído varios artículos sobre la deducción natural modal, pero solo he podido encontrar una explicación clara de []-Introducción ( []Asi Ase puede probar sin suposiciones/premisas). Pero no había reglas separadas para <>-Introducción. En cambio <>A, se definió como ~[]~A. Y no había reglas para la eliminación de cuantificadores en absoluto.

Por razones estéticas, preferiría trabajar en una lógica en la que todos los símbolos se definan de forma primitiva y sus correspondencias sean resultados, y en la que no podamos manipular los términos en el ámbito de un cuantificador.

¿Existe una formalización de la lógica modal de este tipo? ¿Cuáles son sus reglas de introducción y eliminación? ¿Hay papeles al respecto?

<> la introducción/eliminación se describen en el blog de Cogburn . Para cuantificadores ver el capítulo 12 del libro de Garson .
No puedo acceder al libro, pero el blog es genial! Si publica esto como respuesta, tal vez con un pequeño resumen, lo aceptaría en un santiamén.
Gracias, pero no mi taza de té. Como pareces emocionado, tal vez podrías publicar un resumen de auto-respuesta. Para el libro prueba este enlace .
Puede ver: David Siemens, REGLAS DE ESTILO FITCH PARA MUCHAS LÓGICAS MODALES , NDJFL (1977)
Tal vez también el "original": Frederic Brenton Fitch, Lógica simbólica: una introducción , Ronald Press (1952)
Para una descripción general reciente: Andrzej Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logics , Springer (2010).

Respuestas (1)

De la lógica modal para filósofos de Garson (enlace en los comentarios anteriores):

Primero presentamos un nuevo tipo de subdemostración, una subdemostración en caja . No contiene suposiciones y está marcado por []en su inicio, como en

| presmises
|---
| stuff
|| []
||---
|| other stuff
| more stuff

No puede reiterar en una subprueba enmarcada, por lo que lo siguiente no es válido:

| Q
|---
|| []
||---
|| Q R   (BAD! NO! DON'T!)

Obviamente, eso sería una falacia: pasar de "es el caso" a "necesariamente el caso".

Ahora las reglas de inferencia. []-Introducción:

| []
|---
| .
| .
| .
| Q
------ []I
[]Q

También hay una []regla de eliminación. Es la excepción a lo de no reiterar y dice así:

| []Q
|| []
||---
------ []E
|| Q

Tenga en cuenta que esto no es realmente una eliminación, no en la forma normal en que lo pensamos. Lo que realmente esperaría es algo como []Q -> Q, pero esto es en realidad un axioma agregado a K para hacer el sistema T.

Ahora Garson define <>Q := ~[]~Q, pero quiero poder introducirlo y eliminarlo primitivamente. Garson proporciona una regla derivada para la <>eliminación:

<>P
| []
|---
|| P
|| .
|| .
|| .
|| Q
------ <>E
<>Q

Que se puede resumir como

<>P
[](P -> Q)
------ <>E
<>Q

No he podido encontrar una regla de inferencia para la <>introducción. Ahora me parece que tal regla no es posible, porque no hay una manera a priori de descubrir si un enunciado formal es meramente posible o no. Esto contrasta con la necesidad: sabemos a priori que todo enunciado demostrable en lógica no modal es necesario.

¿Qué descubriste acerca de una regla de <>-introducción? Comparto sus gustos estéticos y preferiría tener [] y <> primitivos también, y tengo curiosidad por saber si es posible.
@Adam, no seguí buscando por mucho tiempo, pero nunca encontré nada. : (
Parece que su regla de eliminación <> también es una regla de introducción <>; y no se pueden separar. Está eliminando <>P e introduciendo <>Q, derivando Q bajo una suposición de P en el contexto de un recuadro.
Reglas de introducción y eliminación de la deducción natural para cuantificadores modales
RespuestasAquíPolítica de privacidad1y, 0v