From propositional to hyper–propositional logic

www.bucephalus.org

July 3, 2007

[figure: 𝔹_{A}^{0}; ↭; ⊧_{A}^{0}; 𝔽_{A}^{0}; 𝔹_{A}^{1}; ↭; ⊧_{A}^{1}; 𝔽_{A}^{1}; 𝔹_{A}^{2}; ↭; ⊧_{A}^{2}; 𝔽_{A}^{2}; 𝔹_{A}^{3}; ↭; ⊧_{A}^{3}; 𝔽_{A}^{3}; ⋮; ⋮; mod_{A}^{1}; mod_{A}^{2}; mod_{A}^{3}; mod_{A}^{4}]

Abstract

“Hyper–propositional logic” is our title for a generalization of traditional propositional logic that introduces formulas of arbitrary degree k, such that traditional propositional formulas turn into hyper–propositional formulas of first degree.

Primitive formulas of degree k + 1 are “♢σ” and “□σ”, where σ is a formula of degree k. More complex formulas are constructed by means of conjunctions, disjunctions, and negations, as usual. “♢σ” and “□σ” may be read “σ is satisfiable” and “σ is valid”, respectively, and this is similar to modal logic, however the semantics of hyper– propositional formulas is very different.

Each formula of degree k has possible interpretations of degree k, and as usual, such an interpretation is a model, if it turns the formula into a true statement. So next and parallel to the hierarchical syntax, the corresponding semantics has arbitrary degrees as well. We call these interpretations bit tables, and for each degree we obtain a complete boolean algebra of bit tables. A very strong and elegant property of the whole design is the fact, that the entire model class of a formula actually turns into a single bit table on the next level, i.e. the whole formula algebra of degree k is embedded into the bit table algebra of degree k + 1.

Contents

1  Bit values, characteristic functions and bit tables  4

1.1 Bit values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Power sets and characteristic functions . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Bit tables and their algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2  Logical systems and traditional propositional logic in particular  10

2.1 Optional prelude on logical systems . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2 Traditional propositional logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3  From traditional propositional to hyper–propositional logic  16

3.1 Applying modal operators to formulas . . . . . . . . . . . . . . . . . . . . . . 16 3.2 Higher degree propositional logic . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 The foundation problem and its solution . . . . . . . . . . . . . . . . . . . . . 19 3.4 The final version of hyper–propositional logic . . . . . . . . . . . . . . . . . . 22

List of Figures

1 Mathematical preliminaries . . . . . . . . . . . . . . . 3 2 Bit values and their algebra . . . . . . . . . . . . . . 8 3 The isomorphism between 𝔓 (X) and ℭ𝔥𝔣 (X) …. 8 4 Bit tables and their algebras . . . . . . . . . . . . . . 9 5 Traditional propositional logic . . . . . . . . . . . . . 15 6 Hyper–propositional logic . . . . . . . . . . . . . . . 23 7 Embedding traditional propositional into hyper–

propositional logic . . . . . . . . . . . . . . . . . . . . 24

Introduction and overview

Main objective of this text is the introduction of the syntax and semantics of hyper–digital or hyper–propositional logic by showing how it emerges from traditional propositional logic by adding modal operators to the language and finding a consistent and simple foundation for the whole system. First, we define for each carrier set A and degree k, a set of bit tables 𝔹_{A}^{k} and a couple of operations on them. The result is the bit table algebra 𝔅_{A}^{k}. All that is summarized in two figures: Figure 2 “Bit values and their algebra” and Figure 4 “Bit tables and their algebra”. Bit tables are the worlds, interpretations or semantics of the systems we are about to develop here. The syntax on the other hand are the (hyper–propositional) formula sets 𝔽_{A}^{k}, each one of them also constitutes a (default) formula algebra 𝔉_{A}^{k}. The important result will be that 𝔉_{A}^{k} ↪ 𝔅_{A}^{k+1}, i.e. that each formula algebra has a (very natural) embedding into the bit table algebra of next higher degree. And again, we will summarize all that in Figure 6 “Hyper–propositional logic” In fact, these three figures 2, 4 and 6 comprise the whole syntax and semantics of hyper– digital logic. But instead of presenting the system in an axiomatic fashion, we rather take a more narrative approach in this paper and try to explain, how hyper–propositional logic emerges from traditional propositional logic. Accordingly, we don’t bother to provide the proofs of the “facts” we are about to state.

Figure 1: Mathematical preliminaries

Sets, functions and relations

♣ ∅ , ∩ , ∪ , ⋂ , ⋃ , \ , ⊎ are the usual operations on sets, where X \ Y is the difference of X and Y (all elements of X, but not in Y), and the \underline{disjunct union} X ⊎ Y is the same as the union X ∪ Y, but it is only defined for X ∩ Y = ∅.

♣ P (X) := \{Y | Y ⊆ X\} denotes the \underline{power set} of a given set X,

♣ ℕ := \{0, 1, 2, 3, …\} the set of \underline{natural numbers}, ℝ is the set of \underline{real numbers}.

♣ card (X) is the \underline{cardinality} of a given set X.

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

♣ R : X ↭ Y is our standard notation for the type expression of a relation R between X and Y. For example, ≤: ℝ ↭ ℝ for the usual

linear order ≤ on the real numbers. Quasi–boolean algebras

A \underline{quasi–boolean algebra} is a structure ⟨B, ⊑, ≡, ⊥, ⊤, ⊓, ⊔, ¬⟩ where ♣ B is a set ♣ ⊑ is a quasi–order (i.e. a transitive and reflexive) relation on B ♣ ≡ is the equivalence relation of ⊑, i.e. x ≡ y iff x ⊑ y and y ⊑ x ♣ ⊥ is a (quasi–)least element, i.e. ⊥ ⊑ x for all x ∈ B ♣ ⊤ is a (quasi–)top element, i.e. x ⊑ ⊤ for all x ∈ B ♣ ⊓ is a (quasi–)meet function, i.e. x ⊓ y is a greatest lower bound of x, y ∈ B, ♣ ⊔ is a (quasi–)join function, i.e. x ⊔ y is a least upper bound of x, y ∈ B, ♣ ¬ is a (quasi–)complement function, i.e. ¬x ⊓ x ≡ ⊥ and ¬x ⊔ x ≡ ⊤, for all x ∈ B ♣ ⊓ and ⊔ are mutually (quasi–)distributive, i.e. x ⊓ (y ⊔ z) ≡ (x ⊓ y) ⊔ (x ⊓ z) and x ⊔ (y ⊓ z) ≡ (x ⊔ y) ⊓ (x ⊔ z), for all x, y, z ∈ B Such a quasi–boolean algebra is ♣ \underline{complete}, if there are two more functions

♠ a \underline{supremum} function ∐ which returns a least upper bound ∐S for every S ⊆ B, ♠ an \underline{infimum} function ∏ which returns a greatest lower bound ∏S for every S ⊆ B

♣ \underline{canonic} or a \underline{boolean algebra}, if ⊑ is antisymmetric, i.e. if ≡ is the identity on B.

1 Bit values, characteristic functions and bit tables

1.0.1 Remark

In this section we introduce a whole range of closely related boolean algebras, all of them are complete. We start with the most typical specimens of boolean algebras at all: 𝔅, the one built on just two elements 0 and 1, and 𝔓 (X) the structure which emerges when the subsets of an arbitrary set X are ordered by the inclusion ⊆. We suppose, we don’t need to repeat the concept of a “(complete) boolean algebra” here — it is a common notion for structures that pretty much behave like 𝔅 and 𝔓 (X). Another common notion is the “characteristic function”: it is the same as a “subset”, it just has another form. In other words, there is a bijection between subsets of a given set X and all the characteristic functions on X. ℭ𝔥𝔣 (X) denotes the complete boolean algebra on these charcteristic functions isomorph to 𝔓 (X). Finally, we built a whole recursive hierarchy on these sets of characteristic functions, similar to an iterated application of the power set operator “P(P(… (P(X)) …))”. That way, we also have characteristic functions of first, second, etc “degree”. Our general term for such a construction is “k–degree bit table”. Each of those bit table sets constitues a boolean algebra again, we obtain a whole hierarchy of complete boolean algebras 𝔅_{X}^{1}, 𝔅_{X}^{2}, 𝔅_{X}^{3}, …, starting with 𝔅_{X}^{1} = ℭ𝔥𝔣 (X). The whole matter in this chapter is not very difficult to understand and we state the mentioned theorems without proofs. The main idea is that we built some tools and get used to the notation.

1.1 Bit values

1.1.1 Definition bit values and their algebra

The \underline{bit value set} is the two–element set

𝔹 := { 0 , 1 }

where 0 is the \underline{zero bit} and 1 the \underline{unit bit}. The \underline{bit value algebra} is

𝔅 := ⟨𝔹, ≤, 0, 1, ∧, ∨, ⋀, ⋁, -⟩

where the operations are defined as usual, such that 𝔅 is a complete boolean algebra (see figure 2).

1.2 Power sets and characteristic functions

1.2.1 Definition

For every set X we define the \underline{power set algebra} on X,

𝔓 (X) := ⟨P (X) , ⊆, ∅, 1, ∩, ∪, ⋂, ⋃, ∁⟩

where 1 := X is the \underline{full set}, ∁Y := 1 \ Y is the complement of Y ∈ P (X) and ⋂ is defined on the whole domain P (X) by putting ⋂ ∅ := 1.

1.2.2 Fact

For every set X holds:

(1) card (P (X)) = 2^{card(X)}

(2) 𝔓 (X) is a complete boolean algebra

1.2.3 Definition characteristic functions

A \underline{characteristic function} (on X) is a function χ with codomain 𝔹, i.e.

χ : X ⟶ 𝔹

For such a χ we define Unit (χ) := \{x ∈ X | χ(x) = 1\} the \underline{unit set} of χ

Zero (χ) := \{x ∈ X | χ(x) = 0\} the \underline{zero set} of χ

If X = {x_{1}, …, x_{n}} is finite, we often represent ξ by

χ = [ \begin{matrix}x_{1} & ↦ & χ(x_{1}) \\ x_{2} & ↦ & χ(x_{2}) \\ ⋮ & & ⋮ \\ x_{n} & ↦ & χ(x_{n}) \end{matrix} ]

1.2.4 Example

If X := {a, b, c, d, e}, a characteristic function on X is given by

χ := [\begin{matrix}a ↦ & 0 \\ b ↦ & 1 \\ c ↦ & 1 \\ d ↦ & 0 \\ e ↦ & 1 \end{matrix}]

Then

Unit (χ) = {b, c, e}  and  Zero (χ) = {a, d}

1.2.5 Definition characteristic function of a subset

Given a set X. For every Y ⊆ X we define

cf_{Y} := cf_{Y}^{X} := [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ \begin{cases}1 & if x ∈ Y \\ 0 & if x ∉ Y \end{cases} \end{matrix} ]

the characteristic function of Y (in X)

1.2.6 Example

As in example 1.2.4, let X := {a, b, c, d, e}. For Y := {b, c, e} we obtain

cf_{Y}^{X} = [\begin{matrix}a ↦ & 0 \\ b ↦ & 1 \\ c ↦ & 1 \\ d ↦ & 0 \\ e ↦ & 1 \end{matrix}]

Note, that

Unit (cf_{Y}^{X}) = {b, c, e} = Y

1.2.7 Fact

For every set X holds:

(1) cf_{◯ 1} : P (X) ⟶ (X ⟶ 𝔹) is a bijection

(2) Unit : (X ⟶ 𝔹) ⟶ P (X) is the inverse bijection of

cf_{◯ 1}

(3) card (X ⟶ 𝔹) = 2^{card(X)}

(4) X = Unit (χ) ⊎ Zero (χ), for each χ : X ⟶ 𝔹.

In other words, the domain of each characteristic function is a disjunct union of its unit and zero set.

1.2.8 Definition

The \underline{characteristic function algebra} of a given set X

ℭ𝔥𝔣 (X) := ⟨(X ⟶ 𝔹), ⊑, ⊥, ⊤, ⊓, ⊔, ∏, ∐, ¬⟩

is defined by

χ_{1} ⊑ χ_{2} iff χ_{1}(x) ≤ χ_{2}(x) for all x ∈ X

⊥ := [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ 0 \end{matrix} ] ⊤ := [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ 1 \end{matrix} ]

\begin{aligned}χ_{1} ⊓ χ_{2} & := & [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ χ_{1}(x) ∧ χ_{2}(x) \end{matrix} ] \\ χ_{1} ⊔ χ_{2} & := & [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ χ_{1}(x) ∨ χ_{2}(x) \end{matrix} ] \\ ∏Ξ & := & [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ ⋀\{χ(x) | x ∈ ξ\} \end{matrix} ] \\ ∐Ξ & := & [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ ⋁\{χ(x) | x ∈ ξ\} \end{matrix} ] \\ ¬χ & := & [ \begin{matrix}X ⟶ 𝔹 \\ x ↦ -χ(x) \end{matrix} ] \end{aligned}

for all χ, χ_{1}, χ_{2} : X ⟶ 𝔹 and Ξ ⊆ (X ⟶ 𝔹).

1.2.9 Example

Three characteristic functions on X := {a, b, c, d, e} are given by

χ_{1} = [\begin{matrix}a ↦ & 0 \\ b ↦ & 0 \\ c ↦ & 0 \\ d ↦ & 0 \\ e ↦ & 0 \end{matrix}]  χ_{2} = [\begin{matrix}a ↦ & 0 \\ b ↦ & 1 \\ c ↦ & 1 \\ d ↦ & 0 \\ e ↦ & 1 \end{matrix}]  χ_{3} = [\begin{matrix}a ↦ & 0 \\ b ↦ & 0 \\ c ↦ & 0 \\ d ↦ & 1 \\ e ↦ & 0 \end{matrix}]

Then

(a) χ_{1} ⊑ χ_{2}, because χ_{1}(x) ≤ χ_{2}(x) for each x ∈ X

(b) χ_{3} ⋢ χ_{2}, because χ_{3}(d) = 1 ≰ 0 = χ_{2}(d)

(c) ¬χ_{2} = [\begin{matrix}a ↦ & -0 \\ b ↦ & -1 \\ c ↦ & -1 \\ d ↦ & -0 \\ e ↦ & -1 \end{matrix}] = [\begin{matrix}a ↦ & 1 \\ b ↦ & 0 \\ c ↦ & 0 \\ d ↦ & 1 \\ e ↦ & 0 \end{matrix}]

(d) ∐ \{χ_{1}, χ_{2}, χ_{3}\} = [\begin{matrix}a ↦ & ⋁ \{0, 0, 0\} \\ b ↦ & ⋁ \{0, 1, 0\} \\ c ↦ & ⋁ \{0, 1, 0\} \\ d ↦ & ⋁ \{0, 0, 1\} \\ e ↦ & ⋁ \{0, 1, 0\} \end{matrix}] = [\begin{matrix}a ↦ & 0 \\ b ↦ & 1 \\ c ↦ & 1 \\ d ↦ & 1 \\ e ↦ & 1 \end{matrix}]

1.2.10 Fact

For every set X holds:

(1) Unit : ℭ𝔥𝔣 (X) ≅ 𝔓 (X)

i.e. Unit is not only a bijection from X ⟶ 𝔹 into P (X), but an isomorphism from ℭ𝔥𝔣 (X) into 𝔓 (X)

(2) ℭ𝔥𝔣 (X) is a complete boolean algebra.

1.2.11 Remark

Figure 3 shows the typical order diagram (also called “Hasse diagram”) of the complete boolean algebra 𝔓 (X), where X = {a, b, c} is a simple example of a tree element set. The diagram of the isomorph ℭ𝔥𝔣 (X) thus looks the same, and the two mutually inverse isomorphisms Unit and cf_{◯ 1} point from one diagram to the according places in the other one.

1.3 Bit tables and their algebras

1.3.1 Definition

For every set A and each k ∈ ℕ we define

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

the \underline{bit table} set on (\underline{carrier}) A and (\underline{degree}) k

1.3.2 Remark

For each given A, the (members of the) first bit table sets 𝔹_{A}^{k} also have alternative “geometric” names:

𝔹_{A}^{0} = A  is also called the \underline{bit point} set on A
𝔹_{A}^{1} = A ⟶ 𝔹  are the \underline{bit lines} on A
𝔹_{A}^{2} = (A ⟶ 𝔹) ⟶ 𝔹  the \underline{bit squares} on A
𝔹_{A}^{3} = ((A ⟶ 𝔹) ⟶ 𝔹) ⟶ 𝔹 the \underline{bit cubes} on A
⋮  ⋮

1.3.3 Bit table diagrams

In case both A and k are really small, we can note a bit table Ω ∈ 𝔹_{A}^{k} according to 1.2.3 by

[ \begin{matrix}ω_{1} & ↦ & Ω(ω_{1}) \\ ω_{2} & ↦ & Ω(ω_{2}) \\ ⋮ & & ⋮ \\ ω_{n} & ↦ & Ω(ω_{n}) \end{matrix} ]

But instead, we often picture it by its bit table diagram, which is a littel more compact, when k ≥ 2. For example, let us take A = {a, b, c}.

(i) For k = 0, Ω simply is a member of A and “Ω” very much is its one bit table diagram.

(ii) If k = 1 we draw the diagram for Ω : A ⟶ 𝔹 in two steps

(1) First we list all the arguments a, b, c of Ω

a b c

(2) Then we add for each argument ω its bit value Ω(ω)

Ω = \begin{matrix}a & b & c \\ Ω(a) & Ω(b) & Ω(c) \end{matrix}

(iii) For k = 2, Ω : 𝔹_{A}^{1} ⟶ 𝔹 is again constructed in two steps:

(1) There are 2^{3} = 8 different arguments ω_{1}, …, ω_{n} ∈ 𝔹_{A}^{1} of Ω. We list all these arguments in a compact list

\begin{matrix}a & b & c \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ ⋮ & ⋮ & ⋮ \\ 1 & 1 & 1 \end{matrix}

(2) Then we attach the bit values Ω(ω), for each ω:

a b c 0 0 0 Ω(ω1) 1 0 0 Ω(ω2)
⋮ ⋮ ⋮  ⋮ 1 1 1 Ω(ω8)

The result is a common diagram from traditional propositional logic, where is it usually called a truth table.

(iv) For k = 3, we perform the same two steps to produce a bit table diagram for Ω ∈ 𝔹_{A}^{3}:

(1) First list all the 2^{8} = 256 arguments ω_{1}, …, ω_{256} ∈ 𝔹_{A}^{2}:

a b c
0 0 0 0 1 … 1
1 0 0 1 1 … 1
1 1 0 0 1 … 1

(2) Then attach the corresponding bit values:

a b c
0 0 0  0  1  …  1
1 0 0  1  1  …  1
⋮ ⋮ ⋮  ⋮  ⋮  ⋮
1 1 0  0  1  …  1
Ω(ω1) Ω(ω2) … Ω(ω256)

This can in principle be done for every k > 3 as well. But of course, the size of the diagram grows exponentially. For really small A and k however, the pictures are sometimes useful.

1.3.4

Bit tables with degree higher than 0 are characteristic functions, as defined in 1.2.3. If Ω ∈ 𝔹_{A}^{k} with k > 0, then Ω : 𝔹_{A}^{k−1} ⟶ 𝔹 with

𝔹_{A}^{k−1} = Unit (Ω) ⊎ Zero (Ω)

In our standard notation for functions, such a bit table is given by

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

For every 𝔹_{A}^{k} = 𝔹_{A}^{k−1} ⟶ 𝔹 we can also define the characteristic function algebra of 𝔹_{A}^{k−1} as introduced in 1.2.8. Later on it will be useful to clearly distinguish these algebras for different A and k, and therefore, we attach this information to the operation symbols and write “⊑_{A}^{k}”, “⊥_{A}^{k}”, “⊓_{A}^{k}” instead of simply “⊑”, “⊥”, “⊓” etc.

1.3.5 Definition

For every set A and k ≥ 1 we define

\begin{aligned}𝔅_{A}^{k} & := & ⟨𝔹_{A}^{k}, ⊑_{A}^{k}, ⊥_{A}^{k}, ⊤_{A}^{k}, ⊓_{A}^{k}, ⊔_{A}^{k}, ∏_{A}^{k}, ∐_{A}^{k}, ¬_{A}^{k}⟩ \\ & := & ℭ𝔥𝔣 (𝔹_{A}^{k−1}) \end{aligned}

the \underline{bit table algebra} on (\underline{carrier}) A and (\underline{degree}) k.

1.3.6 Operations in general functional representation

So if A and k ≥ 1 are given, then for all Ω, Ω′ ∈ 𝔹_{A}^{k} and Γ ⊆ 𝔹_{A}^{k},

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

⋮ ⋮ ⋮ ⋮ ⋮  ⋮

⊥_{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} ]

Ω ⊔_{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} ]

1.3.7 Operations in diagram representation

If the bit tables are given by their diagrams, the application of the operations becomes very intuitive. For example, take A = {a, b, c}, k = 1

⊥_{A}^{k} = \begin{matrix}a & b & c \\ 1 & 1 & 1 \end{matrix} and ⊤_{A}^{k} = \begin{matrix}a & b & c \\ 1 & 1 & 1 \end{matrix}

If two members of 𝔹_{A}^{k}, i.e. two bit lines on A are given by

Ω := \begin{matrix}a & b & c \\ 1 & 0 & 0 \end{matrix} and Ω′ := \begin{matrix}a & b & c \\ 1 & 0 & 1 \end{matrix}

then

\begin{matrix}Ω ⊓_{A}^{k} Ω′ = \begin{matrix}a & b & c \\ 1 ∧ 1 & 0 ∧ 0 & 0 ∧ 1 \end{matrix} = \begin{matrix}a & b & c \\ 1 & 0 & 0 \end{matrix} \\ ¬_{A}^{k}Ω = \begin{matrix}a & b & c \\ -1 & -0 & -0 \end{matrix} = \begin{matrix}a & b & c \\ 0 & 1 & 1 \end{matrix} \end{matrix}

and

Ω ⊑_{A}^{k} Ω′ because (\begin{matrix}Ω(a) = 1 ≤ 1 = Ω′(a) and \\ Ω(b) = 0 ≤ 0 = Ω′(b) and \\ Ω(c) = 0 ≤ 1 = Ω′(c) \end{matrix} )

Similar rules hold for other carrier set and degrees. For example, for bit squares (degree=2) on A = {a, b} we have

⊥_{A}^{k} = \begin{matrix}a & b \\ 0 & 0 & 0 \\ 0 & 0 & 0 \\ 0 & 0 & 0 \\ 0 & 0 & 0 \end{matrix} and ⊤_{A}^{k} = \begin{matrix}a & b \\ 0 & 0 & 1 \\ 0 & 0 & 1 \\ 0 & 0 & 1 \\ 0 & 0 & 1 \end{matrix}

and

\begin{matrix}a & b \\ 0 & 0 & 1 \\ 0 & 0 & 0 \\ 0 & 0 & 1 \\ 0 & 0 & 0 \end{matrix} ⊔_{A}^{k} \begin{matrix}a & b \\ 0 & 0 & 0 \\ 0 & 0 & 0 \\ 0 & 0 & 1 \\ 0 & 0 & 0 \end{matrix} = \begin{matrix}a & b \\ 0 & 0 & 1 ∨ 0 \\ 0 & 0 & 0 ∨ 0 \\ 0 & 0 & 1 ∨ 1 \\ 0 & 0 & 0 ∨ 0 \end{matrix} = \begin{matrix}a & b \\ 0 & 0 & 1 \\ 0 & 0 & 0 \\ 0 & 0 & 1 \\ 0 & 0 & 0 \end{matrix}

and so on.

1.3.8 Example

For the same A = {a, b} and k = 2 the entire boolean algebra 𝔅_{A}^{k} is represented by the following order diagram:

[figure: \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 0 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 0 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 0 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}; \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}]

1.3.9 Fact

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

1.3.10 Remark

We call a boolean algebra \underline{degenerated}, if it only has a single element. Usually, one expects a boolean algebra to have at least a bottom and a top element, both being different. Otherwise it doesn’t really make sense to talk about a “boolean algebra” at all. Some authors therefore exclude degenerated boolean algebras from the definition right away. The statement of 1.3.9 is true in general, but 𝔅_{A}^{k} is degenerated, if and only if A = ∅ and k = 1. In that case 𝔹_{A}^{k} has only one element, the empty function of type ∅ ⟶ 𝔹.

Figure 2: 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 3: The isomorphism between 𝔓 (X) and ℭ𝔥𝔣 (X)

[figure: 𝔓 (\{a, b, c\}); ℭ𝔥𝔣 (\{a, b, c\}); cf_{◯ 1}; Unit; \{a, b, c\}; \{a, b\}; \{a, c\}; \{b, c\}; \{a\}; \{b\}; \{c\}; ∅; [\begin{matrix}a ↦ & 1 \\ b ↦ & 1 \\ c ↦ & 1 \end{matrix}]; [\begin{matrix}a ↦ & 1 \\ b ↦ & 1 \\ c ↦ & 0 \end{matrix}]; [\begin{matrix}a ↦ & 1 \\ b ↦ & 0 \\ c ↦ & 1 \end{matrix}]; [\begin{matrix}a ↦ & 0 \\ b ↦ & 1 \\ c ↦ & 1 \end{matrix}]; [\begin{matrix}a ↦ & 1 \\ b ↦ & 0 \\ c ↦ & 0 \end{matrix}]; [\begin{matrix}a ↦ & 0 \\ b ↦ & 1 \\ c ↦ & 0 \end{matrix}]; [\begin{matrix}a ↦ & 0 \\ b ↦ & 0 \\ c ↦ & 1 \end{matrix}]; [\begin{matrix}a ↦ & 0 \\ b ↦ & 0 \\ c ↦ & 0 \end{matrix}]]

Figure 4: 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.

2 Logical systems and traditional propositional logic in particular

2.0.11 Introduction

We are about show how hyper–propositional logic can be developed as a generalization of traditional propositional logic. We first start with a general description of a “logical system” and then introduce “(traditional) propositional logic” as a special example. In itself, our review is incomplete (e.g. we entirely neglect the proof system and the derivation concept of logical systems), the emphasis on certain aspects (like the different representations of an interpretation structure in 2.1.2) might seem awkward, and the whole trip (from “interpretation structures” to “formula algebras”) is somewhat counter–intuitive. But it points out the properties that motivate some of the ideas later on.

2.1 Optional prelude on logical systems

2.1.1 Interpretation structures

An \underline{interpretation structure} is made of three ingredients:^{1}

(i) A formal language, usually represented as a set F ORM of \underline{formulas}.

(ii) A potential reality, usually represented as a class INT of

possible \underline{interpretations}. (iii) A logical semantics, which defines a correspondence be-

tween formulas φ and interpretations Ω: φ can be a \underline{true} formula for Ω. In that case, Ω is also said to \underline{satisfy} φ or be a \underline{model} for φ. Otherwise, φ is \underline{false} for Ω.

2.1.2 Three equivalent representations

In precise mathematical terms, such an interpretation structure can be given in different but equivalent representations:

⊧: INT ↭ F ORM  the \underline{model relation}
Mod : F ORM ⟶ P (INT)  the \underline{model class} function
mod : F ORM ⟶ INT ⟶ 𝔹  the \underline{model function}

“Ω ⊧ φ” is saying that Ω is a model for φ. Otherwise, we write “Ω |̸= φ”, as usual. “Mod (φ) ⊆ INT ” denotes the class of all the models of φ. And mod (φ) : INT ⟶ 𝔹, the model function^{2} of φ, is the characteristic function of this model class. In other words, mod(φ)(Ω) is 1, if Ω is a model for φ, and 0, otherwise.

Most common is the formal definition of a semantics by means of “⊧”. But note, that each of the three representations is equivalent and each one implies the other two.

2.1.3 Transformation rules

Let F ORM and INT be two classes.

(1) Given a model relation ρ : INT ↭ F ORM (a) The model class function of ρ

Mod_{ρ} : F ORM ⟶ P (INT)

is defined by

Mod_{ρ}(φ) := {Ω ∈ INT | Ω ρ φ}

for all φ ∈ F ORM.

(b) The model function of ρ

mod_{ρ} : F ORM ⟶ INT ⟶ 𝔹

is defined by

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

for all φ ∈ F ORM and Ω ∈ INT

(2) Given a model class function M : F ORM ⟶ P (INT)

(a) The model relation of M

⊧_{M}: INT ↭ F ORM

is defined by

Ω ⊧_{M} φ iff Ω ∈ M

for all Ω ∈ INT and φ ∈ F ORM (b) The model function of μ

mod_{M} : F ORM ⟶ INT ⟶ 𝔹

is defined by

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

for all φ ∈ F ORM and Ω ∈ INT.

(3) Given a model function μ : F ORM ⟶ INT ⟶ 𝔹 (a) The model relation of μ

⊧_{μ}: INT ↭ F ORM

is defined by

Ω ⊧_{μ} φ iff μ(φ)(Ω) = 1

(b) The model class function of μ

Mod_{μ} : F ORM ⟶ P (INT)

is defined by

Mod_{μ}(φ) := {Ω ∈ INT | μ(φ)(Ω) = 1}

for all φ ∈ F ORM.

1Actually, this definition of an “interpretation structure” meets every binary relation and is thus not suitable for a description of something like a logical system. Later on in ??lindenbaum structure must be a boolean lattic?? , we put more constraints on interpretation systems to be useful.

2So we call “mod” itself the “model function”, but also its application “mod(φ)”. Later on in the context of hyper-propositional logic, it makes sense to call “mod(φ)” the “super–model of φ”, because a model of φ ∈ 𝔽_{A}^{k} is some ω ∈ 𝔹_{A}^{k}, but mod(φ) ∈ 𝔹_{A}^{k+1}, i.e. a model has the same degree k as the formula, but the model function has degree k + 1, hence the “super–model”.

2.1.4 Sub– and equivalence

Each interpretation structure with formulas F ORM, interpretations INT and a semantics, represented by ⊧, Mod, mod, induces an order on its formulas, usually called “entailment”, “consequence” or “implication”. We prefer the title “subvalence”^{3}) and define two relations

