Universe — Language – Dave, Approximately.

Language

Universe is an attempt to construct a mathematical description of reality from the smallest possible foundations.

We begin with a formal language: a collection of symbols and rules from which more complicated mathematical statements can be constructed. At this stage, the symbols have no assumed mathematical interpretation.

Primitive symbols

$\in,\quad \forall,\quad \downarrow$

Formation rules

${\in}ab$

${\forall}aP$

${\downarrow}PQ$

Notational conventions

Infix notation

$a \in b \mathrel{:=} {\in}ab$

$\forall a: P \mathrel{:=} {\forall}aP$

$P \downarrow Q \mathrel{:=} {\downarrow}PQ$

Logical connectives

$\neg P \mathrel{:=} P \downarrow P$

$P \wedge Q \mathrel{:=} \neg P \downarrow \neg Q$

$P \vee Q \mathrel{:=} \neg (P \downarrow Q)$

$P \Rightarrow Q \mathrel{:=} \neg P \vee Q$

Quantifier notation

$\forall a \in b: P \mathrel{:=} \forall a: (a \in b \Rightarrow P)$

$\forall a, b \in c: P \mathrel{:=} \forall a \in c: \forall b \in c: P$

$\forall a \in b; c \in d: P \mathrel{:=} \forall a \in b: \forall c \in d: P$

Metasyntactic conventions. Variables, formulas, grouping, substitution, and related syntactic operations are understood in their conventional mathematical sense. Their explicit formalisation is deferred.

These definitions establish the syntax and notational conventions used throughout Universe. They do not yet establish which statements are true; that requires axioms and rules of inference.

Source: Universe at commit fe2669962b8a.

Universe — Language