= Logical falsity
{title2=$\bot$}
<Logical falsity>, written $\bot$, 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 $\bot$ 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 $\bot$ 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>.
Back to article page
