Recipe

Check or write one line of a proof

Use when: you are reading someone's proof and need to confirm a line, or writing a line of your own and need its citation

Goal: a line whose citation names a rule, cites earlier available lines of the right shapes, and produces exactly the sentence written

Taught in Proof format: lines, premises, and citations

1. 1

   Look at the citation and find the rule it names. Recall what that rule cites and what it writes, from the table of rules.

   Example

   "\toE 1, 3" names \toE, which cites a conditional A \to B and its antecedent A, and writes B.

   Why: every rule is a fixed pattern, so you can't check a line until you know which pattern it claims to follow.

2. 2

   Every cited number must be smaller than the line's own number. A premise (PR) or assumption (AS) cites nothing at all.

   • a cited line is below the citing line — the line is wrong, whatever it says.
   • the rule cites a subproof — the citation is a range like 3–5, covering the whole subproof.

   Why: a proof is checked from the top down, so a line can only rest on lines already checked.

3. 3

   Find the main connective of each cited line. It must be the connective the rule works on.

   Example

   For \toE 1, 3 with line 1 P \to Q and line 3 P: line 1's main connective is \to, and line 3 is its antecedent P, symbol for symbol.

   Why: rules act on whole lines through their main connective, never on a piece buried inside.

4. 4

   Compare the line's sentence with what the rule produces from those cited lines.

   Example

   \toE on P \to Q and P produces Q. Writing Q \wedge P there would be wrong even though Q is in it.

   Why: a rule licenses one particular sentence, and anything else needs its own step.