·
Ciência da Computação ·
Lógica
Envie sua pergunta para a IA e receba a resposta na hora
Recomendado para você
5
Lógica para Computação 3a Prova 2017 2 Inf1009
Lógica
UMG
6
Lógica para Computação 2a Prova 2017 2 Inf1009
Lógica
UMG
3
Lógica para Computação Teste 1 2017 2 Inf1009
Lógica
UMG
4
Atividades Objetivas 3
Lógica
UMG
11
Leis de Morgan - Resumo e Questões
Lógica
UMG
11
17-desafie-o-seu-raciocinio-1
Lógica
UMG
11
Logica Matematica
Lógica
UMG
2
Resumo_cálculo Proposicional parte 2
Lógica
UMG
1
Matemática na Prática Mod2_f3_matematica_discreta 1
Lógica
ITA
2
Lógica Matemática - Questionário 1 - 5 de 5
Lógica
UNIP
Texto de pré-visualização
O Cálculo Proposicional: uma Abordagem Voltada à Compreensão da Linguagem Prolog Maria Carolina Monard 1 Universidade de São Paulo / IILTC Instituto de Ciências Matemáticas de São Carlos Departamento de Ciência de Computação e Estatística Maria do Carmo Nicoletti Universidade Federal de São Carlos / IILTC Departamento de Computação Raul Hideo Noguchi 1 Universidade de São Paulo Instituto de Ciências Matemáticas de São Carlos Departamento de Ciência de Computação e Estatística Versão 1.0 Agosto 1992 1Trabalho realizado com auxílio do RHAE/IILTC — Instituto de Lógica Filosofia e Teoria da Ciência Contents 1 Cálculo Proposicional ........................................... 2 1.1 Proposições .................................................. 2 1.2 Proposições Compostas .......................................... 3 1.3 Fórmulas Bem Formadas .......................................... 4 1.4 Tabelas-Verdade das Fórmulas Bem Formadas .......................... 5 1.5 Semântica do Cálculo Proposicional .................................. 6 1.6 Validade e Inconsistência .......................................... 6 1.7 Consequência Lógica .............................................. 7 1.8 Equivalência Lógica .............................................. 9 1.9 Propriedades da Negação, Conjunção e Disjunção .................... 10 1.10 Fórmulas Proposicionais Equivalentes .............................. 11 1.11 Verificação de Validade de Argumentos ............................. 12 1.12 Exemplos ....................................................... 13 2 Método Sintático de Prova de Teoremas ................................ 15 2.1 Considerações Preliminares ....................................... 15 2.2 Prova Sintática de Teoremas ....................................... 16 2.3 Algoritmo de Wang ................................................ 17 2.3.1 Regras de Transformação ......................................... 18 2.3.2 Regras de Parada ................................................ 20 2.4 Implementações do Algoritmo de Wang ................................ 21 2.4.1 Implementação de I. Pereira ..................................... 22 2.4.2 Implementação de MCM-MCN ....................................... 31 3 Forma Normal ..................................................... 38 3.1 Forma Normal Conjuntiva — FNC ..................................... 38 3.2 Obtenção da FNC de uma Fórmula Não Tautológica usando Tabela- Verdade ............................................. 39 3.3 Forma Normal Disjuntiva — FND ..................................... 39 3.4 Obtenção da FND de uma Fórmula Não Contraditória usando Tabela- Verdade ............................... 40 3.5 Obtenção da FND e FNC sem o Uso de Tabela-Verdade ................... 41 3.6 Notação Clausal ................................ 42 3.7 Procedimento de Prova por Resolução ......................... 45 3.8 Procedimentos para se usar Resolução ....................... 45 3.9 Exemplos de uso de Resolução ......................... 46 3.9.1 Usando Prova por Redução ao Absurdo através da Negação da Tese .................................... 47 3.9.2 Usando Prova por Redução ao Absurdo através da Negação do Teorema .................................... 47 3.10 Vantagens do Método de Resolução .................... 48 3.11 Propriedades do Cálculo Proposicional .................... 49 4 Programas Prolog Relacionados ao Cálculo Proposicional 49 4.1 Determinação do Valor-verdade de uma Fórmula do Cálculo Proposicional ........................ 50 4.1.1 Versão I ................................ 50 4.1.2 Versão II ................................ 53 4.2 Conversão de uma Fórmula do Cálculo Proposicional para a Forma Clausal 56 5 Conclusões .................................... 65 3. as únicas wff são aquelas definidas por 1. e 2. Cada uma das expressões envolvendo α e β é chamada de forma sentencial. Uma forma sentencial é uma especificação abstrata da sintaxe de um número infinito de wff compostas de símbolos que representam proposições atômicas. Uma wff que sintaticamente se ajusta a uma forma sentencial é chamada de uma instância de substituição da forma sentencial. Por exemplo, a wff: p ∧ (q → r) é uma instância de substituição de qualquer uma das seguintes formas sentenciais: 1. α onde α é p ∧ (q → r) 2. α ∧ β onde α é p e β é q→r 3. α∧ (β →γ) onde α é p, β é q e γ é r 1.4 Tabelas-Verdade das Fórmulas Bem Formadas A forma de uma wff, isto é, a maneira como é construída a partir de proposições e conectivos lógicos, é denominada de sintaxe da wff. A semântica — ou significado — de uma wff (tratada na seção 1.6) é o valor-verdade associado a ela. Os valores-verdade de uma wff são definidos em termos dos valores-verdade de seus componentes atômicos. Geralmente, uma tabela-verdade é usada para tabelar os valores-verdade de suas componentes atômicas e os valores-verdade de seus componentes mostrados a seguir: | a | β | a∧β | a∨β | ¬a | a→β | a↔β | |---|---|------|------|----|------|-------| | v | v | v | v | f | v | v | | v | f | f | v | f | f | f | | f | v | f | v | v | v | f | | f | f | f | f | v | v | v | Prioridade dos Conectivos Dada a wff a∨β → γ, existe a dúvida desta wff ser (a∨β) → γ ou a∨(β →γ). Este problema pode ser contornado através do estabelecimento de uma hierarquia total ou parcial entre os conectivos. A convenção de prioridade que a maioria dos autores estabelece para os conectivos tem a seguinte ordem decrescente de precedência: ¬ maior ∧ ∨ → ↔ menor α→β∨γ significa α→ (β∨γ) α∨β∧γ significa α∨ (β∧γ) α→β∧¬γ∨δ significa α→ ((β∧¬γ)∨ δ) A precedência estabelecida pode ser alterada através da introdução de parênteses. 1.5 Semântica do Cálculo Proposicional Como visto durante a construção de tabelas-verdade — seção 1.4 — o significado de uma fórmula do Cálculo Proposicional é dado pela interpretação dessa fórmula, ou seja, pela atribuição apropriada de valores-verdade v, f — a cada um de seus componentes. Assim, a semântica do Cálculo Proposicional consiste na interpretação de suas fórmulas. Se β for uma fórmula, uma interpretação de β consiste na atribuição de valores-verdade v (ou f) às fórmulas atômicas componentes de β, levando-se em consideração a interpretação dos conectivos ∨, ∧, →, ¬ e ↔. Seja a fórmula ((p ∨ q) → (p ∧ q)) Como esta fórmula possui dois componentes atômicos, ela admite 22 interpretações, onde 2 representa o número de componentes atômicos da fórmula. Para uma fórmula com n componentes atômicos, a tabela-verdade terá 2n linhas, uma linha para cada interpretação. | interpretação | p | q | p∨q | p∧q | (p∨q) | (p∧q) | |---------------|---|---|-----|-----|-------|-------| | interpretação 1 | v | v | v | v | v | v | | interpretação 2 | v | f | v | f | f | f | | interpretação 3 | f | v | v | f | f | f | | interpretação 4 | f | f | f | f | f | v | 1.6 Validade e Inconsistência O valor-verdade — ou simplesmente valor — de uma fórmula diz sempre respeito a uma particular interpretação. Com isto pode-se ter as seguintes situações: 1. Se uma fórmula β tem valor v numa certa interpretação I, diz-se que β é verdadeira na interpretação I. No exemplo anterior, (p ∨ q) → (p ∧ q) é verdadeira nas interpretações 1 e 4. 2. Se uma fórmula β é verdadeira segundo alguma interpretação, diz-se que β é satisfatível (ou consistente). Por exemplo, a fórmula do exemplo anterior é satisfatível. 3. Uma fórmula β é válida quando for verdadeira em todas as suas interpretações. São chamadas tautologias. Por exemplo, a fórmula p ∨ ¬p. 4. Se uma fórmula β tem valor f numa interpretação I, diz-se que β é falsa na interpretação I. A fórmula (p ∨ q) → (p ∧ q) é falsa nas interpretações 2 e 3. 5. Uma fórmula β é insatisfatível (ou inconsistente) quando for falsa segundo qualquer interpretação. São também chamadas de contradições. Por exemplo, a fórmula p ∧ ¬p. 6. Uma fórmula β é inválida quando for falsa segundo alguma interpretação. Por exemplo, a fórmula p ∨ q. 7. No Cálculo Proposicional, as fórmulas que não são nem tautologias e nem contradições são comumente chamadas de contingentes. Por exemplo, a fórmula p. As seguintes observações podem então ser constatadas: Uma fórmula é inconsistente se e somente se sua negação é válida; Uma fórmula é válida se e somente se existe pelo menos uma interpretação na qual ela é falsa; Uma fórmula é consistente se e somente se existe pelo menos uma interpretação na qual ela é verdadeira; • Uma fórmula é válida, então ela é consistente, mas não vice-versa; • Se uma fórmula é inconsistente, então ela é inválida. Pode ser verificado através do uso de tabelas-verdade que: (p ∧ ¬p) é inconsistente e portanto inválida (p ∨ ¬p) é válida e portanto consistente (p → ¬p) é inválida, ainda que consistente 1.7 Consequência Lógica Dadas as fórmulas β1, β2, ..., βn e uma fórmula α, diz-se que α é consequência lógica de β1, β2, ..., βn se e somente se para qualquer interpretação em que β1, β2, ..., βn forem simultaneamente verdadeiras, α é também verdadeira. Se α é consequência lógica de β1, β2, ..., βn, diz-se que α segue-se logicamente de β1, β2, ..., βn. Para indicar este fato, usa-se a seguinte notação: β1, β2, ..., βn ⊨ α Os dois teoremas seguintes permitem demonstrar quando uma fórmula α é consequência lógica de uma outra fórmula: Teorema 1.7.1 Dadas as fórmulas β_1, β_2, ... , β_n e uma fórmula α, α é consequência lógica de β_1, β_2, ... , β_n se e somente se a fórmula β_1 ∧ β_2 ∧ ... ∧ β_n → α é uma tautologia. Prova: Condição Necessária: Sejam as fórmulas β_1, β_2, ... , β_n e α, e seja α consequência lógica de β_1, β_2, ... , β_n. Sejam I uma interpretação qualquer. 1. Se β_1, β_2, ..., β_n forem verdade em I, então α também será verdade em I, pois é consequência lógica das β_i’s. Portanto, β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdade em I. 2. Se um dos β_i’s for falso em I, β_1∧β_2∧...∧β_n será também falso em I. Independente do valor de α, β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdadeiro em I. De 1) e 2) tem-se que β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdade em qualquer interpretação, ou seja, β_1 ∧ β_2 ∧ ... ∧ β_n → α é uma tautologia. Condição Suficiente: Do fato de β_1 ∧ β_2 ∧ ... ∧ β_n → α ser uma tautologia, tem-se que β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdade em qualquer interpretação. Se β_1 ∧ β_2 ∧ ... ∧ β_n for verdade em I, α também será verdade em I, ou seja, α é consequência lógica de β_1, β_2, ..., β_n. Teorema 1.7.2 Dadas as fórmulas β_1, β_2, ... , β_n e uma fórmula α, α é consequência lógica de β_1, β_2, ... , β_n se e somente se a fórmula β_1 ∧ β_2 ∧ ... ∧ β_n ∧ ¬α é uma contradição Prova: Sabe-se pelo teorema anterior que: Das as fórmulas β_1, β_2, ... , β_n e α, α é consequência lógica de β_1, β_2, ... , β_n se e somente se β_1 ∧ β_2 ∧ ... ∧ β_n → α for válida. Equivalentemente, α é consequência lógica de β_1, β_2, ..., β_n se e somente se a negação de β_1 ∧ β_2 ∧ ... ∧ β_n → α for uma contradição. Mas ¬(β_1 ∧ β_2 ∧ ... ∧ β_n → α) ≡ ¬(¬(β_1 ∧ β_2 ∧ ... ∧ β_n) ∨ α) ≡ β_1 ∧ β_2 ∧ ... ∧ β_n ∧ ¬α ou seja, β_1 ∧ β_2 ∧ ... ∧ β_n ∧ ¬α é uma contradição. Estes metateoremas são muito importantes. Eles mostram que provar que uma fórmula é consequência lógica de um conjunto finito de fórmulas é equivalente a mostrar que uma fórmula relacionada a ela é uma tautologia ou uma contradição. 8
Envie sua pergunta para a IA e receba a resposta na hora
Recomendado para você
5
Lógica para Computação 3a Prova 2017 2 Inf1009
Lógica
UMG
6
Lógica para Computação 2a Prova 2017 2 Inf1009
Lógica
UMG
3
Lógica para Computação Teste 1 2017 2 Inf1009
Lógica
UMG
4
Atividades Objetivas 3
Lógica
UMG
11
Leis de Morgan - Resumo e Questões
Lógica
UMG
11
17-desafie-o-seu-raciocinio-1
Lógica
UMG
11
Logica Matematica
Lógica
UMG
2
Resumo_cálculo Proposicional parte 2
Lógica
UMG
1
Matemática na Prática Mod2_f3_matematica_discreta 1
Lógica
ITA
2
Lógica Matemática - Questionário 1 - 5 de 5
Lógica
UNIP
Texto de pré-visualização
O Cálculo Proposicional: uma Abordagem Voltada à Compreensão da Linguagem Prolog Maria Carolina Monard 1 Universidade de São Paulo / IILTC Instituto de Ciências Matemáticas de São Carlos Departamento de Ciência de Computação e Estatística Maria do Carmo Nicoletti Universidade Federal de São Carlos / IILTC Departamento de Computação Raul Hideo Noguchi 1 Universidade de São Paulo Instituto de Ciências Matemáticas de São Carlos Departamento de Ciência de Computação e Estatística Versão 1.0 Agosto 1992 1Trabalho realizado com auxílio do RHAE/IILTC — Instituto de Lógica Filosofia e Teoria da Ciência Contents 1 Cálculo Proposicional ........................................... 2 1.1 Proposições .................................................. 2 1.2 Proposições Compostas .......................................... 3 1.3 Fórmulas Bem Formadas .......................................... 4 1.4 Tabelas-Verdade das Fórmulas Bem Formadas .......................... 5 1.5 Semântica do Cálculo Proposicional .................................. 6 1.6 Validade e Inconsistência .......................................... 6 1.7 Consequência Lógica .............................................. 7 1.8 Equivalência Lógica .............................................. 9 1.9 Propriedades da Negação, Conjunção e Disjunção .................... 10 1.10 Fórmulas Proposicionais Equivalentes .............................. 11 1.11 Verificação de Validade de Argumentos ............................. 12 1.12 Exemplos ....................................................... 13 2 Método Sintático de Prova de Teoremas ................................ 15 2.1 Considerações Preliminares ....................................... 15 2.2 Prova Sintática de Teoremas ....................................... 16 2.3 Algoritmo de Wang ................................................ 17 2.3.1 Regras de Transformação ......................................... 18 2.3.2 Regras de Parada ................................................ 20 2.4 Implementações do Algoritmo de Wang ................................ 21 2.4.1 Implementação de I. Pereira ..................................... 22 2.4.2 Implementação de MCM-MCN ....................................... 31 3 Forma Normal ..................................................... 38 3.1 Forma Normal Conjuntiva — FNC ..................................... 38 3.2 Obtenção da FNC de uma Fórmula Não Tautológica usando Tabela- Verdade ............................................. 39 3.3 Forma Normal Disjuntiva — FND ..................................... 39 3.4 Obtenção da FND de uma Fórmula Não Contraditória usando Tabela- Verdade ............................... 40 3.5 Obtenção da FND e FNC sem o Uso de Tabela-Verdade ................... 41 3.6 Notação Clausal ................................ 42 3.7 Procedimento de Prova por Resolução ......................... 45 3.8 Procedimentos para se usar Resolução ....................... 45 3.9 Exemplos de uso de Resolução ......................... 46 3.9.1 Usando Prova por Redução ao Absurdo através da Negação da Tese .................................... 47 3.9.2 Usando Prova por Redução ao Absurdo através da Negação do Teorema .................................... 47 3.10 Vantagens do Método de Resolução .................... 48 3.11 Propriedades do Cálculo Proposicional .................... 49 4 Programas Prolog Relacionados ao Cálculo Proposicional 49 4.1 Determinação do Valor-verdade de uma Fórmula do Cálculo Proposicional ........................ 50 4.1.1 Versão I ................................ 50 4.1.2 Versão II ................................ 53 4.2 Conversão de uma Fórmula do Cálculo Proposicional para a Forma Clausal 56 5 Conclusões .................................... 65 3. as únicas wff são aquelas definidas por 1. e 2. Cada uma das expressões envolvendo α e β é chamada de forma sentencial. Uma forma sentencial é uma especificação abstrata da sintaxe de um número infinito de wff compostas de símbolos que representam proposições atômicas. Uma wff que sintaticamente se ajusta a uma forma sentencial é chamada de uma instância de substituição da forma sentencial. Por exemplo, a wff: p ∧ (q → r) é uma instância de substituição de qualquer uma das seguintes formas sentenciais: 1. α onde α é p ∧ (q → r) 2. α ∧ β onde α é p e β é q→r 3. α∧ (β →γ) onde α é p, β é q e γ é r 1.4 Tabelas-Verdade das Fórmulas Bem Formadas A forma de uma wff, isto é, a maneira como é construída a partir de proposições e conectivos lógicos, é denominada de sintaxe da wff. A semântica — ou significado — de uma wff (tratada na seção 1.6) é o valor-verdade associado a ela. Os valores-verdade de uma wff são definidos em termos dos valores-verdade de seus componentes atômicos. Geralmente, uma tabela-verdade é usada para tabelar os valores-verdade de suas componentes atômicas e os valores-verdade de seus componentes mostrados a seguir: | a | β | a∧β | a∨β | ¬a | a→β | a↔β | |---|---|------|------|----|------|-------| | v | v | v | v | f | v | v | | v | f | f | v | f | f | f | | f | v | f | v | v | v | f | | f | f | f | f | v | v | v | Prioridade dos Conectivos Dada a wff a∨β → γ, existe a dúvida desta wff ser (a∨β) → γ ou a∨(β →γ). Este problema pode ser contornado através do estabelecimento de uma hierarquia total ou parcial entre os conectivos. A convenção de prioridade que a maioria dos autores estabelece para os conectivos tem a seguinte ordem decrescente de precedência: ¬ maior ∧ ∨ → ↔ menor α→β∨γ significa α→ (β∨γ) α∨β∧γ significa α∨ (β∧γ) α→β∧¬γ∨δ significa α→ ((β∧¬γ)∨ δ) A precedência estabelecida pode ser alterada através da introdução de parênteses. 1.5 Semântica do Cálculo Proposicional Como visto durante a construção de tabelas-verdade — seção 1.4 — o significado de uma fórmula do Cálculo Proposicional é dado pela interpretação dessa fórmula, ou seja, pela atribuição apropriada de valores-verdade v, f — a cada um de seus componentes. Assim, a semântica do Cálculo Proposicional consiste na interpretação de suas fórmulas. Se β for uma fórmula, uma interpretação de β consiste na atribuição de valores-verdade v (ou f) às fórmulas atômicas componentes de β, levando-se em consideração a interpretação dos conectivos ∨, ∧, →, ¬ e ↔. Seja a fórmula ((p ∨ q) → (p ∧ q)) Como esta fórmula possui dois componentes atômicos, ela admite 22 interpretações, onde 2 representa o número de componentes atômicos da fórmula. Para uma fórmula com n componentes atômicos, a tabela-verdade terá 2n linhas, uma linha para cada interpretação. | interpretação | p | q | p∨q | p∧q | (p∨q) | (p∧q) | |---------------|---|---|-----|-----|-------|-------| | interpretação 1 | v | v | v | v | v | v | | interpretação 2 | v | f | v | f | f | f | | interpretação 3 | f | v | v | f | f | f | | interpretação 4 | f | f | f | f | f | v | 1.6 Validade e Inconsistência O valor-verdade — ou simplesmente valor — de uma fórmula diz sempre respeito a uma particular interpretação. Com isto pode-se ter as seguintes situações: 1. Se uma fórmula β tem valor v numa certa interpretação I, diz-se que β é verdadeira na interpretação I. No exemplo anterior, (p ∨ q) → (p ∧ q) é verdadeira nas interpretações 1 e 4. 2. Se uma fórmula β é verdadeira segundo alguma interpretação, diz-se que β é satisfatível (ou consistente). Por exemplo, a fórmula do exemplo anterior é satisfatível. 3. Uma fórmula β é válida quando for verdadeira em todas as suas interpretações. São chamadas tautologias. Por exemplo, a fórmula p ∨ ¬p. 4. Se uma fórmula β tem valor f numa interpretação I, diz-se que β é falsa na interpretação I. A fórmula (p ∨ q) → (p ∧ q) é falsa nas interpretações 2 e 3. 5. Uma fórmula β é insatisfatível (ou inconsistente) quando for falsa segundo qualquer interpretação. São também chamadas de contradições. Por exemplo, a fórmula p ∧ ¬p. 6. Uma fórmula β é inválida quando for falsa segundo alguma interpretação. Por exemplo, a fórmula p ∨ q. 7. No Cálculo Proposicional, as fórmulas que não são nem tautologias e nem contradições são comumente chamadas de contingentes. Por exemplo, a fórmula p. As seguintes observações podem então ser constatadas: Uma fórmula é inconsistente se e somente se sua negação é válida; Uma fórmula é válida se e somente se existe pelo menos uma interpretação na qual ela é falsa; Uma fórmula é consistente se e somente se existe pelo menos uma interpretação na qual ela é verdadeira; • Uma fórmula é válida, então ela é consistente, mas não vice-versa; • Se uma fórmula é inconsistente, então ela é inválida. Pode ser verificado através do uso de tabelas-verdade que: (p ∧ ¬p) é inconsistente e portanto inválida (p ∨ ¬p) é válida e portanto consistente (p → ¬p) é inválida, ainda que consistente 1.7 Consequência Lógica Dadas as fórmulas β1, β2, ..., βn e uma fórmula α, diz-se que α é consequência lógica de β1, β2, ..., βn se e somente se para qualquer interpretação em que β1, β2, ..., βn forem simultaneamente verdadeiras, α é também verdadeira. Se α é consequência lógica de β1, β2, ..., βn, diz-se que α segue-se logicamente de β1, β2, ..., βn. Para indicar este fato, usa-se a seguinte notação: β1, β2, ..., βn ⊨ α Os dois teoremas seguintes permitem demonstrar quando uma fórmula α é consequência lógica de uma outra fórmula: Teorema 1.7.1 Dadas as fórmulas β_1, β_2, ... , β_n e uma fórmula α, α é consequência lógica de β_1, β_2, ... , β_n se e somente se a fórmula β_1 ∧ β_2 ∧ ... ∧ β_n → α é uma tautologia. Prova: Condição Necessária: Sejam as fórmulas β_1, β_2, ... , β_n e α, e seja α consequência lógica de β_1, β_2, ... , β_n. Sejam I uma interpretação qualquer. 1. Se β_1, β_2, ..., β_n forem verdade em I, então α também será verdade em I, pois é consequência lógica das β_i’s. Portanto, β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdade em I. 2. Se um dos β_i’s for falso em I, β_1∧β_2∧...∧β_n será também falso em I. Independente do valor de α, β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdadeiro em I. De 1) e 2) tem-se que β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdade em qualquer interpretação, ou seja, β_1 ∧ β_2 ∧ ... ∧ β_n → α é uma tautologia. Condição Suficiente: Do fato de β_1 ∧ β_2 ∧ ... ∧ β_n → α ser uma tautologia, tem-se que β_1 ∧ β_2 ∧ ... ∧ β_n → α é verdade em qualquer interpretação. Se β_1 ∧ β_2 ∧ ... ∧ β_n for verdade em I, α também será verdade em I, ou seja, α é consequência lógica de β_1, β_2, ..., β_n. Teorema 1.7.2 Dadas as fórmulas β_1, β_2, ... , β_n e uma fórmula α, α é consequência lógica de β_1, β_2, ... , β_n se e somente se a fórmula β_1 ∧ β_2 ∧ ... ∧ β_n ∧ ¬α é uma contradição Prova: Sabe-se pelo teorema anterior que: Das as fórmulas β_1, β_2, ... , β_n e α, α é consequência lógica de β_1, β_2, ... , β_n se e somente se β_1 ∧ β_2 ∧ ... ∧ β_n → α for válida. Equivalentemente, α é consequência lógica de β_1, β_2, ..., β_n se e somente se a negação de β_1 ∧ β_2 ∧ ... ∧ β_n → α for uma contradição. Mas ¬(β_1 ∧ β_2 ∧ ... ∧ β_n → α) ≡ ¬(¬(β_1 ∧ β_2 ∧ ... ∧ β_n) ∨ α) ≡ β_1 ∧ β_2 ∧ ... ∧ β_n ∧ ¬α ou seja, β_1 ∧ β_2 ∧ ... ∧ β_n ∧ ¬α é uma contradição. Estes metateoremas são muito importantes. Eles mostram que provar que uma fórmula é consequência lógica de um conjunto finito de fórmulas é equivalente a mostrar que uma fórmula relacionada a ela é uma tautologia ou uma contradição. 8