Logika pierwszego i drugiego rzędu

(1)

Rachunek lambda, lato 2019-20

Wykład 13

29 maja 2020

1

Logika pierwszego i drugiego rzędu

Symbole relacyjne: wyrażeniaP(x ), Q(t, v ), itp.

są formułami atomowymi. Ich argumentami są zmienne lub termy „indywiduowe” lub „przedmiotowe”.

Kwantyfikatory: zmiennaxjest związana w formułach∀x ϕ(x),∃x ϕ(x).

Logika pierwszego rzędu: kwantyfikatory wiążą tylko zmienne indywiduowe. Symbole relacyjne są stałe.

Logika drugiego rzędu: kwantyfikatory mogą wiązać zmienne relacyjne.

2

Typy zależne (Dependent types)

P(a1, . . . , an)— a type thatdependson the choice of individual valuesa1, . . . ,an.

Na przykład:

M : array(n) Mjest tablicą rozmiarun;

array : Int → „Typ” arrayjest konstruktorem typu (rodziną typów )

3

Wycieranie zależności

Aksjomat indukcji:

∀n (P(n) → P(n + 1)) → P(0) → ∀n P(n).

Jeśli usuniemy z niego wszystko to, co odnosi się do indywiduów (kwantyfikatory i argumenty relacjiP), to otrzymamy taką formułę zdaniową (typ prosty):

(P → P) → P → P.

4

Polimorfizm

5

(Klasyczna) logika drugiego rzędu

Składnia:Zmienne relacyjne i kwantyfikatory∀R, ∃R.

Przykład formuły: ∀P(P(x) → Q(x)) → Q(x) Semantyka w stylu Tarskiego:Interpretujemy zmienne relacyjne jako relacje. Na przykład formuła

Nat(x) = ∀R(∀y (R(y ) → R(s y )) → R(0) → R(x)) definiuje standardowe liczby naturalne.

Wniosek:Aksjomaty Peana plus ∀xNat(x) definiują standardowy model arytmetyki z dokładnością do izomorfizmu.

Wniosek:Zbiór tautologii drugiego rzędu nie jest rekurencyjnie przeliczalny(boTh(N)nie jest).

Wniosek:Nie ma pełnego systemu wnioskowania.

6

Logika drugiego rzędu

Przykład formuły:∀P(P(x) → Q(x)) → Q(x)

Two ways to understand the quantifier∀P:

1. Tarski: the variableP ranges over unary relations (subsets of a domain).

2. Henkin: The variablePranges over definablepredicates.

The set of tautologies wrt (1) is not recursively enumerable.

There is no complete proof system.

We think in terms of (2).

7

Logika drugiego rzędu w stylu Henkina

Semantyka (nieformalna):Interpretujemy zmienne relacyjne jako definiowalne predykaty.

To ma sens klasycznie i intuicjonistycznie.

Reguły wnioskowania:

Xton-arna zmienna relacyjna, σto „formuła znargumentami”.

Γ ` ∀X ϕ(X ) Γ ` ϕ(σ)

Γ ` ϕ(X )

Γ ` ∀X ϕ(X )(X 6∈FV(Γ))

Γ ` ϕ(σ) Γ ` ∃X ϕ(X )

Γ ` ∃X ϕ(X ), Γ, ϕ(X ) ` ψ Γ ` ψ

(X 6∈FV(Γ, ψ))

8

(2)

“Dependency erasure”

Example 1:∀P(P(x) → Q(x)) → Q(x) This is the same principle as ∀p(p → q) → q.

Example 2:Definition of natural numbers:

Nat(n) : ∀R(∀x(R(x) → R(sx)) → R(0) → R(n)) Jak można udowodnić formułęNat(5 )?

Deleting first-order layer: ∀r ((r → r ) → r → r ).

9

Second-order propositional logic

(Ax) Γ, ϕ ` ϕ

(→ I) Γ, ϕ ` ψ Γ ` ϕ → ψ

(→ E)Γ ` ϕ → ψ Γ ` ϕ Γ ` ψ

(∀I) Γ ` ϕ Γ ` ∀p ϕ

(p 6∈ FV(Γ)) (∀E) Γ ` ∀p ϕ Γ ` ϕ[p := ϑ]

(∃I)Γ ` ϕ[p := ϑ]

Γ ` ∃p ϕ

(∃E)Γ ` ∃p ϕ, Γ, ϕ ` ψ Γ ` ψ

(p 6∈ FV(Γ, ψ))

10

Two educated cliches

I Full comprehension:Propositional variables range over all formulas:

∃p (ϕ ↔ p)

∀p ϕ(p) → ϕ(ψ)

The meaning ofpin∀p ϕcan be∀p ϕitself.

I Impredicativity:The meaning of∀p ϕis defined by a reference to a domain to which∀p ϕitself belongs.

11

Comparison with classical logic

I Validity/provability in classical propositional logic is complete in the complexity class. . .co-NP.

I Provability in intuitionistic propositional logic isPSPACE-complete.

I Validity/provability in second-order classical propositional logic (known as the QBF problem) isPSPACE-complete.

I Provability in second-order intuitionistic propositional logic isundecidable.

12

Polymorphic types

I Basic idea:∀p. p → pis a type of a generic identity.

I Church style (explicit polymorphism):

I Generic identityIadmits a type argument.

I The applicationIτis of typeτ → τ.

I Curry style (implicit polymorphism):

I Generic identityIhas all typesτ → τat once.

13

Girard’s System F (Church style)

Γ(x : ϕ) ` x : ϕ

Γ(x : ϕ) ` M : ψ Γ ` (λx :ϕ M) : ϕ → ψ

Γ ` M : ϕ → ψ Γ ` N : ϕ Γ ` (MN) : ψ

Γ ` M : ϕ

Γ ` (Λp M) : ∀p ϕ(p 6∈FV(Γ)) Γ ` M : ∀p ϕ Γ ` Mϑ : ϕ[p := ϑ]

14

Girard’s System F (Church style)

Γ(x :ϕ) ` x :ϕ

Γ(x :ϕ) ` M :ψ Γ` (λx:ϕ M) :ϕ → ψ

Γ` M :ϕ → ψ Γ` N :ϕ Γ` (MN) :ψ

Γ` M :ϕ

Γ` (Λp M) :∀p ϕ(p 6∈FV(Γ)) Γ` M :∀p ϕ Γ` Mϑ :ϕ[p := ϑ]

15

Reduction rules

Beta:

I (λx :τ.M)N =⇒βM[x := N];

I (Λp. M)τ =⇒βM[p := τ ], Eta:

I λx :τ.Mx =⇒ηM (x 6∈FV(M));

I Λp.M p =⇒ηM (p 6∈FV(M)).

Subject reduction:

IfΓ ` M : τandM ^βηNthenΓ ` N : τ

16

(3)

A few examples

^(zamiastλx :τpiszemy λx^τ)

I TermΛqλx^∀p(p→p).x (q → q)(xq)

has type ∀q(∀p(p → p) → q → q);

I Term2 = Λp.λf^p→pλx^p.f (fx )

has type ∀p((p → p) → (p → p));

I Termλf^{∀p(p→q→p)}Λpλx^p.f (q→p)(fpx )

has type ∀p(p → q → p) → ∀p(p → q → q → p).

17

Wycieranie typów

|x| = x

|MN| = |M||N|

|λx:σ. M| = λx. |M|

|Λp. M| = |M|

|Mτ | = |M|

18

Girard’s System F (Church style)

Γ(x : ϕ) ` x : ϕ

Γ(x : ϕ) ` M : ψ Γ ` (λx :ϕ M) : ϕ → ψ

Γ ` M : ϕ → ψ Γ ` N : ϕ Γ ` (MN) : ψ

Γ ` M : ϕ

Γ ` (Λp M) : ∀p ϕ(p 6∈FV(Γ)) Γ ` M : ∀p ϕ Γ ` Mϑ : ϕ[p := ϑ]

19

System F w stylu Curry’ego

Γ(x : τ ) ` x : τ

Γ(x : τ ) ` M : σ Γ ` λx .M : τ → σ

Γ ` M : τ → σ Γ ` N : τ Γ ` NM : σ

Γ ` M : σ

Γ ` M : ∀p σ (p 6∈FV(Γ)) Γ ` M : ∀p σ Γ ` M : σ[p := τ ]

20

Wycieranie redukcji

(λx :τ.M)N =⇒βM[x := N];

(λx . |M|)|N| =⇒β|M|[x := |N|] = |M[x := N]|

(Λp. M)τ =⇒βM[p := τ ],

|M| = |M|

λx :τ.Mx =⇒ηM;

λx . |M|x =⇒η|M|

Λp.M p =⇒ηM;

|M| = |M|

21

Properties of type erasure

(Church is blue,Curry is red.) 1. If Γ ` M : τ thenΓ ` |M| : τ.

2. If Γ ` M : τthen there existsM such that|M| = M orazΓ ` M : τ.

3. If MβNthen|M| β|N|.

4. If |M| →βNthen there existsN such that|N| = NandM →βN.

Uwaga:Tym razem część 4 nie jest oczywista, a w części 3 jest tylko , a nie →.

22

Poprawność redukcji (Curry)

Twierdzenie:

JeśliΓ ` M : τ, orazM →βM⁰toΓ ` M⁰: τ.

Dowód:Nie jest oczywisty.

23

Generation lemma

Writeσ τwhenσ = ∀~p σ⁰andτ = ∀~q.σ⁰[~p := ~%], whereσ⁰6= ∀ . . ., and~qare not free inσ.

Na przykład∀p. p → r ∀q. (q → r ) → r.

Generation lemma:

1. IfΓ ` x : τthenΓ(x ) τ.

2. IfΓ ` MN : τthenΓ ` M : % → σandΓ ` N : %, for some%,σ, with∀~p σ τ, where~p =FV(σ) −FV(Γ).

3. IfΓ ` λx M : τthenτ = ∀~p(% → σ), whereΓ(x :%) ` M : σand~pare not free inΓ.

24

(4)

Subject reduction

Lemma:

1. If Γ(x : τ ) ` M : σandΓ ` N : τ thenΓ ` M[x := N] : σ.

2. If Γ ` (λx M)N : σthenΓ ` M[x := N] : σ.

Proof: (1) Induction. (2) By (1) and generation lemma.

Corollary (subject reduction):

If Γ ` M : σandM βNthenΓ ` N : σ.

25

Subject reduction. . . fails for η

Example:

x : p → ∀q (q → q) ` λy . xy : p → q → q.

x : p → ∀q (q → q) 6` x : p → q → q.

26