Estilo Fitch para dedução natural

Na lógica matemática , o estilo de dedução natural de Fitch é uma variante da dedução natural . Foi proposto pelo lógico Frederic Brenton Fitch . As demonstrações são apresentadas de forma linear, renunciando à estrutura em árvore proposta por Gentzen .

Introdução

As regras estabelecidas neste parágrafo são aquelas para o cálculo de proposições . Eles permitem encadear logicamente as frases, ou seja, introduzir novas frases como consequências lógicas do que foi dito antes. A cada um dos operadores lógicos fundamentais estão associadas duas regras de dedução. Uma das regras é uma regra introdutória : ela explica como provar uma proposição tendo o operador. A outra regra é uma regra de eliminação : explica como usar uma proposição tendo o operador para continuar o raciocínio.

A introdução e a eliminação são necessárias para poder desmontar e remontar as fórmulas. A busca de uma dedução lógica consiste precisamente em analisar as premissas, isto é, desmontá-las e remontar as peças para formar fórmulas que possam ser ligadas logicamente à conclusão. Às vezes, acredita-se que é muito difícil provar matemática, mas em princípio não é muito diferente de um jogo de construção com cubos.

Regras relativas ao envolvimento

A regra para a introdução de implicação ou a regra para o abandono de uma hipótese provisória afirma que, para provar uma implicação "se P então Q", basta proceder da seguinte forma: definimos P como uma hipótese provisória, então fazemos deduções de todas as anteriores sentenças mais P para chegar a Q. Uma vez que Q é alcançado, podemos deduzir "se P então Q". Insistamos em um ponto: Q é provado sob a hipótese P, mas “se P então Q”, depende apenas das premissas anteriores. Se usarmos o método de Fitch, podemos introduzir uma hipótese provisória em uma dedução a qualquer momento. Basta deslocá-lo para a direita em relação às outras premissas. Qualquer coisa que seja inferida sob uma suposição provisória deve estar abaixo dela ou à sua direita, mas nunca à sua esquerda. A regra introdutória nos permite concluir que provamos “se P então Q” sem a hipótese P. Podemos deslocar “se P então Q” para a esquerda com respeito a P, mas não com respeito às outras premissas usadas. a prova de Q. Notaremos:

{\ displaystyle 1 \ quad \ quad P}

(hipótese provisória)

{\ displaystyle 2 \ quad \ quad Q}

(propriedade deduzida de 1)

{\ displaystyle 3 \ quad P \ to Q}

(introdução da implicação entre as duas linhas 1 e 2)

A regra de eliminação de implicação , ou regra de desprendimento ou modus ponens afirma que, das duas sentenças "P" e "se P, então Q" podemos deduzir "Q". Permite passar de condições já conhecidas, P, para novas condições, Q, desde que haja uma lei que o autorize, “se P então Q”, a qual se notará:

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad P \ to Q}

{\ displaystyle 3 \ quad Q}

(eliminação da implicação entre as linhas 1 e 2)

Vamos mostrar, por exemplo, que com essas duas regras podemos deduzir "se P, então R" das duas sentenças "se P, então Q" e "se Q, então R":

{\ displaystyle 1 \ quad P \ to Q}

(hipótese)

{\ displaystyle 2 \ quad Q \ to R}

(hipótese)

{\ displaystyle 3 \ quad \ quad P}

(hipótese provisória)

{\ displaystyle 4 \ quad \ quad Q}

(modus ponens em 3 e 1)

{\ displaystyle 5 \ quad \ quad R}

(modus ponens em 4 e 2)

{\ displaystyle 6 \ quad P \ to R}

(regra de introdução de implicação entre 3 e 5, abandono da hipótese provisória P).

As regras relativas à conjunção

Para a conjunção, as regras são muito simples.

A regra para a introdução da conjunção afirma que das duas sentenças A e B podemos deduzir a sentença (A e B).

{\ displaystyle 1 \ quad A}

{\ displaystyle 2 \ quad B}

{\ displaystyle 3 \ quad A \ land B}

(introdução da conjunção entre 1 e 2)

A regra de eliminação da conjunção afirma que, da sentença (A e B), podemos deduzir as duas sentenças A e B tomadas separadamente.

{\ displaystyle 1 \ quad A \ land B}

{\ displaystyle 2 \ quad A}

(eliminação da conjunção 1)

{\ displaystyle 3 \ quad B}

(eliminação da conjunção 1)

Essas regras permitem reunir ou, ao contrário, asserções separadas que são todas consideradas verdadeiras. É a forma lógica da capacidade da razão de analisar o mundo, isto é, estudar suas partes separadamente, e sintetizá-lo, isto é, reunir os elementos de um estudo. Em um todo. É por isso que essas regras também são chamadas de regras de análise e resumo.

As regras relativas à rescisão

As duas regras de dedução para disjunção são as seguintes.

A regra introdutória de disjunção ou regra de enfraquecimento de uma tese afirma que, da sentença P podemos deduzir a sentença (P ou Q), bem como a sentença (Q ou P), qualquer ou a sentença Q. Esta regra pode não parece interessante, mas na verdade é muito importante. Às vezes é vantajoso deduzir (P ou Q) depois de ter provado P, porque também podemos saber que (P ou Q) tem outras consequências.

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad P \ lor Q}

(introdução da disjunção de 1)

e o mesmo

{\ displaystyle 1 \ quad Q}

{\ displaystyle 2 \ quad P \ lor Q}

(introdução da disjunção de 1)

A regra de eliminação de disjunção ou regra de disjunção de hipótese ou regra de distinção de caso afirma que, se provamos (P ou Q) e também provamos (se P, então R), bem como (se Q então R), então provamos R. Esta regra é útil quando examinamos vários casos possíveis que levam à mesma conclusão.

{\ displaystyle 1 \ quad P \ lor Q}

{\ displaystyle 2 \ quad \ quad P}

(hipótese provisória)

{\ displaystyle 3 \ quad \ quad R}

(propriedade deduzida de 2)

{\ displaystyle 4 \ quad P \ to R}

(introdução da implicação entre 2 e 3)

{\ displaystyle 5 \ quad \ quad Q}

(hipótese provisória)

{\ displaystyle 6 \ quad \ quad R}

(propriedade deduzida de 5)

{\ displaystyle 7 \ quad Q \ to R}

(introdução de implicação entre 5 e 6)

{\ displaystyle 8 \ quad R}

(eliminação da disjunção entre 1, 4, 7)

As regras relacionadas à negação

A regra para introduzir a negação afirma que, se provarmos uma contradição a partir de uma hipótese P, então esta é necessariamente falsa e, portanto, sua negação é verdadeira. Assim, se em uma dedução sob a hipótese provisória P, encontramos uma contradição (Q e não Q), também observada , então podemos deduzir não P de todas as premissas anteriores, exceto P. Com o método de Fitch, portanto, mudamos (não P ) para a esquerda em relação a P, que é representado da seguinte forma: $\ robô$

{\ displaystyle 1 \ quad \ quad \ quad P}

{\ displaystyle 2 \ quad \ quad \ quad \ bot}

{\ displaystyle 3 \ quad \ lnot P}

(introdução da negação entre 1 e 2)

A regra de eliminação da negação ou regra de eliminação da dupla negação ou raciocínio por absurdo afirma que, de (não P) podemos deduzir P. É de fato raciocinar pelo absurdo porque em, tal raciocínio, provar P , assumimos (não P) e procuramos obter uma contradição. Se for esse o caso, provamos (não P) de acordo com a regra de introdução da negação, e é de fato a regra de eliminação da dupla negação que torna possível concluir em P:

{\ displaystyle 1 \ quad \ lnot \ lnot P}

{\ displaystyle 2 \ quad P}

(eliminação da dupla negação 1)

{\ displaystyle 1 \ quad \ quad \ lnot P}

(hipótese provisória [raciocínio pelo absurdo])

{\ displaystyle 2 \ quad \ quad \ bot}

{\ displaystyle 3 \ quad \ lnot \ lnot P}

(introdução da negação entre 1 e 2)

{\ displaystyle 4 \ quad P}

(eliminação da dupla negação 3)

Quando consideramos que toda frase é necessariamente verdadeira ou falsa, a validade desta última regra é óbvia. É característico da lógica clássica , que é apresentada aqui e é usada pela grande maioria dos cientistas. Às vezes é contestado por causa de um problema importante, o das provas de existência pelo absurdo. Às vezes, você pode provar que um problema tem solução sem ser capaz de encontrá-la. Para isso, basta provar que a ausência de solução conduz a uma contradição. O raciocínio pelo absurdo permite então concluir que não é verdade que o problema não tem solução: não não (o problema tem solução). Na lógica clássica, removemos a dupla negação para concluir que o problema tem uma solução. No entanto, a abordagem assim seguida não fornece nenhum processo construtivo para a solução buscada. Esta objeção foi levantada por certos matemáticos e lógicos, incluindo Brouwer , que contestou este método e se opôs a Hilbert que o defendeu. Os matemáticos construtivistas ou intuicionistas consideram que uma prova de existência não tem sentido se não fornecer também um processo construtivo para o objeto em questão. Também estes últimos rejeitam a regra de supressão da dupla negação para substituí-la pela seguinte regra: de P e (não P), pode-se deduzir uma contradição, e dessa contradição qualquer proposição Q (princípio do ex falso quodlibet ).

{\ displaystyle 1 \ quad P}

{\ displaystyle 2 \ quad \ lnot P}

{\ displaystyle 3 \ quad \ bot}

{\ displaystyle 4 \ quad Q}

(eliminação da negação 2 na lógica intuicionista)

Nos exemplos, usaremos essa segunda regra de eliminação quando for possível dispensar a regra de eliminação duplo-negativo.

Podemos introduzir outras regras para os outros operadores booleanos, em particular o operador de equivalência, mas isso não é necessário, porque esses operadores podem ser definidos a partir dos anteriores e suas regras de dedução podem então ser deduzidas das regras anteriores. (P é equivalente a Q) é definido por ((se P então Q) e (se Q então P)).

Exemplos

Damos a seguir alguns exemplos do uso da dedução natural. Na primeira parte, não usaremos a regra para eliminar a dupla negação. Na segunda parte, usaremos essa regra. As fórmulas deduzidas nesta segunda parte não são reconhecidas como válidas pelos matemáticos intuicionistas . Usaremos os seguintes símbolos: para se ... então ... , para ou , para e , para não . O símbolo designa uma contradição, ou seja, uma proposição falsa. $\ para$ $\ lor$ $\ terra$ $\ lnot$ $\ robô$

Exemplos que não usam eliminação de dupla negação

Exemplo 1 : ${\ displaystyle (\ lnot A \ land \ lnot B) \ to \ lnot (A \ lor B)}$

{\ displaystyle 01 \ quad \ quad \ lnot A \ land \ lnot B}

(hipótese provisória)

{\ displaystyle 02 \ quad \ quad \ lnot A}

(eliminação da conjunção 01)

{\ displaystyle 03 \ quad \ quad \ lnot B}

(eliminação da conjunção 01)

{\ displaystyle 04 \ quad \ quad \ quad A \ lor B}

(hipótese provisória)

{\ displaystyle 05 \ quad \ quad \ quad \ quad A}

(hipótese provisória)

{\ displaystyle 06 \ quad \ quad \ quad \ quad \ bot}

contradição entre 02 e 05

{\ displaystyle 07 \ quad \ quad \ quad A \ to \ bot}

(introdução da implicação entre 05 e 06)

{\ displaystyle 08 \ quad \ quad \ quad \ quad B}

(hipótese provisória)

{\ displaystyle 09 \ quad \ quad \ quad \ quad \ bot}

contradição entre 03 e 08

{\ displaystyle 10 \ quad \ quad \ quad B \ to \ bot}

(introdução da implicação entre 08 e 09)

{\ displaystyle 11 \ quad \ quad \ quad \ bot}

(eliminação da disjunção entre 04, 07, 10)

{\ displaystyle 12 \ quad \ quad \ lnot (A \ lor B)}

(introdução da negação entre 04 e 11)

{\ displaystyle 13 \ quad (\ lnot A \ land \ lnot B) \ to \ lnot (A \ lor B)}

(introdução da implicação entre 01 e 12 e fim da dedução)

Mostramos que o inverso também é válido. Mostramos também que , mas para a recíproca desta última propriedade, utilizamos a eliminação da dupla negação. ${\ displaystyle \ lnot (A \ lor B) \ to (\ lnot A \ land \ lnot B)}$ ${\ displaystyle (\ lnot A \ lor \ lnot B) \ to \ lnot (A \ land B)}$

Exemplo 2 : ${\ displaystyle A \ to \ lnot \ lnot A}$

{\ displaystyle 01 \ quad \ quad A}

(hipótese provisória)

{\ displaystyle 02 \ quad \ quad \ quad \ lnot A}

(hipótese provisória)

{\ displaystyle 03 \ quad \ quad \ quad \ bot}

(eliminação da negação entre 01 e 02)

{\ displaystyle 04 \ quad \ quad \ lnot \ lnot A}

(introdução da negação entre 02 e 03)

{\ displaystyle 05 \ quad A \ to \ lnot \ lnot A}

(introdução da implicação entre 01 e 04, fim da dedução)

O inverso decorre diretamente da eliminação da dupla negação e é rejeitado pelos intuicionistas. Mas, curiosamente, não é o mesmo com quem se prova sem essa hipótese, e quem, por sua vez, é aceito pelos intuicionistas. ${\ displaystyle \ lnot \ lnot A \ to A}$ ${\ displaystyle \ lnot \ lnot \ lnot A \ to \ lnot A}$

Exemplo 3 : ${\ displaystyle \ lnot \ lnot \ lnot A \ to \ lnot A}$

{\ displaystyle 01 \ quad \ quad \ lnot \ lnot \ lnot A}

(hipótese provisória)

{\ displaystyle 02 \ quad \ quad \ quad A}

(hipótese provisória)

{\ displaystyle 03 \ quad \ quad \ quad A \ to \ lnot \ lnot A}

(teorema do exemplo 2)

{\ displaystyle 04 \ quad \ quad \ quad \ lnot \ lnot A}

(eliminação de envolvimento ou modus ponens entre 02 e 03)

{\ displaystyle 05 \ quad \ quad \ quad \ bot}

(eliminação da negação entre 01 e 04)

{\ displaystyle 06 \ quad \ quad \ lnot A}

(introdução da negação entre 02 e 05)

{\ displaystyle 07 \ quad \ lnot \ lnot \ lnot A \ to \ lnot A}

(introdução da implicação entre 01 e 06, fim da dedução)

Exemplos usando a eliminação de dupla negação

Os exemplos a seguir usam a eliminação da negação dupla. Pode-se comprovar que esse uso é necessário. Portanto, eles não são aceitos na lógica intuicionista .

Exemplo 4 : ${\ displaystyle \ lnot (A \ land B) \ to (\ lnot A \ lor \ lnot B)}$

{\ displaystyle 01 \ quad \ quad \ lnot (A \ land B)}

(hipótese provisória [raciocínio pelo absurdo])

{\ displaystyle 02 \ quad \ quad \ quad \ lnot (\ lnot A \ lor \ lnot B)}

(hipótese provisória)

{\ displaystyle 03 \ quad \ quad \ quad \ lnot (\ lnot A \ lor \ lnot B) \ to (\ lnot \ lnot A \ land \ lnot \ lnot B)}

(teorema, recíproco do exemplo 1)

{\ displaystyle 04 \ quad \ quad \ quad \ lnot \ lnot A \ land \ lnot \ lnot B}

(eliminação de envolvimento ou modus ponens entre 02 e 03)

{\ displaystyle 05 \ quad \ quad \ quad A \ land B}

(eliminação da dupla negação em 04)

{\ displaystyle 06 \ quad \ quad \ quad \ bot}

(eliminação da negação entre 01 e 05)

{\ displaystyle 07 \ quad \ quad \ lnot \ lnot (\ lnot A \ lor \ lnot B)}

(introdução da negação entre 02 e 06)

{\ displaystyle 08 \ quad \ quad \ lnot A \ lor \ lnot B}

(eliminação da dupla negação em 07)

{\ displaystyle 09 \ quad \ lnot (A \ land B) \ to (\ lnot A \ lor \ lnot B)}

(introdução da implicação entre 01 e 08)

Exemplo 5 : se não requer a eliminação da dupla negação, este é necessário para provar o contrário . ${\ displaystyle (A \ to B) \ to (\ lnot B \ to \ lnot A)}$ ${\ displaystyle (\ lnot B \ to \ lnot A) \ to (A \ to B)}$

Exemplo 6 : Podemos mostrar isso . Na verdade, se nós e , temos (falso) e, portanto, temos . ${\ displaystyle \ lnot A \ to (A \ to B)}$ $\ lnot A$ $NO$ $\ robô$ $B$

Exemplo 7 : da mesma forma, a prova da validade do terceiro excluído usa a eliminação da dupla negação. Assumindo isso , deduzimos (recíproco do exemplo 1), portanto, uma contradição e a validade de . $A \ lor \ lnot A$ ${\ displaystyle \ lnot (A \ lor \ lnot A)}$ ${\ displaystyle \ lnot A \ land \ lnot \ lnot A}$ ${\ displaystyle \ lnot \ lnot (A \ lor \ lnot A)}$

Se os intuicionistas rejeitam os excluídos, eles aceitam, é claro, o princípio da não contradição . Na verdade, a suposição é uma contradição. Temos, portanto, pela introdução da negação. $\ lnot (A \ land \ lnot A)$ ${\ displaystyle A \ land \ lnot A}$ $\ lnot (A \ land \ lnot A)$

Exemplo 7 conhecido sob o nome lei de Peirce : . Curiosamente, embora não contenha uma negação, a dedução desta lei exige a eliminação da dupla negação, por exemplo, através do uso do terceiro excluído. Supomos que sim . De acordo com o terceiro excluído: ${\ displaystyle ((A \ para B) \ para A) \ para A}$ ${\ displaystyle ((A \ para B) \ para A)}$

ou nós temos , $NO$

ou temos e portanto temos (exemplo 6) e como temos com o modus ponens, temos . $\ lnot A$ ${\ displaystyle A \ a B}$ ${\ displaystyle ((A \ para B) \ para A)}$ $NO$

As regras de dedução para quantificadores

O uso de nomes de variáveis em teorias de primeira ordem

As regras de dedução para operadores universais e existenciais governam o uso de nomes de variáveis. Esse uso confere a uma teoria o poder de generalidade, ou seja, a possibilidade de conhecer não cada indivíduo tomado isoladamente, mas todos os indivíduos do mesmo gênero, em uma única frase.

As regras para usar variáveis especificam as condições sob as quais os nomes das variáveis podem ser introduzidos e o que pode ser dito sobre elas. Essas regras são naturais, mas existem algumas dificuldades técnicas sobre as noções de termo, ocorrência livre ou vinculada de uma variável, substituição de um termo por ocorrências de uma variável e substituição de uma variável por ocorrências de um termo.

Para que uma teoria possa usar a lógica de primeira ordem é necessário ter definido um domínio de objetos e é necessário que os predicados atribuídos pela teoria aos seus objetos não sejam eles próprios objetos da teoria.

O significado de um nome de variável de objeto é representar qualquer objeto da teoria: seja x um número. Freqüentemente, introduzimos um nome de variável em premissas que determinam as condições gerais desse objeto. x é qualquer objeto da teoria, desde que satisfaça estas condições: seja x um número primo ... Uma teoria geralmente contém nomes para seus objetos. A teoria dos números inteiros contém, por exemplo, nomes para todos os números: 0, 1, 2, ..., -1, -2, ...

Os termos podem ser simples ou compostos. Esses são os nomes dos objetos, os nomes das variáveis dos objetos e todas as expressões compostas que podem ser formadas a partir deles aplicando os operadores de objetos da teoria. Por exemplo, 1, x, x + 1 e (x + x) +1 são termos da teoria dos números.

Vamos primeiro lembrar a distinção muito importante entre as variáveis vinculadas por um operador e as outras, as variáveis livres. As ocorrências de um nome de variável em uma frase são todos os lugares onde esse nome aparece. Uma ocorrência pode ser gratuita ou vinculada. Quando um operador existencial ou universal em x é aplicado a uma frase complexa, todas as ocorrências de x tornam-se ligadas por este operador. Todas as ocorrências que não estão vinculadas são gratuitas.

Se uma frase contém vários operadores existenciais e universais, é desejável que todos esses operadores se relacionem com diferentes nomes de variáveis. Esta regra não é essencial. Não é respeitado quando colocamos o cálculo de predicados na forma de uma álgebra cilíndrica (uma álgebra cilíndrica é uma álgebra booleana completada por leis específicas para operadores universais e existenciais). Mas é sempre respeitado na prática porque ajuda a evitar confusão.

Uma frase é obtida de outra substituindo um termo t para as ocorrências de uma variável x quando todas as ocorrências livres de x foram substituídas por t. Por exemplo, (o pai de x é humano e o pai de x é honesto) é obtido substituindo o termo pai de x pela variável y na fórmula (y é humano ey é honesto).

Essas preliminares permitem formular as regras de dedução para operadores universais e existenciais.

As regras relativas ao quantificador universal

A regra introdutória do quantificador universal ou regra de generalização afirma que, de P (x) podemos deduzir (para todo x, P (x)) desde que o nome da variável x nunca apareça nas hipóteses das quais P (x) depende.

{\ displaystyle 1 \ quad P (x)}

{\ displaystyle 2 \ quad \ forall x \; P (x)}

(introdução de qualquer coisa , onde x não é livre nas premissas de P)

Muitas vezes, as variáveis são introduzidas em premissas provisórias. Então, raciocinamos sobre eles como se fossem objetos. Podemos então deduzir dele leis gerais, porque o que deduzimos é verdadeiro para todos os objetos que satisfazem as mesmas hipóteses. São as regras para o abandono de uma hipótese provisória e para a generalização que nos permitem concluir.

A regra de eliminação do quantificador universal ou regra de singularização afirma que, de uma sentença da forma (para todo x) P (x), podemos deduzir P (t), para qualquer termo t do qual as variáveis não estão relacionadas em P (x ) P (x) designa qualquer sentença que contém x como uma variável livre, P (t) designa a sentença obtida de P (x) substituindo t por todas as ocorrências livres de x. A regra de singularização é simplesmente aplicar uma lei universal a um caso singular.

{\ displaystyle 1 \ quad \ forall x \; P (x)}

{\ displaystyle 2 \ quad P (t)}

(eliminação de tudo )

Regras relativas ao quantificador existencial

A regra introdutória do quantificador existencial , ou regra de provas diretas da existência, afirma que, a partir da sentença P (t), podemos deduzir que existe um x tal que P (x) para qualquer variável x que não aparecem em P (t) e para qualquer termo t cujos nomes de variáveis não estão relacionados em P (x).

P (t) denota qualquer sentença que contenha o termo t pelo menos uma vez. P (x) é obtido de P (t) substituindo x por t em uma ou mais de suas ocorrências. Nesta regra, não é necessário substituir x para todas as ocorrências de t.

{\ displaystyle 1 \ quad P (t)}

{\ displaystyle 2 \ quad \ exists x \; P (x)}

( existe introdução de lá )

A regra de eliminação do quantificador existencial ou regra das consequências da existência permite, a partir de uma proposição (existe x, P (x)), introduzir uma nova hipótese provisória P (y) onde y é um nome de variável que nunca foi usado antes e onde P (y) é obtido de P (x) substituindo y por todas as ocorrências de x. Podemos então raciocinar sob essa hipótese. A regra das consequências da existência, então, torna possível concluir o seguinte: da sentença (existe um x tal que P (x)) podemos deduzir R quando R foi deduzido sob a única hipótese provisória adicional P ( y) e que y não aparece nas premissas anteriores a P (y) nem em R. y é um tipo de ser hipotético. Ele serve apenas como um intermediário em uma dedução, mas não aparece nem em suas premissas nem em sua conclusão.

{\ displaystyle 1 \ quad \ exists x \; P (x)}

(hipótese)

{\ displaystyle 2 \ quad \ quad P (y)}

( y nova variável)

{\ displaystyle 3 \ quad \ quad R}

(dedução de 2, R não envolvendo y )

{\ displaystyle 4 \ quad R}

(eliminação de existe em 1 e 3)

Exemplos

Exemplo 1 ${\ displaystyle (\ existing x \; \ lnot A (x)) \ to (\ lnot \ forall x \; A (x))}$

{\ displaystyle 1 \ quad \ quad \ exists x \; \ lnot A (x)}

(hipótese provisória)

{\ displaystyle 2 \ quad \ quad \ quad \ forall x \; A (x)}

(hipótese provisória)

{\ displaystyle 3 \ quad \ quad \ quad \ quad \ lnot A (y)}

( y nova variável de 1)

{\ displaystyle 4 \ quad \ quad \ quad \ quad A (y)}

(eliminação de qualquer coisa em 2)

{\ displaystyle 5 \ quad \ quad \ quad \ quad \ bot}

(eliminação da negação 3, 4)

{\ displaystyle 6 \ quad \ quad \ quad \ bot}

(a eliminação existe entre 1 e 5)

{\ displaystyle 7 \ quad \ quad \ lnot (\ forall x \; A (x))}

(introdução de negação entre 2 e 6)

{\ displaystyle 8 \ quad (\ existing x \; \ lnot A (x)) \ to (\ lnot \ forall x \; A (x))}

(introdução da implicação 1, 7)

Exemplo 2 : também temos , mas a prova requer uma eliminação da dupla negação, e este teorema da lógica clássica não é aceito na lógica intuicionista. ${\ displaystyle \ lnot (\ forall x \; A (x)) \ to \ exists x (\ lnot A (x))}$

