Cálculo Proposicional

O Cálculo Proposicional Clássico (CPC) consiste num sistema simbólico de Lógica Clássica. E como todos os sistemas de lógica clássica, segue os seguintes princípios:
Bivalência: Cada fórmula recebe apenas um de dois valores distintos e absolutos, verdadeiro ou falso.
Não-contradição: Dadas uma fórmula e sua negação, uma delas é falsa.
Terceiro Excluído: Dadas uma fórmula e sua negação, uma delas é verdadeira.
Identidade: Se uma fórmula é verdadeira, então esta fórmula é verdadeira.
O CPC se distingue de outros sistemas de Lógica Clássica por lidar apenas com:

Letras sentenciais: No CPC, letras do alfabeto romano maiúsculas são usadas para representar as proposições.
Este sistema foi desenvolvido para propósitos matemáticos, tendo, portanto, limitações no que se refere à análise de raciocínios. Ainda assim, podemos aplicá-lo à filosofia, às ciências e ao conhecimento ordinário, desde que sempre estejamos cientes de suas limitações.

Por ser um sistema de lógica simbólica, devemos ter várias considerações tanto para formalizar proposições da linguagem natural, quanto para interpretar suas fórmulas na linguagem natural.

Proposições
Proposições são estruturas lingüísticas passíveis de serem julgadas verdadeiras ou falsas, tais como “Todos homens são mortais”, “Sócrates é homem”, “A água sob uma atmosfera ferve a 100°C”, “Siegfrid matou Fafnir”, “2 + 2 = 4” etc. Não são proposições as estruturas lingüísticas interrogativas (ex: “Quem é você?”) ou imperativas (ex: “Faça isto”), pois elas não são passíveis de serem julgadas verdadeiras ou falsas.

Termos, Operadores, Conectivos e Valorações
No CPC, fórmulas atômicas representam proposições de uma linguagem . Para escrevê-las, são usadas letras do alfabeto latino maiúsculas (A, B, C, D, E etc.).

Operadores são usados para criar novas fórmulas a partir de fórmulas mais simples, constituindo assim fórmulas moleculares (ou fórmulas não atômicas). Os 5 operadores mais usuais são: a negação (¬), a conjunção (∧), a disjunção (∨), a implicação (→) e a bi-implicação (↔). Parênteses são usadas para delimitar fórmulas evitando assim ambiguidades e facilitando a leitura. Um exemplo de fórmula não atômica é: ¬ ((A ∧ B) ∨ (C ↔ A)). Os conectivos são aqueles operadores que relacionam duas fórmulas.

Fonte: Wikilivros