Logical falsity ($\perp$)

Logical falsity, written $\perp$, is a zero-input logical connective interpreted as false under every Boolean valuation. In standard Intuitionistic propositional logic and classical propositional logic, it has no introduction rule that produces it without premises. The logical falsity elimination rule permits deriving any logical formula from it.

A formal proof can derive $\perp$ from contradictory assumptions: $P$ together with $\neg P$ gives it by the negation elimination rule. A first-order theory is first-order consistent when it has no assumption-free proof of $\perp$ from its own axioms. Thus having no proof is a consistency property of a specified formal proof system, rather than an unconditional definition of logical falsity.