TCS: Propositions as Types

Propositions as Types

Intuitionistic Logic and Natural Deduction

Intuitionistic logic insists upon a constructionist notion of truth. In particular, a proof of $A\lor B$ must show which of $A$ or $B$ holds (different from classic logic).

Natural Deduction

Proof rules should come in pairs:

Introduction rules which are like definitions of the logic operators.
Elimination rules which are the consequences of theirdefinitions.

Both of them should be in harmony.
We will define the four kinds of rules, conjunction, implication, disjunction and falsehood in order.

Gentzen’s contribution:

Subformula principle: Proofs can be normalized so that no concepts enter the proof other than those contained in the final result (subformula).

This means we can use only the known proposition and the subformulas of the conclusion.

Guiding Question for Defining Logic

Martin-Löf: The meaning of a proposition is determined by what counts as a verification (or proof) of it.

Proposition: $A$
Justification: $A \text{ true}$, $A \text{ is true at time } t$, $\dots$

So that we need to determin a proposition by a verification(not only itself).

In this lecture, we only consider justification $A \text{ true}$ so we omit thet suffix $\text{true}$

Conjunction

\[\begin{prooftree} \AXC{$A$} \AXC{$B$} \RightLabel{$(\land I)$} \BIC{$A\land B$} \end{prooftree} \]

\[\begin{prooftree} \AXC{$A\land B$} \RightLabel{$(\land E_1)$} \UIC{$A$} \end{prooftree} \]

\[\begin{prooftree} \AXC{$A\land B$} \RightLabel{$(\land E_2)$} \UIC{$B$} \end{prooftree} \]

We define the local soundness and local completeness as follows:

Local Soundness: The elimination cannot give us new information.

\[\begin{align*} &\quad((\mathcal{D} \to A),\, (\mathcal{E} \to B)) \to (A\land B) \to A \\ &\Rightarrow_{R} (\mathcal{D}\to A) \end{align*} \]

Local Completeness: The elimination can reconstitute the proof by introduction

\[\begin{align*} &\quad (\mathcal{D}\to A)\\ &\Rightarrow_{E}(((\mathcal{D} \to (A\land B)) \to A),\, ((\mathcal{D} \to (A\land B)) \to B)) \to (A\land B) \to A \end{align*} \]

Implication

We define the hypothetical judgment at first:

\[(A\land (B\land C)) \vdash B \]

This is not an inference as it consists of two inferences! We have conjunctions inferences at now.

Then we can define implication introduction and elimination rules:

\[\begin{align*} (\supset I^{x})\qquad &(\overline{A}^{x} \to^{*} B) \to (A\supset B) (\supset E)\qquad & (A\supset B,\, A) \to B \end{align*} \]

In which that the $^{x}$ means the local scope.

Disjunction

Define the disjunction as follows:

\[\begin{align*} (\lor I_{1})\qquad &A \to (A\lor B) \\ (\lor I_{2})\qquad &B \to (A\lor B) \\ (\lor E^{x, y})\qquad &(A\lor B, \overline{A}^{x}\to^{*}C, \overline{B}^{y}\to^{*}C) \to C \end{align*} \]

Falsehood

Falsehood is written as $\bot$.

It has no introduction as we shouldn’t prove it.

\[(\bot E) \bot \to C \]

Intuitionistic Natural Deduction

So, we can use these four to define some other operates such as $\neg$, $\top$ and $\leftrightarrow$

\[\begin{align*} \neg A &\mathop{=}\limits^{\text{def}} A \supset \bot \\ \top &\mathop{=}\limits^{\text{def}} \bot \supset \bot \\ A \leftrightarrow B &\mathop{=}\limits^{\text{def}} (A \supset B) \land (B \supset A) \end{align*} \]

Now we can begin prove! The follows is some interesting conclusion:

\[\begin{align} A \supset &B \supset A \\ A \supset &\neg\neg A \\ (A \supset B) \supset &(\neg B \supset \neg A) \\ \neg (A \lor B) \leftrightarrow &(\neg A \land \neg B) \end{align} \]

But some weird things hapend as the following is not provable:

\[\begin{align} ((A \supset B) \supset A) &\supset A \\ \neg\neg A &\supset A \\ (\neg A \supset \neg B) &\supset (B \supset A) \\ \neg (A \land B) \leftrightarrow &(\neg A \lor \neg B) \end{align} \]

What the f***!

The most interesting is that:

(Gilvenko’s Theorem):, $A$ is valid in classical logic if and only if $\neg\neg A$ is valid in intuitionistic logic!

And intuitionistic logic is PSPACE-complete!

Propositions as Types

We write $M: A$ to represent that $M$ is a proof of $A$ and alternatively $M$ is a program of type $A$.
So we can rewrite the four kinds of roles by $\lambda$-calculus!

Implication

\[\begin{align*} (\supset I^{x})\qquad &((\overline{x:A}^{x})\to (M:B)) \to (\lambda x.M):(A\supset B) \\ (\supset E)\qquad &((M:(A\supset B)), (N:A)) \to (MN: B) \end{align*} \]

From its local soundness we can get $\beta$ reduction, and from local completeness we can get $\eta$ rule!

Turing has proved that typed $\lambda$-calculus always terminates.

Conjunction

\[\begin{align*} (\land I)\qquad((M:A), (N:B)) &\to (\langle M, N\rangle: A\land B) \\ (\land E_{1})\qquad (M:(A\land B)) &\to ((\mathbf{fst}M):A) \\ (\land E_{2})\qquad (M:(A\land B)) &\to ((\mathbf{snd}M):B) \end{align*} \]

The local reduction and expansion can give out the meaning of $\langle \cdot, \cdot\rangle$, $\mathbf{fst}$ and $\mathbf{snd}$

Disjunction

\[\begin{align*} (\lor I_{1})\qquad (M:A) &\to ((\mathbf{inl}M): A\lor B) \\ (\lor I_{2})\qquad (M:B) &\to ((\mathbf{inr}M): A\lor B) \\ (\lor E^{x,y}) \qquad (M:(A\lor B), &(\overline{x:A}^{x} \to (N:C)), (\overline{y:B}^{y} \to (P:C))) \\ &\to \mathbf{case}(M, x.N, y.P):C \end{align*} \]

Falsehood

No introduction rule.

\[(\bot E)\qquad(M:\bot) \to (\mathbf{abort}M:C) \]

本文采用署名-非商业性使用-相同方式共享 4.0 国际许可协议，转载请注明出处。