Proof-theoretic consequence characterises the notion of logical consequence in PL syntactically and it is that relation of syntactical consequence which the turnstile represents. Polish formal logician Jan Lukasiewicz’s objection to the classical view was endorsed and developed slightly differently by another important formal logician, Arend Heyting, who proposed a distinct three-valued account. Given that PL is bivalent we know that each atomic formula of PL can only be true or false. However, this is not the end of the matter but only the beginning. In more formal terms, the overall truth-value of any compound formula of PL is said to be a function of the truth-values of its component parts. Just as PL is of great interest, importance and practical utility as an autonomous formal language independent of any natural language so too ‘&’ is of interest and importance just in itself.