A lógica intuicionista é uma lógica que difere da lógica clássica que a noção de verdade é substituída pela noção de prova construtiva . Uma proposição como "a constante de Euler-Mascheroni é racional ou a constante de Euler-Mascheroni não é racional" não é demonstrada construtivamente (intuicionisticamente) dentro da estrutura de nosso conhecimento matemático atual; porque a tautologia clássica "P ou não P" ( terceiro excluído ) não pertence à lógica intuicionista. A lógica intuicionista estabelece, entre outras coisas, uma distinção entre “ser verdadeiro” e “não ser falso” (formulação mais fraca) porque ¬¬P → P também não é demonstrável na lógica intuicionista.
O intuicionismo foi primeiro uma postura filosófica vis-à-vis matemática proposta pelo matemático holandês L. E. J. Brouwer como uma possibilidade diferente da abordagem conhecida clássica ; isso o levou a não incluir certas formas de raciocínio matemático tradicional, que ele considerou contra-intuitivo:
Brouwer defendia uma matemática que rejeitasse o terceiro excluído e só aceitasse o existencial construtivo . Essa atitude foi ferozmente criticada por matemáticos como David Hilbert, enquanto outros como Hermann Weyl a subscreveram.
Foi então formalizado, sob o nome de lógica intuicionista , por seus alunos V. Glivenko e Arend Heyting , bem como por Kurt Gödel e Andreï Kolmogorov . A interpretação Brouwer-Heyting-Kolmogorov ou simplesmente interpretação BHK é essencialmente o destaque do caráter construtivo da implicação intuicionista: quando um matemático intuicionista afirma , ele quer dizer que está fornecendo um processo de "construção" de uma implicação intuicionista . Demonstração de de uma demonstração de . Em outras palavras, uma prova de é uma função que transforma uma prova de em uma prova de .
Esta interpretação computacional culminará em um dos resultados mais importantes da ciência da computação teórica: a correspondência Curry-Howard, cujo leitmotiv é "provar é programar". Há isomorfismo entre as regras de dedução da lógica intuicionista e as regras de tipagem do cálculo lambda. Conseqüentemente, uma prova de uma proposição é assimilada a um termo (lambda-) do tipo .
Consequentemente, a lógica intuicionista (associada à teoria dos tipos ) adquire um status preponderante na lógica e na informática teórica, tornando-se historicamente a primeira das lógicas construtivas . Este resultado fundamental irá gerar muitos trabalhos derivados ; em particular sua extensão à lógica de ordem superior que requer o uso de tipos dependentes (o cálculo de construções , por exemplo, é a base teórica do software Coq que é, portanto, ao mesmo tempo, um assistente de provas (construtivas), e uma ferramenta para a criação de programas certificados).
A sintaxe da lógica proposicional intuicionista é a mesma da lógica proposicional clássica . A sintaxe da lógica de primeira ordem intuicionista é a mesma que a sintaxe da lógica de primeira ordem clássica .
Construção | Leitura intuitiva em lógica clássica | Leitura intuitiva na lógica intuicionista |
---|---|---|
é verdade | é provável | |
é verdade ou é verdade | é provável ou é provável | |
é verdade e é verdade | é provável e é provável | |
Falso | Falso | |
Se for verdade, então é verdade | Se é provável, então é provável | |
(abreviatura de ) | é falso | é contraditório |
Construção | Leitura intuitiva em lógica clássica | Leitura intuitiva na lógica intuicionista |
---|---|---|
existe um elemento tal que é verdadeiro | podemos construir um elemento tal que seja comprovável | |
para qualquer elemento , é verdade | tomando qualquer elemento , é provável |
A negação pode ser definida a partir da implicação: é definido como . Na lógica proposicional clássica, podemos definir a disjunção (o “ou”) do “e” e a negação graças às leis de Morgan . Por exemplo, pode ser definido como um atalho de escrita para . Na lógica proposicional intuicionista, esse não é mais o caso e cada operador tem uma interpretação diferente (cf. tabela acima). Da mesma forma, não se pode definir como .
Na lógica intuicionista, os conectores não são indefiníveis. É por isso que vamos dar regras para cada conector binário, para o conector unário que é a negação e para o símbolo ⊥ que representa o falso ou o absurdo. Fornecemos uma (ou mais) regra (s) de eliminação e uma (ou mais) regra (s) introdutória (s) para cada conector, típico da dedução natural clássica . Na dedução natural, lê-se "do conjunto de proposições deduzimos a proposição " .
O único conector da lógica mínima implicativa é a implicação . Na dedução natural , suas regras, além da regra do axioma:
estão :
onde a letra denota um conjunto finito de fórmulas, e a notação denota , onde pode ou não estar presente em .
A regra é chamada de regra de eliminação de implicação . É o seguinte: se deduzimos do conjunto de hipóteses e, além disso, se deduzimos do conjunto de hipóteses , então, do conjunto de hipóteses deduzimos . A eliminação do envolvimento também é chamada de modus ponens .
A regra é chamada de regra de introdução de implicação . Diz o seguinte: se do conjunto de hipóteses e da hipótese se deduz, então, do conjunto de hipóteses que se deduz ( pode ou não pertencer ).
A lei Peirce ou proposta , que são tautologias da lógica clássica , não são demonstráveis neste sistema de dedução. Adicionando a ele, por exemplo a lei de Peirce, obtemos um sistema dedutivamente completo no sentido da lógica clássica para fórmulas puramente implicacionais (ver cálculo proposicional de implicação ( fr ) ).
A lógica intuicionista tem as regras de implicação, a lógica mínima, mais as regras abaixo que regem outros conectores.
O absurdoO falso ou absurdo, ⊥, é um conector zero, ou seja, que não tem proposição em discussão, é regido pela regra:
Essa regra é chamada de princípio da explosão ou, em latim, ex falso quodlibet . O princípio da explosão significa que se um conjunto de proposições Γ leva ao absurdo ⊥, então, de Γ , podemos deduzir qualquer proposição .
A negociaçãoTradicionalmente, consideramos a negação como a abreviatura e, portanto, geralmente não fornecemos regras correspondentes à negação. Porém poderíamos dar alguns, para simplificar as demonstrações e seriam:
Deve-se notar que essas regras para a negação intuicionista são mais fracas do que aquelas para a negação clássica, porque, por exemplo, não podemos deduzir daí .
A conjunçãoCom o conector (conjunção), associamos duas regras de eliminação, e , e uma regra introdutória.
onde se lê "A e B". A disjunçãoCom o conector (disjunção), associamos uma regra de eliminação e duas regras introdutórias:
.Observe que a regra de eliminação da disjunção é uma regra triádica: ela tem três premissas.
Além das regras do cálculo proposicional intuicionista, o cálculo de predicados intuicionista contém novas regras de introdução e eliminação para os quantificadores “o que quer que seja” e “existe”.
Nota : Lembramos que A [t / x] significa a substituição de todas as ocorrências livremente substituíveis da variável x pelo termo t; ver cálculo de predicados para as noções de “variável”, “termo”, “substituição” e “livremente substituível”.
O quantificador universalO quantificador existencial
Podemos dar uma semântica à lógica intuicionista que é uma semântica de Kripke . Um modelo Kripke é um gráfico onde:
Para dizer que um mundo satisfaz uma fórmula , também dizemos que o mundo força uma fórmula . A relação de força (ou viabilidade ) é definida por indução estrutural por:
Uma fórmula é válida se para qualquer mundo de qualquer modelo , força .
ExemploConsidere o modelo de Kripke à direita. Não satisfaz o terceiro excluído . Na verdade, por um lado, o mundo inicial não força (intuitivamente, não está provado porque é falso, o que significa que ainda não temos informações suficientes). Por outro lado, o mundo inicial não força não é contraditório, pois ao proporcionar um pouco mais de esforço, pode-se “obter mais informações” e chegar no mundo certo e comprovar . O terceiro excluído não é válido. Também :
A lógica intuicionista está correta com relação aos modelos de Kripke, ou seja, qualquer fórmula demonstrável (por exemplo, com as regras de dedução natural da seção anterior) é válida. Podemos usar esse resultado para mostrar que uma fórmula não pode ser demonstrada na lógica intuicionista. Por exemplo, uma vez que o terceiro excluído ou a lei de Peirce não são válidos, eles não são demonstráveis.
Qualquer fórmula válida é demonstrável . A demonstração é feita da seguinte forma: se não for demonstrável, podemos construir um contra-modelo (infinito), ou seja, um modelo contendo um mundo que não força .
As operações não são definidas umas em relação às outras (veja abaixo) e são definidas apenas por elas mesmas. Eles são definidos pela interpretação que deve ser feita deles. Por isso, além das regras de cálculo, são fornecidas as interpretações que devem ser feitas das expressões de cada operador.
Algumas validadesA tabela a seguir fornece algumas validades da lógica intuicionista.
Validades na lógica intuicionista | Explicações para | Explicações para |
---|---|---|
✔ Se A é provável, então está provado que A não é contraditório. | ✗ Por exemplo, está provado que “chove” não é contraditório (não se obtém uma contradição assumindo que “chove”). No entanto, "está chovendo" não é provável, a menos que você saia e se molhe. | |
✔ Se A for contraditório, então uma prova que não é contraditória dá uma contradição. | ✔ Se temos uma prova que não é contraditória dá uma contradição, então A é contraditório. | |
✔ Se A for contraditório ou B for contraditório, então “A e B” é contraditório. | ✗ Por exemplo, ser alto e baixo é contraditório. No entanto, ser alto não é contraditório, e ser pequeno não é contraditório. | |
✔ Se obtivermos uma contradição de uma prova de A ou de uma prova de B, então A é contraditório e B é contraditório. | ✔ Se A é contraditório e B é contraditório, então, de uma prova de A ou de uma prova de B, obtemos uma contradição. | |
✔ Se A é contraditório ou B é provável, então se eu tenho uma prova de A (que não existe!), Eu tenho uma prova de B. | ✗ Por exemplo, estou construindo uma prova de “x> 0” que usa uma prova “x> 1”. No entanto, “x> 1” não é contraditório e “x> 0” não é demonstrável. | |
✔ Se “existe x tal que A (x)” é contraditório, então para todo x, A (x) é contraditório. | ✔ Se para todo x, A (x) é contraditório, então “existe x tal que A (x)” é contraditório. | |
✔ Se eu puder construir um x tal que A (x) forneça uma contradição, então “para todo x, A (x)” é contraditório. | ✗ Por exemplo, “para todo x, x é pobre” é contraditório (porque vejo que existe riqueza). No entanto, não consigo encontrar um indivíduo x (rico) tal que x é pobre para ser contraditório. |
Na lógica clássica, as fórmulas obtidas pela substituição das implicações por equivalências são validades (a tabela conteria apenas ✔).
NegaçãoPode ser interpretado como: "Está demonstrado que é contraditório".
Temos na lógica intuicionista o seguinte teorema:
No entanto, não se pode concluir disso , porque essa equivalência não pode ser provada na lógica intuicionista.
Negação duplaPode ser interpretado como: "Está demonstrado que é contraditório afirmar que é contraditório", isto é, "Está demonstrado que não é contraditório". Mas não podemos deduzir que " é demonstrável".
O teorema:
pode ser demonstrado na lógica intuicionista. Mas o inverso não pode ser. Nós não temos . A expressão pode ser interpretada como “a partir de uma demonstração de , podemos construir uma demonstração de ”. Mas o fato de não ser contraditório não é suficiente para estabelecer uma demonstração de " ".
Por exemplo, seja x um número real e a proposição x seja racional. Para provar que é dar dois inteiros um e b tal que x = um / b . Se for contraditório (e, portanto, se o tivermos ), então x é não racional ou irracional. Dizer que temos é dizer que supor que x seja irracional leva a uma contradição e, portanto, concluir que x não é irracional. Mas isso não é suficiente para estabelecer a existência efetiva de dois inteiros a e b tal que x = a / b . Assim, na lógica intuicionista, não ser irracional é uma propriedade diferente e mais fraca do que ser racional.
ConjunçãoA interpretação de é: temos uma prova de e uma prova de (comparável ao que é na lógica clássica).
Na lógica intuicionista, a seguinte proposição é um teorema:
Mas, ao contrário do que seria na lógica clássica, é apenas uma consequência de , sendo o inverso falso. Na verdade, supor que isso seja contraditório, é insuficiente na lógica intuicionista para concluir se é apenas isso ou sozinho ou se são os dois. Por exemplo, assumir que um número é racional e irracional é contraditório, mas insuficiente para concluir se esse número é irracional ou não.
DisjunçãoA interpretação de é: temos uma prova de ou uma prova de .
Temos na lógica intuicionista o seguinte teorema:
A e B são mutuamente exclusivos e não são demonstráveis simultaneamente. Esta situação é comparável ao que seria na lógica clássica de Boole e Karnaugh .
Por outro lado, o seguinte teorema:
é válido na lógica intuicionista, mas não em seu inverso. Na verdade, se x é um número real, sabemos que se é racional, então não é irracional, mas não somos, de forma alguma, capazes de concluir se esse número é irracional ou não.
Quantificador existencialA interpretação é: podemos criar um objeto e provar isso . A existência de x é aqui eficaz ou construtiva. Não se trata da existência teórica de um elemento de verificação .
Nós temos o seguinte teorema:
Se não houver x que satisfaça A (x), então para todo x não verificamos A (x) , daí a equivalência (que corresponde à intuição e é formulada naturalmente). Esta propriedade é comparável ao que seria na lógica clássica.
Quantificador universalA interpretação de é: temos uma prova de que para cada x pertencente ao conjunto especificado, podemos provar A (x) (comparável ao que é na lógica clássica).
Temos na lógica intuicionista o seguinte teorema:
Mas, ao contrário do que seria na lógica clássica, o inverso é falso. Na verdade, esse inverso exigiria que, supondo que a universalidade da propriedade seja contraditória , alguém seja capaz de exibir explicitamente um objeto invalidador x , o que raramente é possível.
Podemos dizer também que, na lógica intuicionista, a afirmação de é a afirmação da existência efetiva e construtível de um objeto validador x , enquanto sua única existência teórica, expressando apenas que é contraditório que é universalmente contraditório. A lógica clássica não faz distinção entre essas duas existências, enquanto a lógica intuicionista considera a segunda como mais fraca do que a primeira.
Terceiro excluídoA seguinte proposição
é um teorema da lógica clássica, mas não da lógica intuicionista. Neste último caso, significaria que podemos provar ou provar , o que nem sempre é possível.
Por exemplo, na aritmética provida de lógica intuicionista (conhecida como aritmética de Heyting ), a expressão é válida, pois para qualquer par de inteiros podemos provar que são iguais ou podemos provar que são diferentes. É o mesmo para dois racionais. Mas por dois reais na análise construtiva , não temos um método geral que permita provar ou provar isso . Esta situação corresponde bem ao que se encontra no algoritmo, onde a igualdade ou a desigualdade entre duas realidades pode ser não computável, ou seja, não decidível.
Relação entre regrasPara melhor compreender, notaremos no que precede, que ao contrário do que está na lógica de Boole, a conjunção não pode ser reformulada em termos de disjunção e que o quantificador existencial não pode ser reformulado em termos de quantificador universal ; isso em virtude do princípio do construtivismo. Dito de outra forma e em termos talvez mais próximos da informática: não é permitido reduzir os constrangimentos de uma expressão.
As interpretações das expressões não são feitas com a ajuda de e , mas graças aos conceitos Comprovado e Contraditório .
Kurt Gödel propôs uma tradução da lógica clássica na lógica intuicionista: a " não-não tradução (in) ", que torna demonstrável na lógica intuicionista qualquer fórmula demonstrável na lógica clássica. Assim, nesse sentido preciso, a lógica intuicionista demonstra nada menos que a lógica clássica.
De forma mais econômica do que a saturação de fórmulas e subfórmulas por duplas negações, Gödel percebeu que se considerarmos uma função do conjunto de fórmulas no conjunto de fórmulas definido por:
onde e são quaisquer fórmulas e é uma fórmula tendo como parâmetro;
então temos o seguinte teorema:
Onde está a dedução clássica e está a dedução intuicionista.
A lógica intuicionista pode ser traduzida na lógica modal clássica S4 fornecida com uma modalidade . A construção diz " é provável". A tradução é definida por:
para qualquer variável proposicional ; ; ; ; .Uma fórmula é válida na lógica intuicionista se e somente se for válida na lógica modal S4 clássica (ou seja, válida em modelos de Kripke reflexivos e transitivos).
O problema de decisão de satisfatibilidade e o problema de decisão de validade na lógica proposicional intuicionista são PSPACE-completos . Além disso, eles permanecem PSPACE-completos mesmo se restringirmos as fórmulas a duas variáveis.