DEV Community

Brian Berns
Brian Berns

Posted on

Double negation in C#

Let's take a look at another interesting aspect of the Curry-Howard correspondence using C#.

"Either" type

First, there's something new we need to introduce: the Either<A, B> type. This is a class with a simple purpose: to hold an instance of either type A or type B. Either is actually very useful to have in your programming toolbox (see details here), but for now we're only interested in the role it plays in the C-H correspondence:

English Logic Type
A and B A ∧ B Tuple<A, B>
A or B A ∨ B Either<A, B>

As you can see, Tuple represents logical "and" and our new Either type represents logical "or" (symbolized by ). For example, an instance of, say, Tuple<int, string> holds proof of both int and string, while an instance of Either<int, string> holds proof of int or string.1

OK, now that we know about Either<A, B>, we're ready to put it to use.

Law of excluded middle

In classical logic, it's valid to assume that either A is true or ¬A is true:

A ∨ ¬A
Enter fullscreen mode Exit fullscreen mode

This is called the law of excluded middle. In English, we can read this as "either A is true or A is false", for any proposition A, which seems intuitive enough. Even if we're not yet sure whether a given proposition is actually true or actually false, those are the only two possibilities, so we know one of them must be correct, right? We should be able to convert this law to types using C-H. Let's try:

/// A ∨ ¬A
public static Either<A, Not<A>> ExcludedMiddle<A>()
{
    // implementation?
}
Enter fullscreen mode Exit fullscreen mode

We've represented the law of excluded middle itself as the concrete type Either<A, Not<A>>. If this law is true, we should be able to prove it by creating an instance of this type. Either has two constructors: one that takes an instance of A and another that takes an instance of Not<A>. But we don't yet have proof of A or Not<A> to work with, so how can we call one of Either's constructors?

The answer is: We can't. Which means that the kind of logic we can represent with types is actually not the same as classical logic. The logic of the C-H correspondence is called "constructive" or "intuitionistic". Constructive logic is a more limited, skeptical form of logic than classical logic. Without solid proof of either A or Not<A>, we can't make the leap to showing that one of them must be true.2

Double negation

In classical logic, it's easy to prove that two negations cancel out:

¬¬A → A
Enter fullscreen mode Exit fullscreen mode

In English, if we know that A is not false, then it must be true (because it has to be one or the other). But this proof depends on the law of excluded middle! In constructive logic, we can't prove A merely by knowing that it is not false:

/// ¬¬A → A
A RemoveDoubleNegative<A>(Not<Not<A>> proof_of_not_not_A)
{
    // can't be implemented
}
Enter fullscreen mode Exit fullscreen mode

OK, so if we can't remove a double negative, can we create a double negative? Logically, the proposition is:

A → ¬¬A
Enter fullscreen mode Exit fullscreen mode

Yes, we can prove this constructively:

/// A → ¬¬A
public static Not<Not<A>> CreateDoubleNegative<A>(A proof_of_A)
{
    Absurd not_A_implies_absurd(Not<A> not_A)
        => not_A.Apply(proof_of_A);
    return new Not<Not<A>>(not_A_implies_absurd);
}
Enter fullscreen mode Exit fullscreen mode

It looks complicated, but it just says that if we know A is true, then we know that "not A" is false, so "not (not A)" is true.

Of course, because of the C-H correspondence, this is not just a proof of A → ¬¬A, but also a valid, usable C# function. What happens if we actually use it in a C# program? For example:

Not<Not<int>> proof_of_not_not_int = CreateDoubleNegative(5);
Enter fullscreen mode Exit fullscreen mode

Well, that's interesting. We've created an instance of Not<Not<int>> from the integer 5. What can we do with such a value?

I'll pause here for now and let you ponder that question before we take it up again in the next installment. Thanks for following!


  1. You can think of the arguments to a function as being a tuple. We've been using this to avoid explicit tuples when representing logical "and" so far. For example, the arguments to ModusPonens are (A_implies_B, proof_of_A), which you can look at as two separate arguments, or as a single argument of type Tuple<Func<A, B>, A>. Either way, the arguments correspond to (A → B) ∧ A logically. 

  2. Of course, we could just take the law of excluded middle as an axiom, as though an instance of Either<A, Not<A>> is passed to us via the program's Main function. In that case, the logic of the C-H correspondence would match classical logic. But that's not as much fun. 

Top comments (8)

Collapse
 
daniel13rady profile image
Daniel Brady

@shimmer I see you are transcribing logical relations into C#. If you're not already familiar, you might be interested in playing around with languages that embrace a logical and/or relational programming paradigm! 😄 checkout miniKanren or Prolog

Collapse
 
integerman profile image
Matt Eland

I think the point of this is more towards proving what C# can do from a functional and logical perspective rather than establishing it as the best language for doing these things.

Collapse
 
daniel13rady profile image
Daniel Brady

Oh yes, that was my take-away as well👍 It just made me think of some things I thought OP (and their readers) might be interested in 🙂

Collapse
 
daniel13rady profile image
Daniel Brady • Edited

I also highly recommend Daniel P. Friedman's book The Little Prover 📚

Collapse
 
integerman profile image
Matt Eland

This is a very interesting article. I'm not sure I fully buy that tuple is always and, but I see where you're going with it.

Collapse
 
shimmer profile image
Brian Berns

Thanks, glad you're enjoying it. I'm interested in your thoughts on tuples corresponding to logical "and". Can you describe what doesn't seem right about it?

Collapse
 
integerman profile image
Matt Eland

When I think of a tuple, I think more of "a small record" than "two things that are true together". I can definitely squint to see it, but I almost wonder if a new And type would be clearer to match the Either type.

Thread Thread
 
shimmer profile image
Brian Berns • Edited

I see. It turns out that a custom And type would be a small record as well - exactly the same shape as Tuple but with different names (i.e. the two types are "isomorphic").

Here's Tuple<T1, T2> from the .NET source code:

public class Tuple<T1, T2> : ... {

    private readonly T1 m_Item1;
    private readonly T2 m_Item2;

    public T1 Item1 { get { return m_Item1; } }
    public T2 Item2 { get { return m_Item2; } }

    public Tuple(T1 item1, T2 item2)
    {
        m_Item1 = item1;
        m_Item2 = item2;
    }

    ...

And here's a custom And type:

public class And<A, B> : ... {

    private readonly A _proof_of_A;
    private readonly B _proof_of_B;

    public A ProofOfA { get { return _proof_of_A; } }
    public B ProofOfB { get { return _proof_of_B; } }

    public And(A proof_of_A, B proof_of_B)
    {
        _proof_of_A = proof_of_A;
        _proof_of_B = proof_of_B;
    }

    ...

Usage:

var modus_ponens_input_tuple = new Tuple(A_implies_B, proof_of_A);
var modus_ponens_input_custom = new And(A_implies_B, proof_of_A);