You are here
DNp theorem list
Copyright: the following theorem list is an excerpt from Notes on Propositional Classical Logic (manuscript) by José M. Méndez, and it is reproduced here with permission.
| T | Standard notation | Polish notation |
|---|---|---|
| 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 |