⇒: F ORM ↭ F ORM  the \underline{subvalence} relation
⇔: F ORM ↭ F ORM the \underline{equivalence} relation

by putting

φ ⇒ ψ iff ∀Ω ∈ INT . (Ω ⊧ φ implies Ω ⊧ ψ)
iff Mod (φ) ⊆ Mod (ψ)
iff mod (φ) ⊑ mod (ψ)
φ ⇔ ψ iff ∀Ω ∈ INT . (Ω ⊧ φ iff Ω ⊧ ψ)
iff Mod (φ) = Mod (ψ)
iff mod (φ) = mod (ψ)

for all φ, ψ ∈ F ORM.

Note, that all this is well–defined. Here, “⊆” is the order on P (INT) and “⊑” is the order on the characteristic functions INT ⟶ 𝔹, introduced in 1.2.8. Both are isomorph structures.

2.1.5 A quasi–boolean algebra of formulas

Obviously, ⟨F ORM, ⇒, ⇔⟩ is a quasi–ordered set. ^{4}

But for a proper logical system we want this quasi–ordered set to be a \underline{quasi–boolean algebra of formulas}, i.e. equipped with the following operations: ♣ a \underline{zero} or \underline{false} formula constant f, which is a least element

in ⟨F ORM, ⇒⟩ ♣ a \underline{unit} or \underline{true} element t, which is a greatest element ♣ a \underline{(quasi–)meet} function ⋏ : F ORM × F ORM ⟶ F ORM,

which returns a greatest lower bound φ ⋏ ψ for all φ, ψ ∈ F ORM.

♣ a \underline{join} function ⋎, which returns a least upper bound φ ⋎ ψ,

and ♣ a \underline{complement} function - : F ORM ⟶ F ORM, such that

φ ∨ -φ ⇔ t and φ ∧ -φ ⇔ f, for all φ ∈ F ORM.

Note, that all these ingredients are usually not unique, but only unique up to equivalence. This is the difference between a quasi–order and a (partial) ordered structure.

2.1.6 Example

Suppose we have already given the propositional formula set, together with the usual sub– and equivalence, we have different ways to define a meet function ⋏ for arbitrary arguments φ and ψ. For example,

φ ⋏ φ := [ φ ∧ ψ]

would be the most obvious choice (the \underline{default} version). But in fact, we have infinitely many options for the right side of this definition:

[ ψ ∧ φ]  [ φ ∧ ψ ∧ φ]  [ ψ ↔ φ ↔ t ]  …

All these approaches produce equivalent results, each one a (not the) greatest lower bound of φ and ψ. However, these alternatives all produce formulas that increase in size. Alternatively, there are also more sophisticated versions where the result of all operations like φ ⋏ ψ always is in a certain normal or even canonical form.^{5}

2.1.7 Logical system and Lindenbaum algebras

We do not really care here, but we could say that a given interpretation structure with its quasi–ordered set ⟨F ORM, ⇒, ⇔⟩ is (or makes) a \underline{logical system}, if it is possible to define such a quasi–boolean algebra at all.

There is an alternative criterion for that: we construct the quotient–structure^{6} of the given quasi–ordered set. If and only if this poset has all the properties of a boolean lattice, then the original structure is a logical system in our sense. This boolean quotient structure of a given quasi–ordered set of formulas is usually called the \underline{Lindenbaum} or \underline{Lindenbaum–Tarski} algebra.

2.2 Traditional propositional logic

2.2.1 Definition

Pfm (A) the \underline{propositional formula} set on a given A is recursively defined to comprise the following expressions:

([a])  (\underline{atomic formula})
¬φ  (\underline{negation})
[ φ_{1} ∧ … ∧ φ_{n} ]  (\underline{conjunction})
[ φ_{1} ∨ … ∨ φ_{n} ]  (\underline{disjunction})

for all a ∈ A and φ, φ_{1}, …, φ_{n} ∈ Pfm(A) with n ∈ ℕ.

2.2.2 Remark

3I like the systematics in the following terminology and notation: subvalence “⇒”, equivalence “⇔”, subjunction “→”, and equijunction “↔”.

4⟨F ORM, ⇒, ⇔⟩ is a \underline{quasi–ordered set} iff ⇒ is a quasi–order (i.e. transitive and reflexive) relation on F ORM and ⇔ is its equivalence relation (i.e. φ ⇔ ψ iff φ ⇒ ψ and ψ ⇒ φ).

5See e.g. Theory and implementation of efficient canonical systems for sentential calculus, based on Prime Normal Forms on www.bucephalus.org.

6⇔ is an equivalence relation on F ORM. Its \underline{equivalence classes} are the φ̃ := \{ψ ∈ F ORM | ψ ⇔ φ\}, for φ ∈ F ORM. The overall \underline{quotient set} F ORM/⇔ is the collection of all these equivalent classes, and the subvalence relation is redefined on it by putting φ̃ ˜⇒ ψ̃ iff φ ⇒ ψ. Finally, ⟨F ORM/⇔, ˜⇒⟩ is the wanted \underline{quotient structure}. A quotient structure of a quasi–ordered set is always a \underline{poset} or \underline{(partially) ordered set}.

(1) Most authors don’t distinguish between atoms and atom formulas, i.e. they write “a” instead of our “([a])”. For example, they rather write

“[ a ∨ ¬b]”  instead of our  “[ ([a]) ∨ ¬([b]) ]”

We call that the \underline{convenient form}, and in most examples, we also use that version to make things more readable. However and strictly speaking, we insist on the proper “([a])” version for atom formulas. This keeps things clear, especially when it comes to “higher order” issues, where the atom “a” itself can be a more complex form and things might become ambiguous.

(2) The square brackets “[ …]” are also used as part of the syntax and extra distinction of formulas from terms like “0 ∧ (1 ∨ 0)”, which are not formulas, but applications. We don’t apply the usual preference rules to eliminate brackets, either.

(4) We defined the conjunction and disjunction for any finite number n ∈ ℕ of arguments and we write

(a) [ ∧] and [ ∨] for nullary (i.e. n = 0), and

(b) [ ∧ φ_{1} ] and [ ∨ φ_{1} ] for unary conjunctions and disjunctions, respectively.

(5) We extend the stock of expressions by introducing new junctions as abbreviations for more complex formulas:

(a) t := [ ∧] the \underline{true} symbol

(b) f := [ ∨] the \underline{false} symbol

(c) [ φ_{1} → … → φ_{n} ] := [ [ ¬φ_{1}∨φ_{2} ]∧…∧[ ¬φ_{n−1}∨φ_{n} ] ] the \underline{subjunction}

(d) [ φ_{1} ↔ … ↔ φ_{n} ] := [ [ ¬φ_{1} ∧ … ∧ ¬φ_{n} ] ∨ [ φ_{1} ∧ … ∧

φ_{n} ] ] the \underline{equijunction}

2.2.3 Example

Example formulas of Pfm (A) for A = {a, b, c, …} are the following

(i) [ a ∧ ¬b], which is the convenient form for [ ([a]) ∧ ¬([b]) ] (ii) [ t ∧ ¬[ ¬b ∨ a] ∧ b] wich is the convenient form for

[ t ∧ ¬[ ¬([b]) ∨ ([a]) ] ∧ ([b]) ] (iii) [ a ↔ f ↔ ¬¬a] which is an abbreviation for the conve-

nient form [ [ ¬a ∧ ¬f ∧ ¬¬¬a] ∨ [ a ∧ f ∧ ¬¬a] ]

2.2.4 Remark

A propositional formula turn into a propositions, i.e. an either false or true statement, by assigning bit values to the given bit variables or atoms. In other words, an interpretation for propositional formulas is a characteristic function ω : A ⟶ 𝔹 on the given atom class A. Recall 1.3.2, that (A ⟶ 𝔹) = 𝔹_{A}^{1}. In terms of the bit table terminology and notation, the bit line set 𝔹_{A}^{1} is the interpretation class for Pfm (A). We prefer to write 𝔹_{A}^{1} instead of A ⟶ 𝔹 from now on, because this prepares the generalization to hyperpropositional logic later on. Also recall 2.1.2, that we have three equivalent versions to actually define the interpretation structure for propositional logic. We define them alltogether next in 2.2.5 and just repeat in 2.2.8, that all three are equivalent.

2.2.5 Definition

Given an atom set A.

The \underline{propositional model relation} on A

⊧_{A}: 𝔹_{A}^{1} ↭ Pfm (A)

is defined as follows:

ω ⊧_{A} ([a]) iff ω(a) = 1
ω ⊧_{A} ¬φ iff ω |̸=_{A} φ
ω ⊧_{A} [ φ_{1} ∧ … ∧ φ_{n} ] iff ω ⊧_{A} φ_{i} for all i
ω ⊧_{A} [ φ_{1} ∨ … ∨ φ_{n} ] iff ω ⊧_{A} φ_{i} for some i

for all ω ∈ 𝔹_{A}^{1}, a ∈ A and φ, φ_{1}, …, φ_{n} ∈ Pfm (A).

The \underline{propositional model class} function on A,

Mod_{A} : Pfm (A) ⟶ P (𝔹_{A}^{1})

is defined as follows:

Mod_{A}(([a])) := {ω : A ⟶ 𝔹 | ω(a) = 1}
Mod_{A}(¬φ) := 𝔹_{A}^{1} \ Mod_{A}(φ)
Mod_{A}([ φ_{1} ∧ … ∧ φ_{n} ]) := \begin{cases}𝔹_{A}^{1} & if n = 0 \\ ∩^{n}_{i=1}Mod_{A}(φ_{i}) & else \end{cases}

Mod_{A}([ φ_{1} ∨ … ∨ φ_{n} ]) := ∪^{n}_{i=1}Mod_{A}(φ_{i})

The \underline{propositional model function} on A

mod_{A} : Pfm (A) ⟶ 𝔹_{A}^{1} ⟶ 𝔹

in other words

mod_{A} : Pfm (A) ⟶ 𝔹_{A}^{2}

is defined by:

