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

Definition df-womni 7048
 Description: A weakly omniscient set is one where we can decide whether a predicate (here represented by a function 𝑓) holds (is equal to 1o) 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 = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2oDECID𝑥𝑦 (𝑓𝑥) = 1o)}
Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-womni
StepHypRef Expression
1 cwomni 7047 . 2 class WOmni
2 vy . . . . . . 7 setvar 𝑦
32cv 1331 . . . . . 6 class 𝑦
4 c2o 6316 . . . . . 6 class 2o
5 vf . . . . . . 7 setvar 𝑓
65cv 1331 . . . . . 6 class 𝑓
73, 4, 6wf 5128 . . . . 5 wff 𝑓:𝑦⟶2o
8 vx . . . . . . . . . 10 setvar 𝑥
98cv 1331 . . . . . . . . 9 class 𝑥
109, 6cfv 5132 . . . . . . . 8 class (𝑓𝑥)
11 c1o 6315 . . . . . . . 8 class 1o
1210, 11wceq 1332 . . . . . . 7 wff (𝑓𝑥) = 1o
1312, 8, 3wral 2417 . . . . . 6 wff 𝑥𝑦 (𝑓𝑥) = 1o
1413wdc 820 . . . . 5 wff DECID𝑥𝑦 (𝑓𝑥) = 1o
157, 14wi 4 . . . 4 wff (𝑓:𝑦⟶2oDECID𝑥𝑦 (𝑓𝑥) = 1o)
1615, 5wal 1330 . . 3 wff 𝑓(𝑓:𝑦⟶2oDECID𝑥𝑦 (𝑓𝑥) = 1o)
1716, 2cab 2126 . 2 class {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2oDECID𝑥𝑦 (𝑓𝑥) = 1o)}
181, 17wceq 1332 1 wff WOmni = {𝑦 ∣ ∀𝑓(𝑓:𝑦⟶2oDECID𝑥𝑦 (𝑓𝑥) = 1o)}
 Colors of variables: wff set class This definition is referenced by:  iswomni  7049
 Copyright terms: Public domain W3C validator