The Mathematical Symbol "Does Not Prove (⊬)"

The "Does Not Prove" Symbol (⊬): Logical Implications

The "Does Not Prove" notation, represented as ⊬ is a symbol with significant importance in formal logic and proof theory. It indicates that a particular proposition is not a syntactic consequence of another proposition or set of propositions. In this article, we'll investigate the primary usages of this notation with two illustrative examples.

Role in Formal Logic and Proof Theory

In formal logic and proof theory, the ⊬ symbol is employed to convey that a statement or proposition is not a direct syntactic consequence of a set of premises or propositions. This distinction differs from the semantic consequence often represented by the double turnstile symbol, as it is purely based on syntactic form rather than semantic truth values.

Example 1:

Consider the proposition \(P\) and its negation \( \neg P \). Using the "Does Not Prove" notation, we can state:

\( P ⊬ \neg P \)

This indicates that \(P\) does not syntactically imply its negation \( \neg P \).

Example 2:

For another example, let's take the propositions "All birds fly" and "Penguins are birds". From these, one might be tempted to deduce "Penguins fly". However, in reality, penguins do not fly. Symbolically, given the premises \( BirdsFly \) and \( PenguinsAreBirds \), the conclusion \( PenguinsFly \) does not follow. This relationship can be captured as:

BirdsFly, PenguinsAreBirds ⊬ PenguinsFly

Through these instances, the usage of the "Does Not Prove" notation to highlight non-consequent relationships in logic is clear. As is the case with many logical symbols, understanding the precise interpretation depends on the context and specific propositions under discussion.

Mathematical symbol 'Does Not Prove'

Are You Good at Mathematical Symbols?

Do you know, or can you guess, the technical symbols? Well, let's see!
gold cup

gold cup

gold cup

  • This test has questions.
  • A correct answer is worth 5 points.
  • You can get up to 5 bonus points for a speedy answer.
  • Some questions demand more than one answer. You must get every part right.
  • Beware! Wrong answers score 0 points.
  • 🏆 If you beat one of the top 3 scores, you will be invited to apply for the Hall of Fame.
Scoring System

Guru (+)
Hero (+)
Captain (+)
Sergeant (+)
Recruit (+)

Codes for the ⊬ Symbol

The Symbol
Alt CodeAlt 8876
HTML Code⊬
HTML Entity⊬
CSS Code\22AC
Hex Code⊬

How To Insert the ⊬ Symbol

(Method 1) Copy and paste the symbol.

The easiest way to get the ⊬ symbol is to copy and paste it into your document.

Bear in mind that this is a UTF-8 encoded character. It must be encoded as UTF-8 at all stages (copying, replacing, editing, pasting), otherwise it will render as random characters or the dreaded �.

(Method 2) Use the "Alt Code."

If you have a keyboard with a numeric pad, you can use this method. Simply hold down the Alt key and type 8876. When you lift the Alt key, the symbol appears. ("Num Lock" must be on.)

(Method 3) Use the HTML Decimal Code (for webpages).

HTML TextOutput
<b>My symbol: &#8876;</b>My symbol: ⊬

(Method 4) Use the HTML Entity Code (for webpages).

HTML TextOutput
<b>My symbol: &nvdash;</b>My symbol: ⊬

(Method 5) Use the CSS Code (for webpages).

CSS and HTML TextOutput
span:after {
content: "\22AC";}
<span>My symbol:</span>
My symbol: ⊬

(Method 6) Use the HTML Hex Code (for webpages and HTML canvas).

HTML TextOutput
<b>My symbol: &#x22AC;</b>My symbol: ⊬
On the assumption that you already have your canvas and the context set up, use the Hex code in the format 0x22AC to place the ⊬ symbol on your canvas. For example:
JavaScript Text
const x = "0x"+"E9"
ctx.fillText(String.fromCodePoint(x), 5, 5);

(Method 7) Use the Unicode (for various, e.g. Microsoft Office, JavaScript, Perl).

The Unicode for ⊬ is U+22AC. The important part is the hexadecimal number after the U+, which is used in various formats. For example, in Microsoft Office applications (e.g. Word, PowerPoint), do the following:
[Hold down Alt]
[Press x]

(The 22AC turns into ⊬. Note that you can omit any leading zeros.)
In JavaScript, the syntax is \uXXXX. So, our example would be \u22AC. (Note that the format is 4 hexadecimal characters.)
JavaScript TextOutput
let str = "\u22AC"
document.write("My symbol: " + str)
My symbol: ⊬