 Clearly, a5 is the only contra-classical axiom of C. The consequence relation ⊢C (derivability in C) is defined as usual. A C-frame is a pair F = &lt;W, ≤ &gt;, where ≤ is a reflexive and transitive binary relation on the non-empty set W. Let &lt;W, ≤ &gt;+ be the set of all X ⊆ W such that if u ∈ X and u ≤ w, then w ∈ X. A C-model is a structure M = &lt;W, ≤, v+, v− &gt;, where &lt;W, ≤ &gt; is a C-frame and v+ and v− are valuation functions from the set of propositional variables into &lt;W, ≤ &gt;+. Intuitively, W is a set of information states. The function v+ sends a propositional variable p to the states in W that support the truth of p, whereas v− sends p to the states that support the falsity of p. M = &lt;W, ≤, v+, v− &gt; is said to be the model based on the frame &lt;W, ≤ &gt;. The relations M, t ⊨+ A (“M supports the truth of A at t”) and M, t ⊨− A (“M supports the falsity of A at t”) are inductively defined as follows: