Vrftsjtryk

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. $lnotlnot Qto 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 $lnotlnotlnot 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 (lnotlnot Q)$ is a tautology but $ (lnotlnot 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)