@Austin_Dern That sounds right, yes. At least as long as (S ∪ Q) is consistent, but if it isn't then it isn't sensible to make statements about its ability to prove things, as it proves everything.

@Austin_Dern well uh, oof. I was just typing up something about how I realized that reasoning has to have a flaw in it somewhere, because (S ∪ Q) and (S ∪ ¬Q) can both entail P trivially when S entails P. Your reasoning at least seems sound enough and I'm not sure what the problem is though

@Austin_Dern Right, so, is it possible to have (S → (Q → P)) and (S → (¬Q → P)) and not have (S → P)? I suppose that goes back to what @quartzwing@dragon.style was saying, that classical logic would make it so that (Q ∨ ¬Q), but then isn't the law of excluded middle itself an axiom that would have to be included in S?

@Austin_Dern @quartzwing@dragon.style I think there's no reasonable doubt that (((S ∪ Q) → P) ∧ ((S ∪ ¬Q) → P)) → (S → P), but the original question might have gotten a little muddled in the introduction of the → syntax. The question is on the provability of P in the axiomatic system given by S, not the truth of P under those axioms (which by Gödel's incompleteness theorem are different things)

also that is one mess of symbols and parentheses.