 These last non-existence proofs force our attention on the fact that negated formulas are ‘special’ in intuitionistic logic in that each such formula is equivalent to its own double negation while this is not so for arbitrary formulas. Let us back up and give a clear explanation of the notion of specialness as well as a contrasting notion, in slightly more general terms; for definiteness only, we tailor the account to Set-Fmla. We also begin with the contrasting notion. Say that an n-ary relation R among the formulas of a language is universally representative according to a consequence relation on that language if for any formulas φ1,…,φn of the language, there are formulas ψ1,…,ψn, respectively synonymous with φ1,…,φn according to ⊢, with R(ψ1,…,ψn). (If n = 1, we speak instead of a universally representative class of formulas—a class of formulas such that every formula is synonymous with some formula in the class; likewise in the case of the notion special, defined below.) If ⊢ is congruential then we can replace “synonymous” in this definition with “equivalent” (i.e. such that φi ⊣⊢ ψi, for i = 1,…,n). Say that R is special according to ⊢ if there is some Set-Fmla sequent σ(p1,…, pn) constructed using not necessarily just the variables exhibited, for which for any formulas ψ1,…,ψn with R(ψ1,…,ψn), we have σ(ψ1,…,ψn) ∈ ⊢, while we do not have, for all formulas φ1,…,φn, σ(φ1,…,φn) ∈ ⊢. For substitution-invariant ⊢, this last condition can be simplified to: σ(p1,…, pn) ∉  ⊢.[36]  A consequence of these definitions is that no relation is both universally representative and special according to any given ⊢. A simple example of a special relation—according to more or less any ‘naturally occurring’ consequence relation with ∨ in its language is relation R obtaining between φ and ψ just in case ψ is a disjunction of which φ is a disjunct. Here take σ(p, q) as p ≻ q which is (e.g., in intuitionistic logic, though classical logic or any of many others would do as well) unprovable—i.e., not p ⊢I L q—while φ ⊢I L ψ for all φ, ψ for which R(φ, ψ). A more interesting example is the relation of being (intuitionistically) head-linked, i.e., that relation R such that for all φ, ψ, R(φ, ψ) if and only if: