![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > bj-stdc | GIF version |
Description: Decidability of a proposition is stable if and only if that proposition is decidable. In particular, the assumption that every formula is stable implies that every formula is decidable, hence classical logic. (Contributed by BJ, 9-Oct-2019.) |
Ref | Expression |
---|---|
bj-stdc | ⊢ (STAB DECID 𝜑 ↔ DECID 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nndc 852 | . 2 ⊢ ¬ ¬ DECID 𝜑 | |
2 | bj-nnbist 14736 | . 2 ⊢ (¬ ¬ DECID 𝜑 → (STAB DECID 𝜑 ↔ DECID 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (STAB DECID 𝜑 ↔ DECID 𝜑) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ↔ wb 105 STAB wstab 831 DECID wdc 835 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 |
This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |