PRINCIPIA

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 as

Name = <Unicode character (except “(”, “)”, “[”, “]”, “"”, “'”) sequence> Term = Lit Name | Var Name | Hole | Symtree (Term list)

SYNTAX

Not only terms, but the whole syntax uses S-expressions.

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.

(postulate h₁ h₂ h₃ ... ;; (1) ──────────── axiom-1 ;; (2) h ;; (3) g₁ g₂ g₃ ... ──────────── axiom-2 g ...)

lemma, theorem

(1) is premise names.
(2) is premises self.
(3) is lemma/theorem name.
(4) is conclusion.

(theorem ─── f₁ ─── f₂ ─── f₃ ;; (1) h₁ h₂ h₃ ... ;; (2) ──────────────────────── theorem-1 ;; (3) h ;; (4) ...)