More specifically, in FOL, given any theory $\Sigma$ of sentences, are there disjunctions $\varphi=P \vee Q$ such that:
- $\varphi$ is not provable from any single sentence of $\Sigma$ . So its not logically equivalent to an axiom.
- $\emptyset \not \vdash \varphi $. This is implied by 1. but I want to emphasize that it's not a logical truth.
- $\Sigma \not \vdash P$ and $\Sigma \not \vdash Q$. So they are not individually provable.
- $\Sigma \not\vdash P \iff \neg Q$. So P is not provably equivalent to $\neg Q$.
- No axiom is of the form $(A \circ B$), where $A$ and $B$ are sentences and $\circ$ is a logical operator. This may be a bit too strong, but I found no other way to reject trivial axioms like $(P\vee Q \vee R)$ and ($\neg R$) that give the needed $\varphi $ 'too easily'. I am open to replacing this restriction with a weaker one as long as it rules out this type of derivations. Sadly, the current one rules out ZFC, but it still allows PA and others though.
Is there such $\varphi$ in every theory? In some theory? What would be needed for it to exist? Does it exist in the interesting theories mentioned above? Could CH or other interesting unprovable sentences be part of such $\varphi$?