# proofs in first-order logic

(2.8 hours to learn)

## Summary

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.

## Context

This concept has the prerequisites:

- first-order logic
- propositional proofs (The reasoning steps for propositional logic are included in the reasoning steps for FOL.)

## Goals

- Be able to prove statements in a formal first-order proof system.

## Core resources (read/watch one of the following)

## -Free-

→ Coursera: Introduction to Logic (2014)

An introductory logic course geared towards computer scientists.

Other notes:

- 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.

## -Paid-

→ 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)

## -Paid-

→ 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

Additional dependencies:

- structural induction

Other notes:

- 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.

## See also

-No Additional Notes-