2 added 27 characters in body

The order $\le_{cons}$ isn't linear. There are Godel Lob provability logic $GL$. It's a modal logic with one modality. $GL$ is complete with respect to arithmetic semantic. It was shown by Solovay. Formula $(\diamond \square(\Diamond p \to \diamond Diamond q) \lor (\diamond \square(\Diamond q \to \diamond Diamond p)$ is not theorem of $GL$. So by completeness theorem (it can be proved for $ZF$) there are propositions $A$ and $B$ such that $$ZF ZF \not\vdash not \vdash (Con({\ulcorner} A{\urcorner}) \to Con({\ulcorner} B{\urcorner})) B{\urcorner})) and ZF\not \lor vdash (Con({\ulcorner} B{\urcorner}) \to Con({\ulcorner} A{\urcorner}))$$ A{\urcorner}))$But such$A$and$B$provided by Solovay proof are complex. I don't know any "natural" example. 1 The order$\le_{cons}$isn't linear. There are Godel Lob provability logic$GL$. It's a modal logic with one modality.$GL$is complete with respect to arithmetic semantic. It was shown by Solovay. Formula$(\diamond p \to \diamond q) \lor (\diamond q \to \diamond p)$is not theorem of$GL$. So by completeness theorem (it can be proved for$ZF$) there are propositions$A$and$B$such that $$ZF \not\vdash (Con({\ulcorner} A{\urcorner}) \to Con({\ulcorner} B{\urcorner})) \lor (Con({\ulcorner} B{\urcorner}) \to Con({\ulcorner} A{\urcorner}))$$ But such$A$and$B\$ provided by Solovay proof are complex. I don't know any "natural" example.