proofs in first-order logic
(2.8 hours to learn)
One can prove statements in first-order logic using a formal deductive calculus. Such a formal proof system is a central tool in the foundations of mathematics, since it serves as a formal model of mathematical reasoning more generally.
This concept has the prerequisites:
- first-order logic
- propositional proofs (The reasoning steps for propositional logic are included in the reasoning steps for FOL.)
- Be able to prove statements in a formal first-order proof system.
Core resources (read/watch one of the following)
→ Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
- This actually covers relational logic, but at the level of this concept node, most of the ideas are the same. See the bonus lecture "First order logic (a very brief introduction)" for an explanation of the differences.
- Click on "Preview" to see the videos.
→ The Language of First-Order Logic
An undergraduate logic textbook aimed at philosophers, with an educational software package.
- Section 5.10, "Methods of proof," pages 135-144
- Section 5.11, "Formal proofs," pages 144-150
- Section 6.7, "Methods of proof involving mixed quantifiers," pages 172-177
- Section 6.8, "Formal proofs," pages 177-181
Supplemental resources (the following are optional, but you may find them useful)
→ A Course in Mathematical Logic
A graduate textbook in mathematical logic.
Location: Section 3.1, "The first-order predicate calculus," pages 108-115
→ A Mathematical Introduction to Logic
An undergraduate textbook in mathematical logic, with proofs.
Location: Section 2.4, "A deductive calculus," up through subsection "Tautologies," pages 109-116
- structural induction
- This resource is more mathematically rigorous than the others. It's useful if you're already comfortable writing proofs in FOL and want to analyze the proofs themselves.
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation