Characterizing N-validities

One of the key theorems of our first paper on N was the theorem characterizing valid implications:

Theorem 3: Every N-valid implication φ->ψ satisfies one of the following three conditions:

1. φ is atomic.
2. φ is negated.
3. ψ is N-valid.

Last week I spent some time trying to come up with similar characterizations of validities of other types, that is, characterizations of N-valid atoms, negations, disjunctions, and conjunctions. Three of the four are easy:

• No atom is N-valid [Lemma 2].
• The only N-valid negations are double negations of validities [Theorem 4].
• A conjunct is N-valid iff each conjunct is N-valid [obvious].

So, can we characterize disjunctions? Suppose φVψ is N-valid. There are three cases:

1. Either φ is N-valid or ψ is N-valid.
2. Neither disjunct is N-valid, and neither contains any implication.
3. Neither disjunct is N-valid, but at least one contains an implication.

In the first case, nothing more is needed. For the other two, I have a

Conjecture: (2) At least one atom occurs at least twice in the formula, once with an odd number of negations and once with an even number of negations. NOTE: I do not mean occurs "within the scope of an odd/even number of negations" (as you would find in classical logic) but that attached to the atom itself are an odd or even number (0, of course, being an even number). (3) At least one atom occurs both in the antecedent of a conditional and in either the consequent of a conditional or as a stand alone atomic subformula. (If we wanted a more felicitous phrasing, we could say that an atom is the consequent of a trivial conditional, and then say: "at least one atom occurs in both the antecedent and the consequent of a conditional". But Jesse found this problematic.)

Now we have the following open problem: Prove the conjecture, or find a counterexample.