 Does any of this mean that there is a problem in finding an intuitionistic analogue of exclusive disjunction? Not at all. There are many derived binary connectives all of which form compounds equivalent in classical logic to the exclusive disjunction of φ with ψ and which are in the interesting cases not equivalent to each other intuitionistically—for example, φ ↔ ¬ψ and ¬(φ ↔ ψ) and (φ ∨ ψ) ∧ ¬(φ ∧ ψ). As it happens, the third of these (which is IL-equivalent to (φ ∧ ¬ψ) ∨ (¬ φ ∧ ψ)) has an especially close relationship with the truth-function of exclusive disjunction, like that between intuitionistic ¬ and the negation truth-function, which can be explained in terms of the Kripke semantics for intuitionistic logic (not explained in this entry) by saying that the compound in question is true at a point just in case at every accessible point it is true when evaluated by using the corresponding boolean function and the truth-values of the components at that  point.[40]  Note that the negation truth-function itself has its determinant-induced conditions rules dangerous to the health of intuitionistic logic under both (i) and (ii) of the result at the start of this example: no single connective can conservatively form from a formula a contrary of that formula (as ⟨T, F⟩ demands) and also a subcontrary of that formula (as ⟨F, T⟩ demands). As it is often put, standard intuitionistic negation (¬) forms the deductively weakest contrary of a formula, while dual intuitionistic negation (mentioned only in passing in this entry) forms its deductively strongest  subcontrary.[41]