Not true

It says the left side does not guarantee the right. In the not true symbol ⊭, a valuation means an assignment of truth values. In Γ ⊭ φ, some valuation makes Γ true and φ false. This does-not-entail notation states a relation between formulas in the metalanguage—the part of logic that describes them—not a connective inside them.

The crossed double turnstile has a history tied to Frege’s assertion stroke, a mark for asserting a proposition. Later logic used the double turnstile for semantic consequence or model satisfaction; crossing it denies that relation.

What does ⊭ rule out?

It denies a guarantee, not every possible conclusion. P ⊭ Q means some interpretation makes P true and Q false. It does not say Q is false in every case, or that P ⊨ ¬Q. With no premises, ⊭ φ says φ is not a tautology: some valuation makes it false.

Model theory also uses the double turnstile for satisfaction: A ⊨ Γ says structure A satisfies formulas Γ, while A ⊭ Γ denies that satisfaction.

How do I type ⊭?

Use \nvDash in a LaTeX setup that defines it. The command depends on the symbol package and engine.