Proof theory · Definition

Formal proof

logicproofs

Before you start you need to know

A formal proof is a sequence of checkable steps that leads from the premises to the conclusion.

Definition

A formal proof of \(\varphi_n\) is a sequence \(\varphi_1,\ldots,\varphi_n\) in which each term is an axiom, an admitted hypothesis, or the result of a rule applied to earlier terms.

\[\varphi_1,\varphi_2,\ldots,\varphi_n\vdash\varphi_n\]

Each line of a formal proof must be an axiom, an allowed hypothesis or the result of applying a rule to earlier lines, so that anyone can check it step by step.

Guiding example: from the hypotheses \(P\) and \(P\to Q\) we obtain \(Q\). The proof has three lines: \(P\), \(P\to Q\) and \(Q\), the last justified by modus ponens on the two previous ones.

Typical error: writing a line without justification because it seems obvious. A jump from \(P\) to \(Q\) without a rule leaves a gap, and the proof stops being formal.

Think about it

Can a correct conclusion be part of a proof if it is not justified?

No. A formal proof also requires justifying the steps that lead to a true conclusion.

Exercises 10

  1. A formal proof is a...
  2. Each line of a formal proof must be...
  3. The last line of a proof is usually...
  4. A formal proof depends on...
  5. Which step does not belong to a formal proof?
  6. A formal proof is a sequence of...
  7. The first step of a proof can be...
  8. A line of a proof must be justifiable by...
  9. A formal proof has the lines \(P\to Q\) and \(P\), both allowed hypotheses. Which line can legitimately be added?
  10. If a proof jumps from P to Q without a rule that allows it, then...

References

  • Frederic P. Schuller, Lectures on the Geometrical Anatomy of Theoretical Physics · Lecture 1, Introduction / Logic of Propositions and Predicates, YouTube, 2015.