Logical Connectives

Propositions as types — the Curry-Howard correspondence in Python.

The Curry-Howard Correspondence

The Curry-Howard correspondence is the discovery that propositions in logic correspond to types in programming, and proofs correspond to programs. Deppy makes this correspondence concrete in Python:

Setup

from __future__ import annotations
from dataclasses import dataclass
from typing import TypeVar, Generic, Callable, Union, NoReturn
from deppy import guarantee, check
from deppy.types import Empty, Unit, Sigma

A = TypeVar('A')
B = TypeVar('B')
C = TypeVar('C')

Truth and Falsehood

# True = Unit — the type with exactly one inhabitant
@dataclass(frozen=True)
class Unit:
    """The trivially true proposition."""
    pass

trivially_true: Unit = Unit()  # a proof of True

# False = Empty — the type with NO inhabitants
class Empty:
    """The absurd proposition — cannot be constructed."""
    def __init__(self):
        raise TypeError("Empty has no constructors")

# From False, anything follows (ex falso quodlibet)
@guarantee("from absurdity, derive anything")
def absurd(e: Empty) -> A:
    """If you have a proof of False, you can prove anything."""
    raise RuntimeError("unreachable")  # can never be called

Conjunction (And)

A proof of A ∧ B is a pair: a proof of A and a proof of B.

@dataclass(frozen=True)
class And(Generic[A, B]):
    """Conjunction: A ∧ B"""
    left:  A  # proof of A
    right: B  # proof of B

# Introduction: to prove A ∧ B, provide proofs of both
@guarantee("conjunction introduction")
def and_intro(a: A, b: B) -> And[A, B]:
    return And(a, b)

# Elimination: from A ∧ B, extract either component
@guarantee("conjunction elimination (left)")
def and_left(p: And[A, B]) -> A:
    return p.left

@guarantee("conjunction elimination (right)")
def and_right(p: And[A, B]) -> B:
    return p.right

# Theorem: A ∧ B → B ∧ A  (commutativity)
@guarantee("and is commutative")
def and_comm(p: And[A, B]) -> And[B, A]:
    return And(p.right, p.left)

Z3_VERIFIED — and_comm verified

Disjunction (Or)

A proof of A ∨ B is a tagged value: either a proof of A or a proof of B (but you must say which).

@dataclass(frozen=True)
class Inl(Generic[A]):
    """Left injection: proof of A"""
    value: A

@dataclass(frozen=True)
class Inr(Generic[B]):
    """Right injection: proof of B"""
    value: B

Or = Union[Inl[A], Inr[B]]

# Introduction
def or_left(a: A) -> Or[A, B]:
    return Inl(a)

def or_right(b: B) -> Or[A, B]:
    return Inr(b)

# Elimination: case analysis
@guarantee("disjunction elimination")
def or_elim(
    p: Or[A, B],
    on_left:  Callable[[A], C],
    on_right: Callable[[B], C],
) -> C:
    match p:
        case Inl(a): return on_left(a)
        case Inr(b): return on_right(b)

# Theorem: A ∨ B → B ∨ A  (commutativity)
@guarantee("or is commutative")
def or_comm(p: Or[A, B]) -> Or[B, A]:
    return or_elim(
        p,
        on_left=lambda a: or_right(a),
        on_right=lambda b: or_left(b),
    )

Implication (Functions)

A proof of A → B is a function that transforms any proof of A into a proof of B. This is the most natural connective in Python!

# A → B is just Callable[[A], B]
# A proof of A → B is any function f : A → B

# Modus ponens: if A → B and A, then B
@guarantee("modus ponens")
def modus_ponens(
    f: Callable[[A], B],
    a: A,
) -> B:
    return f(a)

# Hypothetical syllogism: (A → B) → (B → C) → (A → C)
@guarantee("implication is transitive")
def syllogism(
    f: Callable[[A], B],
    g: Callable[[B], C],
) -> Callable[[A], C]:
    return lambda a: g(f(a))

Negation

¬A is defined as A → Empty: a function that, given a proof of A, produces a contradiction.

# ¬A  =  A → Empty  =  Callable[[A], Empty]
Not = Callable[[A], Empty]

# Theorem: A → ¬¬A  (double negation introduction)
@guarantee("double negation introduction")
def double_neg_intro(a: A) -> Callable[[Callable[[A], Empty]], Empty]:
    """Given a, if someone gives us ¬A, we derive ⊥."""
    return lambda not_a: not_a(a)

# Theorem: (A → B) → (¬B → ¬A)  (contraposition)
@guarantee("contraposition")
def contrapositive(
    f: Callable[[A], B],
) -> Callable[[Callable[[B], Empty]], Callable[[A], Empty]]:
    return lambda not_b: lambda a: not_b(f(a))

Universal Quantification (Forall)

∀x:A. P(x) is a dependent function type: a function that, for any x : A, produces a proof of P(x).

# ∀ n : int, n + 0 == n
@guarantee("n + 0 equals n for all integers")
def plus_zero(n: int) -> PathType[int, "n + 0", "n"]:
    return Refl(n)  # Z3 discharges: n + 0 == n  ✅

Existential Quantification (Exists)

∃x:A. P(x) is a dependent pair: a witness x together with a proof that P(x) holds.

@dataclass(frozen=True)
class Exists(Generic[A, B]):
    """Dependent pair: witness + proof."""
    witness: A
    proof:   B

# ∃ n : int, n * n == 144
@guarantee("there exists an int whose square is 144")
def sqrt_144() -> Exists[int, PathType[int, "n*n", "144"]]:
    return Exists(
        witness=12,
        proof=Refl(144)  # Z3 checks: 12 * 12 == 144  ✅
    )

Classical vs Constructive Logic

Deppy is constructive by default. Some classical principles are not provable without additional axioms:

from deppy.classical import lem, classical

# Law of Excluded Middle — available as an axiom
@guarantee("A or not A (classical axiom)")
def excluded_middle() -> Or[A, Callable[[A], Empty]]:
    return lem(A)  # axiomatically assumed

De Morgan's Laws

# De Morgan 1: ¬(A ∨ B) → ¬A ∧ ¬B  (constructively valid)
@guarantee("de Morgan 1")
def de_morgan_1(
    p: Callable[[Or[A, B]], Empty]
) -> And[Callable[[A], Empty], Callable[[B], Empty]]:
    not_a = lambda a: p(Inl(a))
    not_b = lambda b: p(Inr(b))
    return And(not_a, not_b)

# De Morgan 2: ¬A ∧ ¬B → ¬(A ∨ B)  (constructively valid)
@guarantee("de Morgan 2")
def de_morgan_2(
    p: And[Callable[[A], Empty], Callable[[B], Empty]]
) -> Callable[[Or[A, B]], Empty]:
    def refute(ab: Or[A, B]) -> Empty:
        match ab:
            case Inl(a): return p.left(a)
            case Inr(b): return p.right(b)
    return refute

# De Morgan 3: ¬(A ∧ B) → ¬A ∨ ¬B  (REQUIRES LEM)
@guarantee("de Morgan 3 (classical)")
def de_morgan_3(
    p: Callable[[And[A, B]], Empty]
) -> Or[Callable[[A], Empty], Callable[[B], Empty]]:
    # Need LEM to decide which side to negate
    match lem(A):
        case Inl(a):
            # A holds, so ¬B
            return Inr(lambda b: p(And(a, b)))
        case Inr(not_a):
            return Inl(not_a)

Exercises