Skip to content

Instantly share code, notes, and snippets.

Show Gist options
  • Save Nikolaj-K/630d6389131fd0779212ec40ce8d1359 to your computer and use it in GitHub Desktop.
Save Nikolaj-K/630d6389131fd0779212ec40ce8d1359 to your computer and use it in GitHub Desktop.
We discuss how the informal set builder notation, and various expressions where it's used, translates to logical sentences.

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

Language

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))

Logical theories of sets

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)}

Examples

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}

More ad hoc notations

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}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment