The Church–Fitch knowability paradox in the light of structural proof theory

Anti-realist epistemic conceptions of truth imply what is called the know-
ability principle: All truths are possibly known. The principle can be formalized in
a bimodal propositional logic, with an alethic modality ♦ and an epistemic modality
K, by the axiom scheme A ⊃ ♦KA (KP). The use of classical logic and minimal
assumptions about the two modalities lead to the paradoxical conclusion that all truths
are known, A
⊃ KA (OP). A Gentzen-style reconstruction of the Church–Fitch par-
adox is presented following a labelled approach to sequent calculi. First, a cut-free
system for classical (resp. intuitionistic) bimodal logic is introduced as the logical
basis for the Church–Fitch paradox and the relationships between
K and ♦ are taken
into account. Afterwards, by exploiting the structural properties of the system, in
particular cut elimination, the semantic frame conditions that correspond to KP are
determined and added in the form of a block of nonlogical inference rules. Within
this new system for classical and intuitionistic “knowability logic”, it is possible to
give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to con-
firm that OP is only classically derivable, but neither intuitionistically derivable nor
intuitionistically admissible. Finally, it is shown that in classical knowability logic,
the Church–Fitch derivation is nothing else but a fallacy and does not represent a real
threat for anti-realism.