Matematická logika

Materiály

Prerekvizity:

• Skriptá doc. Tomana
• Poznámky z prednášok Úvod do matematickej logiky

1. prednáška:

• logika 2. rádu
• deskriptívna zložitosť
• nerozhodnuteľnosť platnosti a splniteľnosti formuly vo FOL
• monadické logiky
• Beginning Mathematical Logic: A Study Guide (časti 3.1, 3.2, 3.3, 4.1, 4.2)
• prezentácia

2.–4.prednáška:

• Švejdar: Logika --- neúplnost, složitost a nutnost (kap. 3.2.1)

5. prednáška:

• Robinsonova aritmetika
• Smith: Godel Without (Too Many) Tears (kap. 6)

6. prednáška:

• Peanova aritmetika, hierarchia formúl
• Smith: Godel Without (Too Many) Tears (kap. 7, 8)

7. prednáška:

• primitívne rekurzívne funkcie
• Smith: Godel Without (Too Many) Tears (kap. 9, 10 okrem detailov beta-kódovania v 10.2 a 10.3, 11.1 až 11.3)

8. prednáška:

• Prvá Godelova veta o neúplnosti
• Smith: Godel Without (Too Many) Tears (kap. 11, 12, 13)

Lean materials

• Introductory slides (53 to 62): p1.pdf
• Ilustracia taktik: lean-tactics.pdf
• GlimpseOfLean: run via https://live.lean-lang.org/#project=GlimpseOfLean --- the links given in the tutorial are broken, but when you copy-paste raw lean content, it works
  1. Introduction
  2. Rewriting
  3. Iff
  4. Forall
  5. Exists
• grind tactic
• Amazon usage
• Cedar (see section A quick tour of modeling and verifying Cedar with Lean)
• If it compiles, it is correct (zero-knowledge proofs)
• kniha Theorem Proving in Lean 4: kap. 2, 3.2
• Interaktívne tutoriály:
  • modus ponens
  • "Rules" near upper right corner on the first page: use "none" to skip levels and have more tactics available
  • Vpravo hore sa da prepinat zobrazenie ("typewriter mode")
  • Reintroduction to proofs Proofs: Type world, Implication world; Function world (robit dokazy cez intro aj priamou konstrukciou lambda funkcii: fun x y => x + y); Quantifier world; Advanced functions world level 6
  Natural numbers world level 7 (induction)
• ukážky: ako písať verifikovateľné programy v Lean
• kniha The Hitchhiker's Guide to Logical Verification (2026)
  • Even if we try to restrict ourselves to a fragment of Lean's language, Lean often exposes us to more advanced constructs in the output, such as ?m.2396 and ?m.2397 above. Our advice is to adopt a sporty attitude: Do not worry if you do not always understand everything the first time. Use your common sense and your imagination. And, above all, do not hesitate to ask.
  • At this point, you might wonder, “So what does simp do exactly?” Of course, you could study the source code or look up the scientific literature. But this might not be the most efficient use of your time. In truth, even expert users of proof assistants do not fully understand the behavior of the tactics they use daily. The most successful users adopt a relaxed, sporty attitude, trying tactics in sequence and studying the emerging subgoals, if any, to see if they are on the right path.
• kniha Logic and Proof
• Programovanie v Lean 4
• zoznam materialov