Sequent calculi for normal and non-normal deontic logics are introduced. For these calculi we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This yields that the subformula property holds for them and that they are decidable. Then we show that our calculi are equivalent to the axiomatic ones, and therefore that they are sound and complete w.r.t. neighborhood semantics. This is a major step in the development of the proof theory of deontic logics since our calculi allow for a systematic root-first proof search of formal derivations.
Proof Analysis in Deontic Logics / Eugenio Orlandelli. - STAMPA. - 8554:(2014), pp. 139-148. (Intervento presentato al convegno DEON 2014 tenutosi a Ghent nel 12-14 Luglio 2014) [10.1007/978-3-319-08615-6_11].
Proof Analysis in Deontic Logics
ORLANDELLI, EUGENIO
2014
Abstract
Sequent calculi for normal and non-normal deontic logics are introduced. For these calculi we prove that weakening and contraction are height-preserving admissible, and we give a syntactic proof of the admissibility of cut. This yields that the subformula property holds for them and that they are decidable. Then we show that our calculi are equivalent to the axiomatic ones, and therefore that they are sound and complete w.r.t. neighborhood semantics. This is a major step in the development of the proof theory of deontic logics since our calculi allow for a systematic root-first proof search of formal derivations.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
