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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s