Talk:Contains everything

This is a fairly straightforward Boolean logic, assuming that we're working over something like ZFC or FinSet. The following Python interprets statements and decides in linear time whether they are True or False. The trick is understanding that universal claims of elementhood will always fail, so that there is no point in tracking what's in each set, merely whether the variable has been universally quantified; since there are no other quantifiers, this is just a scope check. Extending this with support for input variables should be straightforward. Corbin (talk) 22:41, 15 November 2025 (UTC)

constFalse = lambda _: False
# the constructors
univ = lambda x, p: lambda c: p(c + [x])
elt = lambda s, t: constFalse if s == t else lambda c: s not in c and t not in c
implies = lambda p, q: lambda c: (not p(c)) or q(c)
# example programs
false = univ("x", elt("x", "x"))
true = univ("x", implies(elt("x", "x"), elt("x", "x")))
# running programs and printing results
print("false", false([]))
print("true", true([]))

Running the program univ("x",univ("v",implies(elt("v","x"),elt("x","x")))) gives the result True instead of False. the program says that forall x and v, x is not contained in v. which is false, as sometimes x is contained in v. C++DSUCKER (talk)

Ah, I see. So, the issue is that the universal claims are too strong; they include all sets in the domain of discourse. For (∀x.(x∈v)), no matter which set v is, and regardless of whether we're limited to finite sets only, there is no set of all sets. For (∀x.(v∈x)), regardless of which atom v is, x can be the empty set which has no elements.

I see that you've defined an existential quantifier. The clean definition doesn't give an extensional sugar like you've given, because one universal quantifier needs to stay in scope; check out Metamath's definition of existential quantification for an example. Additionally, to forbid the trivial domain, an axiom of existence is necessary. Corbin (talk) 15:49, 16 November 2025 (UTC)

I love metamath!!! In fact this language was the result of trying to simplify it's 'alphabet' removing not and equality. but i think its uncomputable because you can have statements which are only true for infinite sets. like you can have a statement that says: 'x is a ordinal number' and then say set z is the set of all x which is an ordinal number. C++DSUCKER (talk)