Hyper–digital logic Summarized overview of its syntax and semantics

www.bucephalus.org

June 21, 2007

List of Figures

1 Bit values and their algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

2 Bit tables and their algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

3 Hyper–propositional logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

Figure 1: Bit values and their algebra

\underline{Bit values}

𝔹 := \{0, 1\} is the \underline{bit value} class, where 0 is the \underline{zero bit} and 1 the \underline{unit bit}. Bit value algebra

𝔅 := ⟨𝔹, ≤, 0, 1, ∧, ∨, ⋀, ⋁, -⟩ is the \underline{bit value algebra}, where

β_{1} ≤ β_{2} iff β_{1} = 0 or β_{2} = 1  β_{1} ∧ β_{2} := ⋀ \{β_{1}, β_{2}\}  ⋀ B := \begin{cases}0 & if 0 ∈ B \\ 1 & else \end{cases} β_{1} ∨ β_{2} := ⋁ \{β_{1}, β_{2}\}  ⋁ B := \begin{cases}1 & if 1 ∈ B \\ 0 & else \end{cases}  -β := \begin{cases}0 & if β = 1 \\ 1 & else \end{cases}

for all β, β_{1}, β_{2} ∈ 𝔹 and B ⊆ 𝔹. We also write, for all β_{1}, …, β_{n} ∈ 𝔹 with n ≥ 0,

∧^{n}_{i=1}β_{i} for ⋀ {β_{1}, …, β_{n}}  and  ∨^{n}_{i=1}β_{i} for ⋁ {β_{1}, …, β_{n}}

\underline{Theorem} 𝔅 is a complete boolean algebra.

Figure 2: Bit tables and their algebras

\underline{Bit tables} For every set A and each natural number k we define

𝔹_{A}^{k} := \begin{cases}A & if k = 0 \\ 𝔹_{A}^{k−1} ⟶ 𝔹 & if k > 0 \end{cases}

the \underline{bit table} set of \underline{carrier} A and \underline{degree} k. In our default notation for functions^{a}, each bit table Ω ∈ 𝔹_{A}^{k} with k ≥ 1 is then given by

Ω = [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ Ω(ω) \end{matrix} ]

Similar to geometry, bit tables of small degree k = 0, 1, 2, 3 are also called bit points, bit lines, bit squares and bit cubes, respectively. In traditional propositional logic, bit squares are also known as truth tables.

Bit table diagrams

If both A and k are finite, we can represent each Ω ∈ 𝔹_{A}^{k} by its \underline{bit table diagram}. For example

(1) If A = {a, b} and k = 1 then  (2) If A = {a, b} and k = 2 then  (3) If A = {a} and k = 3 then

\begin{matrix}a & b & c \\ β1 & β2 & β3 \end{matrix} := [ \begin{matrix}& A ⟶ 𝔹 \\ [ & \begin{matrix}a ↦ & β_{1} \\ b ↦ & β_{2} \\ c ↦ & β_{3} \end{matrix} & ] \end{matrix} ]  \begin{matrix}a & b \\ 0 & 0 & β1 \\ 1 & 0 & β2 \\ 0 & 1 & β3 \\ 1 & 1 & β4 \end{matrix} := [ \begin{matrix}& 𝔹_{A}^{1} ⟶ 𝔹 \\ [ & \begin{matrix}\begin{matrix}a & b \\ 0 & 0 \end{matrix} ↦ & β_{1} \\ \begin{matrix}a & b \\ 1 & 0 \end{matrix} ↦ & β_{2} \\ \begin{matrix}a & b \\ 0 & 1 \end{matrix} ↦ & β_{3} \\ \begin{matrix}a & b \\ 1 & 1 \end{matrix} ↦ & β_{4} \end{matrix} & ] \end{matrix} ]  \begin{aligned}a \\ 0 & 0 & 1 & 0 & 1 \\ 1 & 0 & 0 & 1 & 1 \\ & β1 & β2 & β3 & β4 \end{aligned} := [ \begin{matrix}& 𝔹_{A}^{2} ⟶ 𝔹 \\ [ & \begin{matrix}\begin{matrix}a \\ 0 & 0 \\ 1 & 0 \end{matrix} ↦ & β_{1} \\ \begin{matrix}a \\ 0 & 1 \\ 1 & 0 \end{matrix} ↦ & β_{2} \\ \begin{matrix}a \\ 0 & 0 \\ 1 & 1 \end{matrix} ↦ & β_{3} \\ \begin{matrix}a \\ 0 & 1 \\ 1 & 1 \end{matrix} ↦ & β_{4} \end{matrix} & ] \end{matrix} ]

Bit table algebras

𝔅_{A}^{k} := ⟨𝔹_{A}^{k}, ⊑_{A}^{k}, ⊥_{A}^{k}, ⊤_{A}^{k}, ⊓_{A}^{k}, ⊔_{A}^{k}, ∏_{A}^{k}, ∐_{A}^{k}, ¬_{A}^{k}⟩ is the \underline{bit table algebra}, for each set A and k ≥ 1, where

Ω ⊑_{A}^{k} Ω′ iff Ω(ω) ≤ Ω′(ω) for all ω ∈ 𝔹_{A}^{k−1}

Ω ⊓_{A}^{k} Ω′ := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ Ω(ω) ∧ Ω′(ω) \end{matrix} ]  Ω ⊔_{A}^{k} Ω′ := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ Ω(ω) ∨ Ω′(ω) \end{matrix} ]  ¬_{A}^{k}Ω := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ -Ω(ω) \end{matrix} ]

⊥_{A}^{k} := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ 0 \end{matrix} ] ⊤_{A}^{k} := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ 1 \end{matrix} ] ∏_{A}^{k}Γ := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ ⋀\{Ω(ω) | Ω ∈ Γ\} \end{matrix} ] ∐_{A}^{k}Γ := [ \begin{matrix}𝔹_{A}^{k−1} ⟶ 𝔹 \\ ω ↦ ⋁\{Ω(ω) | Ω ∈ Γ\} \end{matrix} ]

for all Ω, Ω′ ∈ 𝔹_{A}^{k} and Γ ⊆ 𝔹_{A}^{k}. Using bit table diagrams and taking A = {a, b} and k = 2 for example, the operations are

\begin{matrix}a & b \\ 0 & 0 & β1 \\ 1 & 0 & β2 \\ 0 & 1 & β3 \\ 1 & 1 & β4 \end{matrix} ⊑_{A}^{2} \begin{matrix}a & b \\ 0 & 0 & γ1 \\ 1 & 0 & γ2 \\ 0 & 1 & γ3 \\ 1 & 1 & γ4 \end{matrix} iff (\begin{matrix}β_{1} ≤ δ_{1} and \\ β_{2} ≤ δ_{2} and \\ β_{3} ≤ δ_{3} and \\ β_{4} ≤ δ_{4} \end{matrix} )  ⊥_{A}^{2} = \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix}  ⊤_{A}^{2} = \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}

¬_{A}^{2} \begin{matrix}a & b \\ 0 & 0 & β1 \\ 1 & 0 & β2 \\ 0 & 1 & β3 \\ 1 & 1 & β4 \end{matrix} = \begin{matrix}a & b \\ 0 & 0 & -β1 \\ 1 & 0 & -β2 \\ 0 & 1 & -β3 \\ 1 & 1 & -β4 \end{matrix}  \begin{matrix}a & b \\ 0 & 0 & β1 \\ 1 & 0 & β2 \\ 0 & 1 & β3 \\ 1 & 1 & β4 \end{matrix} ⊓_{A}^{2} \begin{matrix}a & b \\ 0 & 0 & γ1 \\ 1 & 0 & γ2 \\ 0 & 1 & γ3 \\ 1 & 1 & γ4 \end{matrix} = \begin{matrix}a & b \\ 0 & 0 & β1 ∧ γ1 \\ 1 & 0 & β2 ∧ γ2 \\ 0 & 1 & β3 ∧ γ3 \\ 1 & 1 & β4 ∧ γ4 \end{matrix}  \begin{matrix}a & b \\ 0 & 0 & β1 \\ 1 & 0 & β2 \\ 0 & 1 & β3 \\ 1 & 1 & β4 \end{matrix} ⊔_{A}^{2} \begin{matrix}a & b \\ 0 & 0 & γ1 \\ 1 & 0 & γ2 \\ 0 & 1 & γ3 \\ 1 & 1 & γ4 \end{matrix} = \begin{matrix}a & b \\ 0 & 0 & β1 ∨ γ1 \\ 1 & 0 & β2 ∨ γ2 \\ 0 & 1 & β3 ∨ γ3 \\ 1 & 1 & β4 ∨ γ4 \end{matrix}

These methods hold similarly for other A and k. \underline{Theorem}

𝔅_{A}^{k} is a complete boolean algebra, for every set A and k ≥ 1.

a In our notation we write f = [ \begin{matrix}X ⟶ Y \\ x ↦ f(x) \end{matrix} ] for a function f : X ⟶ Y that maps each x ∈ X to a well–defined f(x) ∈ Y.

Figure 3: Hyper–propositional logic

\underline{Formulas} For every set A and k ∈ ℕ we define 𝔽_{A}^{k} the \underline{(hyper–propositional) formulas} of \underline{carrier} A and \underline{degree} k recursively as follows

(i) If k = 0 then 𝔽_{A}^{0} := A. (ii) If k > 0 then 𝔽_{A}^{k} comprises the following expressions:

\begin{matrix}♢_{k}σ & (\underline{diamond}) \\ □_{k}σ & (\underline{box}) \end{matrix} \} for all σ ∈ 𝔽_{A}^{k−1} \begin{matrix}¬_{k}φ & (\underline{negation}) \\ [ φ_{1} ∧_{k} … ∧_{k} φ_{n} ] & (\underline{conjunction}) \\ [ φ_{1} ∨_{k} … ∨_{k} φ_{n} ] & (\underline{disjunction}) \end{matrix} \} for all φ, φ_{1}, …, φ_{n} ∈ 𝔽_{A}^{k}

We write [ ∧_{k}] and [ ∨_{k}] for nullary, and [ ∧_{k} φ_{1} ] and [ ∨_{k} φ_{1} ] for unary conjunctions and disjunctions, respectively. Super–models and model classes

For every class A and every natural number k ∈ ℕ we define the \underline{(super–) model function}

mod_{A}^{k+1} : 𝔽_{A}^{k} ⟶ 𝔹_{A}^{k} ⟶ 𝔹

where mod_{A}^{k+1}(φ)(Ω) is defined, for each φ ∈ 𝔽_{A}^{k} and Ω ∈ 𝔹_{A}^{k}, by induction on k as follows:

(i) If k = 0 then φ ∈ 𝔽_{A}^{0} = A and Ω ∈ 𝔹_{A}^{0} = A and

mod_{A}^{1}(φ)(Ω) := \begin{cases}1 & if φ = Ω \\ 0 & else \end{cases}

(ii) If k > 0, we define by structural induction on the form of φ as follows:

mod_{A}^{k+1} (♢_{k}σ) (Ω) := ⋁{mod_{A}^{k}(σ)(ω) | ω ∈ 𝔹_{A}^{k−1}, Ω(ω) = 1}
mod_{A}^{k+1} (□_{k}σ) (Ω) := ⋀{mod_{A}^{k}(σ)(ω) | ω ∈ 𝔹_{A}^{k−1}, Ω(ω) = 1}
mod_{A}^{k+1} (¬_{k}φ) (Ω) := -mod_{A}^{k+1}(φ)(Ω)
mod_{A}^{k+1} ([ φ_{1} ∧_{k} … ∧_{k} φ_{n} ]) (Ω) := ⋀ {mod_{A}^{k+1}(φ_{1})(Ω), …, mod_{A}^{k+1}(φ_{n})(Ω)}
mod_{A}^{k+1} ([ φ_{1} ∨_{k} … ∨_{k} φ_{n} ]) (Ω) := ⋁ {mod_{A}^{k+1}(φ_{1})(Ω), …, mod_{A}^{k+1}(φ_{n})(Ω)}

Furthermore: (α) mod_{A}^{k+1}(φ)(Ω) ∈ 𝔹 is the so–called \underline{truth value} of φ and (the \underline{interpretation}) Ω (β) If mod_{A}^{k+1}(φ)(Ω) = 1 we say that “Ω is a \underline{model} for φ” or “Ω \underline{satisfies} φ”, and this is also expressed by writing Ω ⊧ φ . (γ) Accordingly and for each given φ ∈ 𝔽_{A}^{k}, its \underline{model class} is a subset of 𝔹_{A}^{k}, defined by

Mod_{A}^{k}(φ) := {Ω ∈ 𝔹_{A}^{k} | mod_{A}^{k+1}(φ)(Ω) = 1}

(δ) Note, that for each k ∈ ℕ, mod_{A}^{k+1} : 𝔽_{A}^{k} ⟶ 𝔹_{A}^{k+1}, because 𝔹_{A}^{k+1} = (𝔹_{A}^{k} ⟶ 𝔹) (hence the superscript “k + 1” in “mod_{A}^{k+1}”). We

call mod_{A}^{k+1}(φ) ∈ 𝔹_{A}^{k+1} the \underline{super–model} or \underline{truth table} of φ ∈ 𝔽_{A}^{k}. Subvalence and equivalence

Given A and k, we define two relations on 𝔽_{A}^{k}. For all φ, ψ ∈ 𝔽_{A}^{k} let

φ ⇒_{A}^{k} ψ iff ∀Ω ∈ 𝔹_{A}^{k} . (Ω ⊧ φ implies Ω ⊧ ψ)
iff Mod_{A}^{k}(φ) ⊆ Mod_{A}^{k}(ψ)
iff mod_{A}^{k+1}(φ) ⊑_{A}^{k+1} mod_{A}^{k+1}(ψ)

φ ⇔_{A}^{k} ψ iff ∀Ω ∈ 𝔹_{A}^{k} . (Ω ⊧ φ iff Ω ⊧ ψ)
iff Mod_{A}^{k}(φ) = Mod_{A}^{k}(ψ)
iff mod_{A}^{k+1}(φ) = mod_{A}^{k+1}(ψ)

If φ ⇒_{A}^{k} ψ then we say that “φ is \underline{subvalent} to ψ” or “φ \underline{implies} ψ” or “φ \underline{entails} ψ” or “ψ is a \underline{consequence} of φ”. And φ ⇔_{A}^{k} ψ is read as “φ and ψ are \underline{equivalent}”.

The quasi–boolean lattice of formulas

𝔉_{A}^{k} := ⟨𝔽_{A}^{k}, ⇒_{A}^{k}, ⇔_{A}^{k}, f^{k}, t^{k}, ∧^{k}, ∨^{k}, ¬^{k}⟩ is the \underline{default formula algebra} of A and k, where for all φ, ψ ∈ 𝔽_{A}^{k}

f^{k} := [ ∨_{k}] t^{k} := [ ∧_{k}] φ ∧^{k} ψ := [ φ ∧_{k} ψ] φ ∨^{k} ψ := [ φ ∨_{k} ψ] ¬^{k}φ := ¬_{k}φ

\underline{Theorem}

𝔉_{A}^{k} is a quasi–boolean algebra, for every A and k ≥ 1. \underline{Theorem}

mod_{A}^{k+1} : 𝔉_{A}^{k} ↪ 𝔅_{A}^{k+1}, i.e. mod_{A}^{k+1} : 𝔽_{A}^{k} ⟶ 𝔹_{A}^{k+1} is an embedding of 𝔉_{A}^{k} into 𝔅_{A}^{k+1}, for all A and k ≥ 1.