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.
A system of natural deduction for GL
BELLIN, Gianluigi
1985-01-01
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.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
GLNatDed.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
1.38 MB
Formato
Adobe PDF
|
1.38 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
