Falsum

term: Falsum symbol: \bot etymology: 'Do latim falsus — falso. O símbolo ⊥ é o elemento bottom de uma estrutura de reticulado — o piso abaixo de tudo. Seu oposto é ⊤ (top, tautologia). A iconicidade é visual: o T invertido é graficamente o oposto do T reto.' summary: 'A proposição impossível. ⊥ é falsa em todo caso; não tem regra de introdução. De ⊥, qualquer coisa segue (ex falso quodlibet).' relatedModules: [propositional-logic, proof-methods] seeAlso: [nao-contradicao, tautologia]

Símbolo

$\bot$ — lido bottom, falso ou absurdo. O par $\bot$/$\top$ forma os extremos do reticulado de valores-verdade: $\top$ é a tautologia (verdadeira em todo caso), $\bot$ é a contradição (falsa em todo caso).

Definição

$\bot$ é a proposição com valor-verdade falso em toda atribuição possível. Na teoria de tipos, corresponde ao tipo vazio — o tipo sem habitantes, sem termos, sem provas.

Regras

$\bot$ tem exatamente uma regra de eliminação e zero regras de introdução:

Ex falso quodlibet ($\bot E$) — de $\bot$, qualquer proposição $C$ segue.

A ausência de regra de introdução é intencional: nada deveria construir $\bot$ diretamente. Se $\bot$ aparece numa derivação, é porque uma contradição foi produzida — e isso destrói o contexto inteiro.

Registro computacional

Em TypeScript, $\bot$ corresponde ao tipo never — o tipo sem valores. Em Haskell, Void. Em Python, o tipo de raise — a expressão que nunca retorna.

Python
from typing import Never
 
def ex_falso(x: Never) -> object:
    raise AssertionError("nunca alcançado")

Nota sobre a lógica clássica

Na lógica clássica, a regra $\bot_C$ (redução ao absurdo) permite concluir $P$ a partir de $\neg P \vdash \bot$. Essa regra não existe na lógica intuicionista — ali, só é possível concluir $\neg P$ (introdução de negação). A diferença é o que separa as duas lógicas.