(NB: These proofs and more can be found here, with instructions on how to run Python’s type-checker. Feel free to follow along by type-checking some proofs.)

In Python, type annotations are optional and ignored. Here’s a funny tweet that illustrates the point:

So, it may be surprising that Python’s type system is rich enough and descriptive enough for (some) propositional logic theorem proving.

I will demonstrate that Python’s type system is sufficient for formalizing and checking constructive propositional logic via the Curry-Howard correspondence and the BHK interpretation of intuitionistic logic.

In particular, I will derive modus ponens, contrapositive, and modus tollens in Python’s type system. I will also provide an interpretation of Python’s pass and raise statements and show how they are akin to admit in a traditional theorem prover. More proofs can be found here.

A Quick Primer to Python’s Type System

With mypy and PEP 484, type annotations are possible in Python and can even be statically checked before runtime. Let’s go over some of the basics of Python’s type system before we try to construct a propositional logic checker.

Python has several primitive types, such as:

some_integer: int = 42
some_float: float = 3.14

There are also type unions:

some_float_or_integer: Union[int, float] = 0

All of which can be used to annotate functions:

def multiply(a: int, b:int) -> int:
    return a*b

More interestingly, Python also has Callable, which can be used to construct higher-order types like so:

def multiply_alt(a: int) -> Callable[[int], int]:
    def partially_applied_multiply(b: int) -> int:
        return a * b

    return partially_applied_multiply

which we can apply to produce

result: int = multiply_alt(3)(5)

More importantly, Python has type variables:

A = TypeVar("A")

(this declares an unrestricted type variable A that can be any type)

For the rest of this post, assume that any capital letter (e.g. A, B, C, P, Q, R) represents an unrestricted type variable.

Implementing Basic Inference Rules

Under the BHK interpretation, logical implication from P to Q can be thought of as a function that takes a proof of P and transforms it to a proof of Q. If we can prove that such a function exists, then we know that given any proof of P, we can create a proof of Q. In other words, the existence of such a function proves that “p implies q” is true.

In Python, we can think of such a function like so:

p_implies_q: Callable[[P], Q]

If there is a function that can map type variable P to type variable Q, then if there exists an implementation for type variable P, we can trivally produce an implementation of type variable Q. This is because the function p_implies_q can be combined with an implementation of P to produce an implementation of Q via function application. The relationship between implementations like p_implies_q and logical truth is the essence of the Curry-Howard correspondence.

Perhaps the most basic rule to encode is modus ponens, which are arguments of the form:

  • P implies Q
  • P

then:

  • Q

So, what we want is a proof (aka function) that takes in a statement “P implies Q” and “P” and spits out an object of type Q.

Modus Ponens Proof
def modus_ponens(p: P, p_implies_q: Callable[[P], Q]) -> Q:
    return p_implies_q(p)

Does this type-check in Python? Yes!

Trying to Prove Falsity (and failing!)

A good proof system should not prove falsity. So, let’s try to prove something obviously false

def every_proposition_is_true() -> P:
    return None

If this were true, then every proposition in our logic would be true. Thankfully, this does not type-check. Look at that beautiful failure!

error: Incompatible return value type (got "None", expected "P")
Found 1 error in 1 file (checked 1 source file)

More logical inference rules

Let’s try to prove something a bit more complex than modus ponens. In the BHK interpretation of logic, not P (the negation of P) is interpreted as a proof from P to absurdity. In other words, not P is a function from P to the unimplementable type. So, a negation of P in Python’s type system would look like:

not_p: Callable[[P], NotImplementedType]

If we want to prove the contrapositive rule, then we need to transform a proof of:

p_implies_q: Callable[[P], Q]
not_q: Callable[[Q], NotImplementedType])

into:

not_p: Callable[[P], NotImplementedType]
Proof of the Contrapositive
def contrapositive(
    p_implies_q: Callable[[P], Q]
) -> Callable[[Callable[[Q], NotImplementedType]], Callable[[P], NotImplementedType]]:
    def transform_proof_of_not_q(
        not_q: Callable[[Q], NotImplementedType]
    ) -> Callable[[P], NotImplementedType]:
        def proof_not_p(P) -> NotImplementedType:
            return not_q(p_implies_q(P))

        return proof_not_p

    return transform_proof_of_not_q

This function can be translated as:

If I have a proof from P to Q, and if you have a proof from Q to absurdity, I have a proof from P to absurdity.

Cool, right?

We can now derive other cool inference rules, like modus tollens.

Modus Tollens Proof
def modus_tollens(
    p_implies_q: Callable[[P], Q], not_q: Callable[[Q], NotImplementedType]
) -> Callable[[P], NotImplementedType]:
    """
    Given:
        - P -> Q
        - not Q
    then:
        - not P
    for any statements P, Q.
    """
    return contrapositive(p_implies_q)(not_q)

We can also show that logical implication is transitive (if A implies B and B implies C, then A implies C).

Transitive Implication Proof
def transitive_implication(
    f: Callable[[A], B], g: Callable[[B], C]
) -> Callable[[A], C]:
    """
    Given:
        - A->B
        - B->C
    then:
        A->C
    for any statements A, B, C.
    """

    def a_implies_c(a: A) -> C:
        return g(f(a))

    return a_implies_c

Wild, huh?

Admitting axioms

Sometimes, when using a theorem prover, we’d like to admit certain theorems that we know to be true but are not built into the Python type checker (or are too lazy to prove). Turns out Python’s type system can have axioms!

In Python, we are allowed to add type stubs. That is, type annotations for functions that we do not have the implementation for. So, we can use type stubs to introduce axioms that we cannot implement in Python, but that we know to be logically valid.

For example, this was my proof for the contrapositive rule before I figured out how to derive it:

def lazy_contrapositive(
    p_implies_q: Callable[[P], Q]
) -> Callable[[Callable[[Q], NotImplementedType]], Callable[[P], NotImplementedType]]:

In addition to ignoring the implementation of type stubs, mypy will also ignore stop type checking a function if the pass or raise keywords are used. This allows us to use pass or raise to admit parts of a proof that we do not have an implementation for.

Of course, the principle of explosion applies in Python’s type system, so be careful to not admit unnecessary axioms!

Conclusion

This simple demonstration shows that Python’s type system can be (abused? hacked? broken?) into a crude and probably unsound propositional logic checker. Although Python’s type system is not as rich as Coq or Agda et al., it is sufficient to derive the natural deduction inference rules and prove statements in propositional logic. This is also an excellent demonstration of the Curry-Howard correspondence at work!

You can see some other proofs in Python’s type system in this repo here: https://github.com/InnovativeInventor/hack-python-types/

If you liked this post, let me know!