# Is b⊢C∧¬b⊢C∧b⇒C∧¬b⇒C possible?

Are there any cases where b and C are real world statements where b⊢C∧¬b⊢C∧b⇒C∧¬b⇒C where b and C are not tautologies? It may seem like a silly question, but after searching hard and deep, I couldn't find an answer! Please help me with this question.

• Are the two turnstyles (⊢) supposed to be there? I often think of the turnstyle as separating the premises from the conclusion. – Frank Hubeny Mar 15 at 0:45
• @FrankHubeny in this context I am using the turnstile for provability – Math Bob Mar 15 at 0:47
• Your notation is rather weird, but if I understand it correctly, the answer is yes, this would be possible provided C is a tautology. – Bumble Mar 15 at 1:33
• @MathBob, there should still be only one turnstyle in a sequent. – Graham Kemp Mar 15 at 2:15
• The formula is wrongly written and it is impossible to parse it. is not a connective; thus we can read it as b⊢C and ¬b⊢C and b⇒C∧¬b⇒C; but in this case it is lacking a "verb" attached to the last formula. – Mauro ALLEGRANZA Mar 15 at 7:33

Assume classical propositional calculus.

If C is a tautology, then ⊨ C, and thus B ⊢ C for B whatever, and thus ⊢ B → C.

If not, if we have both B ⊢ C and ¬B ⊢ C we apply the Deduction Theorem and we get :

⊢ ¬B → C and ⊢ B → C.

Now, using Excluded Middle ⊢ ¬B ∨ B, we can use Disjunction Elimination to conclude with ⊢ C.

But if C is not a tautology, this contradicts the soundness of the calculus.