 Moreover there is also an issue with primeness in the sense of the proof-theoretic property (which intuitionist logic satisfies) that when \(\vdash\) A \(\vee\) B then either \(\vdash\) A or \(\vdash\) B. Classical theories typically do not have this property and this will pose problems for generalising the CH correspondence and for justifying excluded middle (assuming the formalist does not simply take all non-trivial calculi as legitimate without need of justification). If correctness of a mathematical claim, relative to a particular framework, is identified with provability and if a disjunction can be correct where neither disjunct is provable then the formalist would seem to require some fancy footwork—supervaluationalism is not obviously appropriate here—to justify using classical logic. 