Can The Classical Ladder Be Kicked Away? The View from One Rung Up

Nonclassical logicians often justify their use of classical logic in their metatheoretic reasoning as, to put things in Bob Meyer’s evocative phrasing, “preaching in Classicalese to the Classicalists”. For this justification to be sufficient to allow for these metatheoretic results to bear philosophical weight, they should at least provide evidence that such results can be reproduced in a resolutely nonclassical metatheory. Using as a case study an intuitionistic variant of a class of soundness and completeness results due to Andrew Bacon, which push the use of classical reasoning ‘one rung up’ the metatheoretic ladder, from the metalanguage into the metametalanguage, we show that this is not the case.