LÓGICA PROPOSICIONAL: PARTE 2

LÓGICA PROPOSICIONAL  

UMA INTRODUÇÃO METATEÓRICA (PARTE 2)

VINICIUS DIAS DE SOUZA

b. Regras de Inferência

Aqui, damos uma lista de regras de inferência intuitivamente válidas. As regras são indicadas em forma esquemática . Qualquer inferência em que qualquer wff do idioma PL seja substituído de forma não formal pelas letras esquemáticas nos formulários abaixo constitui uma instância da regra.

Modus ponens (MP):

α → β 
α
β

(Modus ponens às vezes também é chamado de "modus ponendo ponens", "destacamento" ou uma forma de " → " eliminação ").

Modus tollens (MT):

α → β 
¬β
¬α

(Modus tollens às vezes também é chamado de "modus tollendo tollens" ou uma forma de " → -eliminação".)

Silogismo Disjuntivo (DS): (duas formas)

α v β 
¬α
β

α v β 
¬β
α

(O silogismo disjuntivo às vezes também é chamado de "modus tollendo ponens" ou " v-eliminação".)

Adição (DS): (duas formas)

α
α v β

β
α v β

(A adição às vezes também é chamada de "introdução de disjunção" ou "introdução de v ").

Simplificação (Simp): (duas formas)

α & β
α

α & β
β

(Simplificação às vezes também é chamada de "eliminação conjunta" ou " & -eliminação".)

Conjunção (Conj):

α 
β
α & β

(Conjunção às vezes é também chamado de "introdução da conjunção", " & -Introdução" ou "multiplicação lógica".)

Silogismo hipotético (HS):

α → β 
β → γ
α → γ

(O silogismo hipotético às vezes também é chamado de "raciocínio de cadeia" ou "dedução de cadeia").

Dilema construtivo (CD):

(α → γ) & (β → δ) 
α v β
γ v δ

Absorção (Abs):

α → β
α → (α & β)

c. Regras de substituição

As nove regras de inferência listadas acima representam maneiras de inferir algo novo de etapas anteriores em uma dedução. Muitos sistemas de dedução natural, incluindo aqueles inicialmente projetados por Gentzen, são inteiramente de regras semelhantes às acima descritas. Se o idioma de um sistema envolve sinais introduzidos por definição, ele também deve permitir a substituição de um sinal definido pela expressão usada para defini-lo, ou vice-versa. Ainda outros sistemas, embora não façam uso de sinais definidos, permitem que se façam certas substituições de expressões de uma forma para expressões de outra forma em certos casos em que as expressões em questão são logicamente equivalentes. Estas são chamadas de regras de substituição, e o sistema de dedução natural da Copi invoca tais regras. Estritamente falando, as regras de substituição diferem das regras de inferência, porque, em certo sentido, quando uma regra de substituição é usada, não se infere algo novo, mas apenas indica o que equivale à mesma coisa usando uma combinação de símbolos diferente. Em alguns sistemas, as regras de substituição podem ser derivadas das regras de inferência, mas no sistema de Copi, elas são tomadas como primitivas.

As regras de substituição também diferem das regras de inferência de outras maneiras. As regras de inferência só se aplicam quando os principais operadores combinam os padrões fornecidos e apenas se aplicam a declarações inteiras. As regras de inferência também são estritamente unidirecionais: é preciso inferir o que está abaixo da linha horizontal do que está acima e não vice-versa. No entanto, as regras de substituição podem ser aplicadas a partes de declarações e não apenas a declarações inteiras; Além disso, eles podem ser implementados em qualquer direção.

As regras de substituição usadas pela Copi são as seguintes:

Negação dupla (DN):

¬¬α é inter - substituível com α

(A negação dupla também é chamada de "¬-eliminação".)

Comutatividade (Com): (duas formas)

α & β é inter-substituível com β & α 
α v β é inter-substituível com β v α

Associatividade (Assoc): (duas formas)

(α & β) & γ é inter-substituível com α & (β & γ) 
(α v β) v γ é inter-substituível com α v (β v γ)

Tautologia (Taut): (duas formas)

α é inter-substituível com α & α 
α é inter-substituível com α v α

DeMorgan's Laws (DM): (duas formas)

¬ (α & β) é inter - substituível com ¬α v ¬β 
¬ (α v β) é inter-substituível com ¬α & ¬β

Transposição (Trans):

α → β é inter - substituível com ¬β → ¬α

(A transposição também é às vezes chamada de "contraposição").

Implicação de Material (Impl):

α → β é inter - substituível com ¬α v β

Exportação (Exp):

α → (β → γ) é inter-substituível com (α & β) → γ

Distribuição (Dist): (duas formas)

α & (β v γ) é interreutável com (α & β) v (α & γ) 
α v (β & γ) é interreutável com (α v β) & (α v γ)

Equivalência de Material (Equiv): (duas formas)

α ↔ β é interreutável com (α → β) & (β → α) 
α ↔ β é interreutável com (α & β) v (¬α & ¬β)

(A equivalência de material às vezes também é chamada de "introdução / eliminação de biconditional" ou " ↔ -introdução / eliminação").

d. Deduções diretas

Uma dedução direta de uma conclusão de um conjunto de instalações consiste em uma seqüência ordenada de wffs, de modo que cada membro da sequência seja (1) uma premissa, (2) derivada de membros anteriores da sequência por uma das regras de inferência, (3) derivado de um membro anterior da sequência pela substituição de uma parte logicamente equivalente de acordo com as regras de substituição, e tal que a conclusão é o passo final da seqüência.

Para ser ainda mais preciso, uma dedução direta é definida como uma sequência ordenada de wffs, β 1 , β 2 , ..., β n , de modo que, para cada passo β i onde i esteja entre 1 e n inclusive, quer (1 ) β i é uma premissa, (2) β i corresponde à forma dada abaixo da linha horizontal para uma das 9 regras de inferência, e há wffs na sequência anterior a β i correspondente aos formulários dados acima da linha horizontal, (3 ) há um passo anterior na seqüência β j onde j < i e β j diferem de β ino máximo, combinando ou contendo uma parte que corresponde a uma das formas dadas para uma das 10 regras de substituição no mesmo lugar em que i contém o wff da forma correspondente, e tal que a conclusão do argumento é β n .

Usando números de linha e as abreviaturas para as regras do sistema para anotar, a cadeia de raciocínio dada acima em inglês, quando transcrito em linguagem PL e organizado como uma dedução direta, apareceria da seguinte maneira:

1. C v D	Premissa
2. C → O	Premissa
3. D → M	Premissa
4. ¬O	Premissa
5. ¬C	2,4 MT
6. D	1,5 DS
7. M	2,6 MP

Não existe uma derivação única para uma determinada conclusão de um determinado conjunto de instalações. Aqui está uma derivação distinta para a mesma conclusão a partir da mesma premissa:

1. C v D	Premissa
2. C → O	Premissa
3. D → M	Premissa
4. ¬O	Premissa
5. (C → O) & (D → M)	2,3 Conj
6. O v M	1,5 CD
7. M	4,6 DS

Considere o próximo argumento:

P ↔ Q 
(S v T) → Q 
¬P v (¬T & R)
T → U

Este argumento possui seis letras distintas e, portanto, a construção de uma tabela de verdade exigirá 64 linhas. A tabela teria 22 colunas, exigindo assim 1.408 cálculos T / F distintos. Felizmente, a derivação da conclusão das instalações usando nossas regras de inferência e substituição, embora longe de simples, é relativamente menos exaustiva:

1. P ↔ Q	Premissa
2. (S v T) → Q	Premissa
3. ¬P v (¬T & R)	Premissa
4. (P → Q) & (Q → P)	1 Equiv
5. Q → P	4 Simp
6. (S v T) → P	2,5 HS
7. P → (¬T & R)	3 Impl
8. (S v T) → (¬T & R)	6,7 HS
9. ¬ (S v T) v (¬T & R)	8 Impl
10. (¬S & ¬T) v (¬T & R)	9 DM
11. [(¬S & ¬T) v ¬T] & [(¬S & ¬T) v R]	10 Dist
12. (¬S & ¬T) v ¬T	11 Simp
13. ¬ T v (¬S & ¬T)	12 Com
14. (¬T v ¬S) & (¬T v ¬T)	13 Dist
15. ¬T v ¬T	14 Simp
16. ¬T	15 Taut
17. ¬ T v U	16 Adicionar
18. T → U	17 Impl

e. Prova condicional e indireta

Juntos, as nove regras de inferência e dez regras de substituição são suficientes para criar uma dedução para qualquer argumento logicamente válido, desde que o argumento tenha pelo menos uma premissa. No entanto, para cobrir o caso limitante de argumentos sem premissas, e simplesmente para facillizar certas deduções que seriam mais simples, também é costume permitir certos métodos de dedução além da derivação direta. Especificamente, é costume permitir as técnicas de prova conhecidas como prova condicional e prova indireta .

Uma prova condicional é uma técnica de derivação usada para estabelecer um wff condicional, ou seja, um wff cujo operador principal é o sinal '→'. Isso é feito construindo uma sub-derivação dentro de uma derivação na qual o antecedente do condicional é assumido como hipótese. Se, ao usar as regras de inferência e as regras de derivação (e sub-derivações possivelmente adicionais), é possível chegar ao conseqüente, é permitido encerrar a sub-derivação e concluir a verdade da declaração condicional dentro da derivação principal , citando a sub-derivação como uma prova condicional, ou 'CP' para breve. Isso é muito mais claro ao considerar o exemplo seguinte:

P → (Q v R) 
P → ¬S 
S ↔ Q
P → R

Embora seja possível uma derivação direta estabelecendo a validade desse argumento, é mais fácil estabelecer a validade desse argumento usando uma derivação condicional.

1. P → (Q v R)	Premissa
2. P → ¬S	Premissa
3. S ↔ Q	Premissa
4. P	Suposição
5. Q v R	1,4 MP
6. ¬S	2,4 MP
7. (S → Q) & (Q → S)	3 Equiv
8. Q → S	7 Simp
9. ¬Q	6,8 MT
10. R	5,9 DS
11. P → R	4-10 CP

Aqui, para estabelecer a afirmação condicional "P → R", construímos uma sub-derivação, que é a parcela recuada encontrada nas linhas 4-10. Primeiro, assumimos a verdade de 'P', e descobrimos que, com isso, poderíamos derivar 'R'. Dadas as premissas, demonstramos que se 'P' também fosse verdadeiro, então seria 'R'. Portanto, com base na sub-derivação, fomos justificados ao concluir "P → R". Esta é a metodologia usual utilizada em lógica e matemática para estabelecer a verdade de uma declaração condicional.

Outro método comum é o da prova indireta , também conhecida como prova por reductio ad absurdum . (Para uma discussão mais completa, veja a entrada na reductio ad absurdum na enciclopédia.) Em uma prova indireta ('IP' para breve), nosso objetivo é demonstrar que um certo wff é falso com base nas premissas. Novamente, fazemos uso de uma sub-derivação; Aqui, começamos por assumir o oposto do que estamos tentando provar, ou seja, assumimos que o wff é verdadeiro. Se, com base nessa suposição, podemos demonstrar uma contradição óbvia, ou seja, uma declaração da forma α & ¬α , podemos concluir que a afirmação suposta deve ser falsa, porque qualquer coisa que leve a uma contradição deve ser falsa.

Por exemplo, considere o seguinte argumento:

P → Q 
P → (Q → ¬P)
¬P

Embora, novamente, seja possível uma derivação direta da conclusão desse argumento das instalações, é um pouco mais fácil provar que "¬P" é verdade ao mostrar que, dadas as premissas, seria impossível que "P" fosse É verdade, assumindo que é e mostrando isso um absurdo.

1. P → Q	Premissa
2. P → (Q → ¬P)	Premissa
3. P	Suposição
4. Q	1,3 MP
5. Q → ¬P	2,3 MP
6. ¬P	4,5 MP
7. P & ¬P	3,6 Conj
8. ¬P	3-7 IP

Aqui estávamos tentando mostrar que "¬P" era verdadeiro dado as instalações. Para fazer isso, assumimos que "P" era verdade. Como essa hipótese era impossível, justificamos-nos concluir que 'P' é falso, ou seja, que "¬P" é verdade.

Ao fazer uso de prova condicional ou prova indireta, uma vez que uma sub-derivação é concluída, as linhas que compõem não podem ser usadas mais tarde na derivação principal ou em sub-derivações adicionais que possam ser construídas mais tarde.

Isso completa nossa caracterização de um sistema de dedução natural para o idioma PL.

O sistema de dedução natural que acabamos de descrever é formalmente adequado no seguinte sentido. Anteriormente, definimos um argumento válido como um em que não existe uma possível atribuição de valor de verdade às letras de declaração que compõem suas premissas e conclusão que torna as premissas verdadeiras, mas a conclusão é falsa. É provável que um argumento na linguagem de PL seja formalmente válido nesse sentido se e somente se for possível construir uma derivação da conclusão desse argumento a partir das instalações usando as regras de inferências acima, regras de substituição e técnicas de prova condicional e indireta. As limitações do espaço impedem uma prova completa disso na metalinguagem, embora o raciocínio seja muito semelhante ao dado para o Cálculo proposicional axiomático discutido nas Seções VIe VII abaixo.

Informalmente, é bastante fácil ver que nenhum argumento para o qual uma dedução é possível neste sistema pode ser inválido de acordo com as tabelas da verdade. Em primeiro lugar, as regras da inferência são todas preservando a verdade . Por exemplo, no caso do modus ponens , é bastante fácil ver a partir da tabela de verdade para qualquer conjunto de declarações da forma apropriada que nenhuma atribuição de valor de verdade poderia tornar α → β e α verdadeiro ao fazer β falso. Uma consideração semelhante se aplica aos outros. Além disso, as tabelas de verdade podem ser facilmente usadas para verificar que as declarações de uma das formas mencionadas nas regras de substituição são todas logicamente equivalentescom aqueles a regra permite que alguém troque por eles. Assim, as declarações nunca podem diferir em valor de verdade para qualquer atribuição de valor de verdade. Em caso de prova condicional, note que qualquer atribuição de valor de verdade deve tornar o condicional verdadeiro, ou deve tornar o antecedente verdadeiro e conseqüente falso. O antecedente é o que é assumido em uma prova condicional. Então, se a atribuição do valor da verdade faz com que ele e as premissas do argumento sejam verdadeiras, porque as outras regras são todas preservando a verdade, seria impossível derivar o conseqüente, a menos que também fosse verdade. Uma consideração semelhante justifica o uso de provas indiretas.

Este sistema representa um método útil para estabelecer a validade de um argumento que tenha a vantagem de coincidir mais com a maneira como normalmente o Razão. (Conforme observado anteriormente, no entanto, existem muitos sistemas equivalentes de dedução natural, todos coincidindo relativamente perto de padrões de raciocínio comuns). Uma desvantagem que este método tenha, no entanto, é que, ao contrário das tabelas de verdade, não fornece um meio para reconhecer isso um argumento é inválido. Se um argumento for inválido, não há dedução para ele no sistema. No entanto, o próprio sistema não fornece um meio para reconhecer quando uma dedução é impossível.

Outra objeção que pode ser feita ao sistema de dedução esboçado acima é que contém mais regras e mais técnicas do que precisa. Isso nos leva diretamente ao nosso próximo tópico.

6. Sistemas Axiomáticos e o Cálculo Proposicional

O sistema de dedução discutido na seção anterior é um exemplo de um sistema de dedução natural, ou seja, um sistema de dedução para um idioma formal que tenta coincidir o mais próximo possível das formas de raciocínio que a maioria das pessoas realmente emprega. Os sistemas naturais de dedução são tipicamente contrastados com os sistemas axiomáticos . Os sistemas axiomáticos são sistemas minimalistas; em vez de incluir regras correspondentes aos modos naturais de raciocínio, eles utilizam como poucos princípios básicos ou regras possíveis. Uma vez que poucos tipos de etapas estão disponíveis em uma dedução, relativamente falando, um sistema axiomático geralmente requer mais etapas para a dedução de uma conclusão de um dado conjunto de instalações em comparação com um sistema de dedução natural.

Normalmente, um sistema axiomático consiste na especificação de certos wffs que são especificados como "axiomas". Um axioma é algo que é tomado como uma verdade fundamental do sistema que não exige prova. Para permitir a dedução dos resultados dos axiomas ou das premissas de um argumento, o sistema tipicamente também inclui, pelo menos, uma (e muitas vezes apenas uma) regra de inferência. Normalmente, uma tentativa é feita para limitar o número de axiomas ao menor possível, ou pelo menos, limitar o número de formas que os axiomas podem tomar.

Como os sistemas axiomáticos pretendem ser mínimos, tipicamente empregam linguagens com vocabulários simplificados sempre que possível. Para a lógica proposicional da verdade clássica da verdade, isso pode envolver o uso de um idioma mais simples como PL 'ou PL' 'em vez do PL completo.

Para a maior parte do restante desta seção, devemos esboçar um sistema axiomático para a lógica proposicional da verdade clássica da verdade, que devemos dobrar o Cálculo proposicional (ou PC para breve). O Cálculo Proposicional faz uso da linguagem PL ', descrita acima. Ou seja, os únicos conectivos que eles usam são '→' e '¬', e os outros operadores, se forem usados, seriam entendidos como abreviaturas abreviadas, fazendo uso da discussão de definições na Seção III (c) .

O PC do sistema consiste em três esquemas de axioma , que são formas que se ajusta se é axioma, juntamente com uma única regra de inferência: modus ponens . Nós tornamos isso mais preciso especificando certas definições.

Definição: um wff de linguagem PL 'é um axioma de PC se e somente se for uma instância de uma das seguintes três formas:

α → (β → α)	(Esquema Axiom 1 ou AS1)
(α → (β → γ)) → ((α → β) → (α → γ))	(Axiom Schema 2, ou AS2)
(¬α → ¬β) → ((¬α → β) → α)	(Axiom Schema 3, ou AS3)

Note-se que de acordo com esta definição, todo wff da forma α → (β → α) é um axioma. Isso inclui um número infinito de wffs diferentes, de casos simples, como "P → (Q → P)", para casos muito mais complicados, como "(¬R → ¬¬S) → [¬ (¬M → N) → (¬R → ¬¬S)] ".

Uma dedução passo a passo ordenada constitui uma derivação no sistema PC se e somente se cada passo na dedução for (1) uma premissa do argumento, (2) um axioma, ou (3) derivado de etapas anteriores por modus Ponens . Mais uma vez, podemos tornar isso mais preciso com a seguinte definição (mais recôndita):

Definição: uma sequência ordenada de wffs β 1 , β 2 , ..., β n é uma derivação no PC do sistema do wff β n das instalações α 1 , α 2 , ..., α m se e somente se, para cada wff β i na sequência β 1 , β 2 , ..., β n , quer (1) β i é uma das premissas α 1 , α 2 , ..., α m , (2) β i é um axioma de PC, ou (3) β i segue de membros anteriores da série pela regra de inferênciamodus ponens (isto é, existem membros anteriores da sequência, β j e β k , de modo que p j assume a forma β k → β i ).

Por exemplo, considere o seguinte argumento escrito no idioma PL ':

P 
(R → P) → (R → (P → S))
R → S

O seguinte constitui uma derivação no sistema PC da conclusão das instalações:

1. P	Premissa
2. (R → P) → (R → (P → S))	Premissa
3. P → (R → P)	Instância de AS1
4. R → P	1,3 MP
5. R → (P → S)	2,4 MP
6. (R → (P → S)) → ((R → P) → (R → S))	Instância de AS2
7. (R → P) → (R → S)	5,6 MP
8. R → S	4,7 MP

Historicamente, os sistemas axiomáticos originais para a lógica foram concebidos para ser semelhante a outros sistemas axiomáticos encontrados na matemática, como a axiomatização da geometria de Euclides. O objetivo de desenvolver um sistema axiomático para a lógica foi criar um sistema no qual derivar verdades de lógica fazendo uso apenas dos axiomas do sistema e da (s) regra (s) de inferência. Esses wffs que podem ser derivados dos axiomas e da regra de inferência sozinhos, ou seja, sem fazer uso de nenhuma premissa adicional, são denominados teoremas ou teses do sistema. Para tornar isso mais preciso:

Definição: um wff α é dito ser um teorema do PC se e somente se houver uma sequência ordenada de wffs, especificamente, uma derivação, β 1 , β 2 , ..., β n tal que, α é β n e cada wff β i na sequência β 1 , β 2 , ..., β n , é tal que qualquer (1) β i é um axioma de PC, ou (2) β i segue de membros anteriores da série por modus Ponens .

Um teorema muito simples do PC do sistema é o wff "P → P". Podemos mostrar que é um teorema construindo uma derivação de "P → P" que faz uso apenas de axiomas e MP e sem premissas adicionais.

1. P → (P → P)	Instância de AS1
2. P → ((P → P) → P)	Instância de AS1
3. [P → ((P → P) → P)] → [(P → (P → P)) → (P → P)]	Instância de AS2
4. (P → (P → P)) → (P → P)	2,3 MP
5. P → P	1,4 MP

É bastante fácil ver que não só é "P → P" um teorema do PC, mas também é qualquer wff da forma α → α . O que quer que seja, existe uma derivação no PC da mesma forma:

1. α → (α → α)	Instância de AS1
2. α → ((α → α) → α)	Instância de AS1
3. [α → ((α → α) → α)] → [(α → (α → α)) → (α → α)]	Instância de AS2
4. (α → (α → α)) → (α → α)	2,3 MP
5. α → α	1,4 MP

Portanto, mesmo se formos α no acima, o wff mais complicado, por exemplo, "¬ (¬M → N)", uma derivação com a mesma forma mostra que "¬ (¬M → N) → ¬ (¬M → N) "também é um teorema do PC. Por isso, chamamos α → α um esquema de teorema do PC, porque todas as suas instâncias são teoremas do PC. De agora em diante, vamos chamar "Theorem Schema 1", ou "TS1" para baixo.

Os seguintes são também esquemas do theorem do PC:

α → ¬¬α	(Esquema do teorema 2 ou TS2)
¬α → (α → β)	(TS3)
α → (¬β → ¬ (α → β))	(TS4)
(α → β) → ((¬α → β) → β)	(TS5)

Você pode querer verificar isso por si mesmo tentando construir as provas apropriadas para cada um. Esteja avisado que alguns exigem derivações bastante longas!

É comum usar a notação:

⊢ β

para significar que β é um teorema. Da mesma forma, é comum usar a notação:

α 1 , α 2 , ..., α m ⊢ β

para significar que é possível construir uma derivação de β fazendo uso de α 1 , α 2 , ..., α m como premissa.

Considerado em termos de número de regras que emprega, o sistema axiomático PC é muito menos complexo do que o sistema de dedução natural esboçado na seção anterior. O sistema de dedução natural utilizou nove regras de inferência, dez regras de substituição e duas técnicas de prova adicionais. O sistema axiomático, em vez disso, faz uso de esquemas de três axiomas e uma única regra de inferência e sem técnicas de prova adicionais. No entanto, o sistema axiomático não está de forma alguma.

Na verdade, para qualquer argumento usando o idioma PL 'que seja logicamente válido de acordo com as tabelas de verdade, é possível construir uma derivação no PC do sistema para esse argumento. Além disso, todo wff da linguagem PL 'que é uma verdade lógica, ou seja, uma tautologia de acordo com as tabelas da verdade, é um teorema do PC. O inverso desses resultados também é verdadeiro; Todo teorema do PC é uma tautologia, e cada argumento para o qual uma derivação no PC do sistema existe é logicamente válido de acordo com as tabelas da verdade. Estas e outras características do Cálculo proposicional são discutidas, e algumas são comprovadas na próxima seção abaixo.

Enquanto o Cálculo proposicional é mais simples de uma maneira que o sistema de dedução natural esboçado na seção anterior, em muitos aspectos é realmente mais complicado de usar. Para qualquer argumento dado, uma dedução da conclusão das instalações realizadas no PC provavelmente será muito maior e menos psicologicamente natural do que uma realizada em um sistema de dedução natural. Essas deduções são apenas mais simples no sentido de que menos regras distintas são empregadas.

O PC do sistema é apenas uma das muitas formas possíveis de axiomatizar a lógica proposicional. Alguns sistemas diferem do PC de maneiras muito pequenas. Por exemplo, podemos alterar nossa definição de "axioma" para que um wff seja um axioma se for uma instância de (A1), uma instância de (A2) ou uma instância do seguinte:

(A3 ') (¬α → ¬β) → (β → α)

Substituindo o esquema do axioma (A3) por (A3 '), enquanto altera a forma como determinadas deduções devem ser construídas (tornando as provas de muitos resultados importantes mais longos), tem pouco efeito de outra forma; o sistema resultante teria todos os mesmos teoremas e cada argumento para o qual uma dedução é possível no sistema acima também teria uma dedução no sistema revisado e vice-versa.

Nós também observamos acima que, estritamente falando, há um número infinito de axiomas do PC do sistema. Em vez de utilizar um número infinito de axiomas, poderíamos, alternativamente, ter utilizado apenas três axiomas , ou seja, os wffs específicos:

(A1) P → (Q → P) 
(A2 *) (P → (Q → R)) → ((P → Q) → (P → R)) 
(A3 *) (¬P → ¬Q) → ((¬P → Q) → P)

Observe que (A1 *) é apenas um wff exclusivo; nesta abordagem, o wff "(¬R → ¬¬S) → [¬ (¬M → N) → (¬R → ¬¬S)]" não contaria como um axioma, mesmo que compartilhe um comum de (A1 *). Para tal sistema, seria necessário adicionar uma regra de inferência adicional , uma regra de substituição ou substituição uniforme . Isso permitiria inferir, a partir de um teorema do sistema, o resultado de substituir uniformemente qualquer letra de declaração (por exemplo, 'P' ou 'Q') que ocorre dentro do teorema, com qualquer wff, simples ou complexo, desde que o mesmo que substitui todas as ocorrências da mesma letra de declaração no teorema. Nesta abordagem, "(¬R → ¬¬S) → [¬ (¬M → N) → (¬R → ¬¬S)]", enquanto não um axioma, ainda seria um teoremaporque poderia ser derivado da regra da substituição uniforme duas vezes, ou seja, ao substituir primeiro 'P' em (A1 *) por "(¬R → ¬¬S)", e depois substituir 'Q' por "¬ (¬M → N) ". O sistema resultante difere de maneiras sutis do nosso sistema PC anterior. O sistema PC, estritamente falando, usa apenas uma regra de inferência, mas admite um número infinito de axiomas. Este sistema usa apenas três axiomas, mas faz uso de uma regra adicional. O sistema PC, no entanto, evita essa regra de inferência adicional, permitindo que tudo o que se poderia obter por substituição em (A1 *) seja um axioma. Para cada teorema α, portanto, se β se um wff obtido de α substituindo uniformemente wffs por letras de indicação em α, então β também é um teorema de PC,

Também é possível construir sistemas ainda mais ausentes. Na verdade, é possível utilizar apenas um único esquema de axioma (ou um único axioma mais uma regra de substituição). Uma possibilidade, sugerida por CA Meredith (1953), seria definir um axioma como qualquer wff que corresponda à seguinte forma:

((((α → β) → (¬γ → δδ)) → γ) → ε) → ((ε → α) → (δ → α))

O sistema resultante é igualmente poderoso como o sistema PC e tem exatamente o mesmo conjunto de teoremas. No entanto, é muito menos psicologicamente intuitivo e direto, e as deduções mesmo para resultados relativamente simples são muitas vezes muito longas.

Historicamente, o primeiro sistema de esquema axiom único usou, em vez de linguagem PL ', a linguagem ainda mais simples PL' ', na qual o único conectivo é o traço Sheffer,' | ', como discutido acima. Nesse caso, é possível usar apenas o seguinte esquema de axioma:

(α | (β | γ)) | ((δ | (δ | δ)) | ((ε | β) | ((α | ε) | (α | ε))))

A regra de inferência de MP é substituída pela regra que de wffs da forma α | (β | γ) e α, pode-se deduzir o wff γ. Este sistema foi descoberto por Jean Nicod (1917). Mais recentemente, vários sistemas possíveis de axioma único foram encontrados, alguns melhor do que outros em termos de complexidade do axioma único e em termos de quanto tempo as deduções para os mesmos resultados devem ser. (Para pesquisas recentes nesta área, consulte McCune et al., 2002.) Geralmente, no entanto, quanto mais o sistema permite, menor será a dedução.

Além das formas de dedução axiomática e natural, os sistemas de dedução para a lógica proposicional também podem assumir a forma de um cálculo sequencial; aqui, em vez de especificar definições de axiomas e regras de inferência, as regras são declaradas diretamente em termos de derivabilidade ou condições de vinculação; Por exemplo, uma regra pode indicar que se (ou α ⊢ β ou α ⊢ γ), então, se γ, α ⊢ β então α ⊢ β. Os cálculos seqüinos, como os modernos sistemas de dedução natural, foram desenvolvidos pela Gerhard Gentzen. O trabalho de Gentzen também sugere o uso de sistemas de dedução semelhantes a árvores, em vez de sistemas de dedução passo a passo lineares, e esses sistemas de árvores se mostraram mais úteis na prova automatizada de teoremas, ou seja, na criação de algoritmos para a construção mecânica de deduções (por exemplo, por um computador). No entanto, ao invés de explorar os detalhes desses e outros sistemas rivais, na próxima seção, nos concentramos em provar coisas sobre o sistema PC, o sistema axiomático tratado acima.

7. Importantes resultados meta-teóricos para o cálculo proposicional

Nota: esta seção é relativamente mais técnica e é projetada para públicos com antecedentes anteriores em lógica ou matemática. Os principiantes podem querer passar para a próxima seção.

Nesta seção, esboçamos informalmente as provas dadas para certas características importantes do Cálculo proposicional. Nosso primeiro tópico, no entanto, diz respeito ao idioma PL 'em geral.

Resultado metatoreético 1: linguagem PL 'é expressivamente adequado, ou seja, no contexto da lógica bivalente clássica, não há funções verdadeiras que não podem ser representadas nele.

Observamos na Seção III (c) que os conectivos '&', '↔' e ' v ' podem ser definidos usando os conectivos de PL '(' → 'e' ¬ '). Mais geralmente, o resultado metatoreático 1 afirma que qualquer declaração construída usando conectivos verdade-funcionais, independentemente do que esses conectivos são, tem uma declaração equivalente formada usando apenas '→' e '¬'. Aqui está a prova.

1. Suponha que α seja algum wff construído em algum idioma contendo qualquer conjunto de conectivos verdade-funcionais, incluindo aqueles que não foram encontrados em PL, PL 'ou PL' '. Por exemplo, α pode usar alguns conectivos verdade-funcionais de três ou quatro lugares, ou conectivos como o exclusivo ou o sinal '↓', ou qualquer outro que você possa imaginar.

2. Precisamos mostrar que há um wff β formado apenas com os conectivos '→' e '¬' que é logicamente equivalente com α. Porque já mostramos que formas equivalentes às construídas a partir de '&', '↔', e ' v ' podem ser construídas a partir de '→' e '¬', também podemos usá-las.

3. Para que seja logicamente equivalente a α, o wff β que construímos deve ter o mesmo valor de verdade final para cada possível atribuição de valor de verdade para as letras de instrução que compõem α, ou, em outras palavras, deve ter a mesma coluna final em uma tabela de verdade.

4. Deixe p 1 , p 2 , ..., p n ser as letras de declaração distintas que compõem α. Para algumas possíveis atribuições de valores de verdade para essas letras, α pode ser verdade, e para outros α pode ser falso. O único caso difícil seria aquele em que α é contingente. Se α não fosse contingente, deve ser uma tautologia ou uma auto-contradição. Uma vez que claramente as tautologias e as auto-contradições podem ser construídas em PL ', e todas as tautologias são logicamente equivalentes entre si, e todas as auto-contradições são equivalentes entre si, nesses casos, nosso trabalho é fácil. Suponhamos, em vez disso, que α é contingente.

5. Vamos construir um wff β da seguinte maneira.

(a) Considere, por sua vez, cada atribuição de valor de verdade às letras p 1 , p 2 , ..., p n . Para cada atribuição do valor da verdade, construa uma conjunção composta dessas letras, a atribuição do valor da verdade é verdadeira, juntamente com a negação dessas letras, a atribuição do valor da verdade é falsa. Por exemplo, se as letras envolvidas são 'A', 'B' e 'C', e a atribuição de valor de verdade torna 'A' e 'C' verdade, mas 'B' falso, considere a conjunção '((A & ¬ B) & C) '.

(b) A partir das conjunções resultantes, formam uma disjunção complexa formada a partir das conjunções formadas no passo (a) para as quais a atribuição de valor de verdade correspondente faz α real. Por exemplo, se a atribuição de valor de verdade que faz 'A' e 'C' true, mas 'B' false faz α true, inclua a disjunção. Suponhamos, por exemplo, que essa atribuição de valor de verdade faça α true, assim como essa tarefa em que 'A' e 'B' e 'C' são todos falsos, mas nenhuma outra atribuição de valor de verdade torna a real. Nesse caso, a disjunção resultante seria '((A & ¬B) & C) v ((¬A & ¬B) & ¬C)'.

6. O wff β construído no passo 5 é logicamente equivalente a α. Considere que, para aquelas atribuições de valores de verdade que fazem α true, uma das conjunções que compõem a disjunção β é verdadeira e, portanto, a disjunção total também é verdadeira. Para essas atribuições de valor de verdade fazendo α falso, nenhuma das conjunções que compõem β é verdadeira, porque cada conjunção conterá pelo menos um conjunto que é falso naquela atribuição de valor de verdade.

7. Uma vez que β é construído usando apenas '&', ' v ' e '¬', e estes podem, por sua vez, ser definidos usando apenas '¬' e '→', e porque β é equivalente a α, há um wff construído apenas de '¬' e '→' que é equivalente a α, independentemente dos conectivos que compõem α.

8. Portanto, PL 'é expressamente adequado.

Corolário 1.1: Idioma PL '' também é expressivamente adequado.

O corolégio segue imediatamente do resultado metatoreático 1, juntamente com o fato, observado na Seção III (c) , de que '→' e '¬' podem ser definidos usando apenas '|'.

Resultado metaatéreo 2 (também conhecido como "Teorema da Dedução"): no Cálculo proposicional, PC, sempre que ele afirma que α 1 , ..., α n ⊢ β, também afirma que α 1 , ..., α n -1 ⊢ α n → β

O que isso significa é que quando podemos provar um dado resultado no PC usando um certo número de premissas, então é possível, usando todas as mesmas premissas deixando uma exceção, α n , para comprovar a declaração condicional composta pela premissa removida , α n , como antecedente e a conclusão da derivação original, β, como consequente. A importância deste resultado é que, de fato, mostra que a técnica de prova condicional, tipicamente encontrada na dedução natural (ver Seção V ), é desnecessária no PC, porque sempre que é possível provar o conseqüente de um condicional tomando o antecedente como uma premissa adicional, uma derivação diretamente para o condicional pode ser encontrada sem levar o antecedente como premissa.

Aqui está a prova:

1. Suponha que α 1 , ..., α n ⊢ β. Isso significa que há uma derivação de β no Cálculo Proposicional da premissa α 1 , ..., α n . Esta derivação assume a forma de uma sequência ordenada γ 1 , γ 2 , ..., γ m, onde o último membro da sequência, γ m , é β, e cada membro da sequência é (1) uma premissa, ou seja, é um de α 1 , ..., α n , (2) um axioma de PC, (3) derivado de membros anteriores da sequência por modus ponens .

2. Precisamos mostrar que há uma derivação de α n → β , que, embora possivelmente fazendo uso das outras premissas do argumento, não faz uso de α n . Vamos fazer isso mostrando que, para cada membro, γ i , da sequência da derivação original: γ 1 , γ 2 , ..., γ m , pode derivar α n → γ i sem fazer uso de α n como uma premissa.

3. Cada passo γ i na sequência da derivação original foi obtido de uma das três maneiras, conforme mencionado em (1) acima. Independentemente de qual caso estamos lidando, podemos obter o resultado de que α 1 , ..., α n -1 ⊢ α n → γ i . Há três casos a considerar:

Caso (a): Suponha que γ i seja uma premissa do argumento original. Então γ i é um de α 1 , ..., α n -1ou é α n em si. Na última subcasa, o que desejamos obter é que α n → α n pode ser obtido sem usar α n como premissa. Como α n → α n é uma instância do TS1, podemos obtê-lo sem usar nenhumapremissa. No último caso, note que γ i é uma das premissas que podemos usar na nova derivação. Também podemos apresentar a instância de AS1, γ i→ (α n → γ i ) . A partir destes, podemos obter α n → γ i por modus ponens .

Caso (b): Suponha que γ i seja um axioma. Precisamos mostrar que podemos obter α n → γ i sem usar α n como premissa. Na verdade, podemos obtê-lo sem usar qualquer local. Porque γ i é um axioma, podemos também usá-lo na nova derivação. Como no último caso, temos γ i → (α n → γ i ) como outro axioma (uma instância de AS1). A partir desses dois axiomas, chegamos a α n → γ ipor modus ponens .

Caso (c): Suponha que γ i foi derivado de membros anteriores da sequência por modus ponens . Especificamente, existem alguns γ j e γ k, de modo que tanto j quanto k são inferiores a i , e γ jassume a forma γ k → γ i . Podemos assumir que já conseguimos derivar tanto α n → γ j - ou seja, α n → (γ k → γ i ) - e α n → γ kna nova derivação sem fazer uso de α n . (Isso pode parecer duvidoso no caso de que γ j ou γ k foram recebidos pelo modus ponens . Mas perceba que isso apenas empurra a suposição para trás e, eventualmente, um atingirá o início da derivação original. As duas primeiras etapas de a sequência, a saber, γ 1 e γ 2 , não pode ter sido derivada por modus ponens , uma vez que isso exigiria que tenha havido dois membros anteriores da seqüência, o que é impossível.) Assim, em nossa nova derivação, já temos ambos α n → (γ k → γ i ) e αn → γ k . Observe que[α n → (γ k → γ i )] → [(α n → γ k ) → (α n → γ i )]é uma instância do AS2 e, portanto, pode ser introduzido na nova derivação. Por duas etapas de modus ponens , chegamos aα n → γ i , novamente sem usar α n como premissa.

4. Se continuarmos através de cada passo da derivação original, mostrando para cada passo γ i , podemos obter α n → γ i sem usar α n como premissa, eventualmente, chegamos ao último passo da derivação original, γ m , que é β em si. Aplicando o procedimento do passo (3), obtemos α n → β sem fazer uso de α n como premissa. Portanto, a nova derivação assim formada mostra que α 1 , ..., α n -1 ⊢ α n → β, que é o que estávamos tentando mostrar.

O que é interessante sobre esta prova para o resultado metatoreático 2 é que ele fornece uma receita, dada uma derivação para um determinado resultado que faz uso de uma ou mais premissas, para transformar essa derivação em uma declaração condicional em que uma das premissas da argumento original tornou-se o antecedente. Isso pode ser muito mais claro com um exemplo.

Considere a seguinte derivação para o resultado que: Q → R ⊢ (P → Q) → (P → R):

1. Q → R	Premissa
2. (Q → R) → (P → (Q → R))	AS1
3. P → (Q → R)	1,2 MP
4. [P → (Q → R)] → [(P → Q) → (P → R)]	AS2
5. (P → Q) → (P → R)	3,4 MP

É possível transformar a derivação acima em uma que não usa nenhuma premissa que mostra que (Q → R) → ((P → Q) → (P → R)) é um teorema do PC. O procedimento para tal transformação envolve a análise de cada passo da derivação original, e para cada uma delas, tente derivar a mesma afirmação, apenas começando com "(Q → R) → ...", sem usar "(Q → R) "como premissa. Como isso é feito, depende se o passo é uma premissa, um axioma ou um resultado de modus ponens , e dependendo de qual é, aplicando um dos três procedimentos esboçados na prova acima. O resultado é o seguinte:

1. (Q → R) → (Q → R)	TS1
2. (Q → R) → (P → (Q → R))	AS1
3. [(Q → R) → (→ Q (Q → R)) → → {(Q → R) → [(Q → R) → (P → (Q → R))]}	AS1
4. (Q → R) → [(Q → R) → (P → (Q → R))]	2,3 MP
5. {(Q → R) → [(Q → R) → (P → (Q → R))]} → {[(Q → R) → (Q → R)] → [(Q → R) → (P → (Q → R))]}}	AS2
6. [(Q → R) → (Q → R)] → [(Q → R) → (P → (Q → R)]]]	4,5 MP
7. (Q → R) → (P → (Q → R))	1,6 MP
8. [P → (Q → R)] → [(P → Q) → (P → R)]	AS2
9. {[P → (Q → R)] → [(P → Q) → (P → R)]} → [ (Q → R) → {[P → (Q → R)] → [(P → Q) → (P → R)]} ]	AS1
10. (Q → R) → {[P → (Q → R)] → [(P → Q) → (P → R)]}	8,9 MP
11. [ (Q → R) → {[P → (Q → R)] → [(P → Q) → (P → R)]} ] → {[(Q → R) → (P → (Q → R))] → [(Q → R) → ((P → Q) → (P → R))]}}	AS2
12. [(Q → R) → (→ P (Q → R)) → [(Q → R) → ((P → Q) → (P → R))]	10,11 MP
13. (Q → R) → ((P → Q) → (P → R))	7,12 MP

O procedimento para transformar um tipo de derivação em outro é puramente rote. Além disso, o resultado é muitas vezes não a maneira mais elegante ou fácil de mostrar o que você estava tentando mostrar. Observe, por exemplo, no acima que as linhas (2) e (7) são redudentes, e foram tomadas mais etapas do que o necessário. No entanto, o procedimento de roteamento é efetivo.

Este resultado metatheoretico é devido a Jacques Herbrand (1930).

É interessante por conta própria, especialmente quando se reflete sobre isso como uma substituição ou substituição da técnica de prova condicional. No entanto, também é muito útil para provar outros resultados metatheoréticos, como veremos abaixo.

Resultado metatoreético 3: se α é um wff de linguagem PL ', e as letras de instruções que compõem são p 1 , p 2 , ..., p n , então , se considerarmos qualquer possível atribuição de valor de verdade a essas letras, e considere o conjunto de premissas, Δ, que contém p 1 se a atribuição de valor de verdade torna p 1 verdadeira, mas contém ¬p 1 se a atribuição de valor de verdade torna p 1 falsa, e de forma semelhante para p 2 , ..., p n , se a atribuição de valor de verdade fazαverdade, então no PC, ele sustenta que Δ ⊢ α, e se ele faz α falsa, então Δ ⊢ ¬α.

Aqui está a prova.

1. Pela definição de um wff, α é ele próprio uma letra de declaração, ou, em última instância, é construído a partir de letras de declaração pelo '¬' e '→' do conectivo.

2. Se α é em si uma letra de declaração, então, obviamente, ou a sua negação é um membro de Δ. É um membro de Δ se a atribuição do valor da verdade é verdadeira. Nesse caso, obviamente, há uma derivação de α de Δ, uma vez que uma premissa talvez seja introduzida a qualquer momento. Se a atribuição de valor de verdade o torna falso em vez disso, então ¬α é um membro de Δ, e então temos uma derivação de ¬α de Δ, uma vez que uma premissa pode ser introduzida a qualquer momento. Isso abrange o caso em que nosso wff é simplesmente uma carta de declaração.

3. Suponha que α seja construído a partir de algum outro wff β com o sinal '¬', ou seja, suponha que α seja ¬β . Podemos assumir que já obtivemos o resultado desejado para β. (Ou, em seguida, β é uma letra de declaração, caso em que o resultado é válido pelo passo (2) ou, em última instância, é construído a partir de letras de instruções, portanto, mesmo se verificar essa suposição requer fazer uma suposição similar, em última análise, retornaremos para cartas de declaração .) Ou seja, se a atribuição de valor de verdade torna β verdadeira, então temos uma derivação de β de Δ. Se o torna falso, então temos uma derivação de ßβ de Δ. Suponha que isso torne a β verdadeira. Uma vez que α é a negação de β, a atribuição do valor da verdade deve tornar a falso a. Por isso, precisamos mostrar que há uma derivação de ¬α de Δ. Como α é¬β , ¬α é ¬¬β . Se acrescentarmos a nossa derivação de β de Δ a derivação de β → ¬¬β , uma instância de TS2, podemos alcançar uma derivação de ¬¬β por modus ponens , que é o que era necessário. Se assumirmos, em vez disso, que a atribuição de valor de verdade torna β falso, então, por nossa suposição, existe uma derivação de ß de Δ. Como α é a negação de β, esse assermento de valor de verdade deve tornar α real. Agora, α simplesmente é ¬β , então já temos uma derivação dele de Δ.

4. Suponha, em vez disso, que α seja construído a partir de outros wffs β e γ com o signo '→', ou seja, suponha que α seja β → γ . Novamente, podemos assumir que já obtivemos o resultado desejado para β e γ. (Mais uma vez, eles próprios são cartas de declaração ou construídos de forma semelhante a cartas de declaração.) Suponha que a atribuição de valor de verdade que estamos considerando faz a real. Como α é β → γ , pela semântica para o sinal '→', a atribuição de valor de verdade deve tornar true ou γ true. Pegue a primeira subcasa. Se faz β falso, então, por nossa suposição, existe uma derivação de ¬β de Δ. Se acrescentarmos a isto a derivação da instância de TS3, ¬β → (β → γ) , por modus ponens chegamos à derivação deβ → γ , isto é, α, de Δ. Se, em vez disso, a atribuição de valor de verdade torna γ verdadeira, então, pelo nosso pressuposto, há uma derivação de γ de Δ. Se adicionarmos a esta derivação a instância de AS1, γ → (β → γ) , por modus ponens , chegamos novamente a uma derivação de β → γ , ie, α, de Δ. Se, em vez disso, a atribuição de valor de verdade torna a falso, então, uma vez que α é β → γ , a atribuição de valor de verdade em questão deve tornar β true e γ falso. Por nossa suposição, então é possível provar β e ¬γ de Δ. Se concatenarmos estas duas derivações, e adicione-lhes a derivação da instância de TS4, β → [¬γ → ¬ (β → γ)] , então por duas aplicações de modus ponens, podemos derivar ¬ (β → γ) , que é simplesmente ¬α , que é o que foi desejado.

Do acima, vemos que o Propositional Calculus PC pode ser usado para demonstrar os resultados adequados para um wff complexo, se dado como premissa, seja a verdade ou a falsidade de todas as suas partes simples. Este é, naturalmente, o fundamento da lógica verdade-funcional, de que a verdade ou a falsidade dessas afirmações complexas que se pode fazer nela são determinadas inteiramente pela verdade ou falsidade das declarações simples que entram nela. O resultado metaatéreo 3 é novamente interessante por conta própria, mas desempenha um papel crucial na prova de integridade, que passamos para o próximo.

Resultado metatheoretico 4 (Completude): Se α é um wff de linguagem PL 'e uma tautologia, então α é um teorema do Cálculo proposicional.

Essa característica do Cálculo proposicional é chamada de completude porque mostra que o Cálculo Proposicional, como um sistema dedutivo visando capturar todas as verdades da lógica, é um sucesso. Todo wff verdadeiro unicamente em virtude da natureza funcional da verdade dos conectivos que o compõem é que algo pode provar usando apenas os axiomas do PC, juntamente com o modus ponens . Aqui está a prova:

1. Suponha que α seja uma tautologia. Isso significa que toda atribuição de valor de verdade possível às letras da declaração faz com que seja verdade.

2. Deixe as letras da instrução que compõem α ser p 1 , p 2 , ..., p n , dispostas em alguma ordem (diga alfabeticamente e pelo número de seus índices). Isso decorre de (1) e do resultado metatoreático 3, que existe uma derivação no PC de α usando qualquer conjunto possível de premissas que consiste, para cada letra de declaração, de qualquer uma ou sua negação.

3. Pelo resultado metatoreático 2, podemos remover de cada um desses conjuntos de instalações, ou p n ou ¬p n , dependendo do que contém, e torná-lo um antecedente de um condicional em que α é conseqüente e o resultado será provável sem usar p n ou ¬p n como premissa. Isso significa que, para cada conjunto de premissas que consistam em p 1 ou ¬p 1 e assim por diante, até p n -1 , podemos derivar tanto p n → α e ¬p n → α .

4. O wff (p n → α) → ((¬p n → α) → α) é uma instância do TS5. Portanto, para qualquer conjunto de instalações a partir das quais se pode derivar tanto p n → α e ¬p n → α , por duas aplicações de modus ponens , também pode derivar α.

5. Colocando (3) e (4) juntos, temos o resultado de que α pode ser derivado de todos os conjuntos possíveis de instalações consistindo em p 1 ou ¬p 1 e assim por diante, até p n -1 .

6. Podemos aplicar o mesmo raciocínio dado nas etapas (3) - (5) para remover p n -1 ou sua negação dos conjuntos de premissa pelo teorema de dedução, chegando ao resultado que, para cada conjunto de instalações que consista em p 1 ou ¬p 1 e assim por diante, até p n -2 , é possível derivar α. Se continuar a aplicar esse raciocínio, eventualmente, obteremos o resultado de que podemos derivar α com p 1 ou sua negação como nossa única premissa. Novamente, aplicando o teorema de dedução, isso significa que tanto p 1 → α quanto ¬p 1 → α podem ser comprovados no PC sem usar nenhuminstalações, ou seja, são teoremas. Concatenando as derivações desses teoremas ao longo daquela para a instância de TS5, (p 1 → α) → ((¬p 1 → α) → α) , por duas aplicações de modus ponens , segue-se que α em si é um teorema, que é o que procuramos demonstrar.

A prova acima da integridade do PC do sistema é mais fácil de apreciar quando visualizada. Suponha, apenas por uma questão de ilustração, que a tautologia que desejamos demonstrar no sistema PC tem três letras de indicação, 'P', 'Q' e 'R'. Existem oito possíveis atribuições de valores de verdade para essas letras e, como α é uma tautologia, todas elas são verdadeiras. Podemos esboçar, pelo menos, esta tabela de verdade da aa:

P	Q	R	|	α
T  T  T  T  F  F  F  F	T  T  F  F  T  T  F  F	T  F  T  F  T  F  T  F		T  T  T  T  T  T  T  T

Agora, dada essa característica de α, segue-se do resultado metatoreático 3, que para cada combinação possível de premissas que consiste em "P" ou "¬P" (mas não em ambos), quer 'Q' ou '¬Q' e 'R' ou "¬R", é possível a partir dessas premissas construir uma derivação mostrando α. Isso pode ser visualizado da seguinte maneira:

P, Q, R	⊢ α
P, Q, ¬R	⊢ α
P, ¬Q, R	⊢ α
P, ¬Q, ¬R	⊢ α
¬P, Q, R	⊢ α
¬P, Q, ¬R	⊢ α
¬P, ¬Q, R	⊢ α
¬P, ¬Q, ¬R	⊢ α

Pelo teorema da dedução, podemos retirar a última premissa de cada lista de instalações e torná-lo um antecedente. No entanto, devido à mesma lista restante de instalações, obtemos R → α e ¬R → α , podemos obter α por si só dessas instalações de acordo com TS5. Mais uma vez, para visualizar isso:

P, Q	⊢ R → α	... e então P, Q ⊢ α
P, Q	⊢ ¬ R → α
P, ¬Q	⊢ R → α	... e então P, ¬Q ⊢ α
P, ¬Q	⊢ ¬ R → α
¬P, Q	⊢ R → α	... e assim ¬P, Q ⊢ α
¬P, Q	⊢ ¬ R → α
¬P, ¬Q	⊢ R → α	... e assim ¬P, ¬Q ⊢ α
¬P, ¬Q	⊢ ¬ R → α

Podemos continuar esta linha de raciocínio até que todas as instalações sejam removidas.

P, Q ⊢ α	P ⊢Q → α	e então P ⊢ α	e assim ⊢ P → α	e assim ⊢ α
P, ¬Q ⊢ α	P ⊢ ¬Q → α
¬P, Q ⊢ α	¬P ⊢ Q → α	e então ¬P ⊢ α	e então ⊢ ¬P → α
¬P, ¬Q ⊢ α	¬P ⊢¬Q → α

No final deste processo, vemos que α é um teorema. Apesar de ter apenas três esquemas de axioma e uma única regra de inferência, é possível provar qualquer tautologia no simples Cálculo Proposicional, PC. É completo no sentido necessário.

Este método de provar a completude do Cálculo Proposicional é devido a Kalmár (1935).

Corolário 4.1: se um dado wff β de linguagem PL 'é uma conseqüência lógica de um conjunto de wffs α 1 , α 2 , ..., α n , de acordo com a tabela de verdade combinada, então há uma derivação deβ com α 1 , ..., α n como premissa no Cálculo proposicional.

Sem entrar nos detalhes da prova desse corolário, decorre do fato de que se β é uma conseqüência lógica de α 1 , α 2 , ..., α n , então o wff da forma (α 1 → (α 2 → ... (α n → β) ...)) é uma tautologia. Como uma tautologia, é um teorema do PC e, portanto, se um começa com sua derivação no PC e acrescenta uma série de etapas de modus ponens usando α 1 , α 2 , ..., α n como premissa, pode-se derivar β .

Resultado metatoreático 5 (somidez): se um wff α é um teorema do cálculo proposicional (PC), então α é uma tautologia.

Acima, vimos que todas as tautologias são teoremas do PC. O contrário também é verdadeiro: todos os teoremas do PC são tatuologias. Aqui está a prova:

1. Suponha que a seja um teorema do PC. Isso significa que há uma seqüência ordenada de etapas, cada uma das quais é (1) um axioma de PC, ou (2) derivado de membros anteriores da seqüência por modus ponens e tal que α é o último membro da seqüência .

2. Podemos mostrar que não só é α a tautologia, mas também são todos os membros da sequência que leva a ela. A primeira coisa a notar é que cada axioma de PC é uma tautologia. Para ser um axioma do PC, um wff deve corresponder a um dos esquemas do axioma AS1, AS2 ou AS3. Todos esses aspectos devem ser tautologous; Isso pode ser facilmente verificado através da construção de tabelas de verdade para AS1, AS2 e AS3. (Isto é deixado ao leitor.)

3. A regra do modus ponens preserva a tautologia. Se α é uma tautologia e α → β também é uma tautologia, β também deve ser uma tautologia. Isso ocorre porque se β não fosse uma tautologia, seria falso em algumas atribuições de valor de verdade. No entanto, α, como uma tautologia, é verdade para todas as atribuições do valor da verdade. Uma vez que uma declaração da forma α → β é falsa para qualquer atribuição de valor de verdade, tornando α true e β false, então seria então que alguma atribuição de valor de verdade faz α → β false, o que é impossível se também é uma tautologia.

4. Portanto, vemos que os axiomas com os quais começamos a seqüência, e cada passo derivado deles usando modus ponens , devem ser todas tautologias e, conseqüentemente, o último passo da seqüência, α, também deve ser uma tautologia.

Este resultado é chamado de solidez do Cálculo proposicional; Isso mostra que nela, não se pode demonstrar algo que não é logicamente verdadeiro.

Corolário 5.1: Um wff α de linguagem PL 'é uma tautologia se e somente se α é um teorema do PC do sistema.

Isto segue imediatamente a partir dos resultados metatoreáticos 4 e 5.

Corolário 5.2 (Consistência): Não há wff α de linguagem PL 'tal que tanto α como  ¬α são teoremas do Cálculo Proposicional (PC).

Devido ao resultado metatoreático 5, todos os teoremas do PC são tautologias. Portanto, é impossível para ambos α e ¬α ser teoremas, pois isso exigiria tanto para ser tautologias. Isso significaria que ambos são verdadeiros para todas as atribuições de valores de verdade, mas, obviamente, eles devem ter valores de verdade diferentes para qualquer atribuição de valor de verdade e não podem ser ambos verdadeiros para qualquer, e muito menos para todos, tais tarefas.

Este resultado é chamado de consistência porque garante que nenhum teorema do PC do sistema pode ser inconsistente com qualquer outro teorema.

Corolário 5.3: Se houver uma derivação do wff β com α 1 , α 2 , ..., α n como premissa no Cálculo Proposicional, então β é uma conseqüência lógica do conjunto de wffs α 1 , α 2 ,. .., α n , de acordo com a tabela de verdade combinada.

Este é o inverso do Corollary 4.1. Isso se segue pelo raciocínio inverso envolvido nesse corolário. Se houver uma derivação de β tomando α 1 , ..., α n como premissa, então por múltiplas aplicações do teorema de dedução (resultado metatoreático 2), segue-se que (α 1 → (α 2 → ... ( α n → β) ...)) é um teorema do PC. Pelo resultado metatoreático 5, (α 1 → (α 2 → ... (α n → β) ...)) deve ser uma tautologia. Se assim for, então não pode haver uma atribuição de valor de verdade fazendo tudo de α 1 , ..., α nverdadeiro ao fazer β falso e, portanto, β é uma conseqüência lógica de α 1 , ..., α n .

Corolário 5.4: Existe uma derivação do wff β com α 1 , ..., α n como premissa no Cálculo proposicional se e somente se β é uma conseqüência lógica de α 1 , ..., α n , de acordo com seus tabela de verdade combinada.

Isso segue de uma vez dos corolários 4.1 e 5.3. Em suma, então, o método do Cálculo Proposicional de demonstrar algo a seguir dos axiomas da lógica é extenionally equivalente ao método da tabela de verdade para determinar se algo é ou não uma verdade lógica. Da mesma forma, o método da tabela de verdade para testar a validade de um argumento é equivalente ao teste de poder construir uma derivação para ele no Cálculo proposicional. Em suma, o Cálculo Proposicional é exatamente o que queríamos ser.

Corolário 5.5 (Decidibilidade): O Cálculo proposicional (PC) é decidível, ou seja, existe um procedimento de rote finito e efetivo para determinar se um wff α dado ou não é um teorema do PC ou não.

Por Corollary 5.1, um wff α é um teorema do PC se e somente se for uma tautologia. As tabelas de Verdade fornecem um procedimento rotineiro, efetivo e finito para determinar se um wff dado é ou não uma tautologia. Eles também fornecem esse procedimento para determinar se um wff dado é ou não um teorema do PC.

8. Formas da Lógica Proposicional

Até agora, nos concentramos apenas na lógica proposicional clássica, verdade-funcional. Suas características distintivas são (1) que todos os conectivos que ele usa são verdade-funcionais, ou seja, os valores de verdade de enunciados complexos formados com esses conectivos dependem inteiramente dos valores de verdade das partes e (2) que assume a bivalência: Todas as declarações são tomadas para ter exatamente um dos dois valores da verdade - verdade ou falsidade - sem declaração atribuída tanto valores de verdade como nem. A lógica proposicional verdadeira e funcional clássica é a forma mais amplamente estudada e discutida, mas existem outras formas de lógica proposicional.

Talvez a forma mais conhecida de lógica proposicional não-verdade-funcional seja lógica proposicional modal . A lógica proposicional modal envolve a introdução de operadores na lógica envolvendo necessidade e possibilidade, geralmente junto com operadores verdade-funcionais como '→', '&', '¬', etc. Normalmente, o sinal '☐' é usado no lugar de o operador inglês, "é necessário que ...", e o sinal '◇' é usado no lugar do operador inglês "é possível que ...". Às vezes, ambos esses operadores são tomados como primitivos, mas muitas vezes um é definido em termos de outro, uma vez que ¬☐¬α parece ser logicamente equivalente com ◇ α . (Aproximadamente, significa o mesmo dizer que algo não é necessariamente não verdadeiro, pois diz que é possivelmente verdade.)

Para ver essa lógica proposicional modal não é verdade-funcional, basta considerar o seguinte par de declarações:

☐P 
☐ (P v ¬P)

O primeiro afirma que é necessário que P. Suponhamos, de fato, que "P" é verdadeiro, mas pode ter sido falso. Como P não é necessariamente verdadeiro , a declaração "☐ P" é falsa. No entanto, a afirmação "P v ¬P" é uma tautologia e, portanto, não pode ser falsa. Portanto, a afirmação "☐ (P v¬P)" é verdadeira. Observe que ambos 'P' e "P v ¬P" são verdadeiros, mas diferentes valores de verdade resultam quando o operador '☐' é adicionado. Assim, na lógica proposicional modal, o valor da verdade de uma afirmação não depende inteiramente dos valores da verdade das partes.

O estudo da lógica proposicional modal envolve a identificação em que condições as declarações envolvendo ☐ 'e' ◇ 'dos ​​operadores devem ser consideradas verdadeiras. Diferentes noções ou concepções de necessidade levam a respostas diferentes a essa questão. Também envolve a descoberta de quais regras de inferência ou sistemas de dedução seriam apropriados, dado a adição desses operadores. Aqui, há mais controvérsia do que a lógica clássica verdade-funcional. Por exemplo, no contexto das discussões dos sistemas axiomáticos para a lógica proposicional modal, resultam sistemas muito diferentes, dependendo se as instâncias dos esquemas seguintes são consideradas como verdades axiomáticas, ou mesmo verdades:

☐α → ☐☐α 
◇ α → ☐ ◇ α

Se uma declaração for necessária, é necessário? Se uma afirmação é possível, é necessariamente possível? Uma resposta positiva à primeira questão é uma suposição chave em um sistema lógico conhecido como lógica modal S4. As respostas positivas a ambas as questões são pressupostos fundamentais em um sistema lógico conhecido como lógica modal S5. Outros sistemas de lógica modal que evitam tais pressupostos também foram desenvolvidos. (Para uma excelente pesquisa de introdução, veja Hughes e Cresswell, 1996.)

Lógica proposicional de Deontic e lógica proposicional epistêmicasão duas outras formas de lógica proposicional não-verdade-funcional. O primeiro envolve a introdução de operadores similares aos operadores ingleses "é moralmente obrigatório que ..." e "é moralmente permitido que ...". Obviamente, algumas coisas que de fato são verdadeiras não são moralmente obrigatórias, enquanto que algumas coisas que são verdadeiras eram moralmente obrigatórias. Novamente, o valor de verdade de uma declaração na lógica deontica não depende totalmente do valor da verdade das partes. A lógica epistemológica envolve a adição de operadores similares aos operadores ingleses "é sabido que ..." e "acredita-se que ...". Enquanto tudo o que é conhecido como o caso é de fato o caso, nem tudo o que é o caso é conhecido por ser o caso, então uma declaração construída com um "é sabido que ..."sobre a verdade da proposição que modifica, mesmo que dependa dela até certo ponto.

Outra forma amplamente estudada de lógica proposicional não-verdade-funcional é a lógica proposicional de relevância , que envolve a adição de um operador 'Rel' usado conecte duas instruções α e β para formar uma declaração Rel (α, β) , que é interpretada para significa que α está relacionado a β no tema ou assunto. Por exemplo, se 'P' significa que Ben ama Jennifer e 'Q' significa que Jennifer é uma estrela pop , então a afirmação "Rel (P, Q)" é considerada como verdadeira; enquanto que se "S" significa que o sol está brilhando em Tóquio , então "Rel (P, S)" é falso e, portanto, "¬Rel (P, S)" é verdade. Obviamente, seja ou não uma declaração formada usando o conectivo 'Rel'

Uma das motivações para a introdução de lógicas proposicionais não-verdade-funcionais é compensar certas estranhezas da lógica funcional da verdade. Considere a tabela de verdade para o sinal '→' usado na linguagem PL. Uma afirmação da forma α → β é considerada verdadeira sempre que seu antecedente é falso ou conseqüente é verdadeiro. Então, se traduzíssemos a frase inglesa, "se o autor deste artigo viver na França, então a lua é feita de queijo" como "E → M", então, estranhamente, ela aparece como verdade dada a semântica do signo '→' porque o antecedente, 'E', é falso. Na lógica proposicional modal é possível definir um tipo de operador muito mais forte para usar para traduzir os condicionais ingleses da seguinte maneira:

α β  é definido como  ☐ (α → β)

Se transcrevemos o inglês "se o autor deste artigo viver na França, então a lua é feita de queijo" em vez de "E M", então não é tão verdadeira, porque, presumivelmente, é possível ao autor de Este artigo é viver na França sem que a lua esteja feita de queijo. Da mesma forma, em lógica de relevância, também se pode definir um tipo de conectividade mais forte da seguinte maneira:

α ⇒ β  é definido como  Rel (α, β) & (α → β)

Aqui também, se transcrevêssemos o inglês "se o autor deste artigo viver na França, então a lua é feita de queijo" como "E ⇒ M" em vez de simplesmente "E → M", ele aparece como falso, porque o autor deste artigo que vive na França não está relacionado à composição da lua.

Além da lógica não-verdade-funcional, outros sistemas lógicos diferem da lógica clássica da verdade, ao permitir que as afirmações sejam atribuídas a valores da verdade, além da verdade ou da falsidade, ou de não ser atribuída a verdade, nem a falsidade, nem a verdade e a falsidade. Esses tipos de sistemas lógicos ainda podem ser verdade-funcionais no sentido de que o valor da verdade de uma afirmação complexa pode depender inteiramente dos valores de verdade das partes, mas as regras que governam essa funcionalidade de verdade seriam mais complicadas do que as clássicas lógica, porque deve considerar as possibilidades que a lógica clássica rejeita.

Muitas lógicas multivalentes ou de valor são aquelas que consideram mais de dois valores verdadeiros. Eles podem admitir qualquer coisa de três para um número infinito de possíveis valores de verdade. O tipo mais simples de lógica de muitos valores é aquele que admite três valores de verdade, por exemplo, verdade , falsidade e indeterminação . Pode parecer, por exemplo, que certas declarações, como declarações sobre o futuro, ou declarações paradoxais, como "esta frase não é verdadeira", não podem ser facilmente atribuídos a verdade ou a falsidade , e assim, pode ser concluído, deve ter uma indeterminada valor da verdade. A admissão deste terceiro valor de verdade exige que se expandam as tabelas de verdade dadas emSeção III (a) . Lá, demos uma tabela de verdade para declarações formadas usando o operador '→'; na lógica de três valores, temos que decidir qual é o valor da verdade de uma afirmação da forma α → β quando um ou ambos os α e β têm um valor de verdade indeterminado. Provavelmente, se qualquer componente de uma declaração for indeterminado em valor de verdade, a declaração completa também é indeterminada. Isso levaria à seguinte tabela de verdade expandida:

α	β	(α → β)
T  T  T  I  I  I  F  F  F	T  I  F  T  I  F  T  I  F	T  I  F  I  I  I  TI  T

No entanto, talvez desejemos reter a característica da lógica clássica de que uma afirmação da forma α → β é sempre verdadeira quando seu antecedente é falso ou conseqüente é verdade e mantenha que é indeterminado somente quando seu antecedente é indeterminado e conseqüente falso ou quando seu antecedente é verdadeiro e conseqüente indeterminado, de modo que a sua tabela de verdade aparece:

α	β	(α → β)
T  T  T  I  I  I  F  F  F	T  I  F  T  I  F  T  I  F	T  I  F  T  T  I  T  T  T

Esses detalhes terão um efeito sobre os restos dos sistemas lógicos. Por exemplo, se um sistema de dedução axiomático ou natural for criado, e uma característica desejável é que algo seja provável de nenhuma premissa se e somente se for uma tautologia no sentido de ser verdadeira (e não apenas não falso) para toda a verdade possível - atribuições de valor, se fizermos uso da primeira tabela de verdade para '→', "P → P" não deve ser provável, porque é indeterminado quando 'P' é, enquanto que se usarmos a segunda tabela de verdade, "P → P "deve ser provável, uma vez que é uma tautologia de acordo com essa tabela de verdade, ou seja, é verdade, independentemente de qual dos três valores de verdade é atribuído a 'P'.

Aqui temos apenas um vislumbre das complicações criadas pela admissão de mais de dois valores de verdade. Se mais de três forem admitidos, e possivelmente infinitamente muitos, as questões tornam-se ainda mais complicadas.

A lógica proposicional intuitiva resulta da rejeição da suposição de que cada afirmação é verdadeira ou falsa, e afirma as declarações que não são nem uma . O resultado é uma espécie de lógica muito parecida com uma lógica de três valores, uma vez que "nem verdadeiro nem falso", enquanto estritamente falando, a rejeição de um valor de verdade, pode ser pensado como um terceiro valor de verdade. Na lógica intuicionista, a chamada "lei do meio excluído", ou seja, a lei que todas as afirmações da forma α v ¬α é verdadeira é rejeitada. Isso ocorre porque a lógica intuicionista é verdadeira para coincidir com a provabilidade direta, e pode ser que certas declarações, como a conjectura de Goldbach em matemática, não são, nem sempre, o caso nem o caso provável.

Lógica proposicional paraconsistente é ainda mais radical, em countenancing declarações que são ambos verdadeiro e falso. Mais uma vez, dependendo da natureza do sistema, é necessário dar regras semânticas que determinem o valor da verdade ou dos valores de verdade de uma declaração complexa quando suas partes componentes são verdadeiras e falsas. Tais decisões determinam quais tipos de regras de inferência novas ou restritas se aplicariam ao sistema lógico. Por exemplo, as lógicas paraconsistentes, se não triviais, devem restringir as regras de inferência permitidas na lógica clássica da verdade, porque em sistemas como os esboçados nas Seções V e VIacima, de uma contradição, ou seja, uma declaração da formaα & ¬α , é possível deduzir qualquer outra declaração. Considere, por exemplo, a seguinte dedução no sistema de dedução natural esboçado na Seção V .

1. P & ¬ P	Premissa
2. P	1 Simp
3. ¬P	1 Simp
4. P v Q	2 Adicionar
5. Q	3,4 DS

Para evitar esse resultado, as lógicas paraconsistentes devem restringir a noção de inferência válida. Para que uma inferência seja considerada válida, não só deve ser preservadora da verdade, ou seja, que é impossível chegar a algo falso ao começar com premissas verdadeiras, deve ser evasão de falsidade, isto é, deve ser impossível, começando com premissas verdadeiras, para chegar a algo falso. Na lógica paraconsistente, onde uma afirmação pode ser verdadeira e falsa, esses dois requisitos não coincidem. A regra de inferência do silogismo disjuntivo, enquanto preserva a verdade, não é evasão da falsidade. Nos casos em que suas premissas são verdadeiras, sua conclusão ainda pode ser falsa; mais especificamente, desde que pelo menos uma de suas premissas seja verdadeira e falsa, sua conclusão pode ser falsa.

Outras formas de lógica proposicional não clássica e lógica proposicional não verdade-funcional continuam a ser descobertas. Obviamente, qualquer desvio da lógica proposicional bivalente clássica levanta questões lógicas e filosóficas complicadas que não podem ser totalmente exploradas aqui. Para mais detalhes tanto na lógica não-clássica quanto na lógica não-verdade-funcional, veja a seção de leitura recomendada.

9. Sugestões para leitura adicional

• Anderson, AR e ND Belnap [e JM Dunn]. 1975 e 1992. Entailment. 2 vols. Princeton, NJ: Princeton University Press.
• Bocheński, IM 1961. Uma História da Lógica Formal. Notre Dame, Ind .: University of Notre Dame Press.
• Boole, George. 1847. A Análise Matemática da Lógica. Cambridge: Macmillan.
• Boole, George. 1854. Uma investigação sobre as leis do pensamento. Cambridge: Macmillan.
• Carroll, Lewis. 1958. Lógica simbólica e o jogo da lógica. Londres: Dover.
• Igreja, Alonzo. 1956. Introdução à Lógica Matemática. Princeton, NJ: Princeton University Press.
• Copi, Irving. 1953. Introdução à lógica. Nova Iorque: Macmillan.
• Copi, Irving. 1974. Lógica simbólica. 4ª ed. Nova Iorque: Macmillan.
• da Costa, NCA 1974. "Sobre a Teoria dos Sistemas Formais Inconsistentes", Notre Dame Journal of Formal Logic 25: 497-510.
• De Morgan, Augustus. 1847. Lógica formal. Londres: Walton e Maberly.
• Fitch, FB 1952. Lógica simbólica: uma introdução. Nova York: Ronald Press.
• Frege, Gottlob. 1879. Begriffsschrift, ene der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: L. Nerbert. Publicado em Inglês como Notação conceitual , ed. e trans. por Terrell Bynum. Clarendon: Oxford, 1972.
• Frege, Gottlob. 1923. "Gedankengefüge", Beträge zur Philosophie des deutchen Idealismus 3: 36-51. Publicado em inglês como "Pensamentos compostos", no The Frege Reader , editado por Michael Beaney. Oxford: Blackwell, 1997.
• Gentzen, Gerhard. 1934. "Untersuchungen über das logische Schließen" Mathematische Zeitschrift 39: 176-210, 405-31. Publicado em inglês como "Investigations on Logical Deduction", em Gentzen 1969.
• Gentzen, Gerhard. 1969. Colecionados. Editado por ME Szabo. Amsterdã: Holanda do Norte.
• Haack, Susan. 1996. Lógica desviante, lógica fuzzy. Chicago: University of Chicago Press.
• Herbrand, Jacques. 1930. "Pesquisas sobre a teoria da demonstração", Travaux de Ciência das Ciências e daLetra de Varsovie 33: 133-160.
• Hilbert, David e William Ackermann. 1950. Princípios da Lógica Matemática. Nova Iorque: Chelsea.
• Hintikka, Jaakko. 1962. Conhecimento e crença: uma introdução à lógica das duas noções. Ithaca: Cornell University Press.
• Hughes, GE e MJ Cresswell. 1996. Uma nova introdução à lógica modal. Londres: Routledge.
• Jevons, WS 1880. Estudos em Lógica Dedutiva. Londres: Macmillan.
• Kalmár, L. 1935. "Über die Axiomatisierbarkeit des Aussagenkalküls," Acta Scientiarum Mathematicarum 7: 222-43.
• Kleene, Stephen C. 1952. Introdução à Metamathematics. Princeton, NJ: Van Nostrand.
• Kneale, William e Martha Kneale. 1962. O Desenvolvimento da Lógica. Clarendon: Oxford.
• Lewis, CI e CH Langford. 1932. Lógica simbólica. Nova York: Dover.
• Łukasiewicz, janeiro de 1920. "O logice trojwartosciowej", Ruch Filozoficny 5: 170-171. Publicado em inglês como "On Three-Valued Logic", em Łukasiewicz 1970.
• Łukasiewicz, janeiro de 1970. Obras selecionadas. Amsterdã: Norte da Holanda.
• Łukasiewicz, Jan e Alfred Tarski. 1930. "Untersuchungen über den Aussagenkalkül," Comptes Rendus das sessões da Sociedade das Ciências e da Letra de Varsovie 32: 30-50. Publicado em inglês como "Investigações sobre o Cálculo Sentencial", em Tarski 1956.
• Mally, Ernst. 1926. Grundgesetze des Sollens: Elemente der Logik des Willens. Graz: Leuschner und Lubensky.
• McCune, William, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist e Larry Wos. 2002. "Axiomas Únicos Curtos para Álgebra Booleana", Journal of Automated Reasoning 29: 1-16.
• Mendelson, Elliot. 1997. Introdução à Lógica Matemática. 4ª ed. Londres: Chapman e Hall.
• Meredith, CA 1953. "Axiomas simples para os sistemas (C, N), (C, O) e (A, N) do Cálculo proposicional de dois valores," Journal of Computing Systems 3: 155-62.
• Müller, Eugen, ed. 1909. Abriss der Algebra der Logik, de E. Schröder. Leipzig: Teubner.
• Nicod, Jean. 1917. "Uma redução no número das proposições primitivas da lógica", Procedimentos da Cambridge Philosophical Society 19: 32-41.
• Peirce, CS 1885. "Sobre a álgebra da lógica", American Journal of Mathematics 7: 180-202.
• Post, Emil. 1921. "Introdução a uma Teoria Geral das Proposições", American Journal of Mathematics 43: 163-185.
• Sacerdote, Graham, Richard Routley e Jean Norman, eds. 1990. Lógica Paraconsistente. Munique: Verlag.
• Antes, Arthur. 1990. Lógica formal. 2º. ed. Oxford: Oxford University Press.
• Leia, Stephen, 1988. Lógica relevante. Nova Iorque: Blackwell.
• Rescher, Nicholas. 1966. A lógica dos comandos. Londres: Routledge e Kegan Paul.
• Rescher, Nicholas. 1969. Lógica de muitos valores. Nova Iorque: McGraw Hill.
• Rosser, JB 1953. Lógica para matemáticos. Nova Iorque: McGraw Hill.
• Russell, Bertrand. 1906. "A Teoria da Implicação", American Journal of Mathematics 28: 159-202.
• Schlesinger, GN 1985. A faixa da lógica epistêmica. Aberdeen: Aberdeen University Press.
• Sheffer, HM 1913. "Um conjunto de cinco postulados para álgebras booleanas com aplicação para constantes constantes", Transacções da American Mathematical Society 15: 481-88.
• Smullyan, Raymond. 1961. Teoria dos sistemas formais. Princeton: Princeton University Press.
• Tarski, Alfred. 1956. Lógica, semântica e meta-matemática. Oxford: Oxford University Press.
• Urquhart, Alasdair. 1986. "Lógica muito valorizada", Handbook of Philosophical Logic, vol. 3, editado por D. Gabbay e F. Guenthner. Dordrecht: Reidel.
• Venn, John. 1881. Lógica simbólica. Londres: Macmillan.
• Whitehead, Alfred North e Bertrand Russell. 1910-1913. Principia Mathematica. 3 vols. Cambridge: Cambridge University Press.
• Wittgenstein, Ludwig. 1922. Tractatus Logico-Philosophicus . Londres: Routledge e Kegan Paul.