Lógica Clássica vs. Lógica Construtiva

Vimos que não é possível testar se uma proposição p é verdadeira ou não ao definir uma função Kind. Você pode se surpreender ao descobrir que uma restrição semelhante se aplica às provas! Em outras palavras, o seguinte princípio de raciocínio intuitivo não é derivável em Kind:

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
}

Para entender operacionalmente por que esse é o caso, lembre-se de que, para provar uma declaração da forma Either p q, usamos as correspondências de padrão Left e Right, que exigem saber qual lado da disjunção é verdadeiro. Mas a proposição p universalmente quantificada em Excluded_middle é uma proposição arbitrária, sobre a qual não sabemos nada. Não temos informações suficientes para escolher qual de Left ou Right aplicar, assim como Kind não tem informações suficientes para decidir mecanicamente se p é verdadeira ou não dentro de uma função.

No entanto, se soubermos que p é refletida em algum termo booleano b, saber se ela é verdadeira ou não é trivial: basta verificar o valor de b.

#![allow(unused)]
fn main() {
Restricted_excluded_middle <p> <q> (b: Bool)(e: Equivalence p (Equal b Bool.true)) : Either p (Not p) 
Restricted_excluded_middle p q Bool.true  (Equivalence.new pb bp) = Either.left (bp Equal.refl)
Restricted_excluded_middle p q Bool.false (Equivalence.new pb bp) = Either.right (Empty.absurd (Not_implies_our_not pb))
}

Em particular, o terceiro excluído é válido para equações n = m, entre números naturais n e m.

#![allow(unused)]
fn main() {
//TODO: Terminar aqui
Restricted_excluded_middle_eq (n: Nat) (m: Nat) : Either (Equal n m) (Not (Equal n m))
Restricted_excluded_middle_eq n m = ?

To_reme (n: Nat) (m: Nat) (e: Equal n m) : Equal (Nat.equal n m) Bool.true
To_reme Nat.zero Nat.zero e         = Equal.refl
To_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
To_reme (Nat.succ n) (Nat.succ m) e = To_reme n m (Succ_injective n m e)

From_reme (n: Nat) (m: Nat) (e: Equal (Nat.equal n m) Bool.true) : Equal n m
From_reme Nat.zero Nat.zero e         = Equal.refl
From_reme Nat.zero (Nat.succ m) e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) Nat.zero e     = Empty.absurd (Not_implies_our_not e)
From_reme (Nat.succ n) (Nat.succ m) e = Equal.apply (x => Nat.succ x) (From_reme n m e)
}

Pode parecer estranho que o princípio do terceiro excluído não esteja disponível por padrão no Kind; afinal, qualquer afirmação deve ser verdadeira ou falsa. No entanto, há uma vantagem em não assumir o princípio do terceiro excluído: as declarações no Kind podem fazer afirmações mais fortes do que as declarações análogas na matemática padrão. Notavelmente, se houver uma prova no Kind de (Sigma a (x => (p x))), é possível exibir explicitamente um valor de x para o qual podemos provar p x - em outras palavras, toda prova de existência é necessariamente construtiva. Lógicas como a do Kind, que não assumem o princípio do terceiro excluído, são referidas como lógicas construtivas. Sistemas lógicos mais convencionais, como o ZFC, nos quais o princípio do terceiro excluído é válido para proposições arbitrárias, são referidos como clássicos.

O exemplo a seguir ilustra por que assumir o princípio do terceiro excluído pode levar a provas não construtivas:

Afirmação: Existem números irracionais a e b, tais que a^b é racional.

Prova: Não é difícil mostrar que a raiz quadrada de 2 é irracional. Se a raiz quadrada de 2 ^ raiz quadrada de 2 é racional, basta tomar a = b = raiz quadrada de 2 e estamos prontos. Caso contrário, se a raiz quadrada de 2 ^ raiz quadrada de 2 for irracional, podemos tomar a = raiz quadrada de 2 ^ raiz quadrada de 2 e b = raiz quadrada de 2, já que a ^ b = raiz quadrada de 2 ^ (raiz quadrada de 2 * raiz quadrada de 2) = raiz quadrada de 2 ^ 2 = 2.

Você percebeu o que aconteceu aqui? Usamos o princípio do terceiro excluído para considerar separadamente os casos em que a raiz quadrada de 2 ^ raiz quadrada de 2 é racional e onde não é, sem saber qual deles é verdadeiro! Por causa disso, sabemos que tais a e b existem, mas não podemos determinar quais são seus valores reais (pelo menos, usando essa linha de argumento).

Por útil que seja a lógica construtiva, ela tem suas limitações: há muitas declarações que podem ser facilmente provadas na lógica clássica, mas que têm provas construtivas muito mais complicadas, e há algumas que não se sabe ter prova construtiva alguma! Felizmente, assim como a extensão funcionalidade, o princípio do terceiro excluído é conhecido por ser compatível com a lógica do Kind, permitindo-nos adicioná-lo com segurança como um axioma. No entanto, não precisaremos fazer isso neste livro: os resultados que cobrimos podem ser desenvolvidos inteiramente dentro da lógica construtiva a um custo extra negligenciável.

Leva um pouco de prática para entender quais técnicas de prova devem ser evitadas no raciocínio construtivo, mas os argumentos por contradição, em particular, são infames por levar a provas não construtivas. Aqui está um exemplo típico: suponha que queremos mostrar que existe um x com alguma propriedade p, isto é, tal que p x. Começamos assumindo que nossa conclusão é falsa; isto é Not (Sigma a (x => (p x))). A partir desta premissa, não é difícil deduzir (x: a) -> Not (p x). Se conseguirmos mostrar que esse fato intermediário resulta em uma contradição, chegamos a uma prova de existência sem nunca exibir um valor de x para o qual p x seja verdadeiro!

A falha técnica aqui, do ponto de vista construtivo, é que afirmamos provar Sigma a (x => (p x)) usando uma prova de Not (Not (Sigma a (x =>(p x)))). Permitir-nos remover duplas negações de afirmações arbitrárias é equivalente a assumir o terceiro excluído, como mostrado em um dos exercícios abaixo. Assim, essa linha de raciocínio não pode ser codificada em Kind sem assumir axiomas adicionais.

Excluded_middle_irrefutable

A consistência do Kind com o axioma geral do terceiro excluído requer raciocínios complicados que não podem ser realizados dentro do próprio Kind. No entanto, o seguinte teorema implica que é sempre seguro assumir um axioma de decidibilidade (ou seja, uma instância do terceiro excluído) para qualquer tipo específico p. Por quê? Porque não podemos provar a negação de tal axioma; se pudéssemos, teríamos tanto Not (Either p (Not p)) quanto Not (Not (Either p (Not p))), o que é uma contradição.

#![allow(unused)]
fn main() {
Excluded_middle_irrefutable <p> : Not (Not (Either p (Not p)))
Excluded_middle_irrefutable p = ?
}

Not_exists_dist

É um teorema da lógica clássica que as seguintes duas afirmações são equivalentes:

#![allow(unused)]
fn main() {
Not (Sigma a (k => Not (p k))))
(x : a) -> p x
}

O teorema dist_not_exists acima prova um lado dessa equivalência. Curiosamente, a outra direção não pode ser provada na lógica construtiva. Sua tarefa é mostrar que ela é implicada pelo terceiro excluído.

#![allow(unused)]
fn main() {
Not_exists_dist <a> (p: a -> Type) (s: Not (Sigma a (k => Not (p k)))) : (x: a) -> p x
Not_exists_dist a p s = ?
}

sendo que

#![allow(unused)]
fn main() {
Excluded_middle <p>: Either p (Not p)
// Excluded_middle p = Confia 
}

Classical_axioms

Para aqueles que gostam de um desafio, aqui está um exercício retirado do livro Coq'Art de Bertot e Casteran (p. 123). Cada uma das seguintes quatro afirmações, juntamente com excluded_middle, pode ser considerada como caracterizando a lógica clássica. Não podemos provar nenhum deles em Kind, mas podemos adicionar consistentemente qualquer um deles como um axioma se quisermos trabalhar na lógica clássica.

Prove que todas as cinco proposições (essas quatro mais excluded_middle) são equivalentes.

#![allow(unused)]
fn main() {
Peirce <p> <q>(pq: (p -> q) -> p) : p

Double_negation_elimination <p> (np: Not (Not p)) : p

De_morgan_not_not <p> <q> (np: Pair (Not p) (Not q)) : Either p q

Implies_to_or <p> <q> (pq: p -> q) : Either (Not p) q
}