Double negation in C#
Tags: csharp, dotnet, logic, functional
Published: 2020-01-26 21:16:16


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](https://mikhail.io/2016/01/validation-with-either-data-type-in-csharp/)), 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:

```csharp
/// 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:

```csharp
/// ¬¬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:

```csharp
/// 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:

```csharp
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`](https://dev.to/shimmer/the-curry-howard-correspondence-3obh) 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.