Large-cardinal implication and consistency ledger

A supercompact kappa has a normal fine complete measure at every lambda>=kappa by its definition and F1. Forgetting normality gives the fine measures of F2, hence strong compactness. For a strongly compact kappa, consider the co-small filter $\{X\subseteq \kappa :\mathrm{\mid }\kappa \setminus X\mathrm{\mid }<\kappa \}$. It is proper and kappa-complete: a fewer-than-kappa union of small complements remains small by regularity and F7. Extend it by the defining property in F8. The extension contains every singleton complement, so contains no singleton and is nonprincipal. It is a kappa-complete ultrafilter on uncountable kappa, witnessing measurability.

F3 gives measurable implies weakly compact, and F4 gives weakly compact implies Mahlo. A Mahlo cardinal is inaccessible by the definition used in F4. These complete the displayed chain; all are implications about the same cardinal. If an inaccessible exists, F5 supplies its nonempty transitive V_kappa set model, and F6 gives Con(ZFC) in the ambient theory. This conditional conclusion does not assert that its inaccessible hypothesis is consistent.

For any adjacent arrow, let P and Q be the first-order cardinal properties at its stronger and weaker ends, expressed through the stated set-measure definitions when appropriate. The argument gives a finite ZFC proof of $(\mathrm{\exists }\kappa P(\kappa ))\to (\mathrm{\exists }\kappa Q(\kappa ))$. If the weaker extension of ZFC had a finite refutation, prepend this implication proof and the stronger existence axiom, and replace every use of the weaker existence axiom by its derived conclusion. The result is a finite refutation of the stronger extension. Contraposition gives Con(stronger) implies Con(weaker), and composing these transformations gives the nonadjacent implications. This is a transformation of finite proofs, not an assertion of any Con premise or a converse.