I/O Logic in HOL --- First Steps
Christoph Benzmüller Xavier Parent

*
    Mario Bonk and Huy Tran
    Jan 2018
===========================



 A semantical embedding of input/output logic in classical higher-order logic is presented. This embedding enables the mechanisation and automation of reasoning tasks in input/output logic with off-the-shelf higher-order theorem provers and proof assistants. The key idea for the solution presented here results from the analysis of an inaccurate previous embedding attempt, which we will discuss as well.




§ INPUT/OUTPUT LOGIC

Input/output (I/O) logic, initially devised by Makinson 
<cit.> and  further developed by Leon van der Torre and colleagues, is an deontic logic framework that has gained increased recognition in the AI
community. This is evidenced by the fact that the framework has its
own chapter in the handbook of deontic logic and
normative systems <cit.>.

I/O logic operators, such as the (simple-minded) output operation out_1, accept a set G of conditional norms as argument. The conditional norms in G are given as pairs (a,x). The body a of such a pair, called the input, is representing some condition or situation. The head x, called output, is representing what is desirable or obligatory in the given situation. 
a and x are thereby propositional formulas. A key point is that the pair (a,x) is not given a truth-functional semantics in I/O logic. 

Different kinds of I/O operations have been presented in the literature. In this short note we focus on the I/O logic operator out_1. Future work will extend the presented work to other  I/O operations. When out_1 is applied to a set G of conditional norms and a set A of propositions describing of an input situation, it tells us what is desirable or obligatory  in this situation according to G.
 
The semantics of I/O logic operator out_1 is defined as follows (P is the set of propositional formulas and  is the associated propositional logic consequence relation): 
out_1(G,A) := Cn(G(Cn(A))), with Cn(X) := {s ∈ P  | X  s}  and G(X) := {s ∈ P | there exists  a ∈ X  such that  (a,s) ∈ G }. 
For technical reasons we below restrict out_1(G,a) to operate only on a single propositional input formula a. However, one may consider a as the conjunction of all formulas a_i∈ A. 

A proof theory for out_1 is given by the following proof rules:

    


This proof system works as follows. In order to check whether x in out_1(G,a), the proof system is first expanded by adding a rule [](b,c) for each pair (b,c)∈ G. Then it is checked whether the pair (a,x) can be derived 
from finitely many pairs in G using the rules above.




§ EMBEDDING OF I/O LOGIC IN HOL – INITIAL ATTEMPT
 
An initial, naive attempt to embed I/O logic in Isabelle/HOL <cit.> did fail. However, a careful failure analysis was key for devising the proper embedding as presented in Sec. <ref> below. We briefly recap this initial embedding attempt, which is also displayed in Fig. <ref>, and explain the issue. 
 

This section and the remainder of this paper requires some background knowledge about HOL. However, due to lack of space we do not present a respective introduction here and instead refer to the literature <cit.>.



In our naive embedding attempt the statement a  s was simply mapped to implication:
_o  o o := λ  a_o λ s_o (a ⊃ s). This was inspired by the deduction theorem for classical propositional logic: a  s iff a ⊃ s. Subsequently, an operation outpre was defined as 
outpre_((o × o)  o)  o  (o o) := λ G_(o × o)  oλ a_o λ y_o ∃ f_o ((Cn  a) f ∧ G (f,y)), the idea being that outpre(N,a) should denote the set {y ∈ P | exists  f ∈ Cn(a)  such that  (f,y) ∈ N}, that is outpre(G,a) = G(Cn(a)).
In a final step, a pragmatically motivated approximation[In this experimental phase this approximation was sufficient and a proper definition was postponed for later. In fact, this approximation is not influencing the core problem as discussed below.] of out_1 was defined as out_1_((o × o)  o)  o  (o o):= λ G_(o × o)  oλ a_o λ x_o 
∃ h_o ∃ i_o ∃ j_o ((outpre N a h) ∧ (outpre N a i) ∧ (outpre N a j) ∧ ((h ∧ i ∧ j) ⊃ x)). That is, out'_1(N,a) denotes the set {x ∈ P |{a,j,k}⊆ outpre(N,a) ∧ 
((h ∧ i ∧ j) ⊃ x). This is an approximation of out_1 in the sense that not all consequences of outpre(N,a) are modelled, but only those that follow from maximally three formulas in outpre(N,a). Moreover, to keep the discussion as simple as possible we assume here that outpre(N,a) is non-empty.

