Conditional independence of SH

By the given consistency hypothesis and [F1], ZFC+SH has no certified finite refutation. By [F2], ZFC+$\mathrm{\neg }$SH has no certified finite refutation. These are external conclusions about the two fixed proof predicates; the weaker first supplier prevents promoting this conjunction to a new PA theorem here.

Suppose that $d$ were a certified ZFC proof of SH. Every ZFC axiom and logical inference used by $d$ is also available in ZFC+$\mathrm{\neg }$SH. Regard $d$ as a derivation in that extension, append its one added axiom $\mathrm{\neg }$SH, and then append a fixed propositional derivation of the chosen contradiction from SH and $\mathrm{\neg }$SH. This would be a certified finite ZFC+$\mathrm{\neg }$SH refutation, contrary to step 1.1. Hence $\mathrm{Z}\mathrm{F}\mathrm{C}⊬\mathrm{S}\mathrm{H}$.

Conversely, suppose that $e$ were a certified ZFC proof of $\mathrm{\neg }$SH. View $e$ in ZFC+SH, append the single added SH axiom, and use the same fixed propositional contradiction block with its two premises interchanged. This would refute ZFC+SH, again contradicting step 1.1. Hence $\mathrm{Z}\mathrm{F}\mathrm{C}⊬\mathrm{\neg }\mathrm{S}\mathrm{H}$.

Steps 1.1-2.2 give both consistency conclusions and both non-derivability conclusions under external $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})$. The argument transforms only actual certified finite proofs. Malformed codes do not satisfy the proof predicate, and the empty line sequence is not silently treated as a refutation. Each hypothetical non-derivability witness uses exactly one occurrence of the opposite extension's added axiom; no set-theoretic choice is made in either proof splice.