Contains everything

This is a set theory based language, Initially designed by C++DSUCKER (talk) but with the logical operator removed with help of uni on discord (though these changes did not make it into the final language). the original used nand but i eventually went with implies as false is constructible.

It was designed to be as simple as possible.

Instructions

Instruction	Description
(∀x.P)	is predicate P is True for all sets x
(a∈b)	does b contain a
(A→B)	A implies B

Examples

False

(∀x.(x∈x))

Syntatic sugar: ⊥

True

(∀x.((x∈x)→(x∈x)))

Syntatic sugar: ⊤

Invert predicate P

(P→(∀x.(x∈x)))

Syntatic sugar: ¬P

And of predicates P and Q

((P→(Q→(∀x.(x∈x))))→(∀x.(x∈x)))

Syntatic sugar: P∧Q

Or of predicates P and Q

((Q→(∀x.(x∈x)))→P)

Syntatic sugar: P∨Q

Biconditional of P and Q

((((P→Q)→(∀v.(v∈v)))→(Q→P))→(∀v.(v∈v)))

Syntatic sugar: P↔Q

is x the empty set?

(∀v.((v∈x)→(∀t.(t∈t))))

golfed: (∀v.((v∈x)→(v∈v)))

are x and y equal?

(∀v.(((((v∈x)→(v∈y))→(v∈v))→((v∈y)→(v∈x)))→(v∈v)))

Syntatic sugar: x=y

r is the union of a and b

(∀y.(((((((y∈b)→(∀x.(x∈x)))→(y∈a))→(y∈r))→(∀v.(v∈v)))→((y∈r)→(((y∈b)→(∀x.(x∈x)))→(y∈a))))→(∀v.(v∈v))))

Exists x such that P is true

((∀x.(P→(x∈x)))→(∀v.(v∈v)))

Syntatic sugar: ∃x.P

Is x a transitive set?

(∀a.(∀b.((a∈x)→((b∈a)→(b∈x)))))

Is x a von nuemann ordinal?

(((∀a.(∀b.((a∈x)→((b∈a)→(b∈x)))))→((∀y.((y∈x)→(∀a.(∀b.((a∈y)→((b∈a)→(b∈y))))))→(∀x.(x∈x)))))→(∀x.(x∈x)))

is y the succesor of x?

(∀z.((z∈y)↔((z∈x)∨(z=x))))

is x a subset of y

(∀z.((z∈x)→(z∈y)))

is x the powerset of y

(∀w.((((w∈x)→(∀z.((z∈w)→(z∈y))))→(∀z.(z∈z)))→((∀z.((z∈w)→(z∈y)))→(w∈x)))→(∀z.(z∈z)))

Is z the set of all ordinal numbers?

(∀w.(((((∀a.(∀b.((a∈w)→((b∈a)→(b∈w)))))→((∀y.((y∈w)→(∀a.(∀b.((a∈y)→((b∈a)→
(b∈y))))))→(∀x(x∈x)))))→(w∈z))→(((w∈z)→((∀a.(∀b.((a∈w)→((b∈a)→(b∈w)))))→
((∀y.((y∈w)→(∀a.(∀b.((a∈y)→((b∈a)→(b∈y))))))→(∀x.(x∈x))))))→(∀x.(x∈x))))→(∀x.(x∈x))))

Turns (¬P)↔(¬Q) into P↔Q

Is z the set of a and b

(∀w.((w∈z)↔((w=a)∨(w=b))))

is p the ordered pair from x and y

work in progress!

syntatic sugar

Define syntax definitions as this:

_name args :: code

They may not be recursive, as this often leads to paradoxes.

Example:

_false :: ∀v.(v∈v)
_not P :: (P→_false)
_true :: (_not _false)
_paradox :: (_not _paradox)

Diagrams

Based of Tromp diagrams.

Foralls bind a variable so are a horizontal line.

contains look like applications with the contained set coming out, and so are implications with the implied poking out but the contains are always first, because you cant imply a set and contains a proposition.

For example: all sets are the empty set.

-+-------
-|-+-+-+-
 | | | |
 |-+ |-+
 |   |
 |---+
 |

Rayos number equivalent.

Define size as the amount of foralls and implies.

Then the Number is the amount of sets z for which the predicate is true. infinities are discounted

Size	Number	Program
1	0	(z∈z)
2	0	∀a.(a∈a)
3	0	∀a.∀b.(a∈b)
4	1	∀a.((a∈z)→(z∈z))