How many subsets does the set {7} have?

subsets_of_singleton.py

"""
This is the text and python script discussed in the video

https://youtu.be/EEaRWtZEXwk
"""

"""
=== Symbols ===
Logical symbols
$\land\  \lor\  \forall\  \exists\  \implies\  \bot\ =\  \in$
Term variable symbols
$A\ B$
$x\ y\ z\ f\ r$
Predicate variable symbols
$\phi\ \psi$
Auxiliary symbols
$(\ )\  \{\  \} $

Also write "$\phi(x)$" for emphasis on possible depency.
Also write $\forall(x\in A). \phi$ for $\forall x. (x\in A)\implies \phi$, etc.
Also write $\{x\mid \phi(x)\}$ for class definitions (see set builder notation for formal use of terms)

=== Definitions ===
$\neg\phi$ denotes $\phi\implies \bot$
$\phi\iff\psi$ denotes $(\phi\implies\psi)\land(\psi\implies\phi)$
$\exists! x.\, \phi(x)$ denotes $\exists x.\ \forall y.\ (P(y) \iff x=y)$
$\langle x,y \rangle$ denotes $\{\{x\},\{x,y\}\}$
$B^A$ denotes $\{f\mid \forall (x\in A). \exists! (y\in B). \langle x,y \rangle \in f\}$
$A\simeq B$ denotes $\forall z. (z\in A \iff z\in B)$ or $(A\subset B)\land (B\subset A)$
${\mathcal P}_y$ denotes $\{z\mid z\subset y\}$
where, importantly
$A\subset B$ denotes $\forall (z\in A). (z\in B)$

=== Some set theory Axioms ===
Extensionality:
$\forall x. \forall y.\ \ x\simeq y \implies x = y$
Pairing:
$\forall x. \forall y.\ \ \exists r. \forall z. \big((z = x \lor z = y)\iff z\in r\big)$
Exmptyset
$\exists x. \forall y.\, \neg(y \in x)$
Exponentiation:
$\forall x. \forall y.\ \ \exists h. h=y^x$
and, importantly
Separation:
For all $\phi$, which denote some type (e.g. bounded, or any, etc.) of predicates $\phi$,
$\forall y.\ \ \exists s. \forall z. \Big(z\in s \iff \big(z\in y \land \phi(z)\big)\Big)$
Essentially "$\{z\mid z\in y\land \phi(z)\}$ is a set". And a subset of $y$ at that!

=== Some fact ===
(Will holds in virtually any set theory, also constructive)
$\{\}\subset x$ for all $x$
$x\subset x$ for all $x$
So
$(\{\}\subset\{x\})\land (\{x\}\subset\{x\})$
or
$(\{\}\in{\mathcal P}_{\{x\}})\land (\{x\}\in{\mathcal P}_{\{x\}})$
or
$\{\{\}, \{x\}\}\subset{\mathcal P}_{\{x\}}$

Does
${\mathcal P}_{\{x\}}\subset\{\{\}, \{x\}\}$
?
"""

import random
import time


def no_duplicates(X):
    seen = []
    for x in X:
        assert x not in seen
        seen.append(x)

def is_subset(X, S):
    """
    S ... subset candidate
    return S ⊆ X
    """
    no_duplicates(X)
    no_duplicates(S)
    result = all(x in X for x in S)
    print(f"{S} ⊆ {X} is {result}.")
    return result

is_subset([2,3,5], [2,3])
is_subset([2,3,5], [2,3,5])
is_subset([2,3,5], [2,7])
is_subset([2,3,5], [999,5,1])
is_subset([2,3,5], [])
print()
exit()

def propT(x):
    # Constant true predicate, i.e. this is the true proposition, works over any theory
    return x == x

def propF(x):
    # Constant false predicate, i.e. this is the false proposition, works over any theory
    return not propT(x)

def propF_(x):
    # Constant false predicate (assuming we have axioms for such arithemtic)
    return (1 + 2) * 3 == 10

def predE(x):
    # Even
    return x % 2 == 0

def pred5(x):
    # Smaller than 5
    return x < 5

def predD(x):
    # Smaller than 5 and larger than 26
    return pred5(x) or x > 26


def separate(X, pred, dont_print=None):
    no_duplicates(X)
    subset = [x for x in X if pred(x)]
    if not dont_print:
        print(f"The set {subset} was seperated from {X}.")
    return subset


set_of_numbers = [2, 3, 4, 6, 7, 9, 18, 19, 56]
separate(set_of_numbers, propT)
separate(set_of_numbers, predE)
separate(set_of_numbers, propF)
separate(set_of_numbers, pred5)
separate(set_of_numbers, predD)
print()
exit()

some_set_that_exists = set_of_numbers
F = separate(some_set_that_exists, propF, "don't print") # definition of empty set []

def successor_set(x):
    return x + [x] # x union {x}
T = successor_set(F) # singleton, {} union {{}} corresponds to [[]]

print("Seperate from T=[F]=[[]] via the predicate 'propF': ", end="")
separate(T, propF)
print("Seperate from T=[F]=[[]] via the predicate 'propT': ", end="")
separate(T, propT)
# We see that [] and [[]] are subsets of [[]]
# I.e. see that F and T are elements of PT, i.e. PT=[F, T, ...]
print()
exit()

def validate_seperation(set_of_numbers, pred):
    print("validate_seperationing subset relation. Seperating subset...")
    subset = separate(set_of_numbers, pred)
    is_valid = is_subset(set_of_numbers, subset)
    print("Seperation property confirmed.\n" if is_valid else "Is set theory inconsistent???\n")

validate_seperation(set_of_numbers, predD)
validate_seperation(set_of_numbers, propF)
print()
exit()

def predU(x):
    while True:
        pass

def predR(x): # analogy of predicate that could potentially never return true or false
    SLEEP_TIME = 0.01 # seconds
    CHANCE = 1000 # one in CHANCE
    while True:
        time.sleep(SLEEP_TIME)

        n = random.randint(0, CHANCE)

        if n==3:
            print(n, "return True")
            #return True
        elif n==7:
            print(n, "return False")
            #return False
        else:
            print(".", end="", flush=True)

validate_seperation(T, propF)
validate_seperation(T, propT)
#validate_seperation(T, predU) # Separate won't terminate for the predicate predU
validate_seperation(T, predR) # Separate won't terminate for the predicate predR
print()

# What are all the subsets of T, i.e. the elements of PT?
#
# If it merely either the sets F or T, then all possible propositions
# have the same truth values as either propF or propT.
# In other words, if just PT=[F,T], then LEM.