4.3. Raciocínio sobre Conectivos e Quantificadores🔗

A Aula 1 apresentou as regras dos conectivos como figuras de inferência. Cada figura é um teorema ordinário de Lean. Uma regra de introdução tem o conectivo como símbolo mais externo da sua conclusão e diz como prová-lo, e uma regra de eliminação tem o conectivo em uma hipótese e diz como uma prova dele pode ser usada. O quadro abaixo lista as regras de ∧, ∨ e ↔, com metavariáveis nos lugares que as regras deixam em aberto.

And.intro : ?a → ?b → ?a ∧ ?b
And.left  : ?a ∧ ?b → ?a
And.right : ?a ∧ ?b → ?b
Or.inl    : ?a → ?a ∨ ?b
Or.inr    : ?b → ?a ∨ ?b
Or.elim   : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
Iff.intro : (?a → ?b) → (?b → ?a) → (?a ↔ ?b)
Iff.mp    : (?a ↔ ?b) → ?a → ?b
Iff.mpr   : (?a ↔ ?b) → ?b → ?a

As regras do quantificador existencial, a verdade, a falsidade e os princípios clássicos completam o quadro. A implicação e o quantificador universal não aparecem em nenhum desses quadros, porque ambos são tipos de função dependentes, então a sua introdução é intro e a sua eliminação é a aplicação, a justaposição da Aula 2. A negação dispensa regras próprias, pois ¬a é definida como a → False, então intro se aplica a uma conclusão negada, como a Aula 1 mostrou. True.intro é a única regra da verdade, e False.elim é a única regra da falsidade. A lógica central de Lean é construtiva, e ela oferece o raciocínio clássico de forma explícita por meio de Classical.em e Classical.byContradiction, que repousam sobre axiomas adicionais. Ambos aparecem desde a Aula 1 e agora se aplicam regressivamente.

Exists.intro : ∀ (w : ?α), ?p w → ∃ x, ?p x
Exists.elim  : (∃ x, ?p x) → (∀ (w : ?α), ?p w → ?b) → ?b
True.intro   : True
False.elim   : False → ?c
Classical.em : ∀ (p : Prop), p ∨ ¬p
Classical.byContradiction : (¬?a → False) → ?a

Uma metavariável ?a representa um termo ainda por determinar. Quando apply casa a conclusão do objetivo com a conclusão de uma regra, a unificação determina algumas metavariáveis e deixa as demais como novos objetivos, que em geral desaparecem conforme a prova avança. A prova abaixo aplica a regra de introdução de ∧ regressivamente e fecha cada subobjetivo com uma regra de eliminação.

O marcador ·, usado desde a Aula 1, foca cada subobjetivo, e a justaposição instancia uma regra progressivamente, passando a hipótese diretamente em vez de esperar que ela apareça como subobjetivo. Esse é um pequeno passo progressivo dentro de uma prova regressiva, e ele evita as metavariáveis que apply deixa para trás.

A justaposição também instancia uma hipótese universal, exatamente como na Aula 2.

A regra de eliminação de ∨ realiza a análise de casos que a tática cases realizou na Aula 1, e modus_ponens e Not_Not_intro combinam as regras vistas até aqui.

Para provar enunciados de lógica proposicional, o guia oferece as estratégias a seguir.

• Olhe a conclusão. Se ela é uma implicação ou uma negação, intro faz progresso.

• Olhe as hipóteses. Uma conjunção oferece And.left e And.right, uma disjunção oferece Or.elim, e uma equivalência oferece Iff.mp e Iff.mpr.

• Case a conclusão do objetivo com a conclusão de uma regra de introdução e a aplique com apply.

• Prefira táticas que preservam a demonstrabilidade enquanto elas fizerem progresso, e registre os pontos de escolha em que uma tática se compromete com um lado.

• Quando um subobjetivo repete uma hipótese, exact ou assumption o fecha.

• Quando nada construtivo se aplica, considere uma análise de casos sobre Classical.em.

• Se a prova não progride, retroceda até o último ponto de escolha e tente a outra opção.

lefta b:Prophab:a ∧ b⊢ b

righta b:Prophab:a ∧ b⊢ a

selfa b:Prophab:a ∧ b⊢ ?a ∧ b

aa b:Prophab:a ∧ b⊢ Prop