ナビゲーションに移動 検索に移動

The Curry-Howard isomorphism is a striking relationship connecting two seemingly unrelated areas of mathematics — type theory and structural logic.

カリー=ハワード同型は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。

## Introduction 導入

The Curry-Howard isomorphism, hereafter referred to as simply C-H, tells us that in order to prove any mathematical theorem, all we have to do is construct a certain type which reflects the nature of that theorem, then find a value that has that type. This seems extremely weird at first: what do types have to do with theorems? However, as we shall see, the two are very closely related. A quick note before we begin: for these introductory paragraphs, we ignore the existence of expressions like error and undefined whose denotational semantics are ⊥. These have an extremely important role, but we will consider them separately in due time. We also ignore functions that bypass the type system like unsafeCoerce#.

これよりカリー=ハワード同型は単に C-H と表記する。定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということをC-H が示している。これは最初は極めて不思議に思える。型と定理にどんな関係があるというのだろうか？しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。はじめる前に簡単に注意しておくが、導入の章では errorundefinedのような 表示的意味論 が ⊥ である式の存在は無視する。これらはとても重要な役割を果たすのだが、これらについては後ほど別に考えることにする。また、unsafeCoerce#のような型システムを迂回する関数についても無視することにする。

We can build incredibly complicated types using Haskell's higher-order functions feature. We might want to ask the question: given an arbitrary type, under what conditions does there exist a value with that type (we say the type is inhabited)? A first guess might be 'all the time', but this quickly breaks down under examples. For example, there is no function with type a -> b, because we have no way of turning something of type a into something of a completely different type b (unless we know in advance which types a and b are, in which case we're talking about a monomorphic function, such as ord :: Char -> Int).

Haskellの高階関数の機能を使えばとても複雑な型を構築することができる。次のような質問をしてみるといい。すべての型は少なくともひとつは値が存在する(このような型を空でない集合(inhabited)という)だろうか？最初は「どんな型でもそうだ」と思うかもしれないが、次の例はあっさりとその直感を打ち砕く。たとえば、なんらかの型aの値をまったく別の型 b の値に変換する方法は存在しないので(あらかじめ abを知っており ord :: Char -> Intのような単相関数について述べているのでない限り)、型a -> bをもつ関数は存在しない。

Incredibly, it turns out that a type is only inhabited when it corresponds to a true theorem in mathematical logic. But what is the nature of this correspondence? What does a type like a -> b mean in the context of logic?

### A crash course in formal logic 形式論理最速入門

We need some background on formal logic before we can begin to explore its relationship to type theory. This is a very brief introduction; for a wider grounding we recommend you consult an introductory textbook on the subject matter.

In everyday language we use a lot of 'If... then...' sentences. For example, 'If the weather is nice today, then we'll walk into town'. These kinds of statements also crop up in mathematics; we can say things like 'If x is positive, then it has a (real) square root'. Formal logic is a way of translating these statements from loose, woolly, ambiguous English into precise symbolism. We use the → sign (read as 'implies') to indicate that something is true if something else is true. For example, our earlier statement could be recast as 'The weather is nice today → we'll walk into town', which means that it is true that we'll walk into town if it is true that the weather is nice, which is just the same as the 'If... then...' version we used earlier. We'll often use letters to stand for entire statements, so for example if W is the statement 'the weather is nice', and T is the statement 'we'll walk into town', then our example becomes simply WT.

Notice the crafty way we phrased our definition of →. PQ means that if P is true, then Q is true. But if Q is some statement that is always true, no matter what the circumstances — like 'the sun is hot' — then it doesn't matter what P is. P could even be a false statement, Q would still be true if P were true, so PQ would still hold. The fact that Q would be true if P isn't true is a whole different matter; we're not asking that question when we say PQ. So → doesn't really represent any kind of cause-effect relationship; things like 'the sky is pink → the sun is hot' are still valid statements. [1]

Other things that crop up lots in both everyday language and mathematics are things called conjunctions and disjunctions. The former represent statements involving an 'and', the latter statements involving an 'or'. We could represent the statement 'I will buy this magazine if it's in stock and I have enough money' by the symbolism ${\displaystyle (M\wedge S)\to B}$, where M = 'I have enough money', S = 'The magazine is in stock', B = 'I will buy the magazine'. Essentially, one can just read the symbol ${\displaystyle \wedge }$ as 'and'. Similarly, one can read the symbol ${\displaystyle \vee }$ as 'or', so that the statement 'I will either walk or get the train to work' could be represented as ${\displaystyle W\vee T}$, where W = 'I will walk to work', and T = 'I will get the train to work'.

Using these symbols, and a few more which will be introduced as we go, we can produce arbitrarily complicated symbol strings. There are two classes of these symbol strings: those that represent true statements, often called the theorems; and those which represent false statements, called the nontheorems. Note that whether a symbol string is a theorem or nontheorem depends on what the letters stand for, so ${\displaystyle P\vee Q}$ is a theorem if, for example, P represents the statement 'It is daytime' and Q represents the statement 'It is night time' (ignoring exceptions like twilight), but it would be a nontheorem if P were 'Trees are blue' and Q were 'All birds can fly'. We'll often call a symbol string a proposition if we don't know whether it's a theorem or not.

これらの記号とこれから紹介する幾つかのものを使い、任意の複雑な記号列を生成することができる。これらの記号列は、定理(theorems)と呼ばれることもある真の主張と、非定理(nontheorems)と呼ばれることがある偽の主張の二種類に分類できる。あらゆる記号列はその文字が表しているものに従って定理か非定理のどちらかになることに注意すると、例えば、もし P が「昼間である」という文章を表し、Qが「夜である」という文章を表すなら、(夕方のような例外を除けば)${\displaystyle P\vee Q}$ は定理であるが、もしPが「木は青い」でQは「すべての鳥は飛ぶことができる」ならこれは非定理となる。定理かどうかわからない記号列は、命題と呼ぶこともある。

There are many more subtleties to the subject of logic (including the fact that when we say 'If you eat your dinner you'll get dessert' we actually mean 'If and only if you eat your dinner will you get dessert'). If this is a subject that interests you, there are many textbooks around that comprehensively cover the subject.

(「もしあなたが夕食を食べるのなら、その時に限りデザートを食べるだろう」という意味で「もしあなたが夕食を食べるならデザートも食べるだろう」というときのように)論理にはもっと多くの微妙な話題が存在する。もしこれらの話題に興味があるなら、これらの話題を包括的にあつかう多くの教科書がある。

### Propositions are types 定理と型

So, given a type a -> b, what does that mean in terms of symbolistic logic? Handily, it simply means that ab. Of course, this only makes sense if a and b are types which can further be interpreted in our symbolistic logic. This is the essence of C-H. Furthermore, as we mentioned before, ab is a theorem if and only if a -> b is an inhabited type.

それでは、形式論理においては型 a -> b は何を意味するのだろうか？簡単なことに、単にabを意味しているのだ。もちろん、これはabが形式理論において解釈可能な型であるときだけ成り立っている。これは C-H の本質である。また、先程述べたように、a -> b が空でない型であるとき、その時に限り abは定理となる。

Let's see this using one of the simplest of Haskell functions. const has the type a -> b -> a. Translated into logic, we have that aba. This must be a theorem, as the type a -> b -> a is inhabited by the value const. Now, another way of expressing ab is that 'If we assume a is true, then b must be true.' So aba means that if we assume a is true, then if we further assume that b is true, then we can conclude a. This is of course a theorem; we assumed a, so a is true under our assumptions.

もっとも単純な Haskell 関数のひとつを使ってみていこう。consta -> b -> a　という型を持つ。形式論理ではabaとなる。値constがあるので、これは型 a -> b -> a が空ではなく、定理であることは間違いない。いま、abは「もしa が真だとすれば、b は真である」の別の表現なのである。したがって、aba は「もしaが真であり、もしbが真であるなら、aは真であると結論できることを意味する。aが真であると仮定するなら、仮定によりaが真であるから、これはもちろん定理である。

### The problem with ⊥ ⊥にまつわる問題

We've mentioned that a type corresponds to a theorem if that type is inhabited. However, in Haskell, every type is inhabited by the value undefined. Indeed, more generally, anything with type forall a. a, a value with denotational semantics of ⊥, is a problem. ⊥ in type theory corresponds to inconsistency in logic; we can prove any theorem using Haskell types because every type is inhabited. Therefore, Haskell's type system actually corresponds to an inconsistent logic system. However, if we work with a limited subset of Haskell's type system, and in particular disallow polymorphic types, we have a consistent logic system we can do some cool stuff in. Hereafter it is assumed we are working in such a type system.

Now that we have the basics of C-H, we can begin to unpack a little more the relationship between types and propositions.

これで C-H の基礎を身に着けたので、型と命題の関係をさらに解き明かすのを始めることができるようになった。

## Logical operations and their equivalents 論理演算と等価なもの

The essence of symbolic logic is a set of propositions, such as P and Q, and different ways of combining these propositions such as QP or ${\displaystyle P\vee Q}$. These ways of combining propositions can be thought of as operations on propositions. By C-H, propositions correspond to types, so we should have that the C-H equivalents of these proposition combinators are type operations, more normally known as type constructors. We've already seen an example of this: the implication operator → in logic corresponds to the type constructor (->). The rest of this section proceeds to explore the rest of the proposition combinators and explain their correspondence.

### Conjunction and Disjunction 論理積と論理和

In order for ${\displaystyle A\wedge B}$ to be a theorem, both A and B must be theorems. So a proof for ${\displaystyle A\wedge B}$ amounts to proving both A and B. Remember that to prove a proposition A we find a value of type A, where A and A are C-H correspondents. So in this instance we wish to find a value that contains two sub-values: the first whose type corresponds to A, and the second whose type corresponds to B. This sounds remarkably like a pair. Indeed, we represent the symbol string ${\displaystyle A\wedge B}$ by (a, b), where a corresponds to A and b corresponds to B.

${\displaystyle A\wedge B}$が定理となるためには、AB の両方は定理でなければならない。よって、${\displaystyle A\wedge B}$ の証明はABの両方を証明することに等しい。型Aの値を見つけることが 命題 A の証明であることを思い出そう。ここで AA は C-H 対応している。ゆえに、この場合、最初のAと一致する型と２つ目のBと一致する型の、従属する２つの値含む値を見つけたいということになる。これは実にペアに似ているように思える。実際に、記号列${\displaystyle A\wedge B}$(a, b)と表現する。ここでaA に、bBに相当する。

Disjunction is opposite to conjunction. In order for ${\displaystyle A\vee B}$ to be a theorem, either A or B must be a theorem. Again, we search for a value which contains either a value of type A or a value of type B. This is Either. Either A B is the type which corresponds to the proposition ${\displaystyle A\vee B}$.

### Falsity 偽

It is occasionally useful to represent a false statement in our logic system. By definition, a false statement is one that can't be proven. So we're looking for a type which isn't inhabited. Although none of these types exist in the default libraries (don't get confused with the () type, which has precisely one value), we can define one, if we turn on the -XEmptyDataDecls flag in GHC:

data Void


The effect of omitting the constructors means that Void is an uninhabited type. So the Void type corresponds to a nontheorem in our logic. There are a few handy corollaries here:

1. (Void, A) and (A, Void) are both uninhabited types for any type A, corresponding to the fact that ${\displaystyle F\wedge A}$ and ${\displaystyle A\wedge F}$ are both nontheorems if F is a nontheorem. どんな型Aについても、(Void, A)(A, Void) はどちらも空である型であり、もしFが非定理なら ${\displaystyle F\wedge A}$${\displaystyle A\wedge F}$ はどちらも非定理であるという事実と対応する。
2. Either Void A and Either A Void are essentially the same as A for any type A, [3] corresponding to the fact that ${\displaystyle F\vee A}$ and ${\displaystyle A\vee F}$, where F is a nontheorem, are theorems only if A is a theorem. どんな型Aについても、Either Void AEither A Void は本質的に A と同じであり、[4] Fが非定理で A が定理であるとき、${\displaystyle F\vee A}$${\displaystyle A\vee F}$が真であるという事実と対応する。
3. Any type that corresponds to a nontheorem can be replaced with Void. This is because any nontheorem-type must be uninhabited, so replacing it with Void everywhere doesn't change anything. Void is really equivalent to any nontheorem type[5]. 非定理と対応するどんな型もVoidに置き換えることができる。これはどんな非定理型も空であるからで、ゆえになにも変更せずともVoidに置き換えることができるのである。Void は実際にどんな非定理型とも等価である[6].
4. As we remarked in the first section, the implication PQ is true if Q is true, regardless of the truth value of P. So we should be able to find a term with type Void -> a. In fact one does exist, but it's somewhat complicated to explain: the answer is the empty function. We can define a function f :: A -> B as a (probably infinite) set of pairs whose first element is an element of A (the domain) and second element is f's output on this term, an element of B (the range). For example, the successor function on the naturals is represented as {(0,1), (1,2), (2,3), ...}. Note that in order to be a (total and well-defined) function, we must have precisely one pair (a, f a) for each term a with type A.

最初の章で発見したように、Pの値が真であるかどうかにかかわらず、もしQが真であれば論理包含 PQ は真である。したがって、型 Void -> a の項を見つけ出すことができるはずである。実際に存在するのだが、これはすこし説明が複雑になる。答えは 空(empty)関数である。関数 f :: A -> B を 最初の要素が Aの要素であるような(おそらく無限の) 集合の組 (定義域) と ２つ目の要素がB (値域)の要素であるようなこの項におけるfの出力と定義することができる。たとえば、自然数においてある自然数のすぐ次の自然数を得る関数は{(0,1), (1,2), (2,3), ...}と表すことができる。(total かつ well-defined な) 関数とするために、項 aが型Aである組 (a, f a)ひとつをちょうど得ることに注意されたい。

The empty function, let's call it empty is represented in this way by the empty set. But as we must have a pair for each element of the domain, and there no pairs in our representation, the domain type must be empty, i.e. Void. What about the range type? empty never produces any output, so there are no restrictions placed on the range type. Thus, it is valid to assume that the range type has any type, so we can say empty :: forall a. Void -> a. Unfortunately, it's not possible to write this function in Haskell; we'd ideally like to write something like:

この空関数をempty と呼ぶことにしよう。このようにemptyは空集合で表すことができる。 しかし、それぞれ定義域の要素である組がなければならないが、この表現に組は存在せず、定義域は空、すなわち Void でなければならない。値域の型についてはどうだろうか。empty はどんな出力もしないので、値域に課された制限はない。それゆえ、値域の型はどんな型と仮定しても正当であり、empty :: forall a. Void -> aということになる。残念ながら Haskell ではこのような関数を書くことはできないが、理想的には次のように書ければよい。

empty :: Void -> a


And stop there, but this is illegal Haskell. The closest we can come is the following:

empty :: Void -> a
empty _ = undefined


Alternatively:

もしくは、

empty :: Void -> a
empty = empty


Another reasonable way (also disallowed in Haskell) would be to write:

empty x = case x of { }


The case statement is perfectly well formed since it handles every possible value of x.

これはどんなxの値も扱うことができるので、このcase 文は完全に適切な形式(well formed)である。

Note that this is perfectly safe, since the right-hand side of this function can never be reached (since we have nothing to pass it). So, the conclusion of all this is that Void -> a is an inhabited type, just as PQ is true if P is false.

関数の右辺には決して届かない(ゆえに何も渡してはいない)ので、これはまったく安全であることに注意しよう。全体の結論としては、Void -> a は空でない型であり、P が偽であるならばPQ は真である、ということになる。

### Negation 否定

The ¬ operation in logic turns theorems into nontheorems and vice versa: if A is a theorem then ¬A is a nontheorem; if A is a nontheorem then ¬A is a theorem. How can we represent this in Haskell? The answer's a sneaky one. We define a type synonym:

type Not a = a -> Void


So for a type A, Not A is just A -> Void. How does this work? Well, if A was a theorem-type, then A -> Void must be uninhabited: there's no way any function could return any value, because the return type, Void has no values (The function has to provide values for all inhabitants of A)! On the other hand, if A was a nontheorem, then A can be replaced with Void as we explored in the last section. Then the function id :: Void -> Void is an inhabitant of Not A, so Not A is a theorem as required (The function doesn't have to provide any values, since there are no inhabitants in its domain. Nevertheless it's a function — with an empty graph).

だから、Aについて、Not Aの型は単にA -> Voidである。これはどのように働くのだろう？ A が定理型であれば、 A -> Void は空でない集合でなければならない。返り値の型 Void は値を持っていないので、どんな関数もどんな値でも返す方法はない(この関数は A のすべての空でない集合についても値を提供しているはずである)！言い換えれば、先ほどの章で探求したように、A が非定理だったら、AVoidに置き換えることができる。そして、関数　id :: Void -> Void　はNot Aの要素であり、ゆえに要求通りNot Aは定理となる(その定義域に要素がないので、この関数はどんな値も提供する必要はない。それにもかかわらず、これは空のグラフであり、関数なのだ。)。

## Axiomatic logic and the combinatory calculus 公理的論理と組み合わせ計算

So far we've only used some very basic features from Haskell's type system. Indeed, most of the features of logic we've mentioned can be explored using a very basic 'programming language', the combinator calculus. To fully appreciate how closely C-H ties together these two areas of mathematics, we need to axiomatise both our discussion of formal logic and our discussion of programming languages.

### Axiomatic logic 公理的論理

We start with two axioms about how the → operation should behave (from now on, we assume that → is a right-associative function, i.e. ABC means A → (BC)):

→操作がどのように振る舞うべきかについてのふたつの公理から始めよう(いまから、これらの → は右結合関数である、すなわち、ABCA → (BC) を意味するものとする)。

1. ABA
2. (ABC) → (AB) → AC

The first axiom says that given any two propositions A and B, if we assume both A and B, we know that A is true. The second says that if A implies that B implies C (or equivalently, if C is true whenever A and B are true), and A itself implies B, then knowing A is true would be enough to conclude that C is true. This may seem complicated, but a bit of thought reveals it to be common sense. Imagine we have a collection of boxes of various colours, some with wheels, some with lids, such that all the red boxes with wheels also have lids, and all the red boxes have wheels. Pick one box. Let A = 'The box under consideration is red', B = 'The box under consideration has wheels', C = 'The box under consideration has a lid'. Then the second law tells us that, as ABC (all red boxes with wheels also have lids), and AB (all red boxes have wheels), then if A (if the box is red), then C must be true (the box has a lid).

We also allow one inference law, called modus ponens:

モーダス・ポネンスとも呼ばれている推論規則も認めることにする。

1. If AB, and A, then B.　もし AB　かつ A　なら、 B　である。

This law allows us to create new theorems given old one. It should be fairly obvious; it is essentially the definition of what → means. This small basis provides a simple enough logic system which is expressive enough to cover most of our discussions. Here's a sample proof of the law AA in our system:

この法則はもとの定理から新しい定理を作ることを可能にする。これはまったく明白のはずである。→ が何を意味しているかの本質的な定義そのものである。この小さな原理は、ほとんどの我々の議論をカバーする十分な表現力する、単純で十分な論理体系を提供する。このシステムにおける、AAの証明例を示す。

Firstly, we know the two axioms to be theorems:

• ABA
• (ABC) → (AB) → AC

You'll notice that the left-hand side of the second axiom looks a bit like the first axiom. The second axiom guarantees that if we know that ABC, then we can conclude (AB) → AC. In this case, if we let C be the same proposition as A, then we have that if ABA, then (AB) → AA. But we already know ABA, that was the first axiom. Therefore, we have that (AB) → AA is a theorem. If we further let B be the proposition CA, for some other proposition C, then we have that if ACA, then AA. But, again, we know that ACA (it's the first axiom again), so AA, as we wanted.

ふたつめの公理の左辺が最初の公理であるように見えるのに気づくだろう。ふたつめの公理は、もしABCがわかっているなら、(AB) → ACと結論できることを保証する。このとき、もし CA と同じ命題だとすれば、もし ABAならば (AB) → AA を得る。もし B を命題 CA とすれば、ほかの命題 C について、もし ACA ならば AA を得る。しかし、繰り返すが、ACA (これはまた最初の公理だ)であり、ゆえに求めていた AAを得る。

This example demonstrates that given some simple axioms and a simple way to make new theorems from old, we can derive more complicated theorems. It may take a while to get there — here we had several lines of reasoning to prove just that the obvious statement AA is a theorem! — but we get there in the end. This kind of formalisation is attractive because we have essentially defined a very simple system, and it is very easy to study how that system works.

この例の実演はいくつかの単純な公理ともとの定理から新たな定理を創りだす簡単な方法さえあれば、さらに複雑な定理を導出できることを示す。これを得るまでに随分手間がかかるかもしれない。AA が定理であるという明らかな主張を証明するのにも何行もかかった！しかし、最終的にはたどり着いた。本質的にごく簡単なシステムを定義し、このシステムがどのように働くのかを研究するのは非常に簡単なので、この種の形式化は興味深い。

