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 as
SYNTAX
Not only terms, but the whole syntax uses Sexpressions.
variables
(variables α β γ ...)
adds “α”, “β”, “γ” etc
to the variable list.
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 two 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 another bound variable.
This prevents from deducing wrong things like
(∀ b (∃ b (b > b)))
from(∀ a (∃ b (a > b)))
.
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.