# 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.