Forwards Reasoning Link to heading

We start with axioms, and step by step build up a proof until we reach the desired conclusion.

Example in Gentzen’s LK:

  1. We start with a single axiom: \(A \vdash A\).
    It means: any formula implies itself, so this sequent is always true.
  2. We apply the left introduction for conjunction rule: \(\displaystyle \cfrac{\Gamma, A \vdash \Delta}{\Gamma, A \land B \vdash \Delta} \quad (\land L_1)\)
    We get: \(\displaystyle A \land B \vdash A\)

We started from axioms or known facts and builded towards the conclusion. We applied \(\land L_1\) directly on the axiom.

Backwards Reasoning Link to heading

Backwards reasoning/proof means that we start with the statement we want to prove and try to simplify it step by step until we reach an axiom.

Example in Gentzen’s LK:

  1. We start with \(\displaystyle A \land B \vdash A\), we need to reach axiom \(A \vdash A\)
  2. We apply the left conjunction rule: \(\displaystyle \cfrac{\Gamma, A \vdash \Delta}{\Gamma, A \land B \vdash \Delta} \quad (\land L_1)\)
    This rule allows us to move from \(A \land B \vdash A\) to \(A \vdash A\).
    The reasoning is that, if we can derive \(A\) from \(A\), then we can also derive \(A\) from \(A \land B\).
  3. So, applying \(\land L_1\) directly we get \(A\vdash A\)

We started from the goal and worked backward. We used \(\land L_1\)​ to simplify the goal and the completed the proof by reaching our axiom.