2.1. Predicados e Quantificadores🔗

A Aula 1 excluiu "x é par" das proposições porque a sua verdade depende da variável livre x. Um predicado torna essa dependência explícita. Um predicado sobre um tipo α atribui uma proposição a cada elemento de α, então em Lean um predicado é uma função de tipo α → Prop.

fun n => n > 3 : Nat → Prop#check fun n : Nat => n > 3

fun n => n > 3 : Nat → Prop

Quantificadores ligam a variável de um predicado e produzem uma proposição.G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Verlag von Louis Nebert, Halle, 1879. Escrevemos P x para a proposição que o predicado P produz em x.

Símbolo	Nome	Leitura
∀ x, P x	quantificador universal	P x vale para todo x
∃ x, P x	quantificador existencial	P x vale para algum x

O quantificador liga a sua variável, então ∀ x, P x não depende de variável livre e é uma proposição. A variável percorre um tipo. Por exemplo, ∃ n : Nat, n * n = 9 afirma que algum número natural elevado ao quadrado dá 9. Quando o contexto determina o tipo, Lean o infere e omitimos a anotação.