What ⊬ means
Read it as “Q cannot be proved from P.”
P represents the premises: statements you take as starting assumptions. Q is the conclusion you want to establish. The slash negates the proof relation written . You meet this notation in logic textbooks and mathematical discussions of what a set of assumptions can prove.
For example, in ordinary classical logic, “it is raining” alone cannot prove “it is cold.” It might actually be cold; the point is that the starting statement does not establish it. Likewise, P ⊬ Q does not mean that P proves the opposite of Q.
The chosen rules and assumptions matter. Adding a premise can make a previously unprovable conclusion provable. If nothing appears to the left, ⊬ Q usually means Q is not a theorem of the system: it cannot be proved from its axioms and rules alone.
Formal, technical notation about proofs.
“Cannot be proved here” does not mean “false.”
Part of collections
Don't confuse it with
1
Related characters
1
Worth knowing
- The turnstile’s historical ancestor appears in Gottlob Frege’s 1879 Begriffsschrift, a two-dimensional notation for logic. Its original role was to mark an assertion; the modern proof relation developed later.
More like this
11
How to type or find ⊬
- Search it as
- not provable · barred turnstile · nvdash · not derivable
- Shows up in
- Anything that takes text · its shape is whatever your font draws
⊬\22AC\usepackage{amssymb}, then use \nvdash in math mode.Codes and encoding1 code points
A visible symbol can contain several code points. JS .length counts UTF-16 units; UTF-8 counts bytes.