>>14156270Hm that's interesting. Let Sigma be the set of strings over some alphabet containing a NOT character. Let L be a language over these strings, and we say that x is in the language if and only if x and NOT x are in the language (assume NOT NOT x is x). So if you have a list of axioms all axioms would come in pairs, Axiom 1 and NOT Axiom1, Axiom 2 and NOT Axiom 2, and so on. You have a few options for derivation rules. Ultimately you want to say that if x is derivable from the axioms then so is NOT x. That means provable statements imply the existence of a dual proof that proves the negation of the statement.
Trivial example just to show such a system exists:
alphabet = {'NOT', 'x'}
Language = {'x', 'NOT x'}
derivation rules = {} (empty set)
