What is a Formal Proof?

This lecture introduces the concept of a formal proof system, defining it as a set of logical formulas with inference steps. It explains the structure of a proof in a proof system and how proofs can be viewed as directed acyclic graphs. An example system for propositional logic is presented, along with exercises to draw DAGs representing proofs. The lecture covers the soundness of a proof system, derivations from assumptions, semantic consequences, and the importance of sound inference rules in ensuring the validity of formulas.