showing that $(\lnot \lnot Q) \to Q$ is not an inutionistic tautology by using an ad hoc 3-valued logic?

Question

I'm trying to prove that $\lnot \lnot Q \to Q$ is not an intuitionistic tautology by constructing a special finitely-valued logic with strictly more tautologies than intuitonistic logic ... and then showing that that new logic rejects double negation elimination. Is this a valid proof technique?

In particular, there's a three-valued logic that accepts all the axioms of a specific axiomatization of intuitionistic logic (given below). Let's call it $L_3$ . In $L_3$ double negation elimination, i.e. $\lnot\lnot Q\to Q$ is not a tautology.

Can the existence of a logic whose tautologies are a strict superset of intuitionistic logic's tautologies be used to prove that a certain statement is a non-tautology in intuitionistic logic?

By plugging in all possible truth values for the metavariables in the axioms for intuitionistic logic, have I done enough work to show that $L_3$ "agrees" with intuitionistic logic in some sense?

Does it matter that $L_3$ has stray tautologies like triple negation elimination $\lnot\lnot\lnot Q \to Q$ ?

Let's write out the axioms of intuitionistic logic.

Then-1 $$ \phi \to (\chi \to \phi) $$ Then-2 $$ (\phi \to (\chi \to \psi)) \to ((\phi \to \chi) \to (\phi \to \psi)) $$ And-1 $$ (\phi \land \chi) \to \phi $$ And-2 $$ (\phi \land \chi) \to \chi $$ And-3 $$ \phi \to (\chi \to (\phi \land \chi)) $$ Or-1 $$ \phi \to (\phi \lor \chi) $$ Or-2 $$ \chi \to (\phi \lor \chi) $$ Or-3 $$ (\phi \to \psi) \to ((\chi \to \psi) \to ((\phi \lor \chi) \to \psi)) $$ EFQ $$ \bot \to \phi $$

The truth tables for our three-valued logic $L_3$ are as follows. The two designated truth values for our tautologies are $T$ and $U$ . Note that implication returns $U$ unless the right argument is $F$, in which case it cycles the three truth values.

AND               OR             IMP
      F  U  T         F  U  T         F  U  T
  (F) F  F  F     (F) F  U  T     (F) U  U  U
  (U) F  U  U     (U) U  U  T     (U) T  U  U
  (T) F  U  T     (T) T  T  T     (T) F  U  U

As we would hope, $Q \to (\lnot\lnot Q)$ is a tautology but $ (\lnot\lnot Q) \to Q $ is not.

Q→¬¬Q is a tautology, as in intuitionistic logic

T→¬¬T    F→¬¬F    U→¬¬U
T→ ¬F    F→ ¬U    U→ ¬T
T→  U    F→  T    U→  F
    U        U        T


¬¬Q→Q is not a tautology, as in intuitionistic logic
L3 is finitely valued, so we can examine all the cases

¬¬T→T    ¬¬F→F    ¬¬U→U
 ¬F→T     ¬U→F     ¬T→U
  U→T      T→F      F→U
    U        F        U

For reference, here is a Python program I used to check the intuitionistic axioms and a few example tautologies and non-tautologies.

import itertools as it

F = "F"
T = "T"
U = "U"

domain = (F, U, T)


def and_(a, b):
    ttab = {
        F : {F:F, U:F, T:F},
        U : {F:F, U:U, T:U},
        T : {F:F, U:U, T:T},
    }
    return ttab[a][b]


def or_(a, b):
    ttab = {
        F : {F:F, U:U, T:T},
        U : {F:U, U:U, T:T},
        T : {F:T, U:T, T:T},
    }
    return ttab[a][b]


def imp_(a, b):
    ttab = {
        F : {F:U, U:U, T:U},
        U : {F:T, U:U, T:U},
        T : {F:F, U:U, T:U},
    }
    return ttab[a][b]


def is_true(x):
    return x == T or x == U


def check_tautology(func, domain, args):
    counterexample = None
    for x in it.product(domain, repeat=args):
        if not is_true(func(*x)):
            counterexample = x
    if counterexample is not None:
        print(func.__name__, counterexample)
        assert False


def check_non_tautology(func, domain, args):
    counterexample = None
    for x in it.product(domain, repeat=args):
        if not is_true(func(*x)):
            counterexample = x
    if counterexample is None:
        print(func.__name__, "is unexpectedly a tautology")
        assert False


def then1(f, x):
    return imp_(f, imp_(x, f))


check_tautology(then1, domain, 2)


def then2(f, x, p):
    antecedent = imp_(f, imp_(x, p))
    consequent = imp_(imp_(f, x), imp_(f, p))
    return imp_(antecedent, consequent)


check_tautology(then2, domain, 3)


def and1(f, x):
    return imp_(and_(f, x), f)


check_tautology(and1, domain, 2)


def and2(f, x):
    return imp_(and_(f, x), x)


check_tautology(and2, domain, 2)


def and3(f, x):
    return imp_(f, imp_(x, and_(f, x)))


check_tautology(and3, domain, 2)


def or1(f, x):
    return imp_(f, or_(f, x))


check_tautology(or1, domain, 2)


def or2(f, x):
    return imp_(x, or_(f, x))


check_tautology(or2, domain, 2)


def or3(f, x, p):
    antecedent1 = imp_(f, p)
    antecedent2 = imp_(x, p)
    consequent = imp_(or_(f, x), p)
    return imp_(antecedent1, imp_(antecedent2, consequent))


check_tautology(or3, domain, 3)


def efq(x):
    return imp_(F, x)


check_tautology(efq, domain, 1)


# theorems and nontheorems

def double_negation_introduction(x):
    return imp_(x, imp_(imp_(x, F), F))

check_tautology(double_negation_introduction, domain, 1)

def double_negation_elimination_BAD(x):
    return imp_(imp_(imp_(x, F), F), x)

check_non_tautology(double_negation_elimination_BAD, domain, 1)

def contrapositive_introduction(x, p):
    antecedent = imp_(x, p)
    consequent = imp_(imp_(p, F), imp_(x, F))
    return imp_(antecedent, consequent)

check_tautology(contrapositive_introduction, domain, 2)

def contrapositive_elimination_BAD(x, p):
    consequent = imp_(x, p)
    antecedent = imp_(imp_(p, F), imp_(x, F))
    return imp_(antecedent, consequent)

check_non_tautology(contrapositive_elimination_BAD, domain, 2)