### Combinator calculus コンビネータ計算

The lambda calculus is a way of defining a simple programming language from a very simple basis. If you haven't already read the chapter that was just linked to, we recommend you read at least the introductory sections on the untyped version of the calculus. Here's a refresher in case you're feeling dusty. A lambda term is one of three things:

ラムダ計算はごく簡単な原理から単純なプログラミング言語を定義する方法のひとつである。もしまだラムダ計算の章を読んでいないのであれば、少なくとも型なしバージョンの計算の導入の節だけでも読んでおくことを勧める。忘れかけているかもしれないから、念のため確認しておこう。ラムダ項はつぎの３つのうちのひとつである。

• A value, v. , v
• A lambda abstraction ${\displaystyle \lambda x.t}$, where t is another lambda term. ラムダ抽象 ${\displaystyle \lambda x.t}$。ここで t は別のラムダ項である。
• An application ${\displaystyle (t_{1}t_{2})}$, where ${\displaystyle t_{1}}$ and ${\displaystyle t_{2}}$ are lambda terms. 適用 ${\displaystyle (t_{1}t_{2})}$。ここで ${\displaystyle t_{1}}$${\displaystyle t_{2}}$ はどちらもラムダ項である。

There is one reduction law, too, called beta-reduction:

ベータ簡約 と呼ばれる簡約規則がひとつある。

• ${\displaystyle ((\lambda x.t_{1})t_{2})}$${\displaystyle t_{1}[x:=t_{2}]}$, where ${\displaystyle t_{1}[x:=t_{2}]}$ means ${\displaystyle t_{1}}$ with all the free occurrences of x replaced with ${\displaystyle t_{2}}$.　${\displaystyle ((\lambda x.t_{1})t_{2})}$${\displaystyle t_{1}[x:=t_{2}]}$。ここで、${\displaystyle t_{1}[x:=t_{2}]}$はすべての x の自由な出現をともなう${\displaystyle t_{1}}$${\displaystyle t_{2}}$で置換されることを意味する。

As mentioned in the lambda calculus article, the difficulty comes when trying to pin down the notion of a free occurrence of an identifier. The combinator calculus was invented by the American mathematician Haskell Curry (after whom a certain programming language is named) because of these difficulties. There are many variants on the basic combinator calculus, but we consider one of the simplest here. We start with two so-called combinators:

ラムダ計算の項目で言及したように、識別子の自由な出現の記述を束縛するのを試すときには困難が生じる。これらの困難のため、コンビネータ計算はアメリカの数学者ハスケル・カリーによって考案された(のちにプログラミング言語の名前ともなった)。基本的なコンビネータ計算にはいくつかの亜種が存在するが、ここでは最も簡単なものについて考える。ふたつのいわゆる コンビネータ と呼ばれるものから始める。

• K takes two values and returns the first. In the lambda calculus, ${\displaystyle \mathbf {K} =\lambda xy.\ x}$.　K はふたつの値をとり、最初のひとつを返す。ラムダ計算においては、${\displaystyle \mathbf {K} =\lambda xy.\ x}$　である。
• S takes a binary function, a unary function and a value, and applies that value and the value passed into the unary function to the binary function. again, in the lambda calculus: ${\displaystyle \mathbf {S} =\lambda xyz.\ xz(yz)}$. S は２引数の関数、１引数の関数、値をとり、値を１引数の関数に渡して、２引数の関数に適用する。ラムダ計算では、${\displaystyle \mathbf {S} =\lambda xyz.\ xz(yz)}$ である。

The first function you should recognise as const. The second is more complicated, it is the monadic function ap in the ((->) e) monad (which is essentially Reader). These two combinators form a complete basis for the entire lambda calculus. Every lambda calculus program can be written using just these two functions.

## Intuitionistic vs classical logic 直観論理か古典論理か

So far, all of the results we have proved are theorems of intuitionistic logic. Let's see what happens when we try to prove the basic theorem of classical logic,  Not Not A -> A . Recall that this translates as  ((A -> Void) -> Void) -> A . So, given a function of type  (A -> Void) -> Void  we need a function of type A. Now a function of type  (A -> Void) -> Void  exists precisely if type  A -> Void  is uninhabited, or in other words if type A is inhabited. So we need a function which takes any inhabited type, and returns an element of that type. Although it is simple enough to do this on a computer - we need only find the "simplest" or "first" inhabitant of each type - there is no way to do this using standard lambda-calculus or combinator techniques. So we see that this result cannot be proved using these two techniques, and hence that the underlying logic is intuitionistic rather than classical.

これまで証明してきたすべての結果は、直観主義論理の定理である。古典論理の基本的な定理、  Not Not A -> A  を証明することを試みるどうなるのであろうか。  ((A -> Void) -> Void) -> A  と変換されることを思い出そう。すると、型 (A -> Void) -> Void の関数について 型Aを返すような関数が必要だ。いま、もし型  A -> Void  が空である、言い換えれば 型 A が空であるなら、型  (A -> Void) -> Void  の関数がまさに存在する。必要なのはなんらかの空である型をとりその型の要素を返す関数である。それぞれの型の "最も単純"、言い換えれば "最初" の要素を発見するだけであるので、コンピュータにとってはじゅうぶんに容易い。しかし、通常のラムダ計算やコンビネータの技法を使用してこれを果たす方法はない。ゆえに、これらの２つの技法を使ってこの結果を証明することができず、根本的な論理は古典論理というより直観論理であることがわかる。

Instead, consider a traditional error handling function which calls throw when an error occurs, transferring computation to catch. The throw function cancels any return value from the original function, so it has type A -> Void, where A is the type of its arguments. The catch function then takes the throw function as its argument, and, if the throw triggers (i.e. returns a Void) will return the argument of the throw function. So the type of catch is  ((A -> Void) -> Void) -> A . [7]

## Notes

1. ^ Another way of looking at this is that we're trying to define our logical operator → such that it captures our intuition of the "if... then" construct in natural language. So we want statements like for all all naturals ${\displaystyle x}$, "${\displaystyle x}$ is even" → "${\displaystyle x+1}$ is odd" to be true. I.e. that implication must hold when we substitute ${\displaystyle x}$ for any natural including, say, 5. But "5 is even" and "6 is odd" are both false, so we must have that False → False is true. Similarly by considering the statement for all naturals ${\displaystyle x>3}$, "${\displaystyle x}$ is prime" → "${\displaystyle x+1}$ is not prime", we must have that False → True is true. And obviously True → True must be true, and True → False is false. So we have that ${\displaystyle x}$${\displaystyle y}$ unless ${\displaystyle x}$ is true and ${\displaystyle y}$ false.
2. ^ これを導く別の方法としては、自然言語において「もし～ならば」という構造の直感的理解を満たす論理演算子 → を定義しようとするということだ。すべての自然数${\displaystyle x}$について、「${\displaystyle x}$ が偶数」 → 「${\displaystyle x+1}$ が奇数」が真であることを主張したいとする。たとえば、この推論は${\displaystyle x}$ をどんな自然数、例えば 5 に置き換えたとしても満たさなければならない。しかし、「5 が偶数」と「6が奇数」はどちらも偽であり、偽 → 偽 は真でなければならない。同様に、すべての ${\displaystyle x>3}$の自然数について"${\displaystyle x}$ が素数" → "${\displaystyle x+1}$ は素数ではない"を考えると、偽→ 真 は真でなければならない。真→ 真 が真であることや、真 → 偽 は 偽であるのは明らかだ。したがって、 ${\displaystyle x}$ が真で${\displaystyle y}$が偽でない限り、${\displaystyle x}$${\displaystyle y}$ は真なのである。
3. ^ Technically, the types Either Void A and A are isomorphic. Seeing as you can't have a value of type Void, every value in Either Void A must be a Right-tagged value, so the transformation just strips the Right constructors.
4. ^ 専門的には、型Either Void A と型A は同型であるという。型Voidの値を得ることはできないので、Either Void Aのどんな値もRightが付けられた値でなければならず、変換は単に Right構築子を剥がすだけである。
5. ^ Again, the technical statement is that Void is isomorphic to any type which is a nontheorem.
6. ^ 繰り返しになるが、専門的にはこれをVoid は非定理であるようなどんな型とも同型である、という。
7. ^ This argument is taken from Dan Piponi. “Adventures in Classical Land”. The Monad Reader (6).