Cálculo proposicional - Propositional calculus

Regras de transformação
Cálculo proposicional
Regras de inferência
Introdução  / eliminação de implicações ( modus ponens ) Introdução  / eliminação bicondicional Introdução  / eliminação de conjunção Introdução  / eliminação de disjunção Silogismo disjuntivo  / hipotético Dilema construtivo  / destrutivo Absorção  / modus tollens  / modus ponendo tollens Introdução de negação
Regras de substituição
Associatividade Comutatividade Distributividade Negação dupla Leis De Morgan Transposição Implicação material Exportação Tautologia
Lógica de predicado
Regras de inferência
Generalização  / instanciação universal Generalização  / instanciação existencial

O cálculo proposicional é um ramo da lógica . É também chamado de lógica proposicional , lógica das declarações , o cálculo sentencial , lógica sentencial , ou às vezes a lógica de ordem zero . Lida com proposições (que podem ser verdadeiras ou falsas) e relações entre proposições, incluindo a construção de argumentos a partir delas. As proposições compostas são formadas conectando proposições por conectivos lógicos . As proposições que não contêm conectivos lógicos são chamadas de proposições atômicas.

Ao contrário da lógica de primeira ordem , a lógica proposicional não lida com objetos não lógicos, predicados sobre eles ou quantificadores . No entanto, todo o mecanismo da lógica proposicional está incluído na lógica de primeira ordem e nas lógicas de ordem superior. Nesse sentido, a lógica proposicional é a base da lógica de primeira ordem e da lógica de ordem superior.

Explicação

Os conectivos lógicos são encontrados nas linguagens naturais. Em inglês, por exemplo, alguns exemplos são "e" ( conjunção ), "ou" ( disjunção ), "não" ( negação ) e "se" (mas apenas quando usado para denotar condicional material ).

A seguir está um exemplo de uma inferência muito simples dentro do escopo da lógica proposicional:

Premissa 1: Se está chovendo, está nublado.

Premissa 2: está chovendo.

Conclusão: está nublado.

Ambas as premissas e a conclusão são proposições. As premissas são tidas como certas e, com a aplicação do modus ponens (uma regra de inferência ), a conclusão segue.

Como a lógica proposicional não está preocupada com a estrutura das proposições além do ponto onde elas não podem mais ser decompostas por conectivos lógicos, esta inferência pode ser reafirmada substituindo essas declarações atômicas por letras de declarações, que são interpretadas como variáveis ​​que representam declarações:

Premissa 1: ${\ displaystyle P \ a Q}$

Premissa 2: ${\ displaystyle P}$

Conclusão: ${\ displaystyle Q}$

O mesmo pode ser afirmado sucintamente da seguinte maneira:

${\ displaystyle P \ to Q, P \ vdash Q}$

Quando P é interpretado como "Está chovendo" e Q como "está nublado", as expressões simbólicas acima podem ser vistas como correspondendo exatamente à expressão original na linguagem natural. Não só isso, mas também corresponderão a qualquer outra inferência desta forma , que será válida na mesma base desta inferência.

A lógica proposicional pode ser estudada por meio de um sistema formal no qual as fórmulas de uma linguagem formal podem ser interpretadas para representar proposições . Um sistema de axiomas e regras de inferência permite que certas fórmulas sejam derivadas. Essas fórmulas derivadas são chamadas de teoremas e podem ser interpretadas como proposições verdadeiras. Uma sequência construída de tais fórmulas é conhecida como derivação ou prova e a última fórmula da sequência é o teorema. A derivação pode ser interpretada como prova da proposição representada pelo teorema.

Quando um sistema formal é usado para representar a lógica formal, apenas as letras das instruções (geralmente letras romanas maiúsculas, como , e ) são representadas diretamente. As proposições de linguagem natural que surgem quando são interpretadas estão fora do escopo do sistema, e a relação entre o sistema formal e sua interpretação também está fora do próprio sistema formal. ${\ displaystyle P}$${\ displaystyle Q}$${\ displaystyle R}$

Na lógica proposicional funcional de verdade clássica , as fórmulas são interpretadas como tendo precisamente um de dois valores de verdade possíveis , o valor de verdade de verdadeiro ou o valor de verdade de falso . O princípio da bivalência e a lei do terceiro excluído são mantidos. A lógica proposicional funcional de verdade definida como tal e os sistemas isomórficos a ela são considerados lógica de ordem zero . No entanto, lógicas proposicionais alternativas também são possíveis. Para obter mais informações, consulte Outros cálculos lógicos abaixo.

História

Embora a lógica proposicional (que é intercambiável com cálculo proposicional) tinha sido sugerido por filósofos anteriores, foi desenvolvido em uma lógica formal ( lógica estóica ) por Crisipo no século 3 aC e ampliado por seu sucessor estóicos . A lógica estava focada em proposições . Esse avanço foi diferente da lógica silogística tradicional , que era focada em termos . No entanto, a maioria dos escritos originais foi perdida e a lógica proposicional desenvolvida pelos estóicos não foi mais entendida mais tarde na Antiguidade. Consequentemente, o sistema foi essencialmente reinventado por Pedro Abelardo no século 12.

A lógica proposicional foi finalmente refinada usando a lógica simbólica . O matemático dos séculos XVII / XVIII Gottfried Leibniz foi considerado o fundador da lógica simbólica por seu trabalho com o raciocinador de cálculo . Embora seu trabalho fosse o primeiro de seu tipo, era desconhecido para a comunidade lógica mais ampla. Conseqüentemente, muitos dos avanços alcançados por Leibniz foram recriados por lógicos como George Boole e Augustus De Morgan - completamente independentes de Leibniz.

Assim como a lógica proposicional pode ser considerada um avanço da lógica silogística anterior, a lógica de predicados de Gottlob Frege também pode ser considerada um avanço da lógica proposicional anterior. Um autor descreve a lógica de predicados como uma combinação "das características distintas da lógica silogística e da lógica proposicional". Conseqüentemente, a lógica dos predicados deu início a uma nova era na história da lógica; entretanto, avanços na lógica proposicional ainda foram feitos após Frege, incluindo dedução natural , árvores de verdade e tabelas de verdade . A dedução natural foi inventada por Gerhard Gentzen e Jan Łukasiewicz . As árvores da verdade foram inventadas por Evert Willem Beth . A invenção de tabelas de verdade, entretanto, é de atribuição incerta.

Dentro das obras de Frege e Bertrand Russell , existem ideias que influenciaram a invenção de tabelas de verdade. A estrutura tabular real (sendo formatada como uma tabela), em si, geralmente é creditada a Ludwig Wittgenstein ou Emil Post (ou ambos, independentemente). Além de Frege e Russell, outros que foram creditados por terem idéias precedendo as tabelas de verdade incluem Philo, Boole, Charles Sanders Peirce e Ernst Schröder . Outros creditados com a estrutura tabular incluem Jan Łukasiewicz , Alfred North Whitehead , William Stanley Jevons , John Venn e Clarence Irving Lewis . No final das contas, alguns concluíram, como John Shosky, que "está longe de ser claro que qualquer pessoa deveria receber o título de 'inventor' das tabelas de verdade."

Terminologia

Em termos gerais, um cálculo é um sistema formal que consiste em um conjunto de expressões sintáticas ( fórmulas bem formadas ), um subconjunto distinto dessas expressões (axiomas), mais um conjunto de regras formais que definem uma relação binária específica , destinada a ser interpretada como equivalência lógica , no espaço das expressões.

Quando o sistema formal se destina a ser um sistema lógico , as expressões devem ser interpretadas como declarações, e as regras, conhecidas como regras de inferência , normalmente têm a intenção de preservar a verdade. Nesse cenário, as regras, que podem incluir axiomas , podem ser usadas para derivar ("inferir") fórmulas que representam afirmações verdadeiras - de fórmulas fornecidas que representam afirmações verdadeiras.

O conjunto de axiomas pode ser vazio, um conjunto finito não vazio ou um conjunto infinito contável (ver esquema de axioma ). Uma gramática formal define recursivamente as expressões e fórmulas bem formadas da linguagem . Além disso, pode ser fornecida uma semântica que defina a verdade e as avaliações (ou interpretações ).

A linguagem de um cálculo proposicional consiste em

1. um conjunto de símbolos primitivos, variadamente referidos como fórmulas atômicas , marcadores de posição , letras de proposições ou variáveis , e
2. um conjunto de símbolos de operador, interpretados de várias maneiras como operadores lógicos ou conectivos lógicos .

Uma fórmula bem formada é qualquer fórmula atômica, ou qualquer fórmula que pode ser construída a partir de fórmulas atômicas por meio de símbolos de operador de acordo com as regras da gramática.

Os matemáticos às vezes distinguem entre constantes proposicionais, variáveis ​​proposicionais e esquemas. As constantes proposicionais representam alguma proposição particular, enquanto as variáveis ​​proposicionais variam no conjunto de todas as proposições atômicas. Os esquemas, no entanto, abrangem todas as proposições. É comum representar constantes proposicionais por A , B e C , variáveis ​​proposicionais por P , Q e R , e as letras esquemáticas geralmente são letras gregas, na maioria das vezes φ , ψ e χ .

Conceitos Básicos

O seguinte descreve um cálculo proposicional padrão. Existem muitas formulações diferentes que são mais ou menos equivalentes, mas diferem nos detalhes de:

1. sua linguagem (ou seja, a coleção particular de símbolos primitivos e símbolos de operador),
2. o conjunto de axiomas, ou fórmulas distintas, e
3. o conjunto de regras de inferência.

Qualquer proposição dada pode ser representada com uma letra chamada 'constante proposicional', análoga a representar um número por uma letra em matemática (por exemplo, a = 5 ). Todas as proposições requerem exatamente um de dois valores de verdade: verdadeiro ou falso. Por exemplo, seja P a proposição de que está chovendo lá fora. Isso será verdadeiro ( P ) se estiver chovendo lá fora, e falso caso contrário ( ¬ P ).

• Em seguida, definimos os operadores funcionais de verdade , começando com a negação. ¬ P representa a negação de P , o qual pode ser pensada como a negação de P . No exemplo acima, ¬ P expressa que não está chovendo lá fora, ou por uma leitura mais padrão: "Não é o caso que está chovendo lá fora." Quando P é verdadeiro, ¬ P é falso; e quando P é falso, ¬ P é verdadeiro. Como resultado, ¬¬ P sempre tem o mesmo valor de verdade como P .
• Conjugado é um conjuntivo verdade-funcional que forma uma proposição de duas propostas mais simples, por exemplo, P e Q . A conjunção de P e Q é escrita P ∧ Q , e expressa que cada uma é verdadeira. Lemos P ∧ Q como " P e Q ". Para quaisquer duas proposições, existem quatro atribuições possíveis de valores de verdade:
  1. P é verdadeiro e Q é verdadeiro
  2. P é verdadeiro e Q é falso
  3. P é falso e Q é verdadeiro
  4. P é falso e Q é falso

A conjunção de P e Q é verdadeira no caso 1 e, caso contrário, é falsa. Onde P é a proposição de que está chovendo lá fora e Q é a proposição de que uma frente fria está sobre o Kansas, P ∧ Q é verdadeiro quando está chovendo lá fora e há uma frente fria sobre o Kansas. Se não estiver chovendo lá fora, então P ∧ Q é falso; e se não houver frente fria sobre o Kansas, então P ∧ Q também é falso.

• A disjunção se assemelha à conjunção no sentido de que forma uma proposição a partir de duas proposições mais simples. Nós o escrevemos P ∨ Q , e ele é lido como " P ou Q ". Ele expressa que P ou Q são verdadeiros. Assim, nos casos listados acima, a disjunção de P com Q é verdadeira em todos os casos - exceto no caso 4. Usando o exemplo acima, a disjunção expressa que está chovendo lá fora ou há uma frente fria sobre o Kansas. (Note que este uso de disjunção supostamente se assemelha ao uso da palavra inglesa "ou". No entanto, é mais parecido com o inglês inclusivo "ou", que pode ser usado para expressar a verdade de pelo menos uma de duas proposições. Não é como o exclusivo "ou" do inglês, que expressa a verdade de exatamente uma das duas proposições. Em outras palavras, o exclusivo "ou" é falso quando P e Q são verdadeiros (caso 1). Um exemplo do exclusivo ou é: Você pode ter um bagel ou um doce, mas não os dois. Freqüentemente, em linguagem natural, dado o contexto apropriado, o adendo "mas não ambos" é omitido - mas implícito. Em matemática, no entanto, "ou" é sempre inclusivo ou; se for exclusivo ou pretendido, será especificado, possivelmente por "xor".)
• Condicional material também junta duas proposições mais simples, e escrevemos P → Q , que é lido "se P então Q ". A proposição à esquerda da seta é chamada de antecedente e a proposição à direita é chamada de conseqüente. (Não existe tal designação para conjunção ou disjunção, uma vez que são operações comutativas.) Expressa que Q é verdadeiro sempre que P é verdadeiro. Assim, P → Q é verdadeiro em todos os casos acima, exceto no caso 2, porque este é o único caso em que P é verdadeiro, mas Q não. Usando o exemplo, se P, então Q expressa que se está chovendo lá fora, então há uma frente fria sobre o Kansas. O condicional material é freqüentemente confundido com causalidade física. O condicional material, entretanto, relaciona apenas duas proposições por seus valores de verdade - o que não é a relação de causa e efeito. É controverso na literatura se a implicação material representa uma causalidade lógica.
• Bicondicional junta duas proposições mais simples, e escrevemos P ↔ Q , que é lido " P se e somente se Q ". Ele expressa que P e Q têm o mesmo valor de verdade, e nos casos 1 e 4. ' P é verdadeiro se e somente se Q ' é verdadeiro, e é falso caso contrário.

É muito útil olhar as tabelas de verdade para esses diferentes operadores, bem como o método dos quadros analíticos .

Fechamento em operações

A lógica proposicional é fechada sob conectivos funcionais de verdade. Ou seja, para qualquer proposição φ , ¬ φ também é uma proposição. Da mesma forma, para quaisquer proposições φ e ψ , φ ∧ ψ é uma proposição, e da mesma forma para disjunção, condicional e bicondicional. Isso implica que, por exemplo, φ ∧ ψ é uma proposição e, portanto, pode ser conjunta com outra proposição. Para representar isso, precisamos usar parênteses para indicar qual proposição está conjunta com qual. Por exemplo, P ∧ Q ∧ R não é uma fórmula bem formado, porque não se sabe que são conjunção P ∧ Q com R ou se são conjunção P com Q ∧ R . Portanto, devemos escrever ( P ∧ Q ) ∧ R para representar o primeiro, ou P ∧ ( Q ∧ R ) para representar o último. Ao avaliar as condições de verdade, vemos que ambas as expressões têm as mesmas condições de verdade (serão verdadeiras nos mesmos casos) e, além disso, que qualquer proposição formada por conjunções arbitrárias terá as mesmas condições de verdade, independentemente da localização dos parênteses. Isso significa que a conjunção é associativa; no entanto, não se deve presumir que os parênteses nunca tenham um propósito. Por exemplo, a sentença P ∧ ( Q ∨ R ) não tem as mesmas condições de verdade de ( P ∧ Q ) ∨ R , então são sentenças diferentes distinguidas apenas pelos parênteses. Pode-se verificar isso pelo método da tabela de verdade mencionado acima.

Nota: Para qualquer número arbitrário de constantes proposicionais, podemos formar um número finito de casos que listam seus possíveis valores de verdade. Uma maneira simples de gerar isso é por meio de tabelas de verdade, nas quais se escreve P , Q , ..., Z , para qualquer lista de k constantes proposicionais - isto é, qualquer lista de constantes proposicionais com k entradas. Abaixo desta lista, escreve-se 2 ^k linhas, e abaixo de P preenche-se a primeira metade das linhas com verdadeiro (ou T) e a segunda metade com falso (ou F). Abaixo de Q, preenche-se um quarto das linhas com T, depois um quarto com F, então um quarto com T e o último quarto com F. A próxima coluna alterna entre verdadeiro e falso para cada oitavo das linhas, então semicolcheias e assim por diante, até que a última constante proposicional varie entre T e F para cada linha. Isso fornecerá uma lista completa de casos ou atribuições de valor de verdade possíveis para essas constantes proposicionais.

Argumento

O cálculo proposicional então define um argumento como uma lista de proposições. Um argumento válido é uma lista de proposições, a última das quais segue - ou está implícita - das demais. Todos os outros argumentos são inválidos. O argumento válido mais simples é o modus ponens , uma instância do qual é a seguinte lista de proposições:

${\ displaystyle {\ begin {array} {rl} 1. & P \ to Q \\ 2. & P \\\ hline \ portanto & Q \ end {array}}}$

Esta é uma lista de três proposições, cada linha é uma proposição e a última segue das demais. As primeiras duas linhas são chamadas de premissas e a última linha de conclusão. Dizemos que qualquer proposição C decorre de qualquer conjunto de proposições , se C deve ser verdadeiro sempre que todos os membros do conjunto forem verdadeiros. No argumento acima, para qualquer P e Q , sempre que P → Q e P forem verdadeiros, necessariamente Q é verdade. Observe que, quando P é verdadeiro, não podemos considerar os casos 3 e 4 (da tabela verdade). Quando P → Q é verdadeiro, não podemos considerar o caso 2. Isso deixa apenas o caso 1, no qual Q também é verdadeiro. Assim, Q está implícito nas premissas. ${\ displaystyle (P_ {1}, ..., P_ {n})}$${\ displaystyle (P_ {1}, ..., P_ {n})}$

Isso generaliza esquematicamente. Assim, onde φ e ψ podem ser quaisquer proposições,

${\ displaystyle {\ begin {array} {rl} 1. & \ varphi \ to \ psi \\ 2. & \ varphi \\\ hline \ portanto & \ psi \ end {array}}}$

Outras formas de argumento são convenientes, mas não necessárias. Dado um conjunto completo de axiomas (veja abaixo um desses conjuntos), o modus ponens é suficiente para provar todas as outras formas de argumento na lógica proposicional, portanto, eles podem ser considerados uma derivada. Observe que isso não é verdade para a extensão da lógica proposicional a outras lógicas, como a lógica de primeira ordem . A lógica de primeira ordem requer pelo menos uma regra adicional de inferência para obter integridade .

A importância do argumento na lógica formal é que se pode obter novas verdades de verdades estabelecidas. No primeiro exemplo acima, dadas as duas premissas, a verdade de Q ainda não é conhecida ou declarada. Depois que o argumento é apresentado, Q é deduzido. Dessa forma, definimos um sistema de dedução como um conjunto de todas as proposições que podem ser deduzidas de outro conjunto de proposições. Por exemplo, dado o conjunto de proposições , podemos definir um sistema de dedução, Γ , que é o conjunto de todas as proposições que se seguem a partir A . A reiteração é sempre assumida, então . Além disso, do primeiro elemento de A , último elemento, bem como do modus ponens, R é uma consequência e assim . Como não incluímos axiomas suficientemente completos, nada mais pode ser deduzido. Assim, embora a maioria dos sistemas de dedução estudados na lógica proposicional sejam capazes de deduzir , este é muito fraco para provar tal proposição. ${\ displaystyle A = \ {P \ lor Q, \ neg Q \ land R, (P \ lor Q) \ to R \}}$${\ displaystyle P \ lor Q, \ neg Q \ land R, (P \ lor Q) \ to R \ in \ Gamma}$${\ displaystyle R \ in \ Gamma}$${\ displaystyle (P \ lor Q) \ leftrightarrow (\ neg P \ to Q)}$

Descrição genérica de um cálculo proposicional

Um cálculo proposicional é um sistema formal , onde: ${\ displaystyle {\ mathcal {L}} = {\ mathcal {L}} \ left (\ mathrm {A}, \ \ Omega, \ \ mathrm {Z}, \ \ mathrm {I} \ right)}$

A linguagem de , também conhecida como seu conjunto de fórmulas , fórmulas bem formadas , é indutivamente definida pelas seguintes regras: ${\ displaystyle {\ mathcal {L}}}$

1. Base: qualquer elemento do conjunto alfa é uma fórmula de .${\ displaystyle \ mathrm {A}}$${\ displaystyle {\ mathcal {L}}}$
2. Se for fórmulas e estiver dentro , será uma fórmula.${\ displaystyle p_ {1}, p_ {2}, \ ldots, p_ {j}}$${\ displaystyle f}$${\ displaystyle \ Omega _ {j}}$${\ displaystyle \ left (f (p_ {1}, p_ {2}, \ ldots, p_ {j}) \ right)}$
3. Fechado: nada mais é uma fórmula de .${\ displaystyle {\ mathcal {L}}}$

A aplicação repetida dessas regras permite a construção de fórmulas complexas. Por exemplo:

• Pela regra 1, p é uma fórmula.
• Pela regra 2, é uma fórmula.${\ displaystyle \ neg p}$
• Pela regra 1, q é uma fórmula.
• Pela regra 2, é uma fórmula.${\ displaystyle (\ neg p \ lor q)}$

Exemplo 1. Sistema de axioma simples

Vamos , onde , , , são definidos da seguinte forma: ${\ displaystyle {\ mathcal {L}} _ {1} = {\ mathcal {L}} (\ mathrm {A}, \ Omega, \ mathrm {Z}, \ mathrm {I})}$${\ displaystyle \ mathrm {A}}$${\ displaystyle \ Omega}$${\ displaystyle \ mathrm {Z}}$${\ displaystyle \ mathrm {I}}$

• O conjunto alfa é um conjunto infinito de símbolos, por exemplo: ${\ displaystyle \ mathrm {A}}$

  ${\ displaystyle \ mathrm {A} = \ {p, q, r, s, t, u, p_ {2}, \ ldots \}.}$

• Dos três conectivos para conjunção, disjunção e implicação ( , e → ), um pode ser considerado primitivo e os outros dois podem ser definidos em termos dele e negação ( ¬ ). Todos os conectivos lógicos podem ser definidos em termos de um único operador suficiente . O bicondicional ( ↔ ) pode, é claro, ser definido em termos de conjunção e implicação, com definido como .${\ displaystyle \ wedge, \ lor}$${\ displaystyle a \ leftrightarrow b}$${\ displaystyle (a \ a b) \ land (b \ a a)}$
  Adotar a negação e a implicação como as duas operações primitivas de um cálculo proposicional é equivalente a ter a partição do conjunto ômega da seguinte forma: ${\ displaystyle \ Omega = \ Omega _ {1} \ cup \ Omega _ {2}}$

  ${\ displaystyle \ Omega _ {1} = \ {\ lnot \},}$

  ${\ displaystyle \ Omega _ {2} = \ {\ to \}.}$

• Um sistema de axioma proposto por Jan Łukasiewicz , e usado como a parte do cálculo proposicional de um sistema de Hilbert , formula um cálculo proposicional nesta linguagem como segue. Os axiomas são todos instâncias de substituição de:
  • ${\ displaystyle (p \ to (q \ to p))}$
  • ${\ displaystyle ((p \ to (q \ to r)) \ to ((p \ to q) \ to (p \ to r)))}$
  • ${\ displaystyle ((\ neg p \ para \ neg q) \ para (q \ para p))}$
• A regra de inferência é ponente modus (ou seja, a partir de p e , inferir q ). Então é definido como e é definido como . Este sistema é usado no banco de dados de prova formal Metamath set.mm.${\ displaystyle (p \ to q)}$${\ displaystyle a \ lor b}$${\ displaystyle \ neg a \ to b}$${\ displaystyle a \ land b}$${\ displaystyle \ neg (a \ to \ neg b)}$

Exemplo 2. Sistema de dedução natural

Vamos , onde , , , são definidos da seguinte forma: ${\ displaystyle {\ mathcal {L}} _ {2} = {\ mathcal {L}} (\ mathrm {A}, \ Omega, \ mathrm {Z}, \ mathrm {I})}$${\ displaystyle \ mathrm {A}}$${\ displaystyle \ Omega}$${\ displaystyle \ mathrm {Z}}$${\ displaystyle \ mathrm {I}}$

• O conjunto alfa é um conjunto infinito de símbolos, por exemplo: ${\ displaystyle \ mathrm {A}}$

  ${\ displaystyle \ mathrm {A} = \ {p, q, r, s, t, u, p_ {2}, \ ldots \}.}$

• O ômega define as partições da seguinte forma: ${\ displaystyle \ Omega = \ Omega _ {1} \ cup \ Omega _ {2}}$

  ${\ displaystyle \ Omega _ {1} = \ {\ lnot \},}$

  ${\ displaystyle \ Omega _ {2} = \ {\ land, \ lor, \ to, \ leftrightarrow \}.}$

No exemplo a seguir de um cálculo proposicional, as regras de transformação devem ser interpretadas como as regras de inferência de um assim chamado sistema de dedução natural . O sistema particular apresentado aqui não tem pontos iniciais, o que significa que sua interpretação para aplicações lógicas deriva seus teoremas de um conjunto vazio de axiomas.

• O conjunto de pontos iniciais está vazio, ou seja ,.${\ displaystyle \ mathrm {I} = \ varnothing}$
• O conjunto de regras de transformação,, é descrito a seguir:${\ displaystyle \ mathrm {Z}}$

Nosso cálculo proposicional tem onze regras de inferência. Essas regras nos permitem derivar outras fórmulas verdadeiras, dado um conjunto de fórmulas que são consideradas verdadeiras. Os dez primeiros afirmam simplesmente que podemos inferir certas fórmulas bem formadas de outras fórmulas bem formadas. A última regra, entretanto, usa raciocínio hipotético no sentido de que na premissa da regra assumimos temporariamente uma hipótese (não comprovada) como parte do conjunto de fórmulas inferidas para ver se podemos inferir uma certa outra fórmula. Como as primeiras dez regras não fazem isso, geralmente são descritas como regras não hipotéticas e a última como uma regra hipotética .

Ao descrever as regras de transformação, podemos introduzir um símbolo de metalinguagem . É basicamente uma abreviatura conveniente para dizer "inferir que". O formato é , em que Γ é um conjunto (possivelmente vazio) de fórmulas chamadas premissas e ψ é uma fórmula chamada conclusão. A regra de transformação significa que se toda proposição em Γ é um teorema (ou tem o mesmo valor de verdade que os axiomas), então ψ também é um teorema. Observe que, considerando a introdução da seguinte regra de conjunção , saberemos que sempre que Γ tiver mais de uma fórmula, podemos sempre reduzi-la com segurança em uma fórmula usando a conjunção. Resumindo, daquele momento em diante, podemos representar Γ como uma fórmula em vez de um conjunto. Outra omissão por conveniência é quando Γ é um conjunto vazio e, nesse caso, Γ pode não aparecer. ${\ displaystyle \ vdash}$${\ displaystyle \ Gamma \ vdash \ psi}$${\ displaystyle \ Gamma \ vdash \ psi}$

Introdução de negação

De e , inferir .${\ displaystyle (p \ to q)}$${\ displaystyle (p \ to \ neg q)}$${\ displaystyle \ neg p}$

Ou seja ,.${\ displaystyle \ {(p \ to q), (p \ to \ neg q) \} \ vdash \ neg p}$

Eliminação de negação

De , inferir .${\ displaystyle \ neg p}$${\ displaystyle (p \ a r)}$

Ou seja ,.${\ displaystyle \ {\ neg p \} \ vdash (p \ a r)}$

Eliminação de dupla negação

De , inferir p .${\ displaystyle \ neg \ neg p}$

Ou seja ,.${\ displaystyle \ neg \ neg p \ vdash p}$

Introdução de conjunção

De p e q , inferir .${\ displaystyle (p \ land q)}$

Ou seja ,.${\ displaystyle \ {p, q \} \ vdash (p \ land q)}$

Eliminação de conjunção

De , inferir p .${\ displaystyle (p \ land q)}$

De , inferir q .${\ displaystyle (p \ land q)}$

Isso é, e .${\ displaystyle (p \ land q) \ vdash p}$${\ displaystyle (p \ land q) \ vdash q}$

Introdução de disjunção

De p , inferir .${\ displaystyle (p \ lor q)}$

De q , inferir .${\ displaystyle (p \ lor q)}$

Isso é, e .${\ displaystyle p \ vdash (p \ lor q)}$${\ displaystyle q \ vdash (p \ lor q)}$

Eliminação de disjunção

De e e , inferir r .${\ displaystyle (p \ lor q)}$${\ displaystyle (p \ a r)}$${\ displaystyle (q \ para r)}$

Ou seja ,.${\ displaystyle \ {p \ lor q, p \ to r, q \ to r \} \ vdash r}$

Introdução bicondicional

De e , inferir .${\ displaystyle (p \ to q)}$${\ displaystyle (q \ a p)}$${\ displaystyle (p \ leftrightarrow q)}$

Ou seja ,.${\ displaystyle \ {p \ to q, q \ to p \} \ vdash (p \ leftrightarrow q)}$

Eliminação bicondicional

De , inferir .${\ displaystyle (p \ leftrightarrow q)}$${\ displaystyle (p \ to q)}$

De , inferir .${\ displaystyle (p \ leftrightarrow q)}$${\ displaystyle (q \ a p)}$

Isso é, e .${\ displaystyle (p \ leftrightarrow q) \ vdash (p \ to q)}$${\ displaystyle (p \ leftrightarrow q) \ vdash (q \ a p)}$

Modus ponens (eliminação condicional)

De p e , inferir q .${\ displaystyle (p \ to q)}$

Ou seja ,.${\ displaystyle \ {p, p \ to q \} \ vdash q}$

Prova condicional (introdução condicional)

De [aceitar p permite uma prova de q ], inferir .${\ displaystyle (p \ to q)}$

Ou seja ,.${\ displaystyle (p \ vdash q) \ vdash (p \ to q)}$

Formulários de argumento básicos e derivados

Nome	Sequent	Descrição
Modus ponens	${\ displaystyle ((p \ to q) \ land p) \ vdash q}$	Se p, então q ; p ; portanto q
Modus Tollens	${\ displaystyle ((p \ to q) \ land \ neg q) \ vdash \ neg p}$	Se p, então q ; não q ; portanto não p
Silogismo hipotético	${\ displaystyle ((p \ to q) \ land (q \ to r)) \ vdash (p \ to r)}$	Se p, então q ; se q então r ; portanto, se p, então r
Silogismo Disjuntivo	${\ displaystyle ((p \ lor q) \ land \ neg p) \ vdash q}$	Ou p ou q , ou ambos; não p ; portanto, q
Dilema Construtivo	${\ displaystyle ((p \ to q) \ land (r \ to s) \ land (p \ lor r)) \ vdash (q \ lor s)}$	Se p, então q ; e se r, então s ; mas p ou r ; portanto q ou s
Dilema Destrutivo	${\ displaystyle ((p \ to q) \ land (r \ to s) \ land (\ neg q \ lor \ neg s)) \ vdash (\ neg p \ lor \ neg r)}$	Se p, então q ; e se r, então s ; mas não q ou não s ; portanto, não p ou não r
Dilema Bidirecional	${\ displaystyle ((p \ to q) \ land (r \ to s) \ land (p \ lor \ neg s)) \ vdash (q \ lor \ neg r)}$	Se p, então q ; e se r, então s ; mas p ou não s ; portanto q ou não r
Simplificação	${\ displaystyle (p \ land q) \ vdash p}$	p e q são verdadeiros; portanto p é verdadeiro
Conjunção	${\ displaystyle p, q \ vdash (p \ land q)}$	p e q são verdadeiros separadamente; portanto, eles são verdadeiros conjuntamente
Adição	${\ displaystyle p \ vdash (p \ lor q)}$	p é verdadeiro; portanto, a disjunção ( p ou q ) é verdadeira
Composição	${\ displaystyle ((p \ to q) \ land (p \ to r)) \ vdash (p \ to (q \ land r))}$	Se p, então q ; e se p então r ; portanto, se p é verdadeiro, então q e r são verdadeiros
Teorema de De Morgan (1)	${\ displaystyle \ neg (p \ land q) \ vdash (\ neg p \ lor \ neg q)}$	A negação de ( p e q ) é equiv. para (não p ou não q )
Teorema de De Morgan (2)	${\ displaystyle \ neg (p \ lor q) \ vdash (\ neg p \ land \ neg q)}$	A negação de ( p ou q ) é equiv. para (não p e não q )
Comutação (1)	${\ displaystyle (p \ lor q) \ vdash (q \ lor p)}$	( p ou q ) é equiv. para ( q ou p )
Comutação (2)	${\ displaystyle (p \ land q) \ vdash (q \ land p)}$	( p e q ) é equiv. para ( q e p )
Comutação (3)	${\ displaystyle (p \ leftrightarrow q) \ vdash (q \ leftrightarrow p)}$	( p é equivalente a q ) é equiv. a ( q é equivalente a p )
Associação (1)	${\ displaystyle (p \ lor (q \ lor r)) \ vdash ((p \ lor q) \ lor r)}$	p ou ( q ou r ) é equiv. para ( p ou q ) ou r
Associação (2)	${\ displaystyle (p \ land (q \ land r)) \ vdash ((p \ land q) \ land r)}$	p e ( q e r ) são equiv. para ( p e q ) e r
Distribuição (1)	${\ displaystyle (p \ land (q \ lor r)) \ vdash ((p \ land q) \ lor (p \ land r))}$	p e ( q ou r ) é equiv. para ( p e q ) ou ( p e r )
Distribuição (2)	${\ displaystyle (p \ lor (q \ land r)) \ vdash ((p \ lor q) \ land (p \ lor r))}$	p ou ( q e r ) é equiv. para ( p ou q ) e ( p ou r )
Dupla Negação	${\ displaystyle p \ vdash \ neg \ neg p}$ e ${\ displaystyle \ neg \ neg p \ vdash p}$	p é equivalente à negação de não p
Transposição	${\ displaystyle (p \ to q) \ vdash (\ neg q \ to \ neg p)}$	Se p então q é equiv. para se não q então não p
Implicação Material	${\ displaystyle (p \ to q) \ vdash (\ neg p \ lor q)}$	Se p então q é equiv. para não p ou q
Equivalência de material (1)	${\ displaystyle (p \ leftrightarrow q) \ vdash ((p \ to q) \ land (q \ to p))}$	( p sif q ) é equiv. para (se p for verdadeiro, então q é verdadeiro) e (se q for verdadeiro, então p é verdadeiro)
Equivalência de material (2)	${\ displaystyle (p \ leftrightarrow q) \ vdash ((p \ land q) \ lor (\ neg p \ land \ neg q))}$	( p sif q ) é equiv. para qualquer um ( p e q são verdadeiros) ou ( p e q são falsos)
Equivalência de material (3)	${\ displaystyle (p \ leftrightarrow q) \ vdash ((p \ lor \ neg q) \ land (\ neg p \ lor q))}$	( p iff q ) é equivalente a., ambos ( p ou não q é verdadeiro) e (não p ou q é verdadeiro)
Exportação	${\ displaystyle ((p \ land q) \ to r) \ vdash (p \ to (q \ to r))}$	de (se p e q são verdadeiros, então r é verdadeiro), podemos provar (se q é verdadeiro, então r é verdadeiro, se p é verdadeiro)
Importação	${\ displaystyle (p \ to (q \ to r)) \ vdash ((p \ land q) \ to r)}$	Se p então (se q então r ) é equivalente a se p e q então r
Tautologia (1)	${\ displaystyle p \ vdash (p \ lor p)}$	p é verdadeiro é equiv. para p é verdadeiro ou p é verdadeiro
Tautologia (2)	${\ displaystyle p \ vdash (p \ land p)}$	p é verdadeiro é equiv. para p é verdadeiro e p é verdadeiro
Tertium non datur (Lei do Meio Excluído)	${\ displaystyle \ vdash (p \ lor \ neg p)}$	p ou não p é verdade
Lei de Não-Contradição	${\ displaystyle \ vdash \ neg (p \ land \ neg p)}$	p e não p é falso, é uma afirmação verdadeira

Provas em cálculo proposicional

Um dos principais usos de um cálculo proposicional, quando interpretado para aplicações lógicas, é determinar relações de equivalência lógica entre fórmulas proposicionais. Essas relações são determinadas por meio das regras de transformação disponíveis, cujas sequências são chamadas de derivações ou provas .

Na discussão a seguir, uma prova é apresentada como uma sequência de linhas numeradas, com cada linha consistindo em uma única fórmula seguida por um motivo ou justificativa para a introdução dessa fórmula. Cada premissa do argumento, ou seja, uma suposição introduzida como uma hipótese do argumento, é listada no início da sequência e é marcada como uma "premissa" no lugar de outra justificativa. A conclusão está listada na última linha. Uma prova está completa se cada linha segue das anteriores pela aplicação correta de uma regra de transformação. (Para uma abordagem contrastante, consulte as árvores de prova ).

Exemplo de uma prova no sistema de dedução natural

• Para ser mostrado que um → Uma .
• Uma possível prova disso (que, embora válida, contém mais etapas do que o necessário) pode ser organizada da seguinte forma:

Exemplo de prova

Número	Fórmula	Razão
1	${\ displaystyle A}$	premissa
2	${\ displaystyle A \ lor A}$	De ( 1 ) por introdução de disjunção
3	${\ displaystyle (A \ lor A) \ land A}$	De ( 1 ) e ( 2 ) por introdução de conjunção
4	${\ displaystyle A}$	De ( 3 ) por eliminação de conjunção
5	${\ displaystyle A \ vdash A}$	Resumo de ( 1 ) a ( 4 )
6	${\ displaystyle \ vdash A \ a A}$	De ( 5 ) por prova condicional

Interprete como "Assumindo A , inferir A ". Lido como "Não presumindo nada, inferir que A implica A ", ou "É uma tautologia que A implica A ", ou "É sempre verdade que A implica A ". ${\ displaystyle A \ vdash A}$${\ displaystyle \ vdash A \ a A}$

Exemplo de uma prova em um sistema de cálculo proposicional clássico

Agora provamos o mesmo teorema no sistema axiomático de Jan Łukasiewicz descrito acima, que é um exemplo de um sistema de cálculo proposicional clássico , ou um sistema dedutivo do estilo de Hilbert para cálculo proposicional. ${\ displaystyle A \ a A}$

Os axiomas são:

(A1) ${\ displaystyle (p \ to (q \ to p))}$

(A2) ${\ displaystyle ((p \ to (q \ to r)) \ to ((p \ to q) \ to (p \ to r)))}$

(A3) ${\ displaystyle ((\ neg p \ para \ neg q) \ para (q \ para p))}$

E a prova é a seguinte:

