Créditos: La siguiente lista de tautologías está tomada de Apuntes de lógica proposicional clásica (manuscrito) de José M. Méndez, y se reproduce aquí con permiso de su autor.
| T | Notación estándar | Notación polaca |
|---|---|---|
| T1 | A → (B → A) | CpCqp |
| T2 | [A → (B → C)] → [(A → B) → (A → C)] | CCpCqrCCpqCpr |
| T3 | A → A | Cpp |
| T4 | (B → C) → [(A → B) → (A → C)] | CCqrCCpqCpr |
| T5 | [(A → B) → C] → (B → C) | CCCpqrCqr |
| T6 | [(A → B) → (A → C)] → [B → (A → C)] | CCCpqCprCqCpr |
| T7 | [A → (B → C)] → [B → (A → C)] | CCpCqrCqCpr |
| T8 | (A → B) → {[A → (B → C)] → (A → C)} | CCpqCCpCqrCpr |
| T9 | (A → B) → [(B → C) → (A → C)] | CCpqCCqrCpr |
| T10 | [(A → B) → (A → C)] → [A → (B → C)] | CCCpqCprCpCqr |
| T11 | A → [(A → B) → B] | CpCqCpq |
| T12 | [(A → A) → B] → B | CCCppqq |
| T13 | [A → (A → B)] → (A → B) | CCpCpqCpq |
| T14 | (¬ A → ¬ B) → (B → A) | CCNpNqCqp |
| T15a | ¬ A → (A → B) | CNpCpr |
| T15b | A → (¬ A → B) | CpCNpr |
| T16 | ¬¬ A → A | CNNpp |
| T17 | A → ¬¬ A | CpNNp |
| T18 | (¬ A → B) → (¬ B → A) | CCNpqCNqp |
| T19 | (A → B) → (¬ B → ¬ A) | CCpqCNqNp |
| T20 | (A → ¬ B) → (B → ¬ A) | CCpNqCqNp |
| T21 | (¬ A → A) → A | CCNppp |
| T22 | (A → ¬ A) → ¬ A | CCpNpNp |
| T23a | (A → B) → [(A → ¬ B) → ¬ A] | CCpqCCpNqNp |
| T23b | (A → ¬ B) → [(A → B) → ¬ A] | CCpNqCCpqNp |
| T24a | (A → B) → [(¬ A → B) → B] | CCpqCCNpqq |
| T24b | (¬ A → B) → [(A → B) → B] | CCNpqCCpqq |
| T25a | (¬ A → ¬ B) → [(¬ A → B) → A] | CCNpNqCCNpqp |
| T25b | (¬ A → B) → [(¬ A → ¬ B) → A] | CCNpqCCNpNqp |
| T26 | A → (A ∨ B) | CpApq |
| T27 | B → (A ∨ B) | CqApq |
| T28a | (A ∨ B) → [(B → C) → [(A → C) → C]] | CApqCCqrCCprr |
| T28b | (A → C) → [(B → C) → [(A v B) → C]] | CCprCCqrCApqr |
| T29 | (A ∧ B) → A | CKpqp |
| T30 | (A ∧ B) → B | CKpqq |
| T31 | A → [B → (A ∧ B)] | CpCqKpq |
| T32 | (A → B) → [(A → C) → [A → (B ∧ C)]] | CCpqCCprCpKqr |
| T33 | (A ↔ B) → (A → B) | CEpqCpq |
| T34 | (A ↔ B) → (B → A) | CEpqCqp |
| T35 | (A → B) → [(B → A) → (A ↔ B)] | CCpqCCqpEpq |
| T36 | A ↔ A | Epp |
| T37 | (A ↔ B) → (B ↔ A) | CEpqEqp |
| T38 | (A ↔ B) → [(B ↔ C) → (A ↔ C)] | CEpqCEqrEpr |
| T39 | [A → (B → C)] ↔ [(A → B) → (A → C)] | ECpCqrCCpqCpr |
| T40 | [A → (B → C)] ↔ [B → (A → C)] | ECpCqrCqCpr |
| T41 | [A → (A → B)] ↔ (A → B) | ECpCpqCpq |
| T42 | ¬¬ A ↔ A | ENNpp |
| T43 | (¬ A → B) ↔ (¬ B → A) | ECNpqCNqp |
| T44 | (A → B) ↔ (¬ B → ¬ A) | ECpqCNqNp |
| T45 | (A → ¬ B) ↔ (B → ¬ A) | ECpNqCqNp |
| T46 | (¬ A → A) ↔ A | ECNppp |
| T47 | (A → ¬ A) ↔ ¬ A | ECpNpNp |
| T48 | (A ↔ B) ↔ (¬ A ↔ ¬ B) | EEpqENpNq |
| T49 | (¬ A ↔ B) ↔ (A ↔ ¬ B) | EENpqEpNq |
| T50 | [A → (B → C)] ↔ [(A ∧ B) → C] | ECpCqrCKpqr |
| T51 | (A → B) → [(A ∧ C) → (B ∧ C)] | CCpqCKprKqr |
| T52 | (A → B) → [(A v C) → (B v C)] | CCpqCAprAqr |
| T53 | [A → (B ∧ C)] ↔ [(A → B) ∧ (A → C)] | ECpKqrKCpqCpr |
| T54 | [(A v B) → C] ↔ [(A → C) ∧ (B → C)] | ECApqrKCprCqr |
| T55 | [A → (B v C)] ↔ [(A → B) v (A → C)] | ECpAqrACpqCpr |
| T56 | [(A ∧ B) → C] ↔ [(A → C) v (B → C)] | ECKpqrACprCqr |
| T57 | (A v B) ↔ (B v A) | EApqAqp |
| T58 | (A ∧ B) ↔ (B ∧ A) | EKpqKqp |
| T59 | [A v (B v C)] ↔ [(A v B) v C] | EApAqrAApqr |
| T60 | [A ∧ (B ∧ C)] ↔ [(A ∧ B) ∧ C] | EKpKqrKKpqr |
| T61 | A ↔ (A v A) | EpApp |
| T62 | A ↔ (A ∧ A) | EpKpp |
| T63 | A ↔ [A v (A ∧ B)] | EpApKpq |
| T64 | A ↔ [A ∧ (A v B)] | EpKpApq |
| T65 | [A ∧ (B v C)] ↔ [(A ∧ B) v (A ∧ C)] | EKpAqrAKpqKpr |
| T66 | [A v (B ∧ C)] ↔ [(A v B) ∧ (A v C)] | EApKqrKApqApr |
| T67 | ¬ (A v B) ↔ (¬ A ∧ ¬ B) | ENApqKNpNq |
| T68 | ¬ (A ∧ B) ↔ (¬ A v ¬ B) | ENKpqANpNq |
| T69 | (A v B) ↔ ¬ (¬ A ∧ ¬ B) | EApqNKNpNq |
| T70 | (A ∧ B) ↔ ¬ (¬ A v ¬ B) | EKpqNANpNq |
| T71 | (A ∧ B) ↔ ¬ (A → ¬ B) | EKpqNCpNq |
| T72 | (A v B) ↔ (¬ A → B) | EApqCNpq |
| T73 | (A → B) ↔ ¬ (A ∧ ¬ B) | ECpqNKpNq |
| T74 | (A → B) ↔ (¬ A v B) | ECpqANpq |
| T75 | A v ¬ A | ApNp |
| T76 | ¬ (A ∧ ¬ A) | NKpNp |
| T77 | (A → B) v (B → A) | ACpqCqp |
| T78 | [(A → B) → A] → A | CCCpqpp |
| T79 | [A → (B ∧ ¬ B)] → ¬ A | CCpKqNqNp |
| T80 | [¬ A → (B ∧ ¬ B)] → A | CCNpKqNqp |