normalization & classical logic

logical verification week 3 2004 09 22

practical work

• monday noon is the limit

• importance of precise notation

– labels in assumptions should go inside the brackets

[A]^{x} ; ⋮ should be [A^{x}] ; ⋮

– left-right order of hypotheses matters

\frac{⋮ ; A  ⋮ ; A → B}{B} should be \frac{⋮ ; A → B  ⋮ ; A}{B}

contents for today

• recap

• term & proof normalization • variants of propositional logic

recap

minimal logic

→ introduction

\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→

→ elimination

\frac{⋮ ; A → B  ⋮ ; A}{B} E→

λ→ simply typed λ-calculus

variable rule

Γ, x : A, Γ′ ⊢ x : A

x does not occur in Γ′

abstraction rule

\frac{Γ, x : A ⊢ t : B}{Γ ⊢ (λx : A. t) : (A → B)}

application rule

\frac{Γ ⊢ t : A → B Γ ⊢ u : A}{Γ ⊢ t u : B}

Currying

A → B → (C → D)

λ(x : A) (y : B). (λz : C. M)

(f a b) c

A → B → C → D

λ(x : A) (y : B) (z : C). M

f a b c

A → (B → (C → D))

λx : A. λy : B. λz : C. M

((f a) b) c

examples

• permutation

(A → B → C) → (B → A → C)

• weak version of Peirce’s law ((((A → B) → A) → A) → B) → B

Curry-Howard-de Bruijn isomorphism

• propositions as types a term inhabits a type a proof inhabits a proposition

• Brouwer-Heyting-Kolmogorov interpretation λx : A. M : A → B

normalization

term normalization

β-step

… ((λx : A. M) N) …  →_{β}  … (M[x := N]) …
… ((λx : ℝ. x^{2} − 2) 4) …  →_{β}  … (4^{2} − 2) …
… ((λx : A. x) y) …  →_{β}  … y …

substitution

renaming bound variables: α-equivalence λx : A. (… x …) =_{α} λy : A. (… y …)

λx : A → B. (λy : A → B. λx : A. y x) x ↛_{β} λx : A → B. (λx : A. x x)
… λz : A. y z … →_{β} λx : A → B. (λz : A. x z)

de Bruijn indices

λ_{A→B}. (λ_{A→B}. λ_{A}. 1 0) 0 →_{β} λ_{A→B}. (λ_{A}. 1 0)

reduction

iterated beta steps

M_{1} →_{β} M_{2} →_{β} M_{3} →_{β} ... →_{β} M_{n}

M_{1} → →_{β} M_{n}

normal form

detours

combination of I[…]→ and E→

\frac{\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→  ⋮ ; A}{B} E→

‘proof of B using a lemma A’

example

proof of A → B → A with a detour

detour elimination

(cut elimination)

\frac{\frac{[A^{x}] ; ⋮ ; B}{A → B} I[x]→  ⋮ ; A}{B} E→ →  ⋮ ; A ; ⋮ ; B

Curry-Howard-De Bruijn

detour ∼ β-redex

β-redex: combination of abstraction and application detour: combination of → introduction and → elimination

proof normalization ∼ β-reduction
normalization step ∼ reduction step
normal proof ∼ normal form

consistency

proof checking & type checking

? ⊢ M : A

• decidable?

• complexity?

provability & inhabitation

⊢ ? : A

• decidable?

• complexity?

consistency  ⊢ ? : ⊥

second hour

confluence

proposition (not proved in the course)

\xymatrix{ & M \ar@{->>}[dl] \ar@{->>}[dr] \\ M_{1} \ar@{->>}[dr] &  & M_{2} \ar@{->>}[dl] \\  & M′}

termination

proposition (not proved in the course) weak termination: every term has a normal form strong termination: no term has an infinite reduction

does hold for typed λ-calculus does not hold for untyped λ-calculus

(λx. xx) (λx. xx) → →_{β} (λx. xx) (λx. xx)

subject reduction

proposition (not proved in the course)

types are preserved under computation Γ ⊢ M : A & M → →_{β} M′ ⇒ Γ ⊢ M′ : A

characterization of normal forms

x N_{1} N_{2} … N_{k}
λx : A. N

consistency

proposition there is no proof of ⊥ in minimal logic

classical logic

⊥ elimination

\frac{⋮ ; ⊥}{A} E⊥

‘ex falso [sequitur] quodlibet’

elimtype False.

¬ rules

negation is defined: ¬A := A → ⊥

¬ introduction

\frac{[A^{x}] ; ⋮ ; ⊥}{¬A} I[x]¬

¬ elimination

\frac{⋮ ; ¬A  ⋮ ; A}{⊥} E¬

variants of propositional logic

• minimal logic only implication

• minimal logic + falsum

• intuitionistic logic … + conjunction + disjunction

• classical logic

a classical proof

proposition

there are x and y such that x ∉ ℚ and y ∉ ℚ, but x^{y} ∈ ℚ proof

\sqrt{2} ∉ ℚ (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{(\sqrt{2}·\sqrt{2})} = \sqrt{2}^{2} = 2 ∈ ℚ now either \sqrt{2}^{\sqrt{2}} ∈ ℚ or \sqrt{2}^{\sqrt{2}} ∉ ℚ in the first case x = \sqrt{2} and y = \sqrt{2} does the job in the second case x = \sqrt{2}^{\sqrt{2}} and y = \sqrt{2} does the job

the same proof in Mizar

theorem
ex x, y st x is irrational & y is irrational & x.^.y is rational
proof
set w = sqrt 2;
w>0 by AXIOMS:22,SQUARE_1:84;
then A1: (w.^.w).^.w = w.^.(w*w) by POWER:38
 .= w.^.(w^2) by SQUARE_1:def 3
 .= w.^.2 by SQUARE_1:def 4
 .= w^2 by POWER:53
 .= 2 by SQUARE_1:def 4;
per cases;
suppose A2: w.^.w is rational;
 take w, w;
 thus thesis by A2,Th1,INT_2:44;
end;
suppose A3: w.^.w is irrational;
 take w.^.w, w;
 thus thesis by A1,A3,Th1,INT_2:44;
end;
end;

classical logic

• excluded middle

A ∨ ¬A

• double negation rule

¬¬A → A

• Peirce’s law

((A → B) → A) → A

examples of intuitionistic natural deduction

• contraposition

(A → B) → (¬B → ¬A)

• many negations

¬¬(¬¬A → A)

examples of classical natural deduction

• using A ∨ ¬A one can prove ¬¬A → A

• using ¬¬A → A one can prove ((A → B) → A) → A

summary

• term & proof normalization consistency

• variants of propositional logic classical logic