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...
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...