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.
1985
Modal Logic; Provability Logic; Natural Deduction
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/30366
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact