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.