Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-peircestab | Structured version Visualization version GIF version |
Description: Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any formula (that is the interpretation when ⊥ is substituted for 𝜓 and for 𝜒). Therefore, the double negation of the stability of any formula is provable in classical refutability calculus. It is also provable in intuitionistic calculus (see iset.mm/bj-nnst) but it is not provable in minimal calculus (see bj-stabpeirce 34372). (Contributed by BJ, 30-Nov-2023.) Axiom ax-3 8 is only used through Peirce's law peirce 205. (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-peircestab | ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnclav 34364 | . . 3 ⊢ ((((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑 → 𝜓) → 𝜒) → 𝜑)) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒)) | |
2 | ax-1 6 | . . . . . . 7 ⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒)) | |
3 | 2 | imim2i 16 | . . . . . 6 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((((𝜑 → 𝜓) → 𝜒) → 𝜑) → ((𝜑 → 𝜓) → 𝜒))) |
4 | peirce 205 | . . . . . 6 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒)) | |
5 | 3, 4 | syl 17 | . . . . 5 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜑 → 𝜓) → 𝜒)) |
6 | imim2 58 | . . . . 5 ⊢ ((𝜒 → 𝜑) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜑))) | |
7 | peirce 205 | . . . . 5 ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑) | |
8 | 5, 6, 7 | syl56 36 | . . . 4 ⊢ ((𝜒 → 𝜑) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜑)) |
9 | 8 | a1dd 50 | . . 3 ⊢ ((𝜒 → 𝜑) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑 → 𝜓) → 𝜒) → 𝜑))) |
10 | 1, 9 | syl11 33 | . 2 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜒 → 𝜑) → 𝜒)) |
11 | peirce 205 | . 2 ⊢ (((𝜒 → 𝜑) → 𝜒) → 𝜒) | |
12 | 10, 11 | syl 17 | 1 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |