1

(I'm posting this question with my own answer, to show a nice calculational proof for one of the examples in Luke Palmer's blog post Follow Your Nose Proofs.)

In what follows, $A$ and $B$ are sets, with $f,g : A \rightarrow B$ and $h : B \rightarrow A$, and $x \in A$ and $y \in B$.

Given the following definitions: $$ \begin{align} (0) & f \textrm{ is surjection} \;\equiv\; \langle \forall y :: \langle \exists x :: f(x) = y \rangle \rangle \\ (1) & f = g \;\equiv\; \langle \forall x :: f(x) = g(x) \rangle \\ (2) & (h \circ g)(x) \;=\; h(g(x)) \\ (3) & \textrm{Id}_A(x) \;=\; x \\ \end{align} $$ prove that $$ \begin{align} (4) & \langle \exists h :: f \circ h = \textrm{Id}_B \rangle \;\Rightarrow\; f \textrm{ is surjection} \end{align} $$

MarnixKlooster ReinstateMonica
  • 5,576

1 Answers1

0

Looking at the given definitions, we see that the expression $f \circ h = \textrm{Id}_B$ uses the terms defined in definitions (1), (2), and (3). So our straightforward strategy is first to expand these, and see where that leads us.

So we calculate: $$ \begin{align} & f \circ h = \textrm{Id}_B \\ \equiv & \;\;\;\;\;\text{"expand $=$ using definition (1)"} \\ & \langle \forall y :: (f \circ h)(y) = \textrm{Id}_B(y) \rangle \\ \equiv & \;\;\;\;\;\text{"expand $\circ$ using definition (2); expand $\textrm{Id}$ using definition (3)"} \\ & \langle \forall y :: f(h(y)) = y \rangle \\ (*) \equiv & \;\;\;\;\;\text{"logic: one-point rule -- working towards the RHS of definition (0)"} \\ & \langle \forall y :: \langle \exists x : x = h(y) : f(x) = y \rangle \rangle \\ \Rightarrow & \;\;\;\;\;\text{"logic: weaken range of $\exists$"} \\ & \langle \forall y :: \langle \exists x :: f(x) = y \rangle \rangle \\ \equiv & \;\;\;\;\;\text{"definition (0)"} \\ & f \textrm{ is surjection} \end{align} $$

Note how almost every step is of the 'there is really only one thing you can do' variety. The only 'creative' step is $(*)$, but also that step is directly guided by the shape for the formulae, in this case the shape of the RHS of (0).

Calculational proofs which mostly consist of such formula-driven steps are essentially the same proofs which Luke Palmer calls 'follow your nose proofs'.

Now we have the essence of the proof, and there are several ways to formally wrap it up, for example as follows: $$ \begin{align} & \langle \exists h :: f \circ h = \textrm{Id}_B \rangle \;\Rightarrow\; f \textrm{ is surjection} \\ \equiv & \;\;\;\;\;\text{"logic, allowed because the RHS does not contain $h$} \\ & \;\;\;\;\;\;\text{ -- to bring the beginning and the end of our previous calculation together"} \\ & \langle \forall h :: f \circ h = \textrm{Id}_B \;\Rightarrow\; f \textrm{ is surjection} \rangle \\ \equiv & \;\;\;\;\;\text{"the above calculation"} \\ & \textrm{true} \\ \end{align} $$

(See the end of my answer https://math.stackexchange.com/a/332186/11994 for references about this calculational proof style.)

Community
  • 1
MarnixKlooster ReinstateMonica
  • 5,576