Logic and Modeling 2021: Lectures

• Lecture 1
• All videos
• Video 1: Introduction
• Video 2: Course motivation
• Video 3: A logic puzzle
• Video 4: Syntax of propositional logic
• Video 5: Inference rules for implication
• Video 6: Inference rules for conjunction
• Video 7: Natural deduction with implies
• Video 8: Natural deduction with and and implies
• Video 9: Lecture 1 Q&A, Tuesday 30 March
• Lecture 2
• All videos
• Video 1: Negation and falsity
• Video 2: Disjunction
• Video 3: Derivation example
• Video 4: Derivation example
• Video 5: proof by contradiction
• Video 6: strategy for natural deduction
• Video 7: one more or elimination rule
• Video 8: Lecture 2 Q&A, Thursday 1 April
• Lecture 3
• All videos
• Video 1: Syntax and Semantics
• Video 2: Interacting with Lean
• Video 3: and, implies, and not in Lean
• Video 4: First examples of Lean proofs
• Video 5: Negation in Lean
• Video 6: More intro and elim rules in Lean
• Video 7: or elimination and proof by contradiction examples
• Lecture 4
• All videos
• Video 1: Classical vs intuitionistic reasoning
• Video 2: Proving the law of the excluded middle
• Video 3: Proving double negation elimination
• Video 4: Truth and valuation functions
• Video 5: Motivating the semantics of implication
• Video 6: Truth tables
• Video 7: Soundness and completeness
• Lecture 5
• All videos
• Video 1: Intro to first order (predicate) logic
• Video 2: Syntax of first order logic
• Video 3: The universal quantifier
• Video 4: The existential quantifier
• Video 5: Natural deduction with the universal quantifier
• Video 6: Natural deduction with the existential quantifier
• Lecture 6
• All videos
• Video 1: Relativized quantifiers and counterexamples
• Video 2: Natural deduction example
• Video 3: Another natural deduction example
• Video 4: One more natural deduction example
• Video 5: Equality in first order logic
• Video 6: Syntax of first order logic in Lean
• Video 7: Quantifier rules in Lean
• Lecture 7
• All videos
• Video 1: syntax and semantics, revisited
• Video 2: first order models
• Video 3: interpreting unquantified formulas
• Video 4: interpretation of quantifiers
• Video 5: semantic entailment
• Lecture 8
• All videos
• Video 1: semantic equivalence
• Video 2: satisfiability, validity, consistency
• Video 3: FOL translations and interplay of quantifiers
• Video 4: equality in Lean
• Video 5: rewrite and calc mode
• Video 6: calc and rewrite on the integers
• Lecture 9
• All videos
• Video 1: partial orders
• Video 2: strict orders
• Video 3: minimal and smallest elements
• Video 4: equivalence relations
• Lecture 11
• All videos
• Video 1: modal logic intro
• Video 2: Kripke models
• Video 3: interpreting diamond and box
• Video 4: truth in a model
• Video 5: modal entailment, validity, equivalence
• Video 6: examples of determining truth at worlds
• Lecture 12
• All videos
• Video 1: changing labeling functions
• Video 2: frames and characterizing properties
• Video 3: different kinds of relations
• Video 4: reflexive frames
• Video 5: correspondences and transitive frames
• Lecture 13
• All videos
• Video 1: soundness and completeness of FOL
• Video 2: consistency theorem
• Video 3: compactness
• Video 4: infinite and finite model definability (1)
• Video 5: infinite and finite model definability (2)
• Video 6: reachability by a binary relation
• Lecture 14
• All videos
• Video 1: decision problems
• Video 2: the halting problem
• Video 3: the Post Correspondence Problem
• Video 4: undecidability of validity
• Video 5: Godel's incompleteness theorem
• Lecture lean_extras
• All videos
• Video 1: automation
• Video 2: properties of programs
• Video 3: a simple database example