Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-markov GIF version

Definition df-markov 7039
 Description: A Markov set is one where if a predicate (here represented by a function 𝑓) on that set does not hold (where hold means is equal to 1o) for all elements, then there exists an element where it fails (is equal to ∅). Generalization of definition 2.5 of [Pierik], p. 9. In particular, ω ∈ Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.)
Assertion
Ref Expression
df-markov Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-markov
StepHypRef Expression
1 cmarkov 7038 . 2 class Markov
2 vy . . . . . . 7 setvar 𝑦
32cv 1331 . . . . . 6 class 𝑦
4 c2o 6317 . . . . . 6 class 2o
5 vf . . . . . . 7 setvar 𝑓
65cv 1331 . . . . . 6 class 𝑓
73, 4, 6wf 5129 . . . . 5 wff 𝑓:𝑦⟶2o
8 vx . . . . . . . . . . 11 setvar 𝑥
98cv 1331 . . . . . . . . . 10 class 𝑥
109, 6cfv 5133 . . . . . . . . 9 class (𝑓𝑥)
11 c1o 6316 . . . . . . . . 9 class 1o
1210, 11wceq 1332 . . . . . . . 8 wff (𝑓𝑥) = 1o
1312, 8, 3wral 2417 . . . . . . 7 wff 𝑥𝑦 (𝑓𝑥) = 1o
1413wn 3 . . . . . 6 wff ¬ ∀𝑥𝑦 (𝑓𝑥) = 1o
15 c0 3369 . . . . . . . 8 class
1610, 15wceq 1332 . . . . . . 7 wff (𝑓𝑥) = ∅
1716, 8, 3wrex 2418 . . . . . 6 wff 𝑥𝑦 (𝑓𝑥) = ∅
1814, 17wi 4 . . . . 5 wff (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅)
197, 18wi 4 . . . 4 wff (𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))
2019, 5wal 1330 . . 3 wff 𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))
2120, 2cab 2126 . 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
221, 21wceq 1332 1 wff Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
 Colors of variables: wff set class This definition is referenced by:  ismkv  7040
 Copyright terms: Public domain W3C validator