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.
|
2 | added 27 characters in body | ||
|
|
||||
|
|
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. |
||||