Two simple, running examples are used in the remainder of this section to illustrate the fundamental problem with this naive embedding attempt. Let the set of conditional norms G be given as {(a,e),(b,e)}, for propositional symbols a, b, and e.  Example E1 asks whether e is in out_1(G,a), and example E2 asks whether e is in out_1(G,a∨ b).  The former is expected to hold, but the latter not (for simple minded output). However, when utilising the above embedding both E1 and E2 unfold into valid HOL formulas. The reason for this unsound behaviour can be well explained already on the basis of outpre alone, which is preferable since it leads to smaller unfolded HOL formulas we need to discuss. Thus, we modify the examples into E1': e is in outpre(G,a) and E2: e is in outpre(G,a∨ b).

Unfolding the embedding for E1' results in the HOL formula 
∃ f. (a ⊃ f) ∧ ((f,e) = (a,e) ∨ (f,e) = (b,e)), which is valid as intended: simply choose f as a.

Unfolding E2' analogously results in ∃ f. ((a ∨ b) ⊃ f) ∧ ((f,e) = (a,e) ∨ (f,e) = (b,e)). However, contrary to our intention, this formula is also valid in HOL. To see this, choose f as a∨ b: ((a ∨ b) ⊃ (a ∨ b)) ∧ (((a ∨ b),e) = (a,e) ∨ ((a ∨ b),e) = (b,e)). By simplification, Boolean extensionality and congruence this formula is equivalent to[This formula is also equivalent to (a∨ b,e) = (a,e) ∨ (a∨ b,e) = (b,e). For proving this alternative, simplified formula we proceed as follows. We know that (a∨ b) ∨ (a∨ b) holds by the law of excluded middle. We proceed by case distinction. If a∨ b is true we have a is true or b is true. In the former case we get (a∨ b,e) = (a,e) and in the latter case we have (a∨ b,e) = (b,e), and we are done. If (a∨ b) is false, we have a is false and b is false, and thus both (a∨ b,e) = (a,e) and (a∨ b,e) = (b,e) are true by Boolean extensionality and congruence.]
((a∨ b) ⊃ a) ∨ ((a∨ b) ⊃ b), which is valid in classical logic: We know that (a∨ b) ∨ (a∨ b) holds by the law of excluded middle. Hence, we proceed by case distinction. If a∨ b is true, we have a is true or b is true. In both cases the statement follows trivially.  The statement is also trivially true in case a∨ b is false. 

We have thus reduced E2': e is in outpre(G,a∨ b) to ((a∨ b) ⊃ a) ∨ ((a∨ b) ⊃ b). Intuitively, however, we should have reduced E2' to (((a∨ b) ⊃ a) or  ((a∨ b) ⊃ a)), which is not equivalent, since the former does not imply the latter.

The problem obviously is this: a  s, respectively a ⊃ s, cannot be simply encoded as a ⊃ b, at least not when this formula is subsequently nested in other  formulas, as done here in the definition of outpre. Such an encoding and nested usage, in combination with the law of excluded middle, causes the observed unsound behaviour. 
A more appropriate modeling of a ⊃ s is thus required.






§ PROPER EMBEDDING OF I/O LOGIC IN HOL
 
To obtain a proper embedding of I/O Logic in HOL
we devise a suitable encoding of φ, cf. the Isabelle/HOL encoding of our solution in Fig. <ref>.
By suitable we mean that the new encoding of φ can be nested in larger formula contexts without causing the effect as discussed in Sec. <ref>. This can be achieved by lifting the propositional formulas of I/O logic to predicates on possible worlds (or states). We thus reuse a technique from previous work in which the objective was to properly embed (quantified) modal logics in HOL <cit.>. However, the reason for applying this technique is different here. Our challenge is not to properly encode e.g. the modal box operator, but to introduce a suitable encoding of a ⊃ s, so that occurrences of this term can be soundly nested in other formulas, while blocking certain undesirable effects of the law of excluded middle. 


Propositional formulas φ of I/O logic therefore mapped to associated HOL predicates of type i→ o, where type i denotes a (non-empty) set of possible worlds (or states). The logical connectives , ∨, ∧ and ⊃ of I/O logic defined in this mapping as follows: φ := λ w  (φ w), φ∨ψ := λ w (φ w ∨ψ w), φ∧ψ := λ w (φ w ∧ψ w), and φ⊃ψ := λ w (φ w ⊃ψ w). The lifted I/O formulas in HOL are “grounded” again to Boolean type by the following definition of validity: valid φ := ∀ w (φ w). The claim now is that valid φ, denoted in the remainder (and in related papers) also as ⌊φ⌋, suitably encodes φ ins such a way that this term can safely be nested in larger formula context without causing the effects as observed in Sec. <ref>. The previous definitions of outpre is thus changed as follows: outpre := λ G λ a λ y ∃ f (⌊ a ⊃ f⌋∧ G (f,y)). The approximative encoding of out_1, which refers to outpre, remains unchanged.


We once again analyse the running examples, but now for the modified semantical embedding. Example E1': e is in outpre(G,a) now unfolds into the HOL formula ∃ f ((∀ w (a w ⊃ f w)) ∧ ((f, e) = (a, e) ∨ (f, e) = (b, e))). This formula is valid as intended: simply instantiate f with λ x (a x). Similarly, example E1: e is in out_1(G,a) unfolds into a valid HOL formula, and we leave the details of this example to the reader.


The more interesting example E2': e is in outpre(G,a∨ b) now unfolds into ∃ f ((∀ w. (a w ∨ b w) ⊃ f w) ∧  ((f, e) = (a, e) ∨ (f, e) = (b, e)). We apply an analogous idea as before and instantiate f with λ x (a x ∨ b x), which results, after normalisation and simplification, in the HOL formula 


(λ x (a x ∨ b x)), e) = (a, e) ∨ ((λ x (a x ∨ b x)), e) = (b, e). Contrary to the situation in Sec. <ref>, the law of excluded middle cannot be exploited anymore to prove this formula.
This formula in fact has a countermodel:  Consider two possible worlds i_1 and i_2, and choose a as the set {i_2} (i.e., a is true only in world i_2) and b as the set {i_1}; then λ x (a x ∨ b x) denotes the set {i_1, i_2}, and our formula obviously evaluates to false. 
We obtain respective countermodels for both  E2' and E2, and these countermodels are quickly found automatically by the model finder Nitpick <cit.> as illustrated in Fig. <ref>.












§ CONCLUSION



Just in time for the 50st birthday of Leon van der Torre we have devised a proper semantical embedding of the simple minded I/O logic operation out_1 into HOL. Further work includes the formal validation of the faithfulness (soundness and completeness) of the embedding, and extensions to further I/O operations.

Ongoing work is utilising the very same technique as employed in this paper for the embedding of the proof theory of I/O logic in HOL. The current status of these activities is depicted in Fig. <ref>. An advantage is that an approximation of out_1 can easily be avoided. A disadvantage, however, is that proof automation and countermodel finding seems to become less effective, this is what current experiments indicate. Due the cut-introducing nature of the I/O proof rules SO and WI, when applied in backward direction, this is not so surprising though.

Another promising direction for future work is to devise an alternative semantical embedding of I/O logic in HOL based on Parent's recent interpretation of I/O Logic in intuitionistic logic <cit.>. This work could be based on the already existing semantical embedding of intuitionistic logic in HOL <cit.>.















































abbrv


 




