A natural deduction system for discourse representation theory (Q1802396)

At present, the main competing theories of discourse semantics are Groenendijk's and Stokhof's Dynamic Predicate Logic (DPL) and Kamp's Discourse Representation Theory (DRT). Whereas DPL up to now lacks a sound and complete proof system, the author in his paper presents a Fitch-style natural deduction calculus \(S_{\text{DRT}}\) for DRT and sketches a completeness proof. \(S_{\text{DRT}}\) manipulates discourse representations (DRs). Its rules specify how to reason from and towards ``complex conditions'', which are built up from DRs and the logical constants \(\Rightarrow\), \(\vee\) and \(\neg\). These rules are uttermost complex, since there are bunches of side conditions, which make it complicated to identify inferential moves as instantiations of the rules. Therefore, although the rules are extracted from Fitch-style natural deduction for classical logic, it remains doubtful whether \(S_{\text{DRT}}\) may be considered as the kernel of a ``mental logic''.