mod_{A}(([a]))(ω) := ω(a)
mod_{A}(¬φ)(ω) := -mod_{A}(φ)(ω)
mod_{A}([ φ_{1} ∧ … ∧ φ_{n} ])(ω) := ∧^{n}_{i=1}mod_{A}(φ_{i})(ω)
mod_{A}([ φ_{1} ∨ … ∨ φ_{n} ])(ω) := ∨^{n}_{i=1}mod_{A}(φ_{i})(ω)

for all ω ∈ 𝔹_{A}^{1}, a ∈ A and φ, φ_{1}, …, φ_{n} ∈ Pfm (A).

2.2.6 Remark

We use the conventions:

(1) ω ⊧_{A} φ reads “ω \underline{satisfies} φ” or “φ \underline{holds} for ω” or “φ \underline{is true} for ω”

(2) ω |̸=_{A} φ means that ω does not satisfy φ

(3) Mod_{A}(φ) is called the \underline{model class} (on A) of φ.

(4) mod_{A}(φ)(ω) is “the bit value of φ at ω”,

(5) mod_{A}(φ) is the \underline{model function} of φ on A.

2.2.7 Remark

Note, that

ω ⊧_{A} [ ∧]  and  ω |̸=_{A} [ ∨]

in other words

ω ⊧_{A} t  and  ω |̸=_{A} f

which is what one would expect: “true” is true for all interpretations.

2.2.8 Fact

For every set A, each φ ∈ Pfm (A) and ω ∈ 𝔹_{A}^{1} holds

ω ⊧_{A} φ iff ω ∈ Mod_{A}(φ) iff mod_{A}(φ)(ω) = 1

2.2.9 Example

(i) Let A = {a, b} and φ ∈ Pfm (A) be conviently given by [ a ∧ ¬b]. 𝔹_{A}^{1} has four members, namely

ω_{1} = \begin{matrix}a & b \\ 0 & 0 \end{matrix} ω_{2} = \begin{matrix}a & b \\ 1 & 0 \end{matrix} ω_{3} = \begin{matrix}a & b \\ 0 & 1 \end{matrix} ω_{4} = \begin{matrix}a & b \\ 1 & 1 \end{matrix}

Accordingly, we have

mod_{A}(φ)(ω_{1}) = mod_{A}(([a]))(ω_{1}) ∧ mod_{A}(¬([b]))(ω_{1})
= ω_{1}(a) ∧ -ω_{1}(b)
= 0 ∧ -0
= 0
mod_{A}(φ)(ω_{2}) = ω_{2}(a) ∧ -ω_{2}(b) = 1 ∧ -0 = 1
mod_{A}(φ)(ω_{3}) = 0
mod_{A}(φ)(ω_{4}) = 0

so that alltogether

Mod_{A}(φ) = \{ \begin{matrix}a & b \\ 1 & 0 \end{matrix} \} ∈ P (𝔹_{A}^{1})

and

mod_{A}(φ) = [ \begin{matrix}𝔹_{A}^{1} ⟶ 𝔹 \\ ω ↦ \begin{cases}0 & if ω = ω_{1} \\ 1 & if ω = ω_{1} \\ 0 & if ω = ω_{3} \\ 0 & if ω = ω_{4} \end{cases} \end{matrix} ] = \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix} ∈ 𝔹_{A}^{2}

(ii) For the same A = {a, b} and the example formulas f and t we obtain

mod_{A}(f) = \begin{matrix}a & b \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix}  and  mod_{A}(t) = \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 1 \end{matrix}

2.2.10

In the sequel, we often picture the actual logical system by displaying the correspondence between the syntax on the right and the semantics on the left side. The semantic hierarchy is given by the hierarchy of the bit table classes 𝔹_{A}^{k}. So far we only have two bit table classes in this hierarchy on the left and one formula set on the right:

[figure: 𝔹_{A}^{1}; ↭; ⊧_{A}; Pfm (A); 𝔹_{A}^{2}; mod_{A}]

2.2.11 Fact

For each set A and all φ, φ_{1}, …, φ_{n} ∈ Pfm (A)

mod_{A}(f) = ⊥_{A}^{2}
mod_{A}(t) = ⊤_{A}^{2}
mod_{A}(φ) = ¬_{A}^{2}mod_{A}(φ)
mod_{A}([ φ_{1} ∧ … ∧ φ_{n} ]) = ∏_{A}^{2} {mod_{A}(φ_{1}), …, mod_{A}(φ_{n})}
mod_{A}([ φ_{1} ∨ … ∨ φ_{n} ]) = ∐_{A}^{2} {mod_{A}(φ_{1}), …, mod_{A}(φ_{n})}

2.2.12 Definition

Let A be a set. We define two relations ⇒: Pfm (A) ↭ Pfm (A) the \underline{subvalence} relation

⇔: Pfm (A) ↭ Pfm (A) the \underline{equivalence} relation

by putting

φ ⇒ ψ iff ∀ω ∈ 𝔹_{A}^{1} . mod_{A}(φ)(ω) ≤ mod_{A}(ψ)
φ ⇔ ψ iff ∀ω ∈ 𝔹_{A}^{1} . mod_{A}(φ)(ω) = mod_{A}(ψ)

for all φ, ψ ∈ Pfm (A).

2.2.13 Fact

For every set A and all φ_{1}, φ_{2} ∈ Pfm (A) holds:

φ_{1} ⇒ φ_{2} iff Mod_{A}(φ) ⊆ Mod_{A}(φ_{2})
iff mod_{A}(φ_{1}) ⊑_{A}^{2} mod_{A}(φ_{2})
φ_{1} ⇔ φ_{2} iff Mod_{A}(φ) = Mod_{A}(φ_{2})
iff mod_{A}(φ_{1}) = mod_{A}(φ_{2})

2.2.14 Definition

For every set A, the \underline{default propositional formula algebra} on A is

𝔓𝔣𝔪 (A) := ⟨Pfm (A) , ⇒, ⇔, f, t, ∧, ∨, -⟩

where

φ ∧ ψ := [ φ ∧ ψ] (conjunction)
φ ∨ ψ := [ φ ∨ ψ] (disjunction)
-φ := ¬φ  (negation)

2.2.15 Fact For every set A holds:

mod_{A} : 𝔓𝔣𝔪 (A) ↪ 𝔅_{A}^{2}

i.e. mod_{A} is an embedding from 𝔓𝔣𝔪 (A) into 𝔅_{A}^{2}.

2.2.16 Remark The “embedding” in 2.2.15 means as usual, that for all φ, ψ ∈ Pfm (A),

φ ⇒ ψ implies mod_{A}^{2}(φ) ⊑_{A}^{2} mod_{A}^{2}(ψ)

and

mod_{A}^{2}(φ ∧ ψ) = mod_{A}^{2}(φ) ⊓_{A}^{2} mod_{A}^{2}(ψ)

etc. For example, if A = {a, b, c} and

φ := [ ¬([b]) ∨ ([a]) ] and ψ := ¬([c])

then

mod_{A}^{2} (φ ∧ ψ) = mod_{A}^{2} ([ [ ¬([b]) ∨ ([a]) ] ∧ ¬([c]) ])

= \begin{matrix}a & b & c \\ 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 \\ 1 & 1 & 0 & 1 \\ 0 & 0 & 1 & 0 \\ 1 & 0 & 1 & 0 \\ 0 & 1 & 1 & 0 \\ 1 & 1 & 1 & 0 \end{matrix}

= \begin{matrix}a & b & c \\ 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 \\ 1 & 1 & 0 & 1 \\ 0 & 0 & 1 & 1 \\ 1 & 0 & 1 & 1 \\ 0 & 1 & 1 & 0 \\ 1 & 1 & 1 & 1 \end{matrix} ⊓_{A}^{2} \begin{matrix}a & b & c \\ 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 1 \\ 0 & 1 & 0 & 1 \\ 1 & 1 & 0 & 1 \\ 0 & 0 & 1 & 0 \\ 1 & 0 & 1 & 0 \\ 0 & 1 & 1 & 0 \\ 1 & 1 & 1 & 0 \end{matrix}

= mod_{A}^{2}(φ) ⊓_{A}^{2} mod_{A}^{2}(ψ)

Figure 5: Traditional propositional logic

\underline{Formulas} For every given class A, we define Pfm (A) the \underline{propositional formula} class of A as the class comprising the following expressions:

([a])  for each a ∈ A  (\underline{atomic formula})
¬σ  for each σ ∈ Pfm (A)  (\underline{negation})
[ σ_{1} ∧ … ∧ σ_{n} ]  for all φ_{1}, … φ_{n} ∈ Pfm (A) with n ∈ ℕ  (\underline{conjunction})
[ σ_{1} ∨ … ∨ σ_{n} ]  for all φ_{1}, … φ_{n} ∈ Pfm (A) with n ∈ ℕ  (\underline{disjunction})

We write [ ∧] and [ ∨] for nullary (n = 0) and [ ∧ φ_{1} ] and [ ∨ φ_{1} ] for unary conjunctions and disjunctions, respectively. Model function and model class

For every A we define the \underline{model function}

mod_{A} : Pfm (A) ⟶ (A ⟶ 𝔹) ⟶ 𝔹

For every φ ∈ Pfm (A) and ω : A ⟶ 𝔹 we give a definition of mod_{A}(φ)(ω) by structural induction on the form of φ as follows:

mod_{A} (([a])) (ω) := ω(a)
mod_{A} (¬φ) (ω) := -mod_{A}(φ)(ω)
mod_{A} ([ φ_{1} ∧ … ∧ φ_{n} ]) (ω) := ⋀ {mod_{A}(φ_{1})(ω), …, mod_{A}(φ_{n})(ω)}
mod_{A} ([ φ_{1} ∨ … ∨ φ_{n} ]) (ω) := ⋁ {mod_{A}(φ_{1})(ω), …, mod_{A}(φ_{n})(ω)}

Furthermore (α) mod_{A}(φ)(ω) is the so–called \underline{truth value} of φ and (the \underline{interpretation}) ω

(β) If mod_{A}(φ)(ω) = 1 we say that “ω is a \underline{model} for φ” or “ω \underline{satisfies} φ”, and this is expressed by writing ω ⊧ φ

