# What does the "⊢" symbol mean in ⊢ p ⇔ (p & p)?

⊢ p ⇔ (p & p)

what means the right part of these Entailments?

• Which symbol..? Mar 11, 2020 at 12:43
• | – p This is before p Mar 11, 2020 at 13:57
• 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) Mar 11, 2020 at 15:03
• 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

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