TCS: Propositions as Types

本文含有大量复杂的 $\LaTeX$ 公式，因此md文档效果不好，仅供参考！

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

We use ‘ $\to$ ’ to represents the prooftree in PDF.

\begin{align*} (\land I)\qquad &(A, B) \to (A\land B) \\ (\land E_{1})\qquad &(A\land B) \to A \\ (\land E_{2})\qquad &(A\land B) \to B \\ \end{align*}

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!