Limity formálních systémů, důkazů a výpočtů
Jan Křetínský
IV134 Fl MU Podzim 2024
IV134
2/10
► language: Czech/English
► voluntary course
► lecture on Monday, 10-12 or 12-14.
► Gödel, Escher, Bach: an Eternal Golden Braid by Douglas R. Hofstadter
► story of "strange loops" as limits of mathematics and computer science and foundations of intelligence
Frederick the Great Leonhard Euler, ..., J.S. Bach improvised 6-part fugue canons
Bach
3/10
► Frederick the Great
► Leonhard Euler, ..., J.S. Bach
► improvised 6-part fugue
► canons
Frederick the Great Leonhard Euler, ..., J.S. Bach improvised 6-part fugue canons
► copies differing in time, pitch, speed, direction (upside down, crab)
► isomorphic
► multiple meanings of each note
► canon endlessly rising in 6 steps - "strange loop"
Escher
4/10
"Waterfall"
6-step endlessly falling loop
Escher
4/10
"Ascending and Descending" illusion by Roger Penrose
Escher
4/10
Penrose triangle
Faculty of Informatics, Brno
Escher
4/10
"Drawing hands" his first strange loop
Escher
4/10
"Metamorphosis" copies of one theme
ASP
Ä;
Gödel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
Godel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
► mathematical reasoning in exploring mathematical reasoning
► Incompleteness theorem:
All consistent axiomatic formulations of number theory include undecidable propositions.
► strange loop in the proof
Godel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
► mathematical reasoning in exploring mathematical reasoning
► Incompleteness theorem:
All consistent axiomatic formulations of number theory include undecidable propositions.
► strange loop in the proof
► statement about numbers can talk about itself
"This statement of number theory does not have any proof"
Godel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
► mathematical reasoning in exploring mathematical reasoning
► Incompleteness theorem:
All consistent axiomatic formulations of number theory include undecidable propositions.
► strange loop in the proof
► statement about numbers can talk about itself
"This statement of number theory does not have any proof"
code
► numbers <-> statements
Godel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
► mathematical reasoning in exploring mathematical reasoning
► Incompleteness theorem:
All consistent axiomatic formulations of number theory include undecidable propositions.
► strange loop in the proof
► statement about numbers can talk about itself
"This statement of number theory does not have any proof"
code
► numbers <-> statements 215473077557
Godel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
► mathematical reasoning in exploring mathematical reasoning
► Incompleteness theorem:
All consistent axiomatic formulations of number theory include undecidable propositions.
► strange loop in the proof
► statement about numbers can talk about itself
"This statement of number theory does not have any proof"
code
► numbers <-> statements 215473077557 is in binary
0011001000101011001100100011110100110101
Godel
5/10
► Brno
► Epimenides paradox: "All Cretans are liars"
► mathematical reasoning in exploring mathematical reasoning
► Incompleteness theorem:
All consistent axiomatic formulations of number theory include undecidable propositions.
► strange loop in the proof
► statement about numbers can talk about itself
"This statement of number theory does not have any proof"
code
► numbers <-> statements 215473077557 is in binary
0011001000101011001100100011110100110101 read as ASCII 2+2=5
► homework:
34723379178930453204433293597543819411782291432109326918654063662
Mathematical logic
6/10
► different geometries, equally valid
► real world?
► proof?
► David Hilbert: consistency and completeness
► Russel's paradox
Mathematical logic
6/10
► different geometries, equally valid
► real world?
► proof?
► David Hilbert: consistency and completeness
► Russel's paradox
► "ordinary" sets: x $ x
► "self-swallowing" sets: x ex
► R = set of all ordinary sets
Mathematical logic
6/10
► different geometries, equally valid
► real world?
► proof?
► David Hilbert: consistency and completeness
► Russel's paradox
► "ordinary" sets: x & x
► "self-swallowing" sets: x ex
► R = set of all ordinary sets
► Grelling's paradox
► self-descriptive adjectives ("pentasyllable") vs non-self-descriptive
► what about "non-self-descriptive"?
► self-reference drawing hands
The following sentence is false. The preceding sentence is true.
Way out?
7/10
► prohibition (Principia mathematica)
► types, metalanguage
► "In this lecture, I criticize the theory of types" cannot discuss the type theory
Computers
8/10
► Babbage
The course through which I arrived at it was the most entangled and perplexed which probably ever occupied the human mind.
Ada Lovelace (daughter of Lord Byron)
Mechanized intelligence
"Eating its own tail" (altering own program)
► axiomatic reasoning, mechanical computation, psycholgy of intelligence
► Alan Turing ~ Godel's counterpart in computation theory Halting problem is undecidable.
Can intelligent behaviour be programmed? Rules for inventing new rules...
Strange loops in the core of intelligence
► materialism, de la Metrie: L'homme machine
Formal system
9/10
Example (over alphabet M, I, U)
► initial string ("axiom"):
► MI
► rules ("inference/production rules") to enlarge your collection (of "theorems")
requirement of formality: not outside the rules
► last letter I => put U at the end
► Mx => Mxx where x can be any string
► replace III by U
► dropUU
Homework: Can you produce/derive/prove MU ?
► Which rule to use? That's the art.
Theorems of MIU system
10/10
Axiom: MI Rules:
1. xl => xIU
2. Mx => Mxx
3. xllly => xUy
4. xUUy => xy