A Grammar of Finite Cardinals

Definition. A Grammar of Finite Cardinals

Define a grammar for each finite cardinal $𝑛 : ℕ$ .

[0] ≔ ⊥

[𝗌𝗎𝖼 (𝑛)] ≔ ⊤ \oplus [𝑛]

Then define the grammar of all finite cardinals as

𝖥𝗂𝗇 ≔ ⨁_{𝑛 : ℕ} [𝑛]