⊢ p ⇔ (p & p)

what means the right part of these Entailments?

  • Which symbol..? – user253751 Mar 11 at 12:43
  • | – p This is before p – MHghasemi Mar 11 at 13:57
  • 1
    I edited the question to replace "| -" with "⊢". It means that the formula to the right of the "⊢" symbol is provable from the formulas (assumptions) to the left of the "⊢" symbol. For example, P, P → Q ⊢ Q. When there is nothing to the left of the "⊢" symbol, it means that the formula to the right is a theorem; it's provable from no assumptions. – Adam Sharpe Mar 11 at 14:37
  • How much searching did you do? en.wikipedia.org/wiki/Turnstile_(symbol) – puppetsock Mar 11 at 15:03
  • 1
    It's also worth noting the wonderful site detexify! (Which doesn't actually help here since this site doesn't support MathJax - and probably never will, per the meta discussion here - I just like to mention it because it's cool and may be separately useful to the OP and others.) – Noah Schweber Mar 11 at 17:11

In general, when A is a set of sentences and x is a single sentence we write "A ⊢ x" for "A proves x." Here a fixed deduction system is implicit; generally however any reasonable choice will work (apply the relevant completeness theorem).

There are a couple abbreviations which crop up in this context which it's worth mentioning:

  • When A={y_1,...,y_n} is a finite set, we often just write "y_1,...,y_n ⊢ x" for "A ⊢ x."

  • In particular, when A={} we often just write "⊢ x." That's the case in your example.

  • We also write "A ⊢ B" for "For all x in B, we have A ⊢ x." That's not an abbreviation which is relevant here, but it's worth mentioning.

So in your case, what's being said is: "The sentence 'p ⇔ (p & p)' is provable" (note that we just say "provable," not "provable without any extra premises"). You'll often hear this further abbreviated as "p ⇔ (p & p) is a tautology."

| improve this answer | |

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.