(γ) Mod_{A}(φ) := \{ω : A ⟶ 𝔹 | ω ⊧ φ\} is the \underline{model class} of φ ∈ Pfm (A) (δ) The function mod_{A}(φ) : (A ⟶ 𝔹) ⟶ 𝔹 is the \underline{truth table} of φ, and in case of a finite A, this is usually displayed by the typical

truth table diagram. Subvalence and equivalence

For all φ, ψ ∈ Pfm (A) we define

φ ⇒ ψ iff ∀ω : A ⟶ 𝔹 . mod_{A}(φ)(ω) ≤ mod_{A}(φ)(ψ)
iff Mod_{A}(φ) ⊆ Mod_{A}(ψ)
iff mod_{A}(φ) ⊑_{A}^{k} mod_{A}(ψ)

φ ⇔ ψ iff ∀ω : A ⟶ 𝔹 . mod_{A}(φ)(ω) = mod_{A}(φ)(ψ)
iff Mod_{A}(φ) = Mod_{A}(ψ)
iff mod_{A}(φ) = mod_{A}(ψ)

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

The quasi–boolean algebra of propositional formulas

𝔓𝔣𝔪 (A) := ⟨Pfm (A) , ⇒, ⇔, f, t, ∧, ∨, -⟩ is the \underline{default propositional formula algebra}, where for all φ, ψ ∈ Pfm (A)

f := [ ∨]  t := [ ∧]  φ ∧ ψ := [ φ ∧ ψ]  φ ∨ ψ := [ φ ∨ ψ]  -φ := ¬φ

\underline{Theorem} 𝔓𝔣𝔪 (A) is a quasi–boolean algebra, for every class A.

3 From traditional propositional to hyper–propositional logic

3.1 Applying modal operators to formulas

3.1.1 Definition

Mex (F ORM) the \underline{modalized} or \underline{modal expression} set of a given set F ORM is defined to comprise the following expressions:

♢φ (\underline{diamond})  □φ (\underline{box})

for all φ ∈ F ORM.

♢φ also reads “φ is \underline{satisfiable}” or “\underline{sometimes} φ”

□φ also reads “φ is \underline{valid}” or “\underline{always} φ”

3.1.2 Example

Let us consider Mex(Pfm(A)), the modal expressions on propositional formulas with A = {a, b, c, …}. Examples are

(i) □[ a ∨ ¬a] (ii) □[ a ∨ ¬b] (iii) ♢[ a ∨ ¬b] (iii) ♢[ a ↔ f ↔ ¬[ b ∧ a] ]

3.1.3 Interpretations for modalized expressions

Given an interpretation structure, made of two sets F ORM and INT, together with a model relation ⊧: INT ↭ F ORM.

What kind of interpretations would suit these new modal expressions on F ORM? More precisely, what class INT′ is an appropriate candidate for a model relation

⊧′: INT′ ↭ Mex (F ORM)

Putting INT′ := INT doesn’t make sense, because if ω ∈ INT and φ ∈ F ORM, then ω makes φ either true (case ω ⊧ φ) or false. However, we are looking for interpretations, that make φ not just “true”, but “sometimes true” and “always true”.

Therefore, we use another approach and put INT′ := P (INT). That makes sense now: for each M ∈ P (INT) we define

M ⊧′ □φ iff ω ⊧ φ for all ω ∈ M
M ⊧′ ♢φ iff ω ⊧ φ for some ω ∈ M

And since P (INT) is equivalent to INT ⟶ 𝔹, we have an equivalent model relation defined on characteristic functions: for every Ω : INT ⟶ 𝔹 we define

Ω ⊧′ □φ iff ω ⊧ φ for all ω ∈ Unit (Ω)
Ω ⊧′ ♢φ iff ω ⊧ φ for some ω ∈ Unit (Ω)

3.1.4 Interpretations for modalized propositional formulas

We apply the idea of 3.1.3 to our concrete case of propositional formulas and we use the version on characteristic functions by default.

The modal relation for propositional formulas was

⊧_{A}: 𝔹_{A}^{1} ↭ Pfm (A)

Accordingly, the modal relation for modalized propositional formulas is of type

⊧′_{A}: (𝔹_{A}^{1} ⟶ 𝔹) ↭ Mex(Pfm (A))

where again 𝔹_{A}^{1} ⟶ 𝔹 is 𝔹_{A}^{2}.

3.1.5 Definition

The model relation for modalized propositional formulas on a given set A, is defined by

⊧′_{A}: 𝔹_{A}^{2} ↭ Mex(Pfm(A))

with

Ω ⊧′_{A} ♢φ iff ω ⊧ φ for some ω ∈ Unit (Ω)
Ω ⊧′_{A} □φ iff ω ⊧ φ for all ω ∈ Unit (Ω)

for every Ω ∈ 𝔹_{A}^{2} and each σ ∈ Pfm (A).

3.1.6

When we add these new notions to the diagram of 2.2.10, we obtain the following picture

[figure: 𝔹_{A}^{1}; ↭; ⊧_{A}; Pfm (A); 𝔹_{A}^{2}; ↭; ⊧′_{A}; Mex(Pfm(A)); mod_{A}]

The new formula class Mex(Pfm (A)) is distinct to the original set Pfm (A) an its semantics is “one degree higher”.

3.1.7 Example

Let A := {a, b}. Let Ω ∈ 𝔹_{A}^{2} and φ ∈ Pfm (A) be given by

Ω := \begin{matrix}a & b \\ 0 & 0 & 1 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 1 \end{matrix} and φ := [ ¬a ∨ ¬b]

Then

Unit (Ω) = \{ \begin{matrix}a & b \\ 0 & 0 \end{matrix} , \begin{matrix}a & b \\ 1 & 1 \end{matrix} \}

and

\begin{matrix}a & b \\ 0 & 0 \end{matrix} ⊧_{A} φ because -0 ∨ -0 = 1 ∨ 1 = 1

\begin{matrix}a & b \\ 1 & 1 \end{matrix} |̸=_{A} φ because -1 ∨ -1 = 0 ∨ 0 = 0

Therefore ♣ Ω ⊧′_{A} ♢φ

i.e. φ is satisfiable in Ω; “sometimes φ” holds in Ω ♣ Ω |̸=′_{A} □φ

i.e. φ is not valid in Ω; “always φ” does not hold in Ω

3.1.8 Fact

Given a set A. For every φ ∈ Pfm (A) and Ω ∈ 𝔹_{A}^{2} holds:

Ω ⊧′_{A} □φ iff ∀ω ∈ 𝔹_{A}^{1} . Ω(ω) ≤ mod_{A}(φ)(ω)
iff Ω ⊑_{A}^{2} mod_{A}(φ)
Ω ⊧′_{A} ♢φ iff ∃ω ∈ 𝔹_{A}^{1} . Ω(ω) ∧ mod_{A}(φ)(ω) = 1
iff Ω ⊓_{A}^{2} mod_{A}(φ) ≠ ⊥_{A}^{2}

3.1.9 Fact

Given a set A. For all φ, ψ ∈ Pfm (A) holds:

mod_{A}(ψ) ⊧′_{A} □φ iff ψ ⇒ φ
mod_{A}(ψ) ⊧′_{A} ♢φ iff [ ψ ∧ φ] ⇎ f

3.2 Higher degree propositional logic

3.2.1

Modalized propositional formulas ♢φ and □φ are statements and it makes sense to combine them to more complex statements again by means of “and”, “or”, “not” etc. With definition 2.2.1, we already have the means to do that formally: we generalize Mex(Pfm (A)) to Pfm(Mex(Pfm (A))).

This way we obtain new formulas such as

[ [ □a → ♢a] ∨ ¬¬♢b]

which would be the convenient form (see 2.2.2(1)) of

[ [ ([□([a])]) → ([♢([a])]) ] ∨ ¬¬♢([b]) ]

The new semantics is defined according to the traditional recipe as well. We increase

⊧′_{A}: 𝔹_{A}^{2} ↭ Mex(Pfm (A))

to

⊧′′_{A}: 𝔹_{A}^{2} ↭ Pfm(Mex(Pfm (A)))

by declaring

Ω ⊧′′_{A} ([σ]) iff Ω ⊧′_{A} σ
Ω ⊧′′_{A} ¬φ iff Ω |̸=′′_{A} φ
Ω ⊧′′_{A} [ φ_{1} ∧ … ∧ φ_{n} ] iff Ω ⊧′′_{A} φ_{1} and … and Ω ⊧′′_{A} φ_{n}
Ω ⊧′′_{A} [ φ_{1} ∨ … ∨ φ_{n} ] iff Ω ⊧′′_{A} φ_{1} or … or Ω ⊧′′_{A} φ_{n}

as usual. That way, our situation from picture 3.1.6 now becomes

[figure: 𝔹_{A}^{1}; ↭; ⊧_{A}; Pfm (A); 𝔹_{A}^{2}; ↭; ⊧′′_{A}; Pfm(Mex(Pfm(A))); mod_{A}]

3.2.2

The previous picture reveals a pattern that asks for another generalization. Similar to the increase in the semantic hierarchy on the left side from 𝔹_{A}^{1} to 𝔹_{A}^{2}, we have and “upgrade” method for formulas on the right. For every A and k ≥ 1 we have a “k–degree formula set” F_{A}^{k} by putting

F_{A}^{k} := \begin{cases}Pfm (A) & if k = 1 \\ Pfm(Mex(F_{A}^{k−1})) & if k > 1 \end{cases}

In analogy to the first steps, we then have a model relation

⊧_{A}^{k} : 𝔹_{A}^{k} ↭ F_{A}^{k}

for all k ≥ 2 as well. We are going to work out all that in a moment, but we do so with a modified syntax. For degrees k ≥ 2 we add to each of the operation symbols “♢”, “∧”, etc. the degree k itself write

“♢_{k}”, “∧_{k}”, instead.

The outfit of the resulting formulas is usually redundant and not very appealing. But at this stage, we rather have a transparent than elegant syntax. We want to see for each formula of the new hierarchy, to which level it belongs. Since we allowed nullary junctions like “[ ∧]”, we won’t be able to see its degree k, unless we write “[ ∧_{k}]” instead.^{7}

7Actually, the real motivation for this clear syntax lies beyond this text. It becomes relevant first when we combine the formula sets of all degrees to a single one and compare that with the set of traditional modal formulas (see www.bucephalus.org for more information).

3.2.3 Definition

For each set A and k ∈ ℕ, the \underline{k–degree propositional formula} set on A,

Pfm^{k}(A)

is recursively defined as follows: ♣ If k = 0 then Pfm^{0}(A) := A. ♣ If k = 1 then Pfm^{1}(A) := Pfm (A).

♣ If k ≥ 2 then Pfm^{k}(A) is defined to comprise:

\begin{matrix}♢_{k}σ \\ □_{k}σ \end{matrix} \} for σ ∈ Pfm^{k−1}(A)

\begin{matrix}¬_{k}φ \\ [ φ_{1} ∧_{k} … ∧_{k} φ_{n} ] \\ [ φ_{1} ∨_{k} … ∨_{k} φ_{n} ] \end{matrix} \} for φ, φ_{1}, …, φ_{n} ∈ Pfm^{k}(A)

3.2.4 Example

Let A = {a, b, c, …}. A member of Pfm^{4}(A) in its convenient form is given by

♢_{4}[ ¬_{3}□_{3}[ ♢_{2}[ a ∧ ¬b] ∨_{2} □_{2}[ c ∧ ¬a] ] ∧_{3} □_{3}♢_{2}[ a ∨ [ ∧] ] ]

We can decompose it to make sure that it is indeed well–formed according to definition 3.2.3:

♢_{4} [ ¬_{3}□_{3} \underbrace{[ ♢_{2} \underbrace{[ a ∧ ¬b]}_{∈Pfm(A)} ∨_{2} □_{2} \underbrace{[ c ∧ ¬a]}_{∈Pfm(A)} ]}_{∈Pfm2(A)} ∧_{3} □_{3} \underbrace{♢_{2} \underbrace{[ a ∨ [ ∧] ]}_{∈Pfm(A)}}_{∈Pfm2(A)} ]

∈Pfm3(A)

3.2.5 Remark

Starting with any given set A we now have an infinite hierarchy of (pairwise disjunct) formula sets: A, Pfm (A), Pfm^{2}(A), etc. If we consider the syntactical symbols as functions on these sets, we obtain the following picture:

[figure: A; Pfm(A); Pfm^{2}(A); Pfm^{3}(A); Pfm^{4}(A); ⋮; ([ ]); ♢_{2}, □_{2}; ♢_{3}, □_{3}; ♢_{4}, □_{4}; ♢_{5}, □_{5}; ∧ , ∨ , ¬; ∧_{2} , ∨_{2} , ¬_{2}; ∧_{3} , ∨_{3} , ¬_{3}; ∧_{4} , ∨_{4} , ¬_{4}]

(Of course, this picture is not entirely correct, because conjunctions and disjunctions don’t take formulas, but formula tuples as arguments.)

3.2.6

We define the semantics for this hierarchy of formulas:

[figure: 𝔹_{A}^{1}; ↭; ⊧_{A}; Pfm (A); 𝔹_{A}^{2}; ↭; ⊧_{A}^{2}; Pfm^{2}(A); 𝔹_{A}^{3}; ↭; ⊧_{A}^{3}; Pfm^{3}(A); ⋮; ⋮; mod_{A}; mod_{A}^{3}; mod_{A}^{4}]

On the first level, ⊧_{A} is traditional model relation and mod_{A} the model function from ??. For all k ≥ 2, the ⊧_{A}^{k} and mod_{A}^{k+1} are now defined according to our approach so far.

3.2.7 Definition

For every set A and each k ≥ 2 we define a \underline{model relation}

⊧_{A}^{k} : 𝔹_{A}^{k} ↭ Pfm^{k}(A)

as follows:

Ω ⊧_{A}^{k} ♢_{k}σ iff \{ \begin{matrix}∃ω ∈ Unit (Ω) . ω ⊧_{A} σ & if k = 2 \\ ∃ω ∈ Unit (Ω) . ω ⊧_{A}^{k−1} σ & if k > 2 \end{matrix}

Ω ⊧_{A}^{k} □_{k}σ iff \{ \begin{matrix}∀ω ∈ Unit (Ω) . ω ⊧_{A} σ & if k = 2 \\ ∀ω ∈ Unit (Ω) . ω ⊧_{A}^{k−1} σ & if k > 2 \end{matrix}

for all Ω ∈ 𝔹_{A}^{k} and σ ∈ \begin{cases}Pfm (A) & if k = 2 \\ Pfm^{k−1}(A) & if k > 2 \end{cases}

Ω ⊧_{A}^{k} ¬_{k}φ iff Ω |̸=_{A}^{k} φ
Ω ⊧_{A}^{k} [ φ_{1} ∧_{k} … ∧_{k} φ_{n} ] iff Ω ⊧_{A}^{k} φ_{i} for all i
Ω ⊧_{A}^{k} [ φ_{1} ∨_{k} … ∨_{k} φ_{n} ] iff Ω ⊧_{A}^{k} φ_{i} for some i

for all Ω ∈ 𝔹_{A}^{k} and φ, φ_{1}, …, φ_{n} ∈ Pfm^{k}(A)

For every set A and each k ≥ 2 we define a \underline{model function}

mod_{A}^{k+1} : Pfm^{k}(A) ⟶ 𝔹_{A}^{k} ⟶ 𝔹

by putting

mod_{A}^{k+1}(♢_{k}σ)(Ω) := \begin{cases}⋁_{ω∈Unit(Ω)}mod_{A}(σ)(ω) & if k = 2 \\ ⋁_{ω∈Unit(Ω)}mod_{A}^{k}(σ)(ω) & if k > 2 \end{cases}

mod_{A}^{k+1}(□_{k}σ)(Ω) := \begin{cases}⋀_{ω∈Unit(Ω)}mod_{A}(σ)(ω) & if k = 2 \\ ⋀_{ω∈Unit(Ω)}mod_{A}^{k}(σ)(ω) & if k > 2 \end{cases}

for all Ω ∈ 𝔹_{A}^{k} and σ ∈ \begin{cases}Pfm (A) & if k = 2 \\ Pfm^{k−1}(A) & if k > 2 \end{cases}

mod_{A}^{k+1}(¬_{k}φ)(Ω) := -mod_{A}^{k+1}(φ)(Ω)
mod_{A}^{k+1}([ φ_{1} ∧_{k} … ∧_{k} φ_{n} ])(Ω) := ∧^{n}_{i=1}mod_{A}^{k+1}(φ_{i})(Ω)
mod_{A}^{k+1}([ φ_{1} ∨_{k} … ∨_{k} φ_{n} ])(Ω) := ∨^{n}_{i=1}mod_{A}^{k+1}(φ_{i})(Ω)

for all Ω ∈ 𝔹_{A}^{k} and φ, φ_{1}, …, φ_{n} ∈ Pfm^{k}(A).

3.3 The foundation problem and its solution

3.3.1

We now have a syntactical hierarchy of higher–degree propositional formulas and a parallel semantical hierarchy of bit tables, as displayed in the diagramm of 3.2.6. But something is not perfect, yet. Its first level Pfm (A) itself doesn’t fit in entirely and is asking for the possibilities of a more elegant design.

Consider the picture from 3.2.5 again

[figure: A; Pfm(A); Pfm^{2}(A); Pfm^{3}(A); Pfm^{4}(A); ⋮; ([ ]); ♢_{2}, □_{2}; ♢_{3}, □_{3}; ♢_{4}, □_{4}; ♢_{5}, □_{5}; ∧ , ∨ , ¬; ∧_{2} , ∨_{2} , ¬_{2}; ∧_{3} , ∨_{3} , ¬_{3}; ∧_{4} , ∨_{4} , ¬_{4}]

When we replace the atom formula symbol “([ ])” by “♢_{1}” and

“□_{1}”, we obtain a much more elegant syntax. With new names

“𝔽_{A}^{k}” for the formula sets this is:

[figure: 𝔽_{A}^{0}; 𝔽_{A}^{1}; 𝔽_{A}^{2}; 𝔽_{A}^{3}; 𝔽_{A}^{4}; ⋮; ♢_{1}, □_{1}; ♢_{2}, □_{2}; ♢_{3}, □_{3}; ♢_{4}, □_{4}; ♢_{5}, □_{5}; ∧_{1} , ∨_{1} , ¬_{1}; ∧_{2} , ∨_{2} , ¬_{2}; ∧_{3} , ∨_{3} , ¬_{3}; ∧_{4} , ∨_{4} , ¬_{4}]

For every degree k we have a translator τ^{k},

[figure: ⋮; Pfm^{3}(A); Pfm^{2}(A); Pfm(A); A; ⋮; 𝔽_{A}^{3}; 𝔽_{A}^{2}; 𝔽_{A}^{1}; 𝔽_{A}^{0}; τ^{3}; τ^{2}; τ^{1}; id]

and all these τ^{k} are “natural” or “conservative” in the sense that they translation conjunctions into conjunctions, negations into negations etc. In other words, all these translations are determined by the atomic translator, which tells us how the atomic formulas “([a])” in Pfm (A) are translated into 𝔽_{A}^{1}.

Together with this quest for a modification of the syntax goes a change in semantics. Recall the semantical hierarchy so far:

[figure: 𝔹_{A}^{1}; ↭; ⊧_{A}; Pfm (A); 𝔹_{A}^{2}; ↭; ⊧_{A}^{2}; Pfm^{2}(A); 𝔹_{A}^{3}; ↭; ⊧_{A}^{3}; Pfm^{3}(A); ⋮; ⋮; mod_{A}; mod_{A}^{3}; mod_{A}^{4}]

which is defined recursively as well. Does this hierarchy have a nicer foundation, more systematically built on one level lower?

[figure: 𝔹_{A}^{0}; ↭; ⊧_{A}^{0}; 𝔽_{A}^{0}; 𝔹_{A}^{1}; ↭; ⊧_{A}^{1}; 𝔽_{A}^{1}; 𝔹_{A}^{2}; ↭; ⊧_{A}^{2}; 𝔽_{A}^{2}; 𝔹_{A}^{3}; ↭; ⊧_{A}^{3}; 𝔽_{A}^{3}; ⋮; ⋮; mod_{A}^{1}; mod_{A}^{2}; mod_{A}^{3}; mod_{A}^{4}]

It would be nice to have a system where all this fits together. We call this quest the “foundation problem” and we will see, that it has a very nice solution. But first of all, let us work out the definitions for a proper statement of the problem in 3.3.6.

3.3.2 Definition

Given a set A and k ∈ ℕ. The \underline{hyper–propositional formula} set on (\underline{carrier}) A and (\underline{degree}) k, written

𝔽_{A}^{k}

is recursively defined as follows: ♣ If k = 0 then 𝔽_{A}^{0} := A.

♣ If k ≥ 1 we define 𝔽_{A}^{k} to comprise the following expressions:

\begin{matrix}\begin{matrix}♢_{k}σ \\ □_{k}σ \end{matrix} \} & for & σ ∈ 𝔽_{A}^{k−1} \\ \begin{matrix}¬_{k}φ \\ [ φ_{1} ∧_{k} … ∧_{k} φ_{n} ] \\ [ φ_{1} ∨_{k} … ∨_{k} φ_{n} ] \end{matrix} \} & for & φ, φ_{1}, …, φ_{n} ∈ 𝔽_{A}^{k} \end{matrix}