1. ${\ displaystyle A \ to ((B \ to A) \ to A)}$       (instância de (A1))
2. ${\ displaystyle (A \ to ((B \ to A) \ to A)) \ to ((A \ to (B \ to A)) \ to (A \ to A))}$       (instância de (A2))
3. ${\ displaystyle (A \ to (B \ to A)) \ to (A \ to A)}$       (de (1) e (2) por modus ponens )
4. ${\ displaystyle A \ to (B \ to A)}$       (instância de (A1))
5. ${\ displaystyle A \ a A}$       (de (4) e (3) por modus ponens)

Solidez e integridade das regras

As propriedades cruciais desse conjunto de regras são que elas são sólidas e completas . Informalmente, isso significa que as regras estão corretas e que nenhuma outra regra é necessária. Essas alegações podem ser tornadas mais formais da seguinte maneira. Observe que as provas para a integridade e integridade da lógica proposicional não são em si mesmas provas na lógica proposicional; esses são teoremas em ZFC usados ​​como uma metateoria para provar propriedades da lógica proposicional.

Definimos uma atribuição de verdade como uma função que mapeia variáveis ​​proposicionais para verdadeiro ou falso . Informalmente, tal atribuição de verdade pode ser entendida como a descrição de um possível estado de coisas (ou mundo possível ) onde certas afirmações são verdadeiras e outras não. A semântica das fórmulas pode então ser formalizada definindo para qual "estado de coisas" elas são consideradas verdadeiras, que é o que é feito pela seguinte definição.

Definimos quando tal atribuição de verdade A satisfaz uma certa fórmula bem formada com as seguintes regras:

• A satisfaz a variável proposicional P se e somente se A ( P ) = verdadeiro
• A satisfaz ¬ φ se e somente se A não satisfaz φ
• A satisfaz ( φ ∧ ψ ) se e somente se A satisfaz tanto φ quanto ψ
• A satisfaz ( φ ∨ ψ ) se e somente se A satisfaz pelo menos um de φ ou ψ
• A satisfaz ( φ → ψ ) se e somente se não for o caso de A satisfazer φ, mas não ψ
• A satisfaz ( φ ↔ ψ ) se e somente se A satisfaz tanto φ quanto ψ ou não satisfaz nenhum deles

Com esta definição, podemos agora formalizar o que significa para uma fórmula φ estar implícita em um certo conjunto S de fórmulas. Informalmente, isso é verdade se em todos os mundos possíveis, dado o conjunto de fórmulas S, a fórmula φ também for válida. Isso leva à seguinte definição formal: Dizemos que um conjunto S de fórmulas bem formadas implica semanticamente (ou implica ) uma certa fórmula bem formada φ se todas as atribuições de verdade que satisfazem todas as fórmulas em S também satisfazem φ .

Finalmente, definimos a vinculação sintática de modo que φ seja sintaticamente implicada por S se e somente se pudermos derivá-la com as regras de inferência que foram apresentadas acima em um número finito de etapas. Isso nos permite formular exatamente o que significa para o conjunto de regras de inferência ser sólido e completo:

Solidez: se o conjunto de fórmulas bem formadas S sintaticamente acarreta a fórmula bem formada φ, então S semanticamente acarreta φ .

Completude: Se o conjunto de fórmulas bem formadas S semanticamente acarreta a fórmula bem formada φ, então S sintaticamente acarreta φ .

Para o conjunto de regras acima, este é realmente o caso.

Esboço de uma prova de solidez

(Para a maioria dos sistemas lógicos , esta é a direção de prova comparativamente "simples")

Convenções notacionais: Seja G uma variável que abrange conjuntos de sentenças. Deixe A, B e C variarem sobre as frases. Para " G sintaticamente implica A ", escrevemos " G prova A ". Para " G implica semanticamente A " escrevemos " G implica A ".

Queremos mostrar: ( A ) ( G ) (se G prova A , então G implica A ).

Notamos que " G prova A " tem uma definição indutiva, e isso nos dá os recursos imediatos para demonstrar afirmações da forma "Se G prova A , então ...". Portanto, nossa prova procede por indução.

Observe que a Etapa II da Base pode ser omitida para sistemas de dedução natural porque eles não têm axiomas. Quando usado, o Passo II envolve mostrar que cada um dos axiomas é uma verdade lógica (semântica) .

Os passos Base de demonstrar que as frases mais simples demonstráveis de L também estão implicados por L , para qualquer L . (A prova é simples, uma vez que o fato semântico de que um conjunto implica qualquer um de seus membros, também é trivial.) A etapa indutiva cobrirá sistematicamente todas as sentenças adicionais que podem ser prováveis ​​- considerando cada caso em que podemos chegar a uma conclusão lógica usando uma regra de inferência - e mostra que se uma nova sentença é provável, também está logicamente implícita. (Por exemplo, podemos ter uma regra nos dizendo que de " A " podemos derivar " A ou B ". Em III.a presumimos que se A é provável, está implícito. Também sabemos que se A é provável, então " A ou B "é demonstrável. Temos de mostrar que então" A ou B "também está implícito. Fazemos isso apelando à definição semântica e à suposição que acabamos de fazer. A é demonstrável a partir de G , presumimos. Portanto, é também implícito por G. Portanto, qualquer valoração semântica que torne G verdadeiro torna A verdadeiro. Mas qualquer valoração que torne A verdadeiro torna " A ou B " verdadeiro, pela semântica definida para "ou". Portanto, qualquer valoração que torne G verdadeiro torna " A ou B " verdadeiro. Portanto, " A ou B " está implícito. Geralmente, a etapa indutiva consiste em uma análise longa, mas simples, caso a caso, de todas as regras de inferência, mostrando que cada uma "preserva" a semântica implicação.

Pela definição de provabilidade, não há sentenças prováveis ​​a não ser por ser um membro de G , um axioma, ou seguir por uma regra; então, se todas essas estão semanticamente implícitas, o cálculo de dedução é válido.

Esboço da prova de integridade

(Esta é geralmente a direção de prova muito mais difícil.)

Adotamos as mesmas convenções de notação acima.

Queremos mostrar: Se G implica A , então G comprova A . Procedemos por contraposição : Mostramos vez que, se G não não provar A então G não não implica A . Se nós mostramos que há um modelo em que A não é titular, apesar G sendo verdadeiro, então, obviamente, G não implica A . A idéia é construir tal modelo a sair da nossa própria suposição de que G não prova A .

Assim, todo sistema que tem o modus ponens como regra de inferência e prova os seguintes teoremas (incluindo suas substituições) está completo:

• p → (¬p → q)
• (p → q) → ((¬p → q) → q)
• p → (q → (p → q))
• p → (¬q → ¬ (p → q))
• ¬p → (p → q)
• p → p
• p → (q → p)
• (p → (q → r)) → ((p → q) → (p → r))

Os cinco primeiros são usados ​​para a satisfação das cinco condições no estágio III acima, e os três últimos para provar o teorema da dedução.

Exemplo

Como exemplo, pode ser mostrado que, como qualquer outra tautologia, os três axiomas do sistema de cálculo proposicional clássico descrito anteriormente podem ser provados em qualquer sistema que satisfaça o acima, ou seja, que tenha o modus ponens como uma regra de inferência e prova o acima oito teoremas (incluindo suas substituições). Dos oito teoremas, os dois últimos são dois dos três axiomas; o terceiro axioma,, também pode ser provado, como mostramos agora. ${\ displaystyle (\ neg q \ to \ neg p) \ to (p \ to q)}$

Para a prova, podemos usar o teorema do silogismo hipotético (na forma relevante para este sistema axiomático), uma vez que ele depende apenas dos dois axiomas que já estão no conjunto de oito teoremas acima. A prova, então, é a seguinte:

1. ${\ displaystyle q \ to (p \ to q)}$       (instância do 7º teorema)
2. ${\ displaystyle (q \ to (p \ to q)) \ to ((\ neg q \ to \ neg p) \ to (q \ to (p \ to q)))}$       (instância do 7º teorema)
3. ${\ displaystyle (\ neg q \ to \ neg p) \ to (q \ to (p \ to q))}$       (de (1) e (2) por modus ponens)
4. ${\ displaystyle (\ neg p \ to (p \ to q)) \ to ((\ neg q \ to \ neg p) \ to (\ neg q \ to (p \ to q)))}$       (instância do teorema do silogismo hipotético)
5. ${\ displaystyle (\ neg p \ to (p \ to q))}$       (instância do 5º teorema)
6. ${\ displaystyle (\ neg q \ to \ neg p) \ to (\ neg q \ to (p \ to q))}$       (de (5) e (4) por modus ponens)
7. ${\ displaystyle (q \ to (p \ to q)) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q))}$       (instância do segundo teorema)
8. ${\ displaystyle ((q \ to (p \ to q)) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q))) \ to ((\ neg q \ to \ neg p) \ to ((q \ to (p \ to q)) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q))))}$       (instância do 7º teorema)
9. ${\ displaystyle (\ neg q \ to \ neg p) \ to ((q \ to (p \ to q)) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q) )))}$       (de (7) e (8) por modus ponens)
10. ${\ displaystyle ((\ neg q \ to \ neg p) \ to ((q \ to (p \ to q)) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q)))) \ to}$

    ${\ displaystyle (((\ neg q \ to \ neg p) \ to (q \ to (p \ to q))) \ to ((\ neg q \ to \ neg p) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q))))}$       (instância do 8º teorema)

11. ${\ displaystyle ((\ neg q \ to \ neg p) \ to (q \ to (p \ to q))) \ to ((\ neg q \ to \ neg p) \ to ((\ neg q \ to (p \ a q)) \ a (p \ a q)))}$       (de (9) e (10) por modus ponens)
12. ${\ displaystyle (\ neg q \ to \ neg p) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q))}$       (de (3) e (11) por modus ponens)
13. ${\ displaystyle ((\ neg q \ to \ neg p) \ to ((\ neg q \ to (p \ to q)) \ to (p \ to q))) \ to (((\ neg q \ to \ neg p) \ to (\ neg q \ to (p \ to q))) \ to ((\ neg q \ to \ neg p) \ to (p \ to q)))}$       (instância do 8º teorema)
14. ${\ displaystyle ((\ neg q \ to \ neg p) \ to (\ neg q \ to (p \ to q))) \ to ((\ neg q \ to \ neg p) \ to (p \ to q) ))}$       (de (12) e (13) por modus ponens)
15. ${\ displaystyle (\ neg q \ to \ neg p) \ to (p \ to q)}$       (de (6) e (14) por modus ponens)

Verificando a integridade para o sistema de cálculo proposicional clássico

Verificamos agora que o sistema de cálculo proposicional clássico descrito anteriormente pode de fato provar os oito teoremas necessários mencionados acima. Usamos vários lemas comprovados aqui :

(DN1) - Negação dupla (uma direção)${\ displaystyle \ neg \ neg p \ to p}$

(DN2) - Negação dupla (outra direção)${\ displaystyle p \ to \ neg \ neg p}$

(HS1) - uma forma de silogismo hipotético${\ displaystyle (q \ to r) \ to ((p \ to q) \ to (p \ to r))}$

(HS2) - outra forma de silogismo hipotético${\ displaystyle (p \ to q) \ to ((q \ to r) \ to (p \ to r))}$

(TR1) - Transposição${\ displaystyle (p \ to q) \ to (\ neg q \ to \ neg p)}$

(TR2) - outra forma de transposição.${\ displaystyle (\ neg p \ to q) \ to (\ neg q \ to p)}$

(L1) ${\ displaystyle p \ to ((p \ to q) \ to q)}$

(L3) ${\ displaystyle (\ neg p \ a p) \ a p}$

Também usamos o método do metateorema do silogismo hipotético como uma abreviatura para várias etapas de prova.

• p → (¬p → q) - prova:
  1. ${\ displaystyle p \ to (\ neg q \ to p)}$       (instância de (A1))
  2. ${\ displaystyle (\ neg q \ a p) \ a (\ neg p \ a \ neg \ neg q)}$       (instância de (TR1))
  3. ${\ displaystyle p \ to (\ neg p \ to \ neg \ neg q)}$       (de (1) e (2) usando o metateorema de silogismo hipotético)
  4. ${\ displaystyle \ neg \ neg q \ to q}$       (instância de (DN1))
  5. ${\ displaystyle (\ neg \ neg q \ to q) \ to ((\ neg p \ to \ neg \ neg q) \ to (\ neg p \ to q))}$       (instância de (HS1))
  6. ${\ displaystyle (\ neg p \ to \ neg \ neg q) \ to (\ neg p \ to q)}$       (de (4) e (5) usando modus ponens)
  7. ${\ displaystyle p \ to (\ neg p \ to q)}$       (de (3) e (6) usando o metateorema de silogismo hipotético)
• (p → q) → ((¬p → q) → q) - prova:
  1. ${\ displaystyle (p \ to q) \ to ((\ neg q \ to p) \ to (\ neg q \ to q))}$       (instância de (HS1))
  2. ${\ displaystyle (\ neg q \ to q) \ to q}$       (instância de (L3))
  3. ${\ displaystyle ((\ neg q \ to q) \ to q) \ to (((\ neg q \ to p) \ to (\ neg q \ to q)) \ to ((\ neg q \ to p) \ para q))}$       (instância de (HS1))
  4. ${\ displaystyle ((\ neg q \ to p) \ to (\ neg q \ to q)) \ to ((\ neg q \ to p) \ to q)}$       (de (2) e (3) por modus ponens)
  5. ${\ displaystyle (p \ to q) \ to ((\ neg q \ to p) \ to q)}$       (de (1) e (4) usando o metateorema de silogismo hipotético)
  6. ${\ displaystyle (\ neg p \ to q) \ to (\ neg q \ to p)}$       (instância de (TR2))
  7. ${\ displaystyle ((\ neg p \ to q) \ to (\ neg q \ to p)) \ to (((\ neg q \ to p) \ to q) \ to ((\ neg p \ to q) \ para q))}$       (instância de (HS2))
  8. ${\ displaystyle ((\ neg q \ a p) \ a q) \ a ((\ neg p \ a q) \ a q)}$       (de (6) e (7) usando modus ponens)
  9. ${\ displaystyle (p \ to q) \ to ((\ neg p \ to q) \ to q)}$       (de (5) e (8) usando o metateorema de silogismo hipotético)
• p → (q → (p → q)) - prova:
  1. ${\ displaystyle q \ to (p \ to q)}$       (instância de (A1))
  2. ${\ displaystyle (q \ to (p \ to q)) \ to (p \ to (q \ to (p \ to q)))}$       (instância de (A1))
  3. ${\ displaystyle p \ to (q \ to (p \ to q))}$       (de (1) e (2) usando modus ponens)
• p → (¬q → ¬ (p → q)) - prova:
  1. ${\ displaystyle p \ to ((p \ to q) \ to q)}$       (instância de (L1))
  2. ${\ displaystyle ((p \ to q) \ to q) \ to (\ neg q \ to \ neg (p \ to q))}$       (instância de (TR1))
  3. ${\ displaystyle p \ to (\ neg q \ to \ neg (p \ to q))}$       (de (1) e (2) usando o metateorema de silogismo hipotético)
• ¬p → (p → q) - prova:
  1. ${\ displaystyle \ neg p \ to (\ neg q \ to \ neg p)}$       (instância de (A1))
  2. ${\ displaystyle (\ neg q \ to \ neg p) \ to (p \ to q)}$       (instância de (A3))
  3. ${\ displaystyle \ neg p \ to (p \ to q)}$       (de (1) e (2) usando o metateorema de silogismo hipotético)
• p → p - prova dada no exemplo de prova acima
• p → (q → p) - axioma (A1)
• (p → (q → r)) → ((p → q) → (p → r)) - axioma (A2)

Outro esboço para uma prova de integridade

Se uma fórmula é uma tautologia , então há uma tabela verdade para ela que mostra que cada avaliação produz o valor verdadeiro para a fórmula. Considere essa avaliação. Por indução matemática no comprimento das subfórmulas, mostre que a verdade ou falsidade da subfórmula segue da verdade ou falsidade (conforme apropriado para a avaliação) de cada variável proposicional na subfórmula. Em seguida, combine as linhas da tabela verdade duas de cada vez usando "( P é verdadeiro implica S ) implica (( P é falso implica S ) implica S )". Continue repetindo isso até que todas as dependências das variáveis ​​proposicionais tenham sido eliminadas. O resultado é que provamos a tautologia dada. Uma vez que toda tautologia é demonstrável, a lógica está completa.

Interpretação de um cálculo proposicional funcional de verdade

Uma interpretação de um cálculo proposicional verdade-funcional é uma atribuição para cada símbolo proposicional de de um ou o outro (mas não ambos) do valores de verdade verdade ( T ) e falsidade ( F ), e uma designação para os símbolos conjuntivos de de seus significados funcionais de verdade usuais. Uma interpretação de um cálculo proposicional funcional de verdade também pode ser expressa em termos de tabelas de verdade . ${\ displaystyle {\ mathcal {P}}}$${\ displaystyle {\ mathcal {P}}}$ ${\ displaystyle {\ mathcal {P}}}$

Para símbolos proposicionais distintos, existem diferentes interpretações possíveis. Para qualquer símbolo específico , por exemplo, existem interpretações possíveis: ${\ displaystyle n}$${\ displaystyle 2 ^ {n}}$${\ displaystyle a}$${\ displaystyle 2 ^ {1} = 2}$

1. ${\ displaystyle a}$é atribuído a T , ou
2. ${\ displaystyle a}$é atribuído F .

Para o par , existem interpretações possíveis: ${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle 2 ^ {2} = 4}$

1. ambos são atribuídos a T ,
2. ambos são atribuídos a F ,
3. ${\ displaystyle a}$é atribuído T e é atribuído F , ou${\ displaystyle b}$
4. ${\ displaystyle a}$é atribuído F e é atribuído T .${\ displaystyle b}$

Visto que tem , isto é, inumeráveis muitos símbolos proposicionais, existem , e portanto incontáveis ​​muitas interpretações possíveis de . ${\ displaystyle {\ mathcal {P}}}$${\ displaystyle \ aleph _ {0}}$${\ displaystyle 2 ^ {\ aleph _ {0}} = {\ mathfrak {c}}}$${\ displaystyle {\ mathcal {P}}}$

Interpretação de uma frase de lógica proposicional funcional de verdade

Se φ e ψ são fórmulas de e é uma interpretação de seguida, entende-se por: ${\ displaystyle {\ mathcal {P}}}$${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {P}}}$

• Uma sentença de lógica proposicional é verdadeira sob uma interpretação se atribuir o valor de verdade T a essa sentença. Se uma frase é verdadeira sob uma interpretação, essa interpretação é chamada de modelo dessa frase.${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {I}}}$
• φ é falso sob uma interpretação se φ não for verdadeiro sob .${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {I}}}$
• Uma sentença de lógica proposicional é logicamente válida se for verdadeira em todas as interpretações.

  ${\ displaystyle \ models}$ φ significa que φ é logicamente válido.

• Uma sentença ψ da lógica proposicional é uma consequência semântica de uma sentença φ se não houver nenhuma interpretação sob a qual φ é verdadeira e ψ é falsa.
• Uma sentença de lógica proposicional é consistente se for verdadeira sob pelo menos uma interpretação. É inconsistente se não for consistente.

Algumas consequências dessas definições:

• Para qualquer interpretação, uma determinada fórmula é verdadeira ou falsa.
• Nenhuma fórmula é verdadeira e falsa sob a mesma interpretação.
• φ é falso para uma dada interpretação sse for verdadeiro para essa interpretação; e φ é verdadeiro sob uma interpretação iff é falso sob essa interpretação.${\ displaystyle \ neg \ phi}$${\ displaystyle \ neg \ phi}$
• Se φ e são ambos verdadeiros sob uma dada interpretação, então ψ é verdadeiro sob aquela interpretação.${\ displaystyle (\ phi \ to \ psi)}$
• Se e , então .${\ displaystyle \ models _ {\ mathrm {P}} \ phi}$${\ displaystyle \ models _ {\ mathrm {P}} (\ phi \ to \ psi)}$${\ displaystyle \ models _ {\ mathrm {P}} \ psi}$
• ${\ displaystyle \ neg \ phi}$é verdadeiro em iff φ não é verdadeiro em .${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {I}}}$
• ${\ displaystyle (\ phi \ to \ psi)}$é verdadeiro em sse φ não é verdadeiro em ou ψ é verdadeiro em .${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {I}}}$${\ displaystyle {\ mathcal {I}}}$
• Uma sentença ψ de lógica proposicional é uma consequência semântica de uma sentença φ sse é logicamente válida , isto é, sse .${\ displaystyle (\ phi \ to \ psi)}$${\ displaystyle \ phi \ models _ {\ mathrm {P}} \ psi}$${\ displaystyle \ models _ {\ mathrm {P}} (\ phi \ to \ psi)}$

Cálculo alternativo

É possível definir outra versão do cálculo proposicional, que define a maior parte da sintaxe dos operadores lógicos por meio de axiomas e que usa apenas uma regra de inferência.

Axiomas

Sejam φ , χ e ψ representarem fórmulas bem formadas. (As próprias fórmulas bem formadas não conteriam nenhuma letra grega, mas apenas letras romanas maiúsculas, operadores conectivos e parênteses.) Então, os axiomas são os seguintes:

Axiomas

Nome	Esquema Axioma	Descrição
ENTÃO-1	${\ displaystyle \ phi \ to (\ chi \ to \ phi)}$	Adicionar hipótese χ , introdução de implicação
ENTÃO-2	${\ displaystyle (\ phi \ to (\ chi \ to \ psi)) \ to ((\ phi \ to \ chi) \ to (\ phi \ to \ psi))}$	Distribuir hipótese sobre implicação ${\ displaystyle \ phi}$
E 1	${\ displaystyle \ phi \ land \ chi \ to \ phi}$	Elimine a conjunção
AND-2	${\ displaystyle \ phi \ land \ chi \ to \ chi}$
AND-3	${\ displaystyle \ phi \ to (\ chi \ to (\ phi \ land \ chi))}$	Introduzir conjunção
OR-1	${\ displaystyle \ phi \ to \ phi \ lor \ chi}$	Introduzir disjunção
OR-2	${\ displaystyle \ chi \ to \ phi \ lor \ chi}$
OR-3	${\ displaystyle (\ phi \ to \ psi) \ to ((\ chi \ to \ psi) \ to (\ phi \ lor \ chi \ to \ psi))}$	Elimine disjunção
NOT-1	${\ displaystyle (\ phi \ to \ chi) \ to ((\ phi \ to \ neg \ chi) \ to \ neg \ phi)}$	Introduzir negação
NOT-2	${\ displaystyle \ phi \ to (\ neg \ phi \ to \ chi)}$	Elimine a negação
NOT-3	${\ displaystyle \ phi \ lor \ neg \ phi}$	Meio excluído, lógica clássica
IFF-1	${\ displaystyle (\ phi \ leftrightarrow \ chi) \ to (\ phi \ to \ chi)}$	Elimine a equivalência
IFF-2	${\ displaystyle (\ phi \ leftrightarrow \ chi) \ to (\ chi \ to \ phi)}$
IFF-3	${\ displaystyle (\ phi \ to \ chi) \ to ((\ chi \ to \ phi) \ to (\ phi \ leftrightarrow \ chi))}$	Introduzir equivalência

• O axioma THEN-2 pode ser considerado uma "propriedade distributiva de implicação em relação à implicação".
• Os axiomas AND-1 e AND-2 correspondem à "eliminação da conjunção". A relação entre AND-1 e AND-2 reflete a comutatividade do operador de conjunção.
• O axioma AND-3 corresponde à "introdução da conjunção".
• Os axiomas OR-1 e OR-2 correspondem à "introdução da disjunção". A relação entre OR-1 e OR-2 reflete a comutatividade do operador de disjunção.
• O axioma NOT-1 corresponde a "reductio ad absurdum."
• O axioma NOT-2 diz que "qualquer coisa pode ser deduzida de uma contradição."
• O axioma NOT-3 é chamado de " tertium non-datur " ( latim : "um terceiro não é dado") e reflete a valoração semântica de fórmulas proposicionais: uma fórmula pode ter um valor de verdade verdadeiro ou falso. Não existe um terceiro valor de verdade, pelo menos não na lógica clássica. Os lógicos intuicionistas não aceitam o axioma NOT-3 .

Regra de inferência

A regra de inferência é modus ponens :

${\ displaystyle \ phi, \ \ phi \ to \ chi \ vdash \ chi}$.

Regra de meta-inferência

Seja uma demonstração representada por uma sequência, com as hipóteses à esquerda da catraca e a conclusão à direita da catraca. Então, o teorema da dedução pode ser afirmado da seguinte forma:

Se a sequência

${\ displaystyle \ phi _ {1}, \ \ phi _ {2}, \ ..., \ \ phi _ {n}, \ \ chi \ vdash \ psi}$

foi demonstrado, então também é possível demonstrar a sequência

${\ displaystyle \ phi _ {1}, \ \ phi _ {2}, \ ..., \ \ phi _ {n} \ vdash \ chi \ to \ psi}$.

Este teorema de dedução (TD) não é formulado com cálculo proposicional: não é um teorema de cálculo proposicional, mas um teorema sobre cálculo proposicional. Nesse sentido, é um metateorema , comparável aos teoremas sobre a solidez ou integridade do cálculo proposicional.

Por outro lado, o DT é tão útil para simplificar o processo de prova sintática que pode ser considerado e usado como outra regra de inferência, acompanhando o modus ponens. Nesse sentido, DT corresponde à regra de inferência de prova condicional natural que faz parte da primeira versão de cálculo proposicional introduzida neste artigo.

O inverso do DT também é válido:

Se a sequência

${\ displaystyle \ phi _ {1}, \ \ phi _ {2}, \ ..., \ \ phi _ {n} \ vdash \ chi \ to \ psi}$

foi demonstrado, então também é possível demonstrar a sequência

${\ displaystyle \ phi _ {1}, \ \ phi _ {2}, \ ..., \ \ phi _ {n}, \ \ chi \ vdash \ psi}$

na verdade, a validade do inverso da TD é quase trivial em comparação com a da TD:

Se

${\ displaystyle \ phi _ {1}, \ ..., \ \ phi _ {n} \ vdash \ chi \ to \ psi}$

então

1: ${\ displaystyle \ phi _ {1}, \ ..., \ \ phi _ {n}, \ \ chi \ vdash \ chi \ to \ psi}$

2: ${\ displaystyle \ phi _ {1}, \ ..., \ \ phi _ {n}, \ \ chi \ vdash \ chi}$

e de (1) e (2) pode ser deduzido

3: ${\ displaystyle \ phi _ {1}, \ ..., \ \ phi _ {n}, \ \ chi \ vdash \ psi}$

por meio do modus ponens, QED

O inverso do DT tem implicações poderosas: ele pode ser usado para converter um axioma em uma regra de inferência. Por exemplo, o axioma AND-1,

${\ displaystyle \ vdash \ phi \ wedge \ chi \ to \ phi}$

pode ser transformado por meio do inverso do teorema de dedução na regra de inferência

${\ displaystyle \ phi \ wedge \ chi \ vdash \ phi}$

que é a eliminação da conjunção , uma das dez regras de inferência usadas na primeira versão (neste artigo) do cálculo proposicional.

Exemplo de prova

A seguir está um exemplo de uma demonstração (sintática), envolvendo apenas axiomas THEN-1 e THEN-2 :

Prove: (reflexividade de implicação). ${\ displaystyle A \ a A}$

Prova:

1. ${\ displaystyle (A \ to ((B \ to A) \ to A)) \ to ((A \ to (B \ to A)) \ to (A \ to A))}$

   Axioma THEN-2 com${\ displaystyle \ phi = A, \ chi = B \ to A, \ psi = A}$

2. ${\ displaystyle A \ to ((B \ to A) \ to A)}$

   Axioma THEN-1 com${\ displaystyle \ phi = A, \ chi = B \ to A}$

3. ${\ displaystyle (A \ to (B \ to A)) \ to (A \ to A)}$

   De (1) e (2) por modus ponens.

4. ${\ displaystyle A \ to (B \ to A)}$

   Axioma THEN-1 com${\ displaystyle \ phi = A, \ chi = B}$

5. ${\ displaystyle A \ a A}$

   De (3) e (4) por modus ponens.

Equivalência para lógicas equacionais

O cálculo alternativo anterior é um exemplo de sistema de dedução ao estilo de Hilbert . No caso de sistemas proposicionais, os axiomas são termos construídos com conectivos lógicos e a única regra de inferência é o modus ponens. A lógica equacional, conforme usada informalmente na álgebra do ensino médio, é um tipo diferente de cálculo dos sistemas de Hilbert. Seus teoremas são equações e suas regras de inferência expressam as propriedades da igualdade, ou seja, que é uma congruência de termos que admite substituição.

O cálculo proposicional clássico, conforme descrito acima, é equivalente à álgebra booleana , enquanto o cálculo proposicional intuicionista é equivalente à álgebra de Heyting . A equivalência é demonstrada pela translação em cada direção dos teoremas dos respectivos sistemas. Teoremas do cálculo proposicional clássico ou intuicionista são traduzidos como equações da álgebra booleana ou de Heyting, respectivamente. Por outro lado, os teoremas da álgebra booleana ou de Heyting são traduzidos como teoremas do cálculo clássico ou intuicionista, respectivamente, para o qual é uma abreviatura padrão. No caso da álgebra booleana, também pode ser traduzido como , mas essa tradução está incorreta intuicionisticamente. ${\ displaystyle \ phi}$${\ displaystyle \ phi = 1}$${\ displaystyle x = y}$${\ displaystyle (x \ to y) \ land (y \ to x)}$${\ displaystyle x \ equiv y}$${\ displaystyle x = y}$${\ displaystyle (x \ land y) \ lor (\ neg x \ land \ neg y)}$

Tanto na álgebra booleana quanto na de Heyting, a desigualdade pode ser usada no lugar da igualdade. A igualdade é exprimível como um par de desigualdades e . Por outro lado, a desigualdade é expressada como a igualdade , ou como . O significado da desigualdade para os sistemas do estilo de Hilbert é que ela corresponde à dedução do último ou símbolo de implicação . Uma implicação ${\ displaystyle x \ leq y}$${\ displaystyle x = y}$${\ displaystyle x \ leq y}$${\ displaystyle y \ leq x}$${\ displaystyle x \ leq y}$${\ displaystyle x \ land y = x}$${\ displaystyle x \ lor y = y}$${\ displaystyle \ vdash}$

${\ displaystyle \ phi _ {1}, \ \ phi _ {2}, \ \ dots, \ \ phi _ {n} \ vdash \ psi}$

é traduzido na versão de desigualdade do quadro algébrico como

${\ displaystyle \ phi _ {1} \ \ land \ \ phi _ {2} \ \ land \ \ dots \ \ land \ \ phi _ {n} \ \ \ leq \ \ \ psi}$

Por outro lado, a desigualdade algébrica é traduzida como a implicação ${\ displaystyle x \ leq y}$

${\ displaystyle x \ \ vdash \ y}$.

A diferença entre implicação e desigualdade ou implicação ou é que a primeira é interna à lógica, enquanto a última é externa. A implicação interna entre dois termos é outro termo do mesmo tipo. A inscrição como implicação externa entre dois termos expressa uma metatruth fora da linguagem da lógica e é considerada parte da metalinguagem . Mesmo quando a lógica em estudo é intuicionista, a vinculação é normalmente entendida classicamente como de dois valores: ou o lado esquerdo implica, ou é menor ou igual ao lado direito, ou não é. ${\ displaystyle x \ a y}$ ${\ displaystyle x \ leq y}$${\ displaystyle x \ \ vdash \ y}$

Traduções semelhantes, mas mais complexas, de e para a lógica algébrica são possíveis para sistemas de dedução natural como descrito acima e para o cálculo sequencial . As implicações deste último podem ser interpretadas como de dois valores, mas uma interpretação mais perspicaz é como um conjunto, cujos elementos podem ser entendidos como provas abstratas organizadas como morfismos de uma categoria . Nessa interpretação, a regra de corte do cálculo sequencial corresponde à composição na categoria. Álgebras de Booleana e de Heyting entram neste quadro como categorias especiais tendo no máximo um morfismo por homset, ou seja, uma prova por vinculação, correspondendo à ideia de que a existência de provas é tudo o que importa: qualquer prova servirá e não há sentido em distingui-las. .

Cálculos gráficos

É possível generalizar a definição de uma linguagem formal a partir de um conjunto de sequências finitas sobre uma base finita para incluir muitos outros conjuntos de estruturas matemáticas, desde que sejam construídas por meios finitos a partir de materiais finitos. Além do mais, muitas dessas famílias de estruturas formais são especialmente adequadas para uso em lógica.

Por exemplo, existem muitas famílias de gráficos que são análogos o suficiente das linguagens formais para que o conceito de cálculo seja facilmente estendido a eles. Muitas espécies de gráficos surgem como gráficos de análise sintática das famílias correspondentes de estruturas de texto. As exigências da computação prática em linguagens formais freqüentemente exigem que as strings de texto sejam convertidas em representações de estrutura de ponteiro de gráficos de análise, simplesmente como uma questão de verificar se as strings são fórmulas bem formadas ou não. Feito isso, há muitas vantagens em desenvolver o análogo gráfico do cálculo em cordas. O mapeamento de strings para gráficos de análise é chamado de análise e o mapeamento inverso de gráficos de análise para strings é realizado por uma operação que é chamada de atravessar o gráfico.

Outros cálculos lógicos

O cálculo proposicional é o tipo mais simples de cálculo lógico atualmente em uso. Ele pode ser estendido de várias maneiras. (O cálculo "silogístico" aristotélico , que é amplamente suplantado na lógica moderna, é de algumas maneiras mais simples - mas de outras maneiras mais complexo - do que o cálculo proposicional.) A maneira mais imediata de desenvolver um cálculo lógico mais complexo é introduzir regras que são sensível a detalhes mais refinados das frases que estão sendo usadas.

A lógica de primeira ordem (também conhecida como lógica de predicado de primeira ordem) resulta quando as "sentenças atômicas" da lógica proposicional são divididas em termos , variáveis , predicados e quantificadores , todos mantendo as regras da lógica proposicional com algumas novas introduzidas. (Por exemplo, de "Todos os cães são mamíferos" podemos inferir "Se o Rover é um cão, então o Rover é um mamífero".) Com as ferramentas da lógica de primeira ordem, é possível formular uma série de teorias, seja com axiomas explícitos ou por regras de inferência, que podem ser tratadas como cálculos lógicos. A aritmética é a mais conhecida delas; outros incluem teoria dos conjuntos e mereologia . A lógica de segunda ordem e outras lógicas de ordem superior são extensões formais da lógica de primeira ordem. Assim, faz sentido referir-se à lógica proposicional como "lógica de ordem zero" , ao compará-la com essas lógicas.

A lógica modal também oferece uma variedade de inferências que não podem ser capturadas no cálculo proposicional. Por exemplo, de "Necessariamente p " podemos inferir que p . De p podemos inferir "É possível que p ". A tradução entre lógica modal e lógica algébrica diz respeito à lógica clássica e intuicionista, mas com a introdução de um operador unário nas álgebras booleanas ou de Heyting, diferente das operações booleanas, interpretando a modalidade de possibilidade, e no caso da álgebra de Heyting um segundo operador interpretando a necessidade (para a álgebra booleana, isso é redundante, pois necessidade é o dual de possibilidade de De Morgan). O primeiro operador preserva 0 e disjunção, enquanto o segundo preserva 1 e conjunção.

Lógicas de muitos valores são aquelas que permitem que as sentenças tenham valores diferentes de verdadeiro e falso . (Por exemplo, nenhum e ambos são "valores extras" padrão; a "lógica contínua" permite que cada frase tenha qualquer um de um número infinito de "graus de verdade" entre verdadeiro e falso .) Essas lógicas frequentemente requerem dispositivos de cálculo bastante distintos dos proposicionais. cálculo. Quando os valores formam uma álgebra booleana (que pode ter mais de dois ou até infinitos valores), a lógica de muitos valores se reduz à lógica clássica; lógicas de muitos valores são, portanto, de interesse independente apenas quando os valores formam uma álgebra que não seja booleana.

Solucionadores

Encontrar soluções para fórmulas lógicas proposicionais é um problema NP-completo . No entanto, existem métodos práticos (por exemplo, algoritmo DPLL , 1962; algoritmo Chaff , 2001) que são muito rápidos para muitos casos úteis. Um trabalho recente estendeu os algoritmos do solver SAT para trabalhar com proposições contendo expressões aritméticas ; estes são os solucionadores SMT .

Veja também

Níveis lógicos superiores

• Lógica de primeira ordem
• Lógica proposicional de segunda ordem
• Lógica de segunda ordem
• Lógica de ordem superior

tópicos relacionados

Referências

Leitura adicional

• Brown, Frank Markham (2003), Boolean Reasoning: The Logic of Boolean Equations , 1ª edição, Kluwer Academic Publishers, Norwell, MA. 2ª edição, Dover Publications, Mineola, NY.
• Chang, CC e Keisler, HJ (1973), Model Theory , North-Holland, Amsterdam, Netherlands.
• Kohavi, Zvi (1978), Switching and Finite Automata Theory , 1ª edição, McGraw – Hill, 1970. 2ª edição, McGraw – Hill, 1978.
• Korfhage, Robert R. (1974), Discrete Computational Structures , Academic Press, New York, NY.
• Lambek, J. e Scott, PJ (1986), Introdução à Lógica Categórica de Ordem Superior , Cambridge University Press, Cambridge, Reino Unido.
• Mendelson, Elliot (1964), Introdução à Lógica Matemática , D. Van Nostrand Company.

Trabalhos relacionados

• Hofstadter, Douglas (1979). Gödel, Escher, Bach: An Eternal Golden Braid . Livros básicos . ISBN 978-0-465-02656-2.

links externos

• Klement, Kevin C. (2006), "Propositional Logic", em James Fieser e Bradley Dowden (eds.), Internet Encyclopedia of Philosophy , Eprint .
• Formal Predicate Calculus , contém um desenvolvimento formal sistemático ao longo das linhas do cálculo alternativo
• forall x: uma introdução à lógica formal , por PD Magnus , cobre semântica formal e teoria da prova para lógica sentencial.
• Capítulo 2 / Lógica proposicional da lógica em ação
• Provador proposicional de cálculo sequencial no Projeto Nayuki. ( observação : a implicação pode ser inserida no formato ! X | Y , e um sequente pode ser uma única fórmula prefixada com > e sem vírgulas)
• Lógica proposicional - uma gramática gerativa