1.2. Proposições🔗

Uma proposição é uma sentença declarativa que é verdadeira ou falsa. "7 é primo" e "todo número par maior que 2 é a soma de dois primos" são proposições. "Feche a porta" e "x é par" não são, a primeira porque ordena em vez de afirmar, a segunda porque a sua verdade depende da variável livre x.

Em Lean, o tipo Prop classifica as proposições.

True : Prop

Escrevemos P, Q, R para variáveis proposicionais, que representam proposições arbitrárias.