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 '19 at 0:45
  • @FrankHubeny in this context I am using the turnstile for provability – Math Bob Mar 15 '19 at 0:47
  • 3
    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 '19 at 1:33
  • @MathBob, there should still be only one turnstyle in a sequent. – Graham Kemp Mar 15 '19 at 2:15
  • 1
    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 '19 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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.