⊢ p ⇔ (p & p)

what means the right part of these Entailments?

  • Which symbol..?
    – user253751
    Mar 11, 2020 at 12:43
  • | – p This is before p
    – MHghasemi
    Mar 11, 2020 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. Mar 11, 2020 at 14:37
  • How much searching did you do? en.wikipedia.org/wiki/Turnstile_(symbol)
    – puppetsock
    Mar 11, 2020 at 15:03
  • 2
    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.) Mar 11, 2020 at 17:11

2 Answers 2


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."


it means that "p ⇔ (p & p) " can be conculded without any assumptions. sign use to seperate the conclusion from its pemises/evidences/assumptions. The Argument : A ⊢ B means B can be concluded by A . and Argument : ⊢ C means C can be concluded without any assumptions(same in your case).

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .