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

Definition df-markov 7152
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 7151 . 2 class Markov
2 vy . . . . . . 7 setvar 𝑦
32cv 1352 . . . . . 6 class 𝑦
4 c2o 6413 . . . . . 6 class 2o
5 vf . . . . . . 7 setvar 𝑓
65cv 1352 . . . . . 6 class 𝑓
73, 4, 6wf 5214 . . . . 5 wff 𝑓:𝑦⟶2o
8 vx . . . . . . . . . . 11 setvar 𝑥
98cv 1352 . . . . . . . . . 10 class 𝑥
109, 6cfv 5218 . . . . . . . . 9 class (𝑓𝑥)
11 c1o 6412 . . . . . . . . 9 class 1o
1210, 11wceq 1353 . . . . . . . 8 wff (𝑓𝑥) = 1o
1312, 8, 3wral 2455 . . . . . . 7 wff 𝑥𝑦 (𝑓𝑥) = 1o
1413wn 3 . . . . . 6 wff ¬ ∀𝑥𝑦 (𝑓𝑥) = 1o
15 c0 3424 . . . . . . . 8 class
1610, 15wceq 1353 . . . . . . 7 wff (𝑓𝑥) = ∅
1716, 8, 3wrex 2456 . . . . . 6 wff 𝑥𝑦 (𝑓𝑥) = ∅
1814, 17wi 4 . . . . 5 wff (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅)
197, 18wi 4 . . . 4 wff (𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))
2019, 5wal 1351 . . 3 wff 𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))
2120, 2cab 2163 . 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
221, 21wceq 1353 1 wff Markov = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2o → (¬ ∀𝑥𝑦 (𝑓𝑥) = 1o → ∃𝑥𝑦 (𝑓𝑥) = ∅))}
Colors of variables: wff set class
This definition is referenced by:  ismkv  7153
  Copyright terms: Public domain W3C validator