* Como capturar o comportamento dedutivo da ''bi-implicação clássica''?
* Como encontrar regras para ''outros conectivos clássicos'' (ou para suas contrapartes intuicionistas)?
* A regra do ''bottom clássico'' captura uma interação 'não-conectival' entre o bottom e a negação (clássica). O Em geral, dado um conectivo ©, o que o lógico clássico teria a dizer de sobre as interações clássicas entre o bottom e a ''negação de uma conjunção'', ou entre o bottom e a ''negação de uma implicação''©?
== Veja também ==
* [[Estratégias de demonstração]]
* [[Correção e completude para a Lógica Proposicional Clássica]]
* [[Introdução Computacional à Lógica Matemática]]
== Links externos ==
*