An Intuitionistic Investigation of Prerequisite-Effect Structure

This paper studies the prerequisite-effect structures in legal documents from a logical viewpoint. First, we distinguish a written prerequisite-effect structure in legal documents and an application-instance of the written structure to a particular case, and formalize the latter as \(\leadsto\). Second, we specify its semantics as ‘immediately after’ on intuitionistic Kripke model. Third, we establish semantic properties of \(\leadsto\) including the undefinability of \(\leadsto\) in intuitionistic logic, and provide a cut-free and complete labelled sequent calculus with the intuitionistic logic with \(\leadsto\). Finally, we illustrate a formal representation of Articles 7 and 9 of Japanese Income Tax Act with the help of \(\leadsto\).