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

Definition df-womni 7090
 Description: A weakly omniscient set is one where we can decide whether a predicate (here represented by a function ) holds (is equal to ) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9. In particular, WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)
Assertion
Ref Expression
df-womni WOmni DECID
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-womni
StepHypRef Expression
1 cwomni 7089 . 2 WOmni
2 vy . . . . . . 7
32cv 1334 . . . . . 6
4 c2o 6351 . . . . . 6
5 vf . . . . . . 7
65cv 1334 . . . . . 6
73, 4, 6wf 5163 . . . . 5
8 vx . . . . . . . . . 10
98cv 1334 . . . . . . . . 9
109, 6cfv 5167 . . . . . . . 8
11 c1o 6350 . . . . . . . 8
1210, 11wceq 1335 . . . . . . 7
1312, 8, 3wral 2435 . . . . . 6
1413wdc 820 . . . . 5 DECID
157, 14wi 4 . . . 4 DECID
1615, 5wal 1333 . . 3 DECID
1716, 2cab 2143 . 2 DECID
181, 17wceq 1335 1 WOmni DECID
 Colors of variables: wff set class This definition is referenced by:  iswomni  7091
 Copyright terms: Public domain W3C validator