O que é uma "contradição" na lógica construtiva?

Em Fundamentos Práticos para Linguagens de Programação , Robert Harper diz

Se uma proposição para ser verdadeira significa ter uma prova dela, o que significa que uma proposição seja falsa? Isso significa que a refutamos , mostrando que não pode ser provado. Ou seja, uma proposição é falsa se pudermos mostrar que a suposição de que ela é verdadeira (tem uma prova) contradiz fatos conhecidos.

Mas, então, isso levanta a questão - o que é uma contradição na lógica construtiva / intuicionista?

Isso significa no sentido de derivar alguma forma? Como isso aconteceria de maneira sensata? Será que um acórdão do formulário ( A ⊃ ⊥  verdadeiro ) devam ser introduzidas?$(\bot\text{ true})$$(A \supset \bot \text{ true})$

Como alternativa, talvez isso signifique, no sentido de o leitor usar sua discrição, para rotular informalmente algo de contraditório? Por exemplo, a interpretação e um ≠ b como estando em conflito proposições.$a = b$$a \neq b$

É irrelevante falarmos de lógica construtiva ou clássica nessa situação. Se você ler suas perguntas novamente, verá que elas se aplicam aos dois tipos. A única diferença que precisamos tomar conhecimento de é a apresentação de negação . Ele pode ser apresentado de várias maneiras classicamente, mas intuicionisticamente é melhor usá-lo como uma abreviação de A ⇒ ⊥ (que é exatamente o que Bob Harper está sugerindo no parágrafo citado). Mas não confundamos negações e contradições.$\lnot A$$A \Rightarrow \bot$

Nos dois casos, uma contradição é uma situação em que conseguimos provar a falsidade $\bot$ . Como poderíamos derivar maneira sensata? Bem, a partir de um conjunto inconsistente de hipóteses, essa seria uma maneira sensata de fazê-lo.$\bot$

Você não tem o poder de "declarar" uma contradição. Você deve provar que um determinado conjunto de hipóteses é contraditório ao derivar . Por exemplo, se um = b e ¬ ( um = b ) , então podemos utilizar o facto de que ¬ ( um = b ) é uma abreviatura para ( um = b ) ⇒ ⊥ e concluir ⊥ por ponente modus.$\bot$$a = b$$\lnot (a = b)$$\lnot (a = b)$$(a = b) \Rightarrow \bot$$\bot$

$A \land \lnot A$ $\lnot A$$A \Rightarrow \bot$$\bot$$A \land \lnot A$$\bot$$\lnot$

$\bot$

$\bot$$A$$A \Rightarrow \bot$$A$$\lnot A \Rightarrow \bot$$\lnot \lnot A$$\lnot \lnot (\lnot \lnot A \lor \lnot A)$$\lnot \lnot \lnot A \Rightarrow \lnot A$