Hm, maybe we can formulate this using just the intuinistic provability judgement. We associate each formula A with a formula〈A〉which is the type of refutations of A, such that A is disprovable if 〈A〉is (intuinistically) provable. The cases you give for ∧,∨,∃,∀, True and False become

〈A∧B〉= 〈A〉∨〈B〉

〈A∨B〉= 〈A〉∧〈B〉

〈∃ (x:A).B〉= ∀(x:A).〈B〉

〈∀ (x:A).B〉= ∃(x:A).〈B〉

〈True〉= False

〈False〉= True

and we can indeed see that this is "dual" in the sense that 〈〈A〉〉= A.

The domain of the ∀ and ∃ cases is interesting. If we are using just first-order logic it can be omitted, but in higher-order logic and Type Theory we want to say if we are quantifying over individuals, relations, etc. I think the translation of e.g. ∀ (x:A).B makes sense: in order to disprove that we should give a concrete (intuinistically acceptable) construction of an element x that causes it to fail, so we stay in "construct a proof" mode for the A.

But now we have already defined the translation of implication! Using the standard type theory trick to encode A→B as ∀ (x:A).B, where x is a fresh variable not free in B, we get

〈A→B 〉= 〈∀(x:A).B〉=∃ (x:A).〈B〉= A×〈B〉

a pair of a proof of A and a disproof of B. This seems related to your "but not" operator, except here it mixes the logical symbol × and the syntactic operation 〈〉. Similarly the translation of not becomes just

〈not A〉=〈A→False 〉= A × True ~= A

So this basically just the not operator in disguise. The "dualizing translation" in the paper you linked does indeed use a but-not symbol, I guess I should go and read that paper...