We present a Natural Deduction system for the logic GL of Arithmetic Provability. The classical modal logic GL, extending the logic K4 with Loeb's axiom, is formalized here by extending Prawitz Natural Deduction system NK with a single modal rule, which introduces a modal formula as conclusion and at the same time eliminates all open assumptions the minor premise depends on, including a ``diagonal assumption'' of the same form as the conclusion.
Titolo: | A system of natural deduction for GL |
Autori: | |
Data di pubblicazione: | 1985 |
Rivista: | |
Abstract: | We present a Natural Deduction system for the logic GL of Arithmetic Provability. The classical modal logic GL, extending the logic K4 with Loeb's axiom, is formalized here by extending Prawitz Natural Deduction system NK with a single modal rule, which introduces a modal formula as conclusion and at the same time eliminates all open assumptions the minor premise depends on, including a ``diagonal assumption'' of the same form as the conclusion. |
Handle: | http://hdl.handle.net/11562/30366 |
Appare nelle tipologie: | 01.01 Articolo in Rivista |
File in questo prodotto:
File | Descrizione | Tipologia | Licenza | |
---|---|---|---|---|
GLNatDed.pdf | Documento in Post-print | ![]() | Open Access Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.