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
(@ τ₁ τ₂ ...).
Not only terms, but the whole syntax uses S-expressions.
(variables α β γ ...) adds “α”, “β”, “γ” etc
to the variable list.
(macroexpand τ₁ τ₂ τ₃ ...) performs macro expansion of τ₁, τ₂ etc.
(infix ⊗ prec) declares “⊗” as an infix operator
with precedence “prec”.
Then it can be used in such way:
(# a ⊗ b ⊗ c ...) will be converted
(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.
(# a ⊗ (b ⊗ c ⊗ d))
(a ⊗ (b ⊗ (c ⊗ d))), but it is
(a ⊗ (b ⊗ c ⊗ d)). Also note that there is
(a ⊗ (b ⊗ c)) and
(a ⊗ b ⊗ c).
(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.
(1) is premises.
(2) is inference rule name.
(3) is conclusion.
(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.