Ge sch ie de ni s va n d e L o gi c a L o g i c a i n In f o r m a t i c a
Jeroen Goudsmit Universiteit Utrecht
maandag juni
Inhoud
Toepassing
.
Typen
.
Herschrijven
.
.
. Overzicht
O ve r z i c h t
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
van Oostrom
Klop
Barendregt .
Awodey en Warren
.
.
Fourman
Eilenberg en Steenrod
van Dalen
Visser
.
Voevodsky
Došen Rosolini Kan Péter
Sco
Kleene
.
.
.
Dijkstra
Eilenberg en Mac Lane
Heyting
Troelstra
Iemhoff
Brouwer
Turing
Church
.
.
Knuth
.
Vietoris
.
Leray, Cartan
Whitehead & Russel
.
.
Lawvere
.
.
.
.
Kolmogorov
Grothendieck
Rosser Post
Makkai en Reyes
.
Mac Lane en Moerdijk
Kant, Cantor, Frege, Poincaré
Kruskal
Hyland Lambek
Karp
Kőnig
.
Erdős
Schönfinkel
.
Parikh en Tait
.
Girard
Curry
.
Cook
Hilbert
.
Coquand en Huet .
de Bruin Martin-Löf
Gödel
Gentzen
Noether
H e r s c h r i j ve n
Dihedrale Groepen
.
Dihedrale Groepen .
.
.
.
Dihedrale Groepen .
.
.
.
Dihedrale Groepen .
.
.
.
Dihedrale Groepen .
.
.
.
Dihedrale Groepen .
.
.
.
Herschrijven .
r
s .
.
.
.
.
.
.
.
. r
r .
.
.
.
.
s
.
Herschrijfregels
rrr ss sr
Ð→ Ð→ Ð→
e e rrs
Rekenkunde
n + 0 Ð→ n n + (S m) Ð→ S (n + m)
Rekenkunde
n+0 n + (S m) n⋅0 n ⋅ (S m)
Ð→ Ð→ Ð→ Ð→
n S (n + m) 0 n + (n ⋅ m)
Rekenen met Rekenkunde 2 + (2 + (2 ⋅ 0)) (1 + 1) ⋅ (2 + 0) 2 + (2 ⋅ 1)
2 + (2 + 0) 4 . 2+2 (1 + 1) ⋅ 2
S S (2 + 0) S (2 + 1)
S (1 + 0) ⋅ 2
2⋅2
Terminatie
. .
.
.
.
.
...
Terminatie
. .
.
.
.
.
...
.
Amalie Emmy Noether
.
Confluentie .
.
.
. .
.
.
.
.
.
.
.
.
.
..
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Confluentie .
.
.
. .
.
.
.
.
.
.
.
.
.
..
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Alonzo Church & Barkley Rosser
.
.
Uitbreidingen
n ⋅ (x + y)
Ð→ n ⋅ x + n ⋅ y
Uitbreidingen
n ⋅ (x + y)
Ð→ n ⋅ x + n ⋅ y ✓
Uitbreidingen
n ⋅ (x + y) Ð→ n ⋅ x + n ⋅ y ✓ 2 + 2 Ð→ 5
Uitbreidingen
n ⋅ (x + y) Ð→ n ⋅ x + n ⋅ y ✓ 2 + 2 Ð→ 5 ×
Uitbreidingen
n ⋅ (x + y) Ð→ n ⋅ x + n ⋅ y ✓ 2 + 2 Ð→ 5 × 4 Ð→ 2 + 2
Uitbreidingen
n ⋅ (x + y) Ð→ n ⋅ x + n ⋅ y ✓ 2 + 2 Ð→ 5 × 4 Ð→ 2 + 2 ×
Uitbreidingen
n ⋅ (x + y) 2+2 4 2+2
Ð→ Ð→ Ð→ Ð→
n⋅x+n⋅y ✓ 5 × 2+2 × 4
Uitbreidingen
n ⋅ (x + y) 2+2 4 2+2
Ð→ Ð→ Ð→ Ð→
n⋅x+n⋅y 5 2+2 4
✓ × × ✓
Kernbegrippen . Confluentie
.
.
Terminatie
. Betekenis
Onbeslisbaarheid
.
„Recursive Unsolvability of a Problem of Thue” – Post ()
Typ e n
Implicationeel Fragment
Γ, ϕ ⊢ ϕ
Γ, ϕ ⊢ ψ → Γ⊢ϕ→ψ
Γ⊢ϕ→ψ Γ⊢ϕ → Γ⊢ψ
Bewijs van ϕ → ϕ
Bewijs van ϕ → ϕ
ϕ⊢ϕ → ⊢ϕ→ϕ
Bewijs van ϕ → ψ → ϕ
⊢ϕ→ψ→ϕ
Bewijs van ϕ → ψ → ϕ
ϕ⊢ψ→ϕ → ⊢ϕ→ψ→ϕ
Bewijs van ϕ → ψ → ϕ
ψ, ϕ ⊢ ϕ → ϕ⊢ψ→ϕ → ⊢ϕ→ψ→ϕ
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
⊢ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
ϕ → ψ → χ, ϕ → ψ, ϕ ⊢ χ → ϕ → ψ → χ, ϕ → ψ ⊢ ϕ → χ → ϕ → ψ → χ ⊢ (ϕ → ψ) → ϕ → χ → ⊢ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Γ⊢χ → ϕ → ψ → χ, ϕ → ψ ⊢ ϕ → χ → ϕ → ψ → χ ⊢ (ϕ → ψ) → ϕ → χ → ⊢ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Γ⊢ψ→χ
Γ⊢ψ → Γ⊢χ → ϕ → ψ → χ, ϕ → ψ ⊢ ϕ → χ → ϕ → ψ → χ ⊢ (ϕ → ψ) → ϕ → χ → ⊢ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Γ⊢ψ→χ
Γ⊢ϕ→ψ Γ⊢ψ
Γ⊢χ → ϕ → ψ → χ, ϕ → ψ ⊢ ϕ → χ → ϕ → ψ → χ ⊢ (ϕ → ψ) → ϕ → χ → ⊢ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Γ⊢ϕ →
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Γ⊢ϕ→ψ→χ Γ⊢ψ→χ
Γ⊢ϕ
→
Γ⊢ϕ→ψ Γ⊢ψ
Γ⊢χ → ϕ → ψ → χ, ϕ → ψ ⊢ ϕ → χ → ϕ → ψ → χ ⊢ (ϕ → ψ) → ϕ → χ → ⊢ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ
Γ⊢ϕ →
→
Alternatief bewijs voor ϕ → ϕ
⊢(
ϕ. → ( ϕ →. ϕ ) → ϕ. ) → ( ϕ. → ϕ →. ϕ ) → ϕ. → ϕ.
Alternatief bewijs voor ϕ → ϕ
⋮ ⊢(
ϕ. → ( ϕ →. ϕ ) → ϕ. ) → ( ϕ. → ϕ →. ϕ ) → ϕ. → ϕ.
Alternatief bewijs voor ϕ → ϕ
⋮ ⊢(
⋮
ϕ. → ( ϕ →. ϕ ) → ϕ. ) → ( ϕ. → ϕ →. ϕ ) → ϕ. → ϕ.
⊢
ϕ. → ( ϕ →. ϕ ) → ϕ. →
⊢(
ϕ. → ϕ →. ϕ ) → ϕ. → ϕ.
Alternatief bewijs voor ϕ → ϕ
⋮ ⊢(
⋮
ϕ. → ( ϕ →. ϕ ) → ϕ. ) → ( ϕ. → ϕ →. ϕ ) → ϕ. → ϕ.
ϕ. → ( ϕ →. ϕ ) → ϕ.
⊢
⋮
→ ⊢(
ϕ. → ϕ →. ϕ ) → ϕ. → ϕ.
⊢
ϕ. → ϕ →. ϕ →
⊢
ϕ. → ϕ.
λ-Calculus Γ, ϕ ⊢ ϕ
Γ, ϕ ⊢ ψ → Γ⊢ϕ→ψ
Γ⊢ϕ→ψ Γ⊢ϕ → Γ⊢ψ
λ-Calculus ϕ⊢
ϕ
Γ,
ϕ⊢
ψ
Γ⊢
Γ⊢
Γ,
ϕ→ψ
ϕ→ψ Γ⊢
Γ⊢ ψ
→
ϕ
→
λ-Calculus x.
Γ,
∶ϕ⊢
ϕ⊢
Γ, Γ⊢
Γ⊢
x.
∶ϕ
ψ ϕ→ψ
ϕ→ψ Γ⊢
Γ⊢ ψ
→
ϕ
→
λ-Calculus Γ,
x.
∶ϕ⊢
x.
∶ϕ
Γ,
x.
∶ ϕ ⊢ M.
∶ψ
Γ ⊢ λxϕ.. M ∶ ϕ → ψ
Γ⊢
ϕ→ψ Γ⊢
Γ⊢ ψ
→
ϕ
→
λ-Calculus Γ,
x.
∶ϕ⊢
x.
∶ϕ
Γ,
x.
∶ ϕ ⊢ M.
∶ψ
Γ ⊢ λxϕ.. M ∶ ϕ → ψ
Γ ⊢ M.
∶ϕ→ψ
Γ⊢
Γ ⊢ M .N ∶ ψ
N.
→
∶ϕ
→
Bewijs van ϕ → ϕ
ϕ⊢ ⊢
ϕ ϕ→ϕ
→
Bewijs van ϕ → ϕ
x. ⊢
∶ϕ⊢
ϕ ϕ→ϕ
→
Bewijs van ϕ → ϕ
x. ⊢
∶ϕ⊢
x.
∶ϕ
ϕ→ϕ
→
Bewijs van ϕ → ϕ
x.
∶ϕ⊢
x.
∶ϕ
⊢ λxϕ. . x ∶ ϕ → ϕ
→
Identiteitsfunctie
.
Bewijs van ϕ → ψ → ϕ
ψ, ϕ⊢ ⊢
ϕ⊢
ϕ ψ→ϕ
ϕ→ψ→ϕ
→
→
Bewijs van ϕ → ψ → ϕ
y.
∶ ψ, x.
⊢
x.
∶ϕ⊢
∶ϕ⊢
ϕ ψ→ϕ
ϕ→ψ→ϕ
→
→
Bewijs van ϕ → ψ → ϕ
y.
∶ ψ, x.
⊢
x.
∶ϕ⊢
∶ϕ⊢
x.
∶ϕ
ψ→ϕ ϕ→ψ→ϕ
→
→
Bewijs van ϕ → ψ → ϕ
y.
∶ ψ, x.
⊢
x.
∶ϕ⊢
x.
∶ϕ
∶ ϕ ⊢ λy ψ. . x ∶ ψ → ϕ ϕ→ψ→ϕ
→
→
Bewijs van ϕ → ψ → ϕ
y.
∶ ψ, x.
x.
∶ϕ⊢
x.
∶ϕ
∶ ϕ ⊢ λy ψ. . x ∶ ψ → ϕ
. ψ. x ∶ ϕ → ψ → ϕ ⊢ λxϕ . λy
→
→
Constante functie-functie
.
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
ϕ→ψ→χ Γ⊢
ϕ → ψ,
ϕ,
Γ⊢
ϕ →
ψ→χ Γ⊢ ϕ → ψ → χ,
ϕ→ψ→χ
Γ⊢
ϕ→ψ
Γ⊢
Γ⊢ ψ →
χ → ϕ→ψ⊢
ϕ→χ →
ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
ϕ →
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
ϕ→ψ→χ Γ⊢
x.
∶ ϕ,
g.
∶ ϕ → ψ,
Γ⊢
ϕ →
ψ→χ Γ⊢ f.
f.
∶ ϕ → ψ → χ,
g.
f.
Γ⊢
∶ϕ→ψ→χ
ϕ→ψ
Γ⊢
Γ⊢ ψ →
χ → ∶ϕ→ψ⊢
ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
ϕ →
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ Γ⊢
x.
∶ ϕ,
g.
∶ ϕ → ψ,
Γ⊢
ϕ →
ψ→χ Γ⊢ f.
f.
∶ ϕ → ψ → χ,
g.
f.
Γ⊢
∶ϕ→ψ→χ
ϕ→ψ
Γ⊢
Γ⊢ ψ →
χ → ∶ϕ→ψ⊢
ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
ϕ →
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ Γ⊢
x.
∶ ϕ,
g.
∶ ϕ → ψ,
Γ⊢
ϕ →
ψ→χ Γ⊢ f.
f.
∶ ϕ → ψ → χ,
g.
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ⊢
Γ⊢ ψ →
χ → ∶ϕ→ψ⊢
ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
ϕ →
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ Γ⊢
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
ψ→χ
∶ ϕ → ψ,
→
Γ⊢ f. f.
∶ ϕ → ψ → χ,
g.
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ⊢
Γ⊢ ψ →
χ → ∶ϕ→ψ⊢
ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
x.
∶ϕ
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
Γ ⊢ f .x ∶ ψ → χ
∶ ϕ → ψ,
→
Γ⊢ f. f.
∶ ϕ → ψ → χ,
g.
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ⊢
Γ⊢ ψ →
χ → ∶ϕ→ψ⊢
ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
x.
∶ϕ
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
Γ ⊢ f .x ∶ ψ → χ
∶ ϕ → ψ,
→
Γ⊢ f. f.
∶ ϕ → ψ → χ,
g.
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ⊢
Γ ⊢ g .x ∶ ψ
→
χ → ∶ϕ→ψ⊢
ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
x.
∶ϕ
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
Γ ⊢ f .x ∶ ψ → χ
∶ ϕ → ψ,
→
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ ⊢ g .x ∶ ψ
Γ ⊢ (f x) .(g x) ∶ χ f. f.
∶ ϕ → ψ → χ,
g.
∶ϕ→ψ⊢
Γ⊢ →
→ ϕ→χ →
∶ϕ→ψ→χ⊢
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
x.
∶ϕ
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
Γ ⊢ f .x ∶ ψ → χ
∶ ϕ → ψ,
→
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ ⊢ g .x ∶ ψ
Γ ⊢ (f x) .(g x) ∶ χ f. f.
∶ ϕ → ψ → χ,
∶ϕ→ψ→χ⊢
g.
Γ⊢
∶ ϕ → ψ ⊢ λxϕ . (f .x) (g x) ∶ ϕ → χ
→
→ →
(ϕ → ψ) → ϕ → χ →
⊢
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
x.
∶ϕ
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
Γ ⊢ f .x ∶ ψ → χ
∶ ϕ → ψ,
→
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ ⊢ g .x ∶ ψ
Γ ⊢ (f x) .(g x) ∶ χ f. f. ⊢
∶ ϕ → ψ → χ,
g.
Γ⊢
∶ ϕ → ψ ⊢ λxϕ . (f .x) (g x) ∶ ϕ → χ
→
→
∶ ϕ → ψ → χ ⊢ λg ϕ→ψ . λxϕ. . (f x) (g x) ∶ (ϕ → ψ) → ϕ → χ
→
(ϕ → ψ → χ) → (ϕ → ψ) → ϕ
→
x.
∶ϕ
→
Bewijs van (ϕ → ψ → χ) → (ϕ → ψ) → ϕ → χ Γ ∶=
Γ⊢
f.
∶ϕ→ψ→χ
x.
∶ ϕ,
g.
Γ⊢
x.
∶ϕ
Γ ⊢ f .x ∶ ψ → χ
∶ ϕ → ψ,
→
f.
Γ⊢
∶ϕ→ψ→χ
g.
∶ϕ→ψ
Γ ⊢ g .x ∶ ψ
Γ ⊢ (f x) .(g x) ∶ χ f. f.
∶ ϕ → ψ → χ,
g.
Γ⊢
∶ ϕ → ψ ⊢ λxϕ . (f .x) (g x) ∶ ϕ → χ
→
→
∶ ϕ → ψ → χ ⊢ λg ϕ→ψ . λxϕ. . (f x) (g x) ∶ (ϕ → ψ) → ϕ → χ
→
⊢ λf ϕ→ψ→χ . λg ϕ→ψ. . λxϕ . (f x) (g x) ∶ (ϕ → ψ → χ) → (ϕ → ψ) → ϕ
→
x.
∶ϕ
→
Fusiefunctie
.
Omwegen
ϕ⊢ ⊢
ϕ ϕ→ϕ
→
ϕ⊢
ϕ⊢ ϕ
ϕ
→
Omwegen
ϕ⊢ ⊢
ϕ ϕ→ϕ
→
ϕ⊢
ϕ⊢
ϕ⊢ ϕ
ϕ
ϕ
→
Omwegen x.
∶ϕ⊢
x.
∶ϕ
⊢ λxϕ. . x ∶ ϕ → ϕ
→
y.
∶ϕ⊢
y.
∶ ϕ ⊢ (λxϕ .. x) y ∶ ϕ
y.
∶ ϕ ⊢ x[ x .↦ y] ∶ ϕ
y.
∶ϕ
→
Omwegen ⋮ Γ,
x.
∶ ϕ ⊢ M.
∶ψ
Γ ⊢ λxϕ.. M ∶ ϕ → ψ Γ,
y.
Γ,
y.
→
y.
∶ϕ⊢
∶ ϕ ⊢ (λxϕ . .M ) y ∶ ψ
⋮ ∶ ϕ ⊢ M [ x. ↦ y] ∶ ψ
y.
∶ϕ
→
Omwegen ⋮ Γ,
x.
∶ ϕ ⊢ M.
∶ψ
Γ ⊢ λxϕ.. M ∶ ϕ → ψ
→
⋮ ∆⊢
. )N ∶ψ Γ, ∆ ⊢ (λxϕ . M
⋮ Γ, ∆ ⊢ M [ x .↦ N ] ∶ ψ
N.
∶ϕ
→
Evaluatie
(λxϕ. M ) N = M [ x ↦ N ]
Evaluatie
(λxϕ. M ) N Ð→ M [ x ↦ N ]
Kernbegrippen . Confluentie
.
.
Terminatie
. Betekenis
Bewijzen voor ϕ → ϕ S ∶= λf A→B→A . λg A→B . λxA . f x (g x), S K. K
K ∶= λpP . λq Q . p
Bewijzen voor ϕ → ϕ K ∶= λpP . λq Q . p (λf A→B→A . λg A→B .. λxA . f x (g x)) K K
Bewijzen voor ϕ → ϕ K ∶= λpP . λq Q . p . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ)
Bewijzen voor ϕ → ϕ K ∶= λpP . λq Q . p . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ) (λg ϕ→(ϕ→ϕ) . λxϕ . K x (g x)) K
Bewijzen voor ϕ → ϕ . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ) (λg ϕ→(ϕ→ϕ) . λxϕ . (λpP . λq Q . p) x (g x)) K
Bewijzen voor ϕ → ϕ . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ) (λg ϕ→(ϕ→ϕ) . λxϕ . (λpϕ . λq ϕ→ϕ . p) x (g x)) K
Bewijzen voor ϕ → ϕ . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ) (λg ϕ→(ϕ→ϕ) . λxϕ . (λpϕ . λq ϕ→ϕ . p) x (g x)) K
(λg ϕ→(ϕ→ϕ) . λxϕ . (λq ϕ→ϕ . x) (g x)) K
Bewijzen voor ϕ → ϕ . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ) (λg ϕ→(ϕ→ϕ) . λxϕ . (λpϕ . λq ϕ→ϕ . p) x (g x)) K
(λg ϕ→(ϕ→ϕ) . λxϕ . (λq ϕ→ϕ . x) (g x)) K
(λg ϕ→(ϕ→ϕ) . λxϕ . x) K
Bewijzen voor ϕ → ϕ . . λxϕ . f x (g x)) K K (λf ϕ→(ϕ→ϕ)→ϕ . λg ϕ→(ϕ→ϕ) (λg ϕ→(ϕ→ϕ) . λxϕ . (λpϕ . λq ϕ→ϕ . p) x (g x)) K
(λg ϕ→(ϕ→ϕ) . λxϕ . (λq ϕ→ϕ . x) (g x)) K
(λg ϕ→(ϕ→ϕ) . λxϕ . x) K λxϕ . x
Gelijkheid
.
Curry-Howard correspondentie
type λ-term redex bewoning
formule bewijs omweg bewijsbaarheid
Samuel Eilenberg & Saunders Mac Lane
.
.
Categoriëen .
. .
.
.
Categoriëen .
f
g
. .
.
h
.
Categoriëen .
idY
f
idX
. .
g
.
h
.
idZ
idR
Categoriëen Y .
idY
f
idX
X .
g R
.
.
h Z .
idZ
idR
Categoriëen Y .
idY
f
idX
X .
g R
.
.
gf h Z .
idZ
idR
Verzamelingen
Verzamelingen & Functies
Verzamelingen
Verzamelingen & Bijecties
Verzamelingen
Verzamelingen & Relaties
Syntactische Categorie
Curry-Howard correspondentie
type λ-term redex bewoning
formule bewijs omweg bewijsbaarheid
Curry-Howard correspondentie
type λ-term redex bewoning
formule bewijs omweg bewijsbaarheid
object pijl gelijkheid verbondenheid
To e p as s i n g
Bewijsassistenten
Coq
Bewijsassistenten
Coq Inductive
Bewijsassistenten
Coq Inductive Calculus of Constructions
Bewijsassistenten
Coq Inductive Calculus of Constructions Demo
Coq identiteisbewijs
Lemma I:A -> A. intro hypothese. apply hypothese. Qed.
Afbeeldingen ▸
Alonzo Church: University of St. Andrews
▸
Barkley Rosser: Society for Industrial and Applied Mathematics
▸
Emmy Noether: Physikerinnen.de
▸
Emil Leon Post: University of St. Andrews
▸
Samuel Eilenberg: Oberwolfach Photo Collection
▸
Saunders Mac Lane: Oberwolfach Photo Collection
▸
Schönfinkel’s combinatoren, University of Lethbridge, Works of Haskell Curry collection
