In this paper we lay the foundations of a new proof-theory for classical first-order logic that allows for a natural characterization of a notion of inferential depth. The approach we propose here aims towards extending the proof-theoretical framework presented in [6] by combining it with some ideas inspired by Hintikka’s work [18]. Unlike standard natural deduction, in this framework the inference rules that fix the meaning of the logical operators are symmetrical with respect to assent and dissent and do not involve the discharge of formulas. The only discharge rule is a classical dilemma rule whose nested applications provide a sensible measure of inferential depth. The result is a hierarchy of decidable depth-bounded approximations of classical first-order logic that expands the hierarchy of tractable approximations of Boolean logic investigated in [11, 10, 7].

Towards Depth-Bounded Natural Deduction for Classical First-order Logic / M. D'Agostino, C. Larese, S. Modgil. - In: THE IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS. - ISSN 2055-3706. - 8:2 (Special Issue)(2021 Mar), pp. 423-451.

Towards Depth-Bounded Natural Deduction for Classical First-order Logic

M. D'Agostino
Co-primo
;
C. Larese
Co-primo
;
2021

Abstract

In this paper we lay the foundations of a new proof-theory for classical first-order logic that allows for a natural characterization of a notion of inferential depth. The approach we propose here aims towards extending the proof-theoretical framework presented in [6] by combining it with some ideas inspired by Hintikka’s work [18]. Unlike standard natural deduction, in this framework the inference rules that fix the meaning of the logical operators are symmetrical with respect to assent and dissent and do not involve the discharge of formulas. The only discharge rule is a classical dilemma rule whose nested applications provide a sensible measure of inferential depth. The result is a hierarchy of decidable depth-bounded approximations of classical first-order logic that expands the hierarchy of tractable approximations of Boolean logic investigated in [11, 10, 7].
Natural Deduction; Classical First-order Logic; Bounded rationality; Analytic-synthetic distinction
Settore M-FIL/02 - Logica e Filosofia della Scienza
LOGIC AND COGNITION: Theory, experiments, and applications
http://collegepublications.co.uk/contents/ifcolog00044.pdf
Article (author)
File in questo prodotto:
File Dimensione Formato  
ifcolog00044.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Publisher's version/PDF
Dimensione 1.56 MB
Formato Adobe PDF
1.56 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

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/2434/828073
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact