Can there be some provable disjunction $P \vee Q$ in which neither $P$ nor $Q$ can be proved?

Question

More specifically, in FOL, given any theory $\Sigma$ of sentences, are there disjunctions $\varphi=P \vee Q$ such that:

1. $\varphi$ is not provable from any single sentence of $\Sigma$ . So its not logically equivalent to an axiom.
2. $\emptyset \not \vdash \varphi $. This is implied by 1. but I want to emphasize that it's not a logical truth.
3. $\Sigma \not \vdash P$ and $\Sigma \not \vdash Q$. So they are not individually provable.
4. $\Sigma \not\vdash P \iff \neg Q$. So P is not provably equivalent to $\neg Q$.
5. 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$?

Answer 1

Let $P$ be any sentence which is independent of $T$ (or actually, any sentence which is not provable from any single sentence in $T$), and let $Q$ be any sentence which is provably equivalent to $\lnot P$, but not logically equivalent to $\lnot P$. Then $T$ proves that $P\lor Q$ is equivalent to $P\lor \lnot P$, but this is equivalence is not provable from $\emptyset$, i.e., $T\vdash P\lor Q$ but $\emptyset\not\vdash P\lor Q$.

For example, in $ZF$, let $P$ be the axiom of choice, and let $Q$ be the sentence "there exists a vector space which does not have a basis".

---

Edit: To deal with your new requirement that $T\not \vdash (P\leftrightarrow \lnot Q)$, just replace $P$ with $P\lor R$, where $R$ is any other statement independent from $T\cup P$. So for example, let $P$ be $AC\lor CH$, the disjunction of the axiom of choice and the continuum hypothesis, and let $Q$ be "there exists a vector space with no basis".

I'm worried this is going to quickly devolve into a "shifting the goalposts" situation. Instead of coming up with a list of increasingly complex requirements, you should take a step back and try to clearly explain the motivation behind your question. Then other users might be able to help you ask the right question.