3.3.3 Definition

An \underline{atomic model relation} on a given set A is a relation

ρ : A ↭ A

Each such atomic model relation ρ induces a \underline{k–degree model relation} of ρ

⊧_{ρ}^{k} : 𝔹_{A}^{k} ↭ 𝔽_{A}^{k}

for every k ∈ ℕ, which is recursively defined as follows: ♣ If k = 0 then

α ⊧_{ρ}^{0} φ iff α ρ φ

for every α ∈ 𝔹_{A}^{0} = A and φ ∈ 𝔽_{A}^{0} = A ♣ If k > 0 then

Ω ⊧_{ρ}^{k} ♢_{k}σ iff ω ⊧_{ρ}^{k−1} σ for some ω ∈ Unit (Ω)
Ω ⊧_{ρ}^{k} □_{k}σ iff ω ⊧_{ρ}^{k−1} σ for all ω ∈ Unit (Ω)
Ω ⊧_{ρ}^{k} ¬_{k}φ iff Ω |̸=_{A}^{k} φ

Ω ⊧_{ρ}^{k} [ φ_{1} ∧_{k} … ∧_{k} φ_{n} ] iff Ω ⊧_{ρ}^{k} φ_{i} for all i
Ω ⊧_{ρ}^{k} [ φ_{1} ∨_{k} … ∨_{k} φ_{n} ] iff Ω ⊧_{ρ}^{k} φ_{i} for some i

for all Ω ∈ 𝔹_{A}^{k}, all σ ∈ 𝔽_{A}^{k−1} and φ, φ_{1}, …, φ_{n} ∈ 𝔽_{A}^{k−1}

3.3.4 Definition

An \underline{atomic translator} of a given set A is a function

τ : A ⟶ 𝔽_{A}^{1}

Each such atomic translator τ induces a \underline{k–degree translator} of τ

τ^{k} : Pfm^{k}(A) ⟶ 𝔽_{A}^{k}

for every k ≥ 1, which is recursively defined as follows: ♣ If k = 1 then

\begin{aligned}τ^{1} (([a])) & := & τ(a) \\ τ^{1} (¬φ) & := & ¬_{1}τ^{1} (φ) \\ τ^{1} ([ φ_{1} ∧ … ∧ φ_{n} ]) & := & [ τ^{1} (φ_{1}) ∧_{1} … ∧_{1} τ^{1} (φ_{n}) ] \\ τ^{1} ([ φ_{1} ∨ … ∨ φ_{n} ]) & := & [ τ^{1} (φ_{1}) ∨_{1} … ∨_{1} τ^{1} (φ_{n}) ] \end{aligned}

♣ If k ≥ 2 then

\begin{aligned}τ^{k} (♢_{k}σ) & := & ♢_{k}τ^{k−1}(σ) \\ τ^{k} (□_{k}σ) & := & □_{k}τ^{k−1}(σ) \\ τ^{k} (¬_{k}φ) & := & ¬_{k}τ^{k} (φ) \\ τ^{k} ([ φ_{1} ∧_{k} … ∧_{k} φ_{n} ]) & := & [ τ^{k} (φ_{1}) ∧_{k} … ∧_{k} τ^{k} (φ_{n}) ] \\ τ^{k} ([ φ_{1} ∨_{k} … ∨_{k} φ_{n} ]) & := & [ τ^{k} (φ_{1}) ∨_{k} … ∨_{k} τ^{k} (φ_{n}) ] \end{aligned}

3.3.5 Example

An example of an atom translation is given by

τ := [ \begin{matrix}A ⟶ 𝔽_{A}^{1} \\ a ↦ ♢_{1}a \end{matrix} ]

If we take example 3.2.4 again, where φ ∈ Pfm^{4}(A) was given by

φ = ♢_{4}[ ¬_{3}□_{3}[ ♢_{2}[ a ∧ ¬b] ∨_{2} □_{2}[ c ∧ ¬a] ] ∧_{3} □_{3}♢_{2}[ a ∨ [ ∧] ] ]

then the translation τ^{4}(φ) ∈ 𝔽_{A}^{4} is

♢_{4}[ ¬_{3}□_{3}[ ♢_{2}[ ♢_{1}a ∧_{1} ¬_{1}♢_{1}b] ∨_{2} □_{2}[ ♢_{1}c ∧_{1} ¬_{1}♢_{1}a] ] ∧_{3} □_{3}♢_{2}[ ♢_{1}a ∨_{1} [ ∧_{1} ] ] ]

3.3.6 Definition foundation problem

Given some set A. The \underline{foundation problem} is the question, if an atom translator τ and an atomic relation ρ exist, such that

Ω ⊧_{ρ}^{k} τ^{k}(φ) iff Ω ⊧_{A}^{k} φ

for each k ≥ 1 and all Ω ∈ 𝔹_{A}^{k} and φ ∈ Pfm^{k}(A).

3.3.7 Fact the solution of the foundation problem

The foundation problem has a solution, given by the atomic translator

t : A ⟶ 𝔽_{A}^{1} with t (a) := ♢_{1}a for all a ∈ A

and the identity on A as the atomic model relation, i.e.

id : A ↭ A with id (a) = a for all a ∈ A

3.4 The final version of hyper– propositional logic

3.4.1 Definition

For every set A and each k ∈ ℕ we define a system of \underline{hyper–propositional logic} of (\underline{carrier}) A and (\underline{degree}) k as follows:

(1) Syntax:

The hyper–propositional formula set 𝔽_{A}^{k} was defined in 3.3.2.

(2) Interpretation structure: The \underline{model relation} (of k and A)

⊧_{A}^{k} : 𝔹_{A}^{k} ↭ 𝔽_{A}^{k}

is defined by

Ω ⊧_{A}^{k} φ iff Ω ⊧_{id}^{k} φ for all Ω ∈ 𝔹_{A}^{k} and φ ∈ 𝔽_{A}^{k}

According to 2.1.3, this also provides us, for every φ ∈ 𝔽_{A}^{k}, with the definition of the \underline{model class}

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

and a \underline{model function} or \underline{super–model}

mod_{A}^{k+1}(φ) := [ \begin{matrix}𝔹_{A}^{k} ⟶ 𝔹 \\ Ω ↦ \begin{cases}1 & if Ω ⊧_{A}^{k} φ \\ 0 & else \end{cases} \end{matrix} ]

(3) Quasi–boolean order: According to 2.1.4, we also have a \underline{subvalence} and \underline{equivalence} relation on 𝔽_{A}^{k}, defined by

φ ⇒_{A}^{k} ψ iff ∀Ω ∈ 𝔹_{A}^{k} . (Ω ⊧_{A}^{k} φ implies Ω ⊧_{A}^{k} ψ)
φ ⇔_{A}^{k} ψ iff ∀Ω ∈ 𝔹_{A}^{k} . (Ω ⊧_{A}^{k} φ iff Ω ⊧_{A}^{k} ψ)

(4) Quasi–boolean lattice of formulas According to 2.1.5 and similar to the default propositional formula 𝔓𝔣𝔪A we define the \underline{default hyper–propositional formula algebra} of A and k as

𝔉_{A}^{k} := ⟨𝔽_{A}^{k}, ⇒_{A}^{k}, ⇔_{A}^{k}, f^{k}, t^{k}, ∧^{k}, ∨^{k}, ¬^{k}⟩

where

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

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

¬^{k}φ := ¬_{k}φ

3.4.2 Fact

For every set A and k ≥ 1, ♣ 𝔉_{A}^{k} is a quasi–boolean algebra

♣ mod_{A}^{k+1} is an embedding of 𝔉_{A}^{k} into 𝔅_{A}^{k+1}

3.4.3 Fact

For each set A holds: t^{1} : Pfm (A) ↪ 𝔽_{A}^{1}, i.e. t^{1} is an embedding of 𝔓𝔣𝔪A into 𝔉_{A}^{1}.

3.4.4 Remark

In figure 6 we summarize the syntax and semantics of hyper– propositional logic. Figure 5 was a summarized repetition of the syntax and semantics of traditional logic. Figure 7 repeats 3.4.3.

Figure 6: 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.

Figure 7: Embedding traditional propositional into hyper–propositional logic

\underline{Definition} For every set A we put

t^{1} := [ \begin{matrix}& Pfm (A) ⟶ 𝔽_{A}^{1} \\ [ & \begin{matrix}([a]) ↦ & ♢_{1}a \\ ¬σ ↦ & ¬_{1}t^{1}(σ) \\ [ σ_{1} ∧ … ∧ σ_{n} ] ↦ & [ t^{1}(σ_{1}) ∧_{1} … ∧_{1} t^{1}(σ_{n}) ] \\ [ σ_{1} ∨ … ∨ σ_{n} ] ↦ & [ t^{1}(σ_{1}) ∨_{1} … ∨_{1} t^{1}(σ_{n}) ] \end{matrix} & ] \end{matrix} ]

\underline{Theorem} t^{1} : 𝔓𝔣𝔪 (A) ↪ 𝔉_{A}^{1} for every set A, i.e. t^{1} is an embedding of 𝔓𝔣𝔪 (A) into 𝔉_{A}^{1}.