# BERTRAND

### TYPES

Unlike Metamath and like Bourbaki terms in PRINCIPIA are represented as S-expressions.
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 S-expressions.

#### 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.