Ideality and subideality from a computational point of view

Why should Law need automated proof systems? The answer to this question implies an answer to the following question: Is logic needed in Law? In fact it has been argued that logics are useless for Law (see, for example, Kelsen 1989). We believe that logic, and deontic logics in particular - but also modal logics - have a role to play in Law; for example if one wants to study what the relationships are among the various degrees of adjudication in Italian Law, one should note that they give rise to a transitive, irreflexive and finite structure, which is the frame of the modal logic of provability GL; one of the most important properties of such a logic is that no system, (no court) in this frame, could claim its own correctness without becoming incorrect (Boolos 1993, Smullyan 1988), but the correctness of a lower court can be established by a higher one. This example shows that the study of modal logic can help in finding certain already known properties of legal systems. Moreover, each time we are dealing with the notions of Obligation and Permission, and we are interested in the study of their mutual relationship, we can arrange them into a deontic framework, thus producing a certain kind of deontic logic. Finally a hint for the use of logic in legal reasoning is given, for example in the Italian case, by the law itself; in fact article 192, 1 comma of the "Italian code of criminal procedure" prescribes that the judges state the reasons of their adjudication; moreover several other articles of the same code, state: when evidence is valid, how evidence should be used in order to lead to an adjudication, etc. On this basis the "Italian code of criminal procedure" can be thought of as a deductive system where its articles act as the inference rules, whereas the articles of the "Italian code of criminal law" are the axioms. What does a proof system do? A proof system can work in two ways. The first of them consists of producing admissible steps one after the other according to the inference rules; in this way each step is guaranteed to be correct, but we are not led to the goal we want to prove. The other one consists of verifying whether a conclusion follows from given premises, i.e., if the adjudication follows logically from the evidence, mainly by refuting the negation of the conclusion. The system we propose is based on the logic of ideality and subideality developed by Jones and Porn, and it verifies in the above mentioned logical framework whether a given conclusion follows from given premises. Moreover, due to its basic control structure it can also be used as an analytic direct proof system