Incomparable consistency strengths

[Anton Freund]

> Can anyone give explicitly (not merely prove they exist, but actually give
> the axioms or schemes in a level of specificity and detail typical of
> published math papers) two axiomatized theories A and B such that
> 1) ZF proves Con(A)
> 2) ZF proves Con(B)
> 3) PA does not prove Con(A)->Con(B)
> 4) PA does not prove Con(B)->Con(A)

In Section II of the following paper there is an example of A and B that
satisfy 3) and 4) (but not 1) and 2), because the theories involve large
cardinals):

Kai Hauser & W. Hugh Woodin, Strong Axioms of Infinity and the Debate
About Realism, Journal of Philosophy 111 (8):397-419 (2014),
https://doi.org/10.5840/jphil2014111828.

Specifically, let MC and MC2 be the assertions that there are at least one
resp. two measurable cardinals. In the cited paper, A is the extension of
ZFC by MC; and B is the extension by the statement "if ZFC+MC2 proves no
contradiction in k steps, then A=ZFC+MC proves no contradiction in
2^(2^(2^k)) steps".

Best,
Anton