The reasoning for this qualitative question is similar to the propositional question.
Theorem (c4):
Proof !c4(c4): We begin with an instance of the first axiom for qualitative questions
which, by definition of c3, can be written as
Instantiating the axiom for reply we have
and it follows from the two lines above that
which by definition of c4 we can write as
Due to the frame axioms, the conclusion established in the first question
also holds in context c4.
Theorem (frame):
Proof !frame(frame): We first instantiate the second axiom for qualitative questions to get
The two lines above imply
which, by definition of c3, can be written as
Now we apply the following instance of the reply axiom
to get
which, by definition of c4, can be written as
