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

Definition df-markov 7078
 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 ) 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-markov
StepHypRef Expression
1 cmarkov 7077 . 2 Markov
2 vy . . . . . . 7
32cv 1334 . . . . . 6
4 c2o 6351 . . . . . 6
5 vf . . . . . . 7
65cv 1334 . . . . . 6
73, 4, 6wf 5163 . . . . 5
8 vx . . . . . . . . . . 11
98cv 1334 . . . . . . . . . 10
109, 6cfv 5167 . . . . . . . . 9
11 c1o 6350 . . . . . . . . 9
1210, 11wceq 1335 . . . . . . . 8
1312, 8, 3wral 2435 . . . . . . 7
1413wn 3 . . . . . 6
15 c0 3394 . . . . . . . 8
1610, 15wceq 1335 . . . . . . 7
1716, 8, 3wrex 2436 . . . . . 6
1814, 17wi 4 . . . . 5
197, 18wi 4 . . . 4
2019, 5wal 1333 . . 3
2120, 2cab 2143 . 2
221, 21wceq 1335 1 Markov
 Colors of variables: wff set class This definition is referenced by:  ismkv  7079
 Copyright terms: Public domain W3C validator