• Dato un insieme di oggetti P, che chiamo lettere proposizionali, chiamo enunciati proposizionali gli elementi di P e gli oggetti ottenuti a partire da questi mediante l'applicazione di connettivi (se A e B sono enunciati, anche ¬(A), (A) → (B) sono enunciati, leggibili come "non A" e "A implica B"). Nella pratica matematica non si ha a che fare con "enunciati proposizionali" ma con "formule". Vedi qui.
• Possono essere definiti a partire da questi connettivi altri connettivi. Il numero di parentesi può essere ridotto usando apposite convenzioni (se un enunciato A è una lettera proposizionale invece di ¬(A) si può scrivere ¬A, ecc.).

Assiomi del CALCOLO PROPOSIZIONALE

Se φ, φ e χ sono enunciati proposizionali qualunque, i seguenti sono assiomi del calcolo proposizionale:

φ → (ψ → φ)
¬ φ → (φ → ψ)
(φ → ψ) → ((¬ φ → ψ) → ψ)
(φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))

Come già detto, oltre a ¬ e → si possono usare altri connettivi, come ∨ ("or", o "vel" in latino) e & ("and"), ponendo φ ∨ ψ come abbreviazione di ¬φ → ψ e φ ∧ ψ come abbreviazione di ¬(¬φ ∨ ¬ψ).

Regola, o regola di inferenza:

 φ, φ → ψ   (del taglio, o "modus ponens")
 ————————
    ψ

Teoremi

Un enunciato A si dice che è un teorema del calcolo proposizionale se esiste una sequenza finita di enunciati A₁, A₂,..., A_n (chiamata prova, derivazione o dimostrazione) tali che, per ogni i tra 1 ed n, A_i è un assioma del calcolo proposizionale o deriva da qualche enunciato tra A₁, A₂,..., A_i-1 mediante l'applicazione della regola di inferenza (m.p.).
L'insieme delle conseguenze di I viene chiamata teoria (del 1º ordine), ogni formula di I viene chiamata suo assioma proprio (o specifico) ed ogni sua conseguenza viene chiamata teorema di I.

Tutti i teoremi del calcolo proposizionale sono verificabili (e il loro significato è meglio comprensibile) utilizzando le tavole di verità (vedi qui). O, meglio, chiamata tautologia ogni enunciato che sia sempre vero, indipendentemente dai valori di verità delle sue lettere enunciative, si ha che un enunciato è un teorema del calcolo proposizionale se e solo se è una tautologia.

Esempi di teoremi, dove A e B sono enuciati qualunque:
A → A     (¬A → ¬B) → (B → A)     A → (B → (A & B))

Vediamo, ad esempio, una dimostrazione del primo:

[1] (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) dal 4º assioma
[2] A → ((A → A) → A)                               dal 1º assioma
[3] (A → (A → A)) → (A → A)                         da [1],[2] per m.p.
[4] A → (A → A)                                     dal 1º assioma
[5] A → A                                           da [3],[4] per m.p.

Vediamo, ad esempio, che il secondo è una tautologia (indicando con 0 il falso e con 1 il vero):

A  B    ¬A    ¬B    ¬A → ¬B    B → A     (¬A → ¬B) → (B → A)
————————————————————————————————————————————————————————————
1  1     0    0        1         1                 1
1  0     0    1        1         1                 1
0  1     1    0        0         0                 1
0  0     1    1        1         1                 1

Schema di assiomi: gli "assiomi proposizionali" non sono dei singoli assiomi ma degli insiemi infiniti di assiomi che variano al variare delle formule (φ, ψ, χ) che compaiono in essi; per questo sono più propriamente chiamati "schemi di assiomi".