## DEV Community is a community of 862,249 amazing developers

We're a place where coders share, stay up-to-date and grow their careers.

# 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
``````

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?
}
``````

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
``````

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
}
``````

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

``````A → ¬¬A
``````

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);
}
``````

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);
``````

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.

## Discussion (8) @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 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. 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 🙂 I also highly recommend Daniel P. Friedman's book The Little Prover 📚 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. 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? 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. Brian Berns • Edited on

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> : ... {

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> : ... {

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);
``````