TYPES
Unlike Metamath
and like Bourbaki
terms in PRINCIPIA are represented as Sexpressions.
They will be converted to an internal AST, which is defined inductively.
[τ₁ τ₂ ...]
in terms is converted to (@ τ₁ τ₂ ...)
.
SYNTAX
Not only terms, but the whole syntax uses Sexpressions.
variables
(variables α β γ ...)
adds “α”, “β”, “γ” etc
to the variable list.
macroexpand
(macroexpand τ₁ τ₂ τ₃ ...)
performs macro expansion of τ₁, τ₂ etc.
infix
(infix ⊗ prec)
declares “⊗” as an infix operator
with precedence “prec”.
Then it can be used in such way:
(# a ⊗ b ⊗ c ...)
will be converted
to (a ⊗ (b ⊗ (c ...)))
.
Multiple infix operators in one form
will be resolved according to their precedences.
But be careful: by default, trees inside (# ...)
will not be resolved as infix.
So, (# a ⊗ (b ⊗ c ⊗ d))
is not (a ⊗ (b ⊗ (c ⊗ d)))
, but it is
(a ⊗ (b ⊗ c ⊗ d))
. Also note that there is
distinction between (a ⊗ (b ⊗ c))
and (a ⊗ b ⊗ c)
.
bound
(bound (Π x _) (Σ y _) ...)
declares “Π” and “Σ” as bindings.
Generally binding can have another form rather than
(φ x _)
.
It can be, for example, (λ (x : _) _)
.
Bound variables (they appear in declaration) have special meaning.
We cannot do three things with them:

Replace the bound variable with Lit or Symtree.
This prevents us, for example, from deducing
(λ (succ : ℕ) (succ (succ succ)))
(this is obviosly meaningless) from(λ (x : ℕ) (succ (succ x)))
. 
Replace the bound variable with a variable that is present in the term.
This prevents from deducing wrong things like
(∀ b (∃ b (b > b)))
from(∀ a (∃ b (a > b)))
.  Replace (bound or not) variable with a bound variable.
postulate
(1) is premises.
(2) is inference rule name.
(3) is conclusion.
lemma, theorem
(1) is premise names.
(2) is premises self.
(3) is lemma/theorem name.
(4) is conclusion.
(5) is application of theorem/axiom g₁/g₂/gₙ in which
variable α₁/β₁/ε₁ is replaced with term τ₁/ρ₁/μ₁,
variable α₂/β₂/ε₂ is replaced with term τ₂/ρ₂/μ₂,
and so on.