Como verificar a exatidão de um raciocínio?

A essas doze regras, ou quatorze, se contarmos que a regra de eliminação da conjunção é de fato uma regra dupla, e o mesmo para a regra de introdução da disjunção, devemos adicionar uma décima quinta, muito simples, a regra de repetição : você sempre pode repetir uma tese anterior, a menos que dependa de uma hipótese que foi abandonada. Podemos, portanto, repetir todas as teses, desde que não as movamos para a esquerda. Essa regra é necessária quando se deseja repetir uma premissa em uma conclusão ou quando se precisa de uma tese anterior no corpo de uma dedução sob hipótese provisória para aplicar uma regra.

A lista das quinze regras anteriores é completa no sentido de que é suficiente para fazer todas as deduções corretas. Kurt Gödel provou, ( Teorema da Completude ) para um sistema lógico diferente, mas equivalente ao que acabamos de apresentar, que basta formalizar todas as deduções corretas do Cálculo dos predicados de primeira ordem .

As deduções corretas são, em primeiro lugar, aquelas que respeitam estritamente essas regras fundamentais. Todas as sentenças devem ser axiomas, ou hipóteses provisórias, ou consequências das sentenças que as precedem em virtude de uma das quinze regras. Por uma questão de velocidade, você também pode usar regras derivadas (por exemplo, encaminhar por ). Uma regra derivada é correta quando pode ser mostrado que qualquer coisa que pode ser deduzida com ela também pode ser deduzida sem ela, apenas com as regras básicas. ${\ displaystyle \ lnot (A \ lor B)}$ ${\ displaystyle (\ lnot A \ land \ lnot B}$

Desde que as deduções sejam formalizadas, é sempre possível reconhecer, inclusive por meio de um programa, se uma dedução está correta porque as regras de dedução são em número finito e sempre é possível verificar em um tempo finito se uma fórmula é a consequência de um ou mais outros sob uma dessas regras. Esta abordagem realiza parte do programa às vezes denominado finitaire proposto por David Hilbert para resolver os problemas dos fundamentos da matemática. Hilbert estava procurando um método eficiente que permita decidir por qualquer enunciado matemático se é um teorema, isto é, uma verdade matemática. O cálculo de predicados tornou possível reduzir o problema à questão de se uma fórmula é uma lei lógica ou não.

Mas se é possível verificar a validade de uma dedução que leva a uma fórmula, inversamente, a questão de se uma dada fórmula é uma lei lógica ou não não pode ser resolvida em geral. Na verdade, não existe um método universal que permita dizer se uma fórmula é uma lei lógica ou não. Esta inexistência é deduzida do teorema da incompletude de Gödel . Diz-se que a questão de saber se uma fórmula é uma lei lógica é indecidível.

Verificar a exatidão das deduções na linguagem atual é mais difícil. É necessário primeiro traduzir as frases familiares para uma linguagem formalizada de cálculo de predicados. Esta etapa às vezes representa um problema se você tiver dúvidas sobre a precisão da tradução. Mas a maior dificuldade vem do fato de que as deduções atuais geralmente deixam um grande lugar para o implícito. Mesmo as relações de dependência de uma hipótese nem sempre são explicitadas. Ao contrário, as deduções formais não deixam nada às escuras. As que são propostas aqui são muito semelhantes às deduções atuais, exceto que explicam tudo. A fim de certificar o correto raciocínio e as demonstrações usuais, tudo o que está implícito deve ser explicado. Por isso, muitas vezes é necessário estudar muito e conhecer todo o implícito antes de saber se um raciocínio está correto.

Bibliografia

Jon Barwise e John Etchemendy , Language proof and logic , Seven Bridges Press e CSLI, 1999.
Pelletier, Jeff, " A History of Natural Deduction and Elementary Logic Textbooks. "

Estilo Fitch para dedução natural

Introdução

Regras relativas ao envolvimento

As regras relativas à conjunção

As regras relativas à rescisão

As regras relacionadas à negação

Exemplos

Exemplos que não usam eliminação de dupla negação

Exemplos usando a eliminação de dupla negação

As regras de dedução para quantificadores

O uso de nomes de variáveis ​​em teorias de primeira ordem

As regras relativas ao quantificador universal

Regras relativas ao quantificador existencial

Exemplos

Como verificar a exatidão de um raciocínio?

Bibliografia

O uso de nomes de variáveis em teorias de primeira ordem