principio di sostituzione proposizionale:

• ⊨ φ(P)   ⇔   ⊨ φ(ψ)

principio di congruenza proposizionale:

• ⊨ ψ ↔ χ   ⇔   ⊨ φ(ψ) ↔ φ(χ)

siano:

• φ* : la formula ottenuta da φ per scambio di ∧ con ∨ e viceversa
• φ(¬) : la formula ottenuta da φ rimpiazzando gli atomi con i negati

principio di dualità proposizionale:

• ⊨ φ*   ⇔   ⊨ ¬φ(¬)

teorema di deduzione proposizionale:

• φ ⊨ ψ   ⇔   ⊨ φ → ψ

def.: equivalenza proposizionale: φ ≡ ψ se le due formule hanno
ugual valore di verità per ogni valutazione booleana delle variabili

principio di equivalenza proposizionale: φ ≡ ψ   ⇔   ⊨ φ ↔ ψ

qualsiasi sistema di assiomi completo per le algebre di Boole fornisce un calcolo deduttivo completo per la logica proposizionale

• infatti, gli assiomi Booleani bastano a trasformare ogni formula in una equivalente DNF, che determina la tavola di verità della formula

dagli assiomi di Boole si deriva φ = ψ sse ⊨ φ ↔ ψ, e φ = 1 sse ⊨ φ

• possiamo costruire un'algebra Booleana delle formule proposizionali, dove si identifichino formule equivalenti? (semantica algebrica)

l'algebra di Lindenbaum-Tarski è una tal costruzione; fissato un insieme V di variabili proposizionali:

• dominio: il quoziente dell'insieme delle formule proposizionali con variabili in V per la relazione di equivalenza proposizionale
• operazioni booleane sulle classi di equivalenza: definite per il tramite dei connettivi proposizionali su rappresentanti delle classi

si veda in proposito l'esercizio 3

una proprietà fondamentale della logica predicativa, che qui consideriamo per il suo frammento proposizionale, è la compattezza:

• un insieme numerabile di formule proposizionali è soddisfacibile sse lo è ogni suo sottoinsieme finito

una direzione della doppia implicazione è ovvia... l'altra no: asserisce che dall'esistenza di modelli (magari diversi) delle parti finite di un insieme Ψ di formule consegue l'esistenza di un modello di tutte le formule di Ψ (infinito): perché crederci?

• per il lemma di König : ogni albero finitario infinito ha qualche ramo infinito

questo serve nell'ipotesi che l'insieme V delle variabili proposizionali di Ψ sia infinito (numerabile); in caso contrario basta molto meno (v. esercizio 4)

se V non è finito, siano V₁, ... V_n, ... e ψ₁, ... ψ_n, ... risp. denumerazioni di V e Ψ; costruiamo un albero binario ordinato dove:

• cammini distinti dalla radice a vertici di livello n rappresentano valutazioni booleane distinte delle variabili V₁, ... V_n, tali da soddisfare ψ₁, ... ψ_n

il ramo infinito che, per il lemma di König, tale albero deve avere, dà una valutazione booleana di V che soddisfa Ψ

1. Algebra Booleana e logica proposizionale
   La costruzione dell'algebra di Lindenbaum-Tarski suggerisce l'esistenza di una stretta connessione fra logica proposizionale e algebra Booleana. Un profondo risultato in proposito è dato dal teorema di rappresentazione di Stone, che stabilisce che ogni algebra Booleana è isomorfa ad un'algebra Booleana di insiemi. Approfondimenti su questi ed altri argomenti nell'ambito del tema sono reperibili attraverso la pagina Progetto:Matematica/Elenco di voci sull'algebra booleana della Wikipedia italiana, dove però molte voci sono in attesa di stesura. Un elenco più completo è disponibile nella Wikipedia inglese: List of Boolean algebra topics.
2. Logica proposizionale intuizionista
   Alcune delle voci elencate alle pagine suddette riguardano estensioni e generalizzazioni della logica proposizionale. La logica intuizionista, proposta agli inizi del XX secolo da L. Brouwer, generalizza quella classica abbandonando il principio del terzo escluso, e costituisce un sistema deduttivo per la matematica costruttiva. Le algebre di Heyting sono il fondamento algebrico della logica proposizionale intuizionista, analogamente al ruolo delle algebre Booleane rispetto alla logica proposizionale classica.