3

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
  • 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 at 1:33
  • @MathBob, there should still be only one turnstyle in a sequent. – Graham Kemp Mar 15 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 at 7:33
3

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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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