# Disproof of a conjecture by Setzer (2008)

Conjecture: If your password is not correct, you will be redirected to a non-existing page (Setzer 2008).

Disproof. Formalise as $$\forall x : P.~\neg C(x) \rightarrow R(x)$$. We want to prove $$(\forall x : P.~\neg C(x) \rightarrow R(x)) \rightarrow \bot$$, where $$P$$ is the type of passwords, $$C(x)$$ is true iff $$x$$ is the correct password and $$R(x)$$ means we are redirected to a void by $$x$$.

Suppose $$\forall x : P.~\neg C(x) \rightarrow R(x)$$. $$\neg C(\mbox{../../..’})$$ holds, where $$\mbox{../../..’} : P$$, thus we must have $$R(\mbox{../../..’})$$. However by the true constructive meaning of $$R$$, namely typing the password into the form and observing the result—redirection to http://www.cs.swan.ac.uk/~csetzer/index.html—we can conclude $$\neg R(\mbox{../../..’})$$, which may be written $$R(\mbox{../../..’}) \rightarrow \bot$$. From $$R(\mbox{../../..’})$$ and $$R(\mbox{`../../..’}) \rightarrow \bot$$ we get $$\bot$$ by arrow-elimination, thus we can discharge our assumption. QED.