https://en.wikipedia.org/wiki/Set_builder_notation
https://en.wikipedia.org/wiki/Intuitionistic_logic
https://en.wikipedia.org/wiki/Natural_deduction
https://en.wikipedia.org/wiki/Template:Transformation_rules
A, B, C ... propositions X, Y, a ... term symbols P, Q ... predicate x, y ... term variables
and ¬ => or <=>
A <=> B ≡ A => B and B => A
A or B <=> ¬(¬A and ¬B)
A and B and C <=> ¬(¬A or ¬B or ¬C)
¬A ≡ A => False
∃ ∀
∄x. P(x) ≡ ¬∃x. P(x)
∃x. P(x) P(a) or P(b) or P(c)
∀x. P(x) <=> ¬∃x. ¬P(x) P(a) and P(b) and P(c) <=> ¬(¬P(a) or ¬P(b) or ¬P(c))
∈
x ∉ X ≡ ¬(x ∈ X)
∃(x ∈ X). P(x) ≡ ∃x. (x ∈ X) and P(x) ∀(x ∈ X). P(x) ≡ ∀x. x ∈ X => P(x)
X ⊆ Y ≡ ∀(x ∈ X). x ∈ Y
####### Set builder notation (Informal notation)
a ∈ {x | P(x)} claims P(a)
X = {x | P(x)} claims ∀x. x ∈ X <=> P(x)
{x | P(x)} = {x | Q(x)} claims ∀x. P(x) <=> Q(x)
In all cases we should be careful to use it only when the collection of all x for which P(x) forms a set.
We also use the shorthands
{x ∈ X | P(x)} ≡ {x | x ∈ Y and P(x)}
{f(x) | P(x)} ≡ {y | ∃x. y=f(x) and P(x)}
a ∈ {x | ∃(y ∈ Y). x={y} } claims ∃(y ∈ Y). a={y} S_Y = {x | ∃(y ∈ Y). x={y} } claim ∀x. x ∈ S_Y <=> ∃(y ∈ Y). x={y}
a ∈ {x | x ⊆ y} claims a ⊆ y P_y = {x | x ⊆ y} claims ∀x. x ∈ P_y <=> x ⊆ y
X = {x ∈ {1,2,3,4,5,6,7} | x % 2 == 0}, which may be written as X = {2,4,6} X = {2 * n | n ∈ N and n > 9001}
X = {1, 2, 3} claims ∀(x ∈ X). x=1 or x=2 or x=3 X = {x | x=1 or x=2 or x=3}
{0, 2, 4 ...} ≡ {2 * n | n ∈ N}