Bucanon Syntax

www.bucephalus.org September 6, 2002

The syntax of formulas

in LaTeX notation in Bucanon notation

formula

theory formula τ

atom α non-empty string of letters (A,…,Z,a,…,z), non-empty string of letters (A,…,Z,a,…,z),

digits (0,1,…,9), and the understroke ( ) digits (0,1,...,9), and the understroke ( )

boolean junction

bit value

zero bit  ?  ?
unit bit  !  !
negation  ¬τ  'τ

                                                                               -τ

conjunction  [ ∧] or [ ∧τ ] or [ τ_{1} ∧ ⋯ ∧ τ_{n} ] with n ≥ 2  [,] or [,τ] or [τ_{1},…,τ_{n}] with n ≥ 2
[*] or [*τ] or [τ_{1}*… *τ_{n}] with n ≥ 2

disjunction [ ∨] or [ ∨τ ] or [ τ_{1} ∨ ⋯ ∨ τ_{n} ] with n ≥ 2 [;] or [;τ] or [τ_{1};…;τ_{n}] with n ≥ 2

[+] or [+τ] or [τ_{1}+… +τ_{n}] with n ≥ 2
subjunction  [ τ_{1} → τ_{2} ]  [τ_{1} -> τ_{2}]
equijunction  [ τ_{1} ↔ τ_{2} ]  [τ_{1} <-> τ_{2}]

boolean relation

subvalence  [ τ_{1} ⇒ τ_{2} ]  [τ_{1} => τ_{2}]
equivalence  [ τ_{1} ⇔ τ_{2} ]  [τ_{1} <=> τ_{2}]

expansion or reduction

expansion  [ τ ∥ λ] or [ τ ∥ α_{1} α_{2} … α_{n} ] with n ≥ 0  [τ || λ] or [τ || α_{1} α_{2} … α_{n}] with n ≥ 0
infimum reduction  [ τ ⇑ λ] or [ τ ⇑ α_{1} α_{2} … α_{n} ] with n ≥ 0  [τ <| λ] or [τ <| α_{1} α_{2} … α_{n}] with n ≥ 0
supremum reduction  [ τ ⇓ λ] or [ τ ⇓ α_{1} α_{2} … α_{n} ] with n ≥ 0  [τ |> λ] or [τ |> α_{1} α_{2} … α_{n}] with n ≥ 0
standard reduction  @|τ  @|τ

atom list formula λ

atom list  [ α_{1} α_{2} … α_{n} ] with n ≥ 0  [α_{1} α_{2} … α_{n}] with n ≥ 0
atom list function  @τ  @τ
negative atom list function  −@τ  -@τ
positive atom list function  +@τ  +@τ

The syntax of boolean formulas (a subset of theory formulas)

in LaTeX notation in Bucanon notation

boolean formula φ

atom α non-empty string of letters (A,…,Z,a,…,z), non-empty string of letters (A,…,Z,a,…,z),

digits (0,1,…,9), and the understroke ( ) digits (0,1,...,9), and the understroke ( )

boolean junction

bit value

zero bit  ?  ?
unit bit  !  !
negation  ¬φ  'φ

                                                                           -φ

conjunction  [ ∧] or [ ∧φ] or [ φ_{1} ∧ ⋯ ∧ φ_{n} ] with n ≥ 2  [,] or [,φ] or [φ_{1},…,φ_{n}] with n ≥ 2
[*] or [*φ] or [φ_{1}*… *φ_{n}] with n ≥ 2

disjunction [ ∨] or [ ∨φ] or [ φ_{1} ∨ ⋯ ∨ φ_{n} ] with n ≥ 2 [;] or [;φ] or [φ_{1};…;φ_{n}] with n ≥ 2

[+] or [+φ] or [φ_{1}+… +φ_{n}] with n ≥ 2

subjunction  [ φ_{1} → φ_{2} ]  [φ_{1} -> φ_{2}]
equijunction  [ φ_{1} ↔ φ_{2} ]  [φ_{1} <-> φ_{2}]