A logical concept of meaning

B. Bucephalus May 1997

Contents

1 Basic concepts 4 1.1 Basic mathematical concepts . . . . . . . . . . . . . . . . . . . . 4 1.2 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

1.2.1 Bit values . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.2 Bit variables . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.3 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2.4 The standard example . . . . . . . . . . . . . . . . . . . . 5 1.2.5 Formula spaces . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.6 Formal equality . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.7 Atomic equality . . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.8 Definite formulas . . . . . . . . . . . . . . . . . . . . . . . 6 1.2.9 Normal forms (CNF and DNF) . . . . . . . . . . . . . . . 6 1.2.10 Maximal normal forms (MCNF and MDNF) . . . . . . . 7 1.2.11 Canonic normal forms (CCNF an CDNF) . . . . . . . . . 7 1.2.12 Conventional formal notations . . . . . . . . . . . . . . . 8

1.3 Evaluations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

1.3.1 Evaluation of definite formulas . . . . . . . . . . . . . . . 9 1.4 Valuations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

1.4.1 Valuations . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4.2 Valuation spaces . . . . . . . . . . . . . . . . . . . . . . . 10 1.4.3 Ordinal numbers of finite valuations . . . . . . . . . . . . 10 1.4.4 Valuation of a formula . . . . . . . . . . . . . . . . . . . . 11 1.4.5 Definite and minimal definite valuations . . . . . . . . . . 11 1.4.6 Zero and unit valuations . . . . . . . . . . . . . . . . . . . 11 1.4.7 Contradictions and tautologies . . . . . . . . . . . . . . . 12 1.4.8 Decision algorithms . . . . . . . . . . . . . . . . . . . . . 12 1.4.9 Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.4.10 Finite valuations as literal conjunctions . . . . . . . . . . 14 1.4.11 The CDNF of a formula . . . . . . . . . . . . . . . . . . . 14 1.4.12 CDNF’s and sets of valuations . . . . . . . . . . . . . . . 14

1.5 Tables and double tables . . . . . . . . . . . . . . . . . . . . . . . 15 1.5.1 Tables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.5.2 Double tables . . . . . . . . . . . . . . . . . . . . . . . . . 16

1.6 Propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.6.1 Equivalence and propositional equality . . . . . . . . . . . 17 1.6.2 Propositions . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.6.3 Proposition spaces . . . . . . . . . . . . . . . . . . . . . . 18

1.7 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 1.7.1 Bi-equivalence and theoretic equality . . . . . . . . . . . . 18 1.7.2 Thories and pseudo theories . . . . . . . . . . . . . . . . . 19 1.7.3 Theory spaces . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.7.4 Valent and invalent atoms . . . . . . . . . . . . . . . . . . 20

1.8 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 1.8.1 Pseudo messages and messages . . . . . . . . . . . . . . . 22 1.8.2 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 1.8.3 Assertion spaces . . . . . . . . . . . . . . . . . . . . . . . 22 1.8.4 Satisfiable and absolute satisfiable assertions . . . . . . . 23 1.8.5 Subvalence and derivation . . . . . . . . . . . . . . . . . . 24 1.8.6 Truth values . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.8.7 The truth function . . . . . . . . . . . . . . . . . . . . . . 24

2 Atom expansion and reduction 25 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.2 Atom expansion . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.3 Atom reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.4 An example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.5 Conjuntive atom reduction . . . . . . . . . . . . . . . . . . . . . 27 2.6 Disjuntive atom reduction . . . . . . . . . . . . . . . . . . . . . . 27

3 Theory intervals and vector schemes 29 3.1 The subvalence as an order relation . . . . . . . . . . . . . . . . . 29 3.2 Relative and absolute minima and maxima . . . . . . . . . . . . 29 3.3 Theory intervals . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.4 Vector schemes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.5 Intersection sets of theory intervals . . . . . . . . . . . . . . . . . 32

4 Opposition, verification, and definition 34 4.1 Basic concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.1.1 Opposition . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.1.2 Verifications . . . . . . . . . . . . . . . . . . . . . . . . . . 35 4.1.3 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . 36

4.2 Verification and definition theories . . . . . . . . . . . . . . . . . 37 4.2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.2.2 Verification and definition theories . . . . . . . . . . . . . 37 4.2.3 Each definition theory is a verification theory . . . . . . . 38 4.2.4 Only assertions are verifiable and defineable . . . . . . . . 38

4.3 Numbers of verification and definition theories . . . . . . . . . . 39 4.3.1 Bounds . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 4.3.2 The existence of verification theories . . . . . . . . . . . . 39 4.3.3 The non–uniqueness of verification theories . . . . . . . . 40 4.3.4 The non–existence of definition theories . . . . . . . . . . 40 4.3.5 The non–uniqueness of definition theories . . . . . . . . . 40

4.4 Criteria for verification . . . . . . . . . . . . . . . . . . . . . . . . 41 4.4.1 Construction of verification theories . . . . . . . . . . . . 41 4.4.2 An example . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.4.3 Minimal and maximal verification theories . . . . . . . . . 43 4.4.4 The main lemma of verification . . . . . . . . . . . . . . . 44

4.5 Criteria for definition . . . . . . . . . . . . . . . . . . . . . . . . . 44 4.5.1 Construction of definition theories . . . . . . . . . . . . . 44 4.5.2 Two examples . . . . . . . . . . . . . . . . . . . . . . . . 46 4.5.3 Minimal and maximal definition theories and a criterion

for defineability . . . . . . . . . . . . . . . . . . . . . . . . 47 4.5.4 The main lemma of definition . . . . . . . . . . . . . . . . 48

5 Meaning 50 5.1 Meaning functions . . . . . . . . . . . . . . . . . . . . . . . . . . 50 5.2 The true meaning function . . . . . . . . . . . . . . . . . . . . . . 50

5.2.1 The true meaning function . . . . . . . . . . . . . . . . . 50 5.2.2 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 5.2.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

5.3 The absolute satisfying meaning function . . . . . . . . . . . . . 54 5.3.1 The absolute satisfying meaning function . . . . . . . . . 54 5.3.2 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 5.3.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

5.4 Meaning functions on messages . . . . . . . . . . . . . . . . . . . 58

Chapter 1

Basic concepts

1.1 Basic mathematical concepts

A set is a collection of it’s elements. As usual the set parentheses { and } and the element symbol ∈ in an expression x ∈ y are used to express that the element x is a member of the set y. The empty set is denoted by {}. Let x and y be sets, then the following denotations will be used

— x ∪ y for the union set of x and y,

— x ∩ y for the intersection set of x and y,

— x \ y for the subtraction set of x and y,

— x = y means that the sets x and y contain exactly the same elements,

— x ⊆ y means that each element of x is also an element of y, in which case x is said to be a subset of y.

⋃_{i} x_{i} denotes the union set of all sets x_{i}. card(x) denotes the number of elements in the set x. If card(x) is a natural number, the set x is called finite, otherwise infinite. A tupel (x_{0}, ..., x_{n−1}) is an ordered finite set of elements x_{0}, ..., x_{n−1} where n ≥ 0. For n = 2 the tupel is called a pair, for n = 3 a tripel.

1.2 Formulas

1.2.1 Bit values

A bit value is eiter the zero bit 0 or the unit bit 1.

1.2.2 Bit variables

Bit variables will be denoted by capital (possibly indexed) letters: A, A_{0}, A_{1}, A_{2}, ..., B, ..., C, ..., D, ...

Any expression will be permitted as an index. But since expressions shall not be formally defined here, the strict reader might choose the set of integers, rational or real numbers as the index set. B then denotes the set of all bit variables. Besides it will be presupposed that B can be lineary ordered and that < in connection with bit variables denotes a linear order relation on B. For two bit variables A_{0} and A_{1} with A_{0} < A_{1} it is said that A_{0} is (lexically) smaller than A_{1}.

1.2.3 Formulas

A formula is an expression defined as follows:

— Any bit value is a formula.

— Any bit variable is a formula and is then called an atomic formula or atom in short.

— For formulas α, α_{0}, ..., α_{n−1} the following expressions are formulas too:

¬α the negation of α,

(∧ α_{0} ... α_{n−1}) the conjunction of α_{0}, ..., α_{n−1}, (∨ α_{0} ... α_{n−1}) the disjunction of α_{0}, ..., α_{n−1}, (α_{1} → α_{2}) the subjunction of α_{1} and α_{2}, (α_{1} ↔ α_{2}) the equijunction of α_{1} and α_{2}.

It follows from the definition that

— the empty conjunction (∧),

— the empty disjunction (∨),

— the unary conjunction (∧ α_{0}),

— the unary disjunction (∨ α_{0}) are formulas as well. In the sequel formulas will be denoted by small greek (possibly indexed) letters:

α, α_{0}, α_{1}, α_{2}, ..., β, ..., γ, ..., δ, ... Let α be a formula, then

Atoms(α) denotes the set of all bit variables occuring in α.

1.2.4 The standard example

For example

(∧ ¬(∧ R S) (W ↔ (∨ R S)) (R → H) (S → ¬H)) is a formula which frequently will be used as a standard example and shall be abbreviated by θ_{w}. Then there is

Θ_{w} := Atoms(θ_{w}) = {H, R, S, W } (For an intuitive interpretation of the standard example see the introduction.)

1.2.5 Formula spaces

Let Φ ⊆ B be a set of bit variables, then

F ormΦ is the set of all formulas α with Atoms(α) ⊆ Φ. F ormΦ is called the formula space on Φ. For any Φ ⊆ B the cardinal card(F ormΦ) is infinite.

1.2.6 Formal equality

Two formulas α_{1} and α_{2} are said to be formally equal, written

α_{1} = α_{2} if and only if they are identic expressions, that means they are conform as written signs.

1.2.7 Atomic equality

Two formulas α_{1} and α_{2} are said to be atomically equal if and only if Atoms(α_{1}) = Atoms(α_{2})

1.2.8 Definite formulas

A formula α is called definite if Atoms(α) = {}. An example would be

((∧ ¬0 1 0) → (∨ 1 ¬1)) So F orm{} is the set of all definite formulas.

1.2.9 Normal forms (CNF and DNF)

A literal is either

— a positive literal, that is a bit variable, or

— a negative literal, that is a negated bit variable. A literal conjunction is a conjunction of literals. A literal disjunction is a disjunction of literals. A conjunctive normal form (CNF) is a conjunction of literal disjunctions. A disjunctive normal form (DNF) is a disjunction of literal consjunctions. Examples are

— (∧ (∨ ¬A B C) (∨ A ¬B) (∨ A ¬C)) is a CNF

— (∧) is a CNF

— (∧ (∨) (∨)) is a CNF

— (∨ (∧ ¬A B C) (∧ A ¬B) (∧ A ¬C)) is a DNF

— (∨) is a DNF

— (∨ (∧) (∧)) is a DNF

1.2.10 Maximal normal forms (MCNF and MDNF)

Let Φ = {A_{0}, ..., A_{n−1}} be a set of bit variables and {λ_{0}, ..., λ_{m−1}} be a set of literals. The literal conjunction (∧ λ_{0} ... λ_{m−1}) and the literal disjunction (∨ λ_{0} ... λ_{m−1}) are called maximal according to Φ, if n = m and

Atoms((∧ λ_{0} ... λ_{m−1})) = Atoms((∨ λ_{0} ... λ_{m−1})) = {A_{0}, ..., A_{n−1}}. A CNF or DNF α is called a maximal conjunctive normal form (MCNF) or maximal disjunctive normal form (MDNF) respectively, if all literal conjunctions or disjunctions are maximal according to Atoms(α). Examples are:

— (∧ (∨ ¬A B ¬C) (∨ ¬A ¬C B) (∨ A B ¬C)) is a MCNF

— (∧) is a MCNF

— (∧ (∨) (∨)) is a MCNF

— (∨ (∧ ¬A B ¬C) (∧ ¬A ¬C B) (∧ A B ¬C)) is a MDNF

— (∨) is a MDNF

— (∨ (∧) (∧)) is a MDNF

1.2.11 Canonic normal forms (CCNF an CDNF)

A canonic normal form is a maximal normal form, wherein the literals and literal conjunctions or disjunctions are ordered in an unequivocal way which shall further be described. Let λ_{0}, ..., λ_{m−1} be literals with {A_{0}} = Atoms(λ_{0}), ..., A_{n−1} = Atoms(λ_{n−1}) and let A_{0} < ... < A_{n−1}. Then the literal conjunction (∧ λ_{0} ... λ_{n−1}) and the literal disjunction (∨ λ_{0} ... λ_{n−1}) are ordered. (Empty and unary literal conjunctions and disjunctions are ordered as well.) For a literal λ let

litbit(λ) := \{ \begin{matrix}1 & if λ is a positive literal \\ 0 & if λ is a negative literal \end{matrix}

Let

— (∧ λ_{0} ... λ_{n−1}) and (∧ μ_{0} ... μ_{n−1}) be ordered literal conjunctions,

— (∨ λ_{0} ... λ_{n−1}) and (∨ μ_{0} ... μ_{n−1}) be ordered literal disjunctions, so that

{A_{0}} = Atoms(λ_{0}) = Atoms(μ_{0}), ...,
{A_{n−1}} = Atoms(λ_{n−1}) = Atoms(μ_{n−1})

then it is said that

— (∧ λ_{0} ... λ_{n−1}) is smaller than (∧ μ_{0} ... μ_{n−1}), written as (∧ λ_{0} ... λ_{n−1}) < (∧ μ_{0} ... μ_{n−1}) and

— (∨ λ_{0} ... λ_{n−1}) is smaller than (∨ μ_{0} ... μ_{n−1}), written as (∨ λ_{0} ... λ_{n−1}) < (∨ μ_{0} ... μ_{n−1})

when the condition

∑_{i=0}^{n−1} litbit(λ_{i}) · 2^{i} < ∑_{i=0}^{n−1} litbit(μ_{i}) · 2^{i} holds in which the bit variables 0 and 1 are used as the arithmetic 0 and 1 respectively.

Let κ be a MCNF, so it has the form (∧δ_{0}...δ_{m−1}) where the δ_{0}, ..., δ_{m−1} are zero or more literal disjunctions, which are all maximal according to Atoms(κ). Then κ is a canonic conjunctive normal form (CCNF), when the following conditions are satisfied:

— Each of the δ_{0}, ..., δ_{m−1} is an ordered literal disjunction.

— δ_{0} < ... < δ_{m−1}. Let δ be a MDNF, so it has the form (∨ κ_{0} ... κ_{m−1}) where the κ_{0}, ..., κ_{m−1} are zero or more literal conjunctions, which are all maximal according to Atoms(δ). Then δ is a canonic disjunctive normal form (CDNF), when the following conditions are satisfied:

— Each of the κ_{0}, ..., κ_{m−1} is an ordered literal conjunction.

— κ_{0} < ... < κ_{m−1}. For a finite set Φ of bit variables

— CCNF Φ denotes the set of all canonic conjunctive normal forms on Φ, that is the set of all CCNF’s of the form (∧δ_{0} ...δ_{m−1}), where the (possibly zero) literal disjunctions δ_{0}, ..., δ_{m−1} are maximal according to Φ.

— CDNF Φ denotes the set of all canonic disjunctive normal forms on Φ, that is the set of all CDNF’s of the form (∨κ_{0}...κ_{m−1}), where the (possibly zero) literal conjunctions κ_{0}, ..., κ_{m−1} are maximal according to Φ.

Note that for any bit variable set Φ

— (∧) ∈ CCNF Φ and

— (∨) ∈ CDNF Φ. There is for any bit variable set Φ

— card(CCNF Φ) = 2^{2^{card(Φ)}},

— card(CDNF Φ) = 2^{2^{card(Φ)}}.

1.2.12 Conventional formal notations

Conjunctions (∧α_{0}...α_{n−1}) and disjunctions (∨α_{0}...α_{n−1}) are commonly written in infix notation as (α_{0} ∧ ... ∧ α_{n−1}) and (α_{0} ∨ ... ∨ α_{n−1}) if n ≥ 2. To save parentheses and to increase readability it is commonly declared that in the list of the so-called junctors

¬ ∧ ∨ → ↔ each junctor standing more left binds stronger than anyone standing more right of it. For example

¬A ∧ 1 ∧ ¬C → D ∨ A ∧ 0 ↔ ¬A ∨ B is an abbreviated notation for

(((¬A ∧ 1 ∧ ¬C) → (D ∨ (A ∧ 0))) ↔ (¬A ∨ B)) In an expression like α → β → γ putting parentheses goes from left to right ((α → β) → γ). A negative literal ¬A is commonly written as \overline{A}. A literal conjunction (∧ λ_{0} λ_{1} ... λ_{m−1}) with at least one literal is written as λ_{0}λ_{1}...λ_{m−1}. So a DNF which is not the empty disjunction, for example

(∨ (∧ ¬A B ¬C) (∧ C) (∧ ¬A ¬B) (∧ A ¬B ¬C)) is usually written in the shorter version

\overline{A}B\overline{C} ∨ C ∨ \overline{A}\overline{B} ∨ A\overline{B}\overline{C} It should be emphasized that these conventions are introduced only to increase readability and that the abbreviated formulas do not belong to the calculus. A formula in it’s original and in an abbreviated notation are considered as being formally equal.

1.3 Evaluations

1.3.1 Evaluation of definite formulas

Let α ∈ F orm{} be a definite formula. The evaluation

eval(α) of α is the bit value, that results from the recursive application of the following instuctions:

— eval(0) := 0

— eval(1) := 1

— eval(¬α) := \{ \begin{matrix}0 & if eval(α) = 1 \\ 1 & if eval(α) = 0 \end{matrix}

— eval((∧ α_{0} ... α_{n−1})) := \{ \begin{matrix}0 & if 0 ∈ \{eval(α_{0}), ..., eval(α_{n−1})\} \\ 1 & else \end{matrix}

— eval((∨ α_{0} ... α_{n−1})) := \{ \begin{matrix}1 & if 1 ∈ \{eval(α_{0}), ..., eval(α_{n−1})\} \\ 0 & else \end{matrix}

— eval((α → β)) := \{ \begin{matrix}0 & if eval(α) = 0 and eval(β) \\ 1 & else \end{matrix}

— eval((α ↔ β)) := \{ \begin{matrix}1 & if eval(α) = eval(β) \\ 0 & else \end{matrix}

For example eval(((∧ ¬0 1 0) → (∨ 1¬1))) = eval(((∧ 1 1 0) → (∨ 1 0))) = eval((0 → 1)) = 1

By virtue of that definition there is

— eval((∧)) = 1

— eval((∨)) = 0 In other words

— 1 is the neutral element of conjunction and

— 0 is the neutral element of disjunction.

1.4 Valuations

1.4.1 Valuations

Let Φ be a set of bit variables. A valuation of Φ is a function, which assigns a bit value to any of the bit variables of Φ. Φ is then called the valuation domain of that valuation. Usually ω is used to denote a valuation. A valuation ω of Φ is called finite, if Φ is finite. Otherwise ω is called infinite. If Φ = {A_{0}, ..., A_{n−1}} is finite and A_{0} < ... < A_{n−1}, a valuation ω of Φ is written as

ω = {A_{0}/a_{0}, ..., A_{n−1}/a_{n−1}}

where a_{i} = ω(A_{i}) for i = 0, ..., n − 1. The (only) valuation of the empty set {} of bit variables is consequently also written as {} and is called the empty valuation.

1.4.2 Valuation spaces

For a set Φ of bit variables

V al(Φ) or simply V alΦ denotes the valuation space on Φ, that is the set of all valuations with Φ as their valuation domain. Besides let

V al∞ := ⋃_{Φ⊆B} V alΦ. For a formula α the valuation space of α is defined as

V al(α) := V al(Atoms(α)). So if α is a definite formula

V al(α) = V al{} = {{}}. For any (especially finite) set Φ of bit variables

card(V alΦ) = 2^{card(Φ)}.

1.4.3 Ordinal numbers of finite valuations

Let Φ = {A_{0}, ..., A_{n−1}} be a finite number of bit variables with A_{0} < ... < A_{n−1}. For ω ∈ V alΦ and o ∈ {0, 1, ..., 2^{n} − 1} the equation

o = ∑_{i=1}^{n−1} ω(A_{i}) · 2^{i} where each bit value ω(A_{i}) is interpreted as the arithmetic 0 or 1 respectively, defines a one-to-one mapping between V alΦ and {0, 1, ..., 2^{n} − 1}. This defines a numbering and order on V alΦ. For example for n = 3 and Φ = {A_{0}, A_{1}, A_{2}} this correspondence is

\begin{matrix}o & ω \\ 0 & \{A_{0}/0, A_{1}/0, A_{2}/0\} \\ 1 & \{A_{0}/1, A_{1}/0, A_{2}/0\} \\ 2 & \{A_{0}/0, A_{1}/1, A_{2}/0\} \\ 3 & \{A_{0}/1, A_{1}/1, A_{2}/0\} \\ 4 & \{A_{0}/0, A_{1}/0, A_{2}/1\} \\ 5 & \{A_{0}/1, A_{1}/0, A_{2}/1\} \\ 6 & \{A_{0}/0, A_{1}/1, A_{2}/1\} \\ 7 & \{A_{0}/1, A_{1}/1, A_{2}/1\} \end{matrix}

According to this mapping for each pair of o and ω

— o is called the ordinal number of ω, written as o = ord(ω),

— ω is called the o-th valuation of Φ or V alΦ, written as ω = val(o, Φ).

1.4.4 Valuation of a formula

Let ω be a valuation and α be a formula.

subst(α, ω) denotes the formula, which results from α by replacing each bit variable A in α, occuring in the valuation domain of ω, by ω(A). For instance for

ω = {A/1, B/0, C/1} and

α = (A ∧ 0) ∨ (¬D ∧ (B → C))

there is

subst(α, ω) = (1 ∧ 0) ∨ (¬D ∧ (0 → 1)).

1.4.5 Definite and minimal definite valuations

Let ω be a valuation with the valuation domain Φ_{1} and α a formula with Φ_{2} := Atoms(α). ω is called

— definite for α (or for Φ_{2}) if Φ_{2} ⊆ Φ_{1}, and

— minimal definite for α (or for Φ_{2}) if Φ_{2} = Φ_{1}. Thus ω is definite for α if and only if subst(α, ω) is a definite formula, and minimal definite for α if and only if ω ∈ V al(α).

1.4.6 Zero and unit valuations

Let ω be a valuation and α a formula. ω is called a

— zero valuation for α, if ω is definite for α and eval(subst(α, ω)) = 0,

— unit valuation for α, if ω is definite for α and eval(subst(α, ω)) = 1.

Zeroval(α) denotes the set of all minimal definite zero valuations for α. Unitval(α) denotes the set of all minimal definite unit valuations for α. For any formula α there is

— Zeroval(α) ∪ Unitval(α) = V al(α)

— Zeroval(α) ∩ Unitval(α) = {} For instance for

α = ¬A → B there is

Zeroval(α) = {{A/0, B/0}}
Unitval(α) = {{A/1, B/0}, {A/0, B/1}, {A/1, B/1}}

For

α = 1

there is

Zeroval(α) = {}
Unitval(α) = {{}}

For the standard example

θ_{w} = ¬(R ∧ S) ∧ (W ↔ (R ∨ S)) ∧ (R → H) ∧ (S → ¬H) there is

Unitval(θ_{w}) =
{{H/0, R/0, S/0, W/0}, {H/1, R/0, S/0, W/0},
{H/1, R/1, S/0, W/1}, {H/0, R/0, S/1, W/1}}.

For any set Φ of bit variables and α ∈ F ormΦ let

— Zeroval(α, Φ) := {ω ∈ V alΦ|eval(subst(α, ω)) = 0},

— Unitval(α, Φ) := {ω ∈ V alΦ|eval(subst(α, ω)) = 1}. Thus

— Zeroval(α) = Zeroval(α, Atoms(α))

— Unitval(α) = Unitval(α, Atoms(α))

1.4.7 Contradictions and tautologies

A formula α is a

— contradiction if and only if Zeroval(α) = V al(α)

— tautology if and only if Unitval(α) = V al(α)

A formula α is a contradiction if and only if ¬α is a tautology; and vice versa.

1.4.8 Decision algorithms

Let the function taut defined by

taut(α) := \{ \begin{matrix}1 & if α is a tautology \\ 0 & else \end{matrix}

for any formula α.

This function is efficiently computable as the following algorithm does, by example.

     Algorithm taut(α)
     begin

o := 0 ;

m := 2^{card(Atoms(α))} ; b := 1 ;

        repeat

if eval(subst(α, val(o, Atoms(α)))) = 0

           then b := 0

else o := o + 1

        until b = 0 or o = m ;
        return b ;
     end.

In the sequel for each property of formulas always such kind of decision algorithm will be given. In fact they will all be implemented by means of this algorithm taut. For instance the decision algorithm for contradictions

contr(α) := \{ \begin{matrix}1 & if α is a contradiction \\ 0 & else \end{matrix}

is easily implemented by contr(α) := taut(¬α).

1.4.9 Satisfiability

A non-empty set {α_{0}, ..., α_{n−1}} of formulas is called satisfiable if there is a valuation

ω ∈ V al(Atoms(α_{0}) ∪ ... ∪ Atoms(α_{n−1})) so that

eval(subst(α_{0}, ω)) = ... = eval(subst(α_{n−1}, ω)) = 1.

Otherwise the set is called non-satisfiable. Thus the set {α} of one formula α is satisfiable if and only if α is not a contradiction. In that case the formula α itself is called satisfiable. In a similar way each n–elementary case can be reduced to the simple case, because each non-empty formula set {A_{0}, ..., A_{n−1}} is satisfiable if and only if (∧ α_{0} ... α_{n−1}) is satisfiable. (Consequently the empty set {} could be defined as satisfiable.) The decision algorithm

sat(α_{0}, ..., α_{n−1}) := \{ \begin{matrix}1 & if \{A_{0}, ..., A_{n−1}\} is satisfiable \\ 0 & if \{A_{0}, ..., A_{n−1}\} is non-satisfiable \end{matrix}

can be implemented by

sat(α_{0}, ..., α_{n−1}) := \{ \begin{matrix}0 & if taut(¬(∧ α_{0} ... α_{n−1})) = 1 \\ 1 & if taut(¬(∧ α_{0} ... α_{n−1})) = 0. \end{matrix}

1.4.10 Finite valuations as literal conjunctions

Let ω be a finite valuation with the valuation domain {A_{0}, ..., A_{n−1}}, so that it has the form

ω = {A_{0}/a_{0}, ..., A_{n−1}/a_{n−1}} with bit values a_{0}, ..., a_{n−1}. By the function litconj a literal conjunciton is assigned to each such valuation, namely by

litconj(ω) := (∧ λ_{0} ... λ_{n−1}) where for i := 0, ..., n − 1

λ_{i} := \{ \begin{matrix}A_{i} & if a_{i} = 1 \\ ¬A_{i} & if a_{i} = 0. \end{matrix}

So for instance litconj({A/0, B/1, C/0, D/0, E/1})

= (∧ ¬A B ¬C ¬D E)
= \overline{A}B\overline{C}\overline{D}E.

Let Φ be a finite set of bit variables, then for any ω, ω′ ∈ V alΦ

— litconj(ω) < litconj(ω′) if and only if ord(ω) < ord(ω).

1.4.11 The CDNF of a formula

Let α be a formula and

{ω_{0}, ..., ω_{m−1}} = Unitval(α) with

ord(ω_{0}) < ... < ord(ω_{m−1})

So there is also

litconj(ω_{0}) < ... < litconj(ω_{m−1}) and the formula

(∨ litconj(ω) ... litconj(ω_{m−1})) is a CDNF, called the canonic disjunctive normal form of α or the CDNF of α in short, written as

cdnf(α) For example

— cdnf(θ_{w}) = \overline{H}\overline{R}\overline{S}\overline{W} ∨ H\overline{R}\overline{S}\overline{W} ∨ HR\overline{S}W ∨ \overline{H}\overline{R}SW

— cdnf(1) = (∨ (∧))

— cdnf(0) = (∨)

1.4.12 CDNF’s and sets of valuations

So there is a close connection between sets of valuations and formulas. The CDNF of a formula is unambiguous and identic with the set of unit valuations of the formula, if this set is ordered according to the ordinal number of the valuations. In short,

CDNF’s and sets of valuations can be identified with each other.

(In the introduction valuations were written as literal conjunctions anyway, but furthermore the two notations will be kept separate.)

1.5 Tables and double tables

1.5.1 Tables

Let Φ = {A_{0}, ..., A_{n−1}} be a finite set of bit variables and α ∈ F ormΦ. Then the table of α according to (A_{0}, ..., A_{n−1}) has the following form (where n = 3 is chosen for illustration):

\begin{matrix}A_{0} & A_{1} & A_{n−1} & α \\ 0 & 0 & 0 & †_{0}^{(A_{0},...,A_{n−1})} \\ 1 & 0 & 0 & †_{1}^{(A_{0},...,A_{n−1})} \\ 0 & 1 & 0 & †_{2}^{(A_{0},...,A_{n−1})} \\ 1 & 1 & 0 & †_{3}^{(A_{0},...,A_{n−1})} \\ 0 & 0 & 1 & †_{4}^{(A_{0},...,A_{n−1})} \\ 1 & 0 & 1 & †_{5}^{(A_{0},...,A_{n−1})} \\ 0 & 1 & 1 & †_{6}^{(A_{0},...,A_{n−1})} \\ 1 & 1 & 1 & †_{2^{n}−1}^{(A_{0},...,A_{n−1})} \end{matrix}

On the left side each line represents one of the valuations of {ω_{0}, ..., ω_{2^{n}−1}} = V alΦ.

The right column contains the bit values †_{i}^{α,(A_{0},...,A_{n−1})} for i = 1, ..., 2^{n}−1 where

†_{i}^{α,(A_{0},...,A_{n−1})} := eval(subst(α, val(i, Φ))). The expression

†^{α,(A_{0},...,A_{n−1})} := (†_{0}^{α,(A_{0},...,A_{n−1})} ... †_{2^{n}−1}^{α,(A_{0},...,A_{n−1})}) is called the vector or canonic junctor of α according to (A_{0}, ..., A_{n−1}). Therewith the formula α could unambigiously be written in the form

(†^{α,(A_{0},...,A_{n−1})}, (A_{0}, ..., A_{n−1})) what could be called the canonic junction form of α according to (A_{0}, ..., A_{n−1}). For a formula α the table of α is the table of α according to (A_{0}, ..., A_{n−1}), where A_{0} < ... < A_{n−1} and Atoms(α) = {A_{0}, ..., A_{n−1}}. If the context indicates the full interpretation, the sign †^{α,(A_{0},...,A_{n−1})} is mostly written as †^{α} or simply as †. †^{α,Φ} denotes †^{α,(A_{0},...,A_{n−1})} for {A_{0}, ..., A_{n−1}} = Φ and A_{0} < ... < A_{n−1}. If it is not stated otherwise †^{α} stands for †^{α,Atoms(α)}. For Θ_{w} = {H, R, S, W } with H < R < S < W the table of θ_{w} is the table of θ_{w} according to (H, R, S, W) which is

\begin{matrix}H & R & S & W & θ_{w} \\ 0 & 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 & 0 \\ 1 & 1 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 & 0 \\ 1 & 0 & 1 & 0 & 0 \\ 0 & 1 & 1 & 0 & 0 \\ 1 & 1 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 & 0 \\ 1 & 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 1 & 0 \\ 1 & 1 & 0 & 1 & 1 \\ 0 & 0 & 1 & 1 & 1 \\ 1 & 0 & 1 & 1 & 0 \\ 0 & 1 & 1 & 1 & 0 \\ 1 & 1 & 1 & 1 & 0 \end{matrix}

and the canonic junction form of θ_{w} (according to (H, R, S, W) is ((1100000000011000), (H, R, S, W))

1.5.2 Double tables

Let Φ = {A_{0}, ..., A_{n−1}} and Φ′ = {B_{0}, ..., B_{m−1}} be finite sets of bit variables, Φ ∩ Φ′ = {}, and α ∈ F orm(Φ ∪ Φ′). Often it will be very usefull to demonstrate α not as a table, but rather as the double table of α according to (A_{0}, ..., A_{n−1}) and (B_{0}, ..., B_{m−1}), which has the following form (where n = 3 and m = 2 is chosen for illustration):

α  0  1  0  1  B_{0}
0  0  1  1  B_{m−1}
0 0  0  ‡‡_{0,0}  ‡‡_{0,1}  ‡‡_{0,2}  ‡‡_{0,2^{m}−1}
1 0  0  ‡‡_{1,0}  ‡‡_{1,1}  ‡‡_{1,2}  ‡‡_{1,2^{m}−1}
0 1  0  ‡‡_{2,0}  ‡‡_{2,1}  ‡‡_{2,2}  ‡‡_{2,2^{m}−1}
1 1  0  ‡‡_{3,0}  ‡‡_{3,1}  ‡‡_{3,2}  ‡‡_{3,2^{m}−1}
0 0  1  ‡‡_{4,0}  ‡‡_{4,1}  ‡‡_{4,2}  ‡‡_{4,2^{m}−1}
1 0  1  ‡‡_{5,0}  ‡‡_{5,1}  ‡‡_{5,2}  ‡‡_{5,2^{m}−1}
0 1  1  ‡‡_{6,0}  ‡‡_{6,1}  ‡‡_{6,2}  ‡‡_{6,2^{m}−1}
1 1  1  ‡‡_{2^{n}−1,0} ‡‡_{2^{n}−1,1} ‡‡_{2^{n}−1,2} ‡‡_{2^{n}−1,2^{m}−1}
A_{0} A_{1} A_{n−1}

The left block of bit values contains the valuations ω_{0}, ..., ω_{2^{n}−1} ∈ V alΦ, the upper block of bit values consists of the ω′_{0}, ..., ω′_{2^{m}−1} ∈ V alΦ′. For i = 0, ..., 2^{n} − 1 and j = 0, ..., 2^{m} − 1 the upper right block of bit values

‡‡_{i,j}

or more pecisely

‡‡_{i,j}^{α,(A_{0},...,A_{n−1}),(B_{0},...,B_{m−1})}

or

‡‡_{i,j}^{α,Φ,Φ′} if A_{0} < ... < A_{n−1} and B_{0} < ... < B_{m−1} is the matrix, where

‡‡_{i,j} := eval(subst(subst(α, ω_{i}), ω′_{j})). The double table of θ_{w} according to (R, S) and (H, W) is for instance

θ_{w}  0 1 0 1 H
0 0 1 1 W
0 0 1 1 0 0
1 0 0 0 0 1
0 1 0 0 1 0
1 1 0 0 0 0
R S

and the double table of θ_{w} according to (H, R, S, W) and () has a matrix which is equal to the vector †^{θ_{w},(H,R,S,W)} and that looks like

θ_{w}

0 0 0 0 1
1 0 0 0 1
0 1 0 0 0
1 1 0 0 0
0 0 1 0 0
1 0 1 0 0
0 1 1 0 0
1 1 1 0 0
0 0 0 1 0
1 0 0 1 0
0 1 0 1 0
1 1 0 1 1
0 0 1 1 1
1 0 1 1 0
0 1 1 1 0
1 1 1 1 0
H R S W

1.6 Propositions

1.6.1 Equivalence and propositional equality

Two formulas α_{1} and α_{2} are equivalent or propositionally equal, written as

α_{1} ⇔ α_{2} if and only if

eval(subst(α_{1}, ω)) = eval(subst(α_{2}, ω)) for every valuation ω ∈ V al(Atoms(α_{1}) ∪ Atoms(α_{2})). There is for Φ := Atoms(α_{1}) ∪ Atoms(α_{2}):

α_{1} ⇔ α_{2}

if and only if

Unitval(α_{1}, Φ) = Unitval(α_{2}, Φ) if and only if

Zeroval(α_{1}, Φ) = Zeroval(α_{2}, Φ) if and only if

†^{α_{1},Φ} = †^{α_{2},Φ} if and only if

α_{1} ↔ α_{2} ⇔ 1. The last version motivates for the algorithm

eqval(α_{1}, α_{2}) := \{ \begin{matrix}1 & if α_{1} ⇔ α_{2} \\ 0 & else \end{matrix}

the implementation

eqval(α_{1}, α_{2}) := taut(α_{1} ↔ α_{2}) Besides, if Atoms(α_{1}) = Atoms(α_{2}) there is

α_{1} ⇔ α_{2} if and only if cdnf(α_{1}) = cdnf(α_{2}).

1.6.2 Propositions

The equivalence ⇔ is an equivalence relation on the set F ormB of all formulas and thus entails a partition of F ormB in equivalence classes. For a formula α the proposition of α is

⟨α⟩ := {β|β ∈ F ormB and α ⇔ β}. α is the representing formula or the prososition formula of ⟨α⟩. Two propositions ⟨α_{1}⟩ and ⟨α_{2}⟩ are equal, written as

⟨α_{1}⟩ = ⟨α_{2}⟩ if and only if α_{1} ⇔ α_{2}.

1.6.3 Proposition spaces

For a set Φ of bit variables

P ropΦ := {⟨α⟩|α ∈ F ormΦ} is the proposition space on Φ. There is

card(P ropΦ) = 2^{2^{card(Φ)}}.

1.7 Theories

1.7.1 Bi-equivalence and theoretic equality

Two formulas α_{1} and α_{2} are bi-equivalent or theoretically equal, written as

α_{1} ⇌ α_{2}

if and only if they are propositionally and atomically equal; so if

α_{1} ⇔ α_{2} and Atoms(α_{1}) = Atoms(α_{2}). It is

α_{1} ⇌ α_{2}

if and only if

Unitval(α_{1}) = Unitval(α_{2}) and Zeroval(α_{1}) = Zeroval(α_{2}) if and only if

Φ := Atoms(α_{1}) = Atoms(α_{2}) and †^{α_{1},Φ} = †^{α_{2},Φ}.

1.7.2 Thories and pseudo theories

The bi-equivalence ⇌ again is an equivalence relation on the set F ormB of all formulas. The equivalence classes shall be called theories. For a formula α the theory of α is written and defined by

[α] := {β|β ∈ F ormB and α ⇌ β} where

— α is called the theory formula of [α],

— Atoms[α] := Atoms(α) is the set of theory atoms of [α] and

— ⟨α⟩ is the theory proposition of [α]. Two theories [α_{1}] and [α_{2}] are equal if and only if

— α_{1} ⇌ α_{2} and

— Atoms(α_{1}) = Atoms(α_{2}). Therefore a second, more common definition of theories shall be introduced, in which these two constitutive aspects of a theory are explicitly noted. Instead of being equivalence classes, there the theory is described purely syntactically. A conception that will be preferred by a constructive point of view. Let α be a set of bit variables and α ∈ F ormΦ. Then

[α, Φ] denotes a theory, where

— α is the theory formula of [α, Φ],

— Φ is the set of theory atoms of [α, Φ] and

— ⟨α⟩ is the theory proposition of [α, Φ]. For the relation of this two notations the following holds. Two theories [α_{1}] and [α_{2}, Φ] are equal if and only if

— α_{1} ⇔ α_{2} and

— Atoms(α_{1}) = Φ. For instance, there is

[1, {A}] = [A ∨ ¬A, {A}] = [A ∨ ¬A] ≠ [1]. From now on a theory is mostly written in its standard form [α, Φ], but of course all what is going to be said is independent of the notation. A transformation of the notation [α] into the standard notation is given by the rule

[α] = [α, Atoms(α)] Another abbreviating way of writing is the notation

f[α, Φ] instead of f([α, Φ]) for a function f and a theorie [α, Φ]. A theory [α, Φ] is finite, if Φ is finite and infinite else. Of course only finite theories can be written in the form [α]. From now on it is silently assumed that a theory is always finite. This restriction is not compelling, all concepts that will be developed furthermore can be easily applied to the infinite case. Only the methods and algorithms might have to be transformed, because they might not terminate for the infinite case. For a theory [α, Φ] there is

— Zeroval[α, Φ] := Zeroval(α, Φ) the set of zero valuations and

— Unitval[α, Φ] := Unitval(α, Φ) the set of unit valuations of [α, Φ]. If for an expression [α, Φ] the condition α ∈ F ormΦ is weakened to α ∈ F ormB, the expression [α, Φ] is a pseudo theory. For instance

[A → B, {A, C}] is a pseudo theory, but not a theory.

1.7.3 Theory spaces

For a set Φ of bit variables

T heoΦ := {[α, Φ]|α ∈ F ormΦ} is the theory space on Φ. There is

card(T heoΦ) = 2^{2^{card(Φ)}}. Besides let

T heo∞ := ⋃_{Φ⊆B} T heoΦ.

1.7.4 Valent and invalent atoms

Let α be a formula and A a bit variable. A is invalent for α, if

subst(α, {A/0}) ⇔ subst(α, {A/1}). Otherwise A is valent for α. If additionally A ∈ Atoms(α) holds, A is said to be invalent (or valent) in α. Examples:

— A is invalent for B → C.

— A is invalent in A ∧ 0.

— A is valent in A ∧ 1.

— A is invalent in A ∧ ¬A.

— A is invalent and B is valent in (A ∧ B) ∨ (¬A ∧ B). With double tables this phenomenon can be well demonstrated: A is invalent for α exactly when both columns of the matrix ‡‡^{α,Atoms(α)\{A},{A}} are identic.

In other words, if both rows of the matrix ‡‡^{α,{A},Atoms(α)\{A}} are identic. For instance for α = (A ∧ B) ∨ (¬A ∧ B) the double table of α according to (A) and (B) is

α 0 1 B
0 0 1
(1 0 1) / A

The rows are identic, so A is invalent for α; the columns are different, so B is valent for α. In general: A set Φ of bit variables consists of invalent atoms for a formula α if and only if all columns of the matrix ‡‡^{α,Atoms(α)\Φ,Φ} are identic; in other words, if all the rows of ‡‡^{α,Φ,Atoms(α)\Φ} are identic. A formula α is called atom reduced, if every atom of α is valent in α. For any formula there is an equivalent atom reduced formula. Examples are:

— 0, which is an atom reduced equivalent to A ∧ 0.

— 0 is also an atom reduced equivalent of A ∧ ¬A.

— B is an atom reduced equivalent to (A ∧ B) ∨ (¬A ∧ B). On the other hand, for any formula α and any set Φ of bit variables with Atoms(α) ⊆ Φ there is a formula α′ with α ⇔ α′ and Atoms(α) = Φ. This formula α′ can be constructed for example as

α′ := α ∨ (A_{0} ∧ ¬A_{0}) ∨ ... ∨ (A_{n−1} ∧ ¬A_{n−1}) if {A_{0}, ..., A_{n−1}} = Φ \ Atoms(α). This would also be a rule to transform any finite theory given in the form [α, Φ] into a form [α′] so that [α, Φ] = [α′]. The concept of valent and invalent atoms, which is defined for formulas, can not be transferred to propositions, because there is for instance

⟨A ∧ 0⟩ = ⟨0⟩ but the set of invalent atoms of the representing formulas are not equal:

{A} = {}. But for theories this definition is possible and usefull. Let [α, Φ] be a theory and A a bit variable. A is invalent for [α, Φ] if

subst(α, {A/0}) ⇔ subst(α, {A/1}). Otherwise A is valent for [α, Φ]. If additionally A ∈ Φ holds, A is said to be invalent (or valent) in [α, Φ]. A is invalent for instance in the following theories:

— [A ∧ 0, {A}]

— [A ∧ 0, {A, B}]

— [(A ∧ B) ∨ (¬A ∧ B), {A, B}] In the last case B is a valent atom, in the second case B is also invalent in the given theory.

1.8 Assertions

1.8.1 Pseudo messages and messages

A pair of pseudo theories is a pseudo message. A pair of theories is a message. Let Φ_{0} and Φ_{1} be two sets of bit variables, α_{0} ∈ F ormΦ_{0} and α_{1} ∈ F ormΦ_{1}, then the following notations for messages are defined:

— [α_{0}, Φ_{0} | α_{1}, Φ_{1}] := ([α_{0}, Φ_{0}], [α_{1}, Φ_{1}])

— [α_{0} | α_{1}, Φ_{1}] := ([α_{0}], [α_{1}, Φ_{1}])

— [α_{0}, Φ_{0} | α_{1}] := ([α_{0}, Φ_{0}], [α_{1}])

— [α_{0} | α_{1}] := ([α_{0}], [α_{1}]) From now on assertions are going to be written in the first of these four forms most of the times, but of course what is to be expressed by that does not depend on that notation. A transformation of the other forms into this standard form is simply given by

— [α_{0} | α_{1}, Φ_{1}] = [α_{0}, Atoms(α_{0}) | α_{1}, Φ_{1}]

— [α_{0}, Φ_{0} | α_{1}] = [α_{0}, Φ_{0} | α_{1}, Atoms(α_{1})]

— [α_{0} | α_{1}] = [α_{0}, Atoms(α_{0}) | α_{1}, Atoms(α_{1})] Another abbreviation is the notation

f[α_{0}, Φ_{0} | α_{1}, Φ_{1}] instead of f([α_{0}, Φ_{0} | α_{1}, Φ_{1}]) for a function f on a set of messages.

1.8.2 Assertions

A message [α_{0}, Φ_{0} | α_{1}, Φ_{1}] is

— an assertoric message or assertion, if Φ_{1} ⊆ Φ_{0}, and

— a non-assertoric message in the other case.

1.8.3 Assertion spaces

For a set Φ of bit variables

AssertΦ := {[α_{0}, Φ | α_{1}, Φ_{1}]|Φ_{1} ⊆ Φ, α_{0} ∈ F ormΦ, α_{1} ∈ F ormΦ_{1}} is the assertion space on Φ. For n = card(Φ) holds:

card(AssertΦ)

= card(T heoΦ) · ∑_{Φ_{1}∈Φ} card(T heoΦ_{1})
= 2^{2^{n}} · ∑_{k=0}^{n} \binom{n}{k} · 2^{2^{k}}

where

\binom{n}{k} := \{ \begin{matrix}\frac{n·(n−1)·...·(n−k+1)}{1·2·...·k} & for 0 < k ≤ n \\ 1 & for k = 0 \end{matrix}

as usual. Furthermore let

Assert∞ := ⋃_{Φ⊆B} AssertΦ.

1.8.4 Satisfiable and absolute satisfiable assertions

An assertion [α_{0}, Φ_{0} | α_{1}, Φ_{1}] is satisfiable, if there is a ω ∈ V alΦ_{0} such that

eval(subst(α_{0}, ω)) = eval(subst(α_{1}, ω,)) = 1. Otherwise it is unsatisfiable. If [α_{0}, Φ_{0} | α_{1}, Φ_{1}] is satisfiable/unsatisfiable it is also said that [α_{1}, Φ_{1}] is satisfiable/unsatisfiable in [α_{0}, Φ_{0}]. For an assertion [α_{0}, Φ_{0} | α_{1}, Φ_{1}] the set

Unitval(α_{0} ∧ α_{1}, Φ_{0}) is called the satisfaction set. An assertion is satisfiable if and only if the satisfaction set is not empty. An assertion [α_{0}, Φ_{0} | α_{1}, Φ_{1}] is absolute satisfiable, if

[α_{0}, Φ_{0} | κ, Φ_{1}] is satisfiable for all κ ∈ {litconj(ω)|ω ∈ Unitval[α_{1}, Φ_{1}]}. Otherwise it is not absolute satisfiable. If [α_{0}, Φ_{0} | α_{1}, Φ_{1}] is (not) absolute satisfiable it is also said that [α_{1}, Φ_{1}] is (not) absolute satisfiable in [α_{0}, Φ_{0}]. Actually the absolute satisfiability is an aggravation of the satisfiability; that means: if an assertion is absolute satisfiable, it is satisfiable. But there is the following exception of this rule. Let [α_{0}, Φ_{0} | α_{1}, Φ_{1}] be an assertion, then there are two cases to be distinguished:

— If α_{1} satisfiable:

if the assertion is absolute satisfiable, it is satisfiable as well.

— If α_{1} is unsatisfiable:

the assertion is absolute satisfiable, but not satisfiable. For the following examples there is again

[θ_{w}] = [¬(R ∧ S) ∧ (W ↔ (R ∨ S)) ∧ (R → H) ∧ (S → ¬H)]

— [R] is satisfiable and absolute satisfiable in [θ_{w}].

— [R ∧ S] is neither satisfiable nor absolute satisfiable in [θ_{w}].

— [R ∧ ¬S] is satisfiable and absolute satisfiable in [θ_{w}].

— [R, {R, S}] is satisfiable, but not absolute satisfiable in [θ_{w}]. This is, because the set of unit valuations of [R, {R, S}], written as literal conjunctions, is \{R\overline{S}, RS\} and there is

— [θ_{w} | R\overline{S}] satisfiable (see third example), but

— [θ_{w} | RS] is unsatisfiable (see second example) and thus [R, {R, S}] is not absolute satisfiable in [θ_{w}].

— [R ∨ S] is satisfiable, but not absolute satisfiable in [θ_{w}]. The set of unit valuations, written as literal conjunctions, is \{R\overline{S}, \overline{R}S, RS\} and there is

— [θ_{w} | R\overline{S}] satisfiable (see third example) and

— [θ_{w} | \overline{R}S] is satisfiable as well, but

— [θ_{w} | RS] is unsatisfiable (see second example)

and thus [R ∨ S] is not absolute satisfiable in [θ_{w}].

1.8.5 Subvalence and derivation

For α_{0}, α_{1} ∈ F ormΦ there is

α_{0} ⇒ α_{1} to be read as

α_{1} is valid in α_{0} or

α_{1} derives from α_{0}

if and only if

Unitval(α_{0}, Φ) ⊆ Unitval(α_{1}, Φ). A term which is unusual but fits better into the terminology pattern applied here, would be the title subvalence instead of derivation. Then α_{0} ⇒ α_{1} is expressed as

— α_{0} is subvalent to α_{1} and

— α_{1} is supervalent to α_{0}. The decision algorithm

subval(α_{0}, α_{1}) := \{ \begin{matrix}1 & if α_{0} ⇒ α_{1} \\ 0 & else \end{matrix}

can be implemented by subval(α_{0}, α_{1}) := taut(α_{0} → α_{1}).

1.8.6 Truth values

Every assertion [α_{0}, Φ_{0} | α_{1}, Φ_{1}] has a truth value, that is

— true or 1, if α_{0} ⇒ α_{1} and

— false or 0, else.

1.8.7 The truth function

The fact that every assertion has exactly one truth value from {0, 1} can be expressed in a functional way by the so-called truth function, which is for every assertion [α_{0}, Φ_{0} | α_{1}, Φ_{1}] defined by

truth[α_{0}, Φ_{0} | α_{1}, Φ_{1}] := \{ \begin{matrix}1 & if α_{0} ⇒ α_{1} \\ 0 & else \end{matrix}

So the truth function can be implemented by truth[α_{0}, Φ_{0} | α_{1}, Φ_{1}] := subval(α_{0}, α_{1}).

Atom expansion and reduction

2.1 Introduction

Now for theories [θ, Θ] the concepts expansion of theories by atoms and reduction of theories by atoms, in short: atom expansion and atom reduction shall be defined. That is the act of increasing or decreasing the set Θ of theory atoms by further atoms Φ so that the theory proposition ⟨θ⟩ remains the same. The definition of atom expansion is trivial. For atom reduction the problem arises that the atom reduced expression [θ, Θ\Φ] in general is not a theory any more, because θ ∈ F orm(Θ \ Φ) and for θ there exists an equivalent theory formula θ′ ∈ F orm(Θ \ Φ) if and only if Φ does not contain any valent atoms for θ. Thus in general for atom reduced theories [θ′, Θ \ Φ] holds that θ′ is not equivalent to θ. Two ways to construct such a θ′ shall be defined: the so-called conjunctive and the disjunctive atom reduction.

2.2 Atom expansion

For a theory [θ, Θ] and a set Φ of bit variables the theory [θ, Θ ∪ Φ] is the atom expansion of [θ, Θ] by Φ.

2.3 Atom reduction

Let [θ, Θ] be a theory and Φ a set of bit variables. If [θ, Θ] shall be atom reduced by Φ, this results in a theory [θ′, Θ′] where Θ′ = Θ \ Φ. The process of atom reduction can be well demonstrated at the double table of θ according to Θ′ and Φ.

\begin{matrix}θ & & Φ \\ ‡ & ‡ & θ,Θ′,Φ \\ Θ′ \end{matrix}  \begin{matrix}Θ′ & θ′ \\ † & θ′,Θ′ \end{matrix}

The process is then

— Given: ‡‡^{θ,Θ′,Φ}

— Wanted: †^{θ′,Θ′} Two special methods of atom reduction are:

— The conjunctive atom reduction:

For i = 0, ..., 2^{card(Θ′)} − 1 there is: †_{i}^{θ′,Θ′} is 1 if and only if the i–th row of the matrix ‡‡^{θ,Θ′,Φ} has only unit bits. So †_{i}^{θ′,Θ′} is the evaluation of the conjunction of all bit values of the i–th row of ‡‡^{θ,Θ′,Φ}

— The disjunctive atom reduction:

For i = 0, ..., 2^{card(Θ′)} − 1 there is: †_{i}^{θ′,Θ′} is 1 if and only if the i–th row of the matrix ‡‡^{θ,Θ′,Φ} has at least one unit bit. So †_{i}^{θ′,Θ′} is the evaluation of the disjunction of all bit values of the i–th row of ‡‡^{θ,Θ′,Φ}

⌜ Lemma 1 Let [θ, Θ] be a theory, Φ a set of bit variables, Θ′ = Θ \ Φ, and

— [θ_{et}, Θ′] the conjunctive atom reduction of [θ, Θ] by Φ

— [θ_{vel}, Θ′] the disjunctive atom reduction of [θ, Θ] by Φ then it holds that

— θ ⇒ θ_{vel}

— θ_{et} ⇒ θ

— θ_{et} ⇒ θ_{vel}.

⌟

2.4 An example

Suppose the theory [θ_{w}, Θ_{w}] shall be reduced by Φ, where

— θ_{w} = ¬(R ∧ S) ∧ (W ↔ (R ∨ S)) ∧ (R → H) ∧ (S → ¬H)

— Θ_{w} = {H, R, S, W }

— Φ = {H, W } Thus there is

Θ′_{w} := Θ_{w} \ Φ = {R, S} and let

— [θ_{et}, Θ′_{w}] be the conjunctive atom reduction and

— [θ_{vel}, Θ′_{w}] the disjunctive atom reduction of [θ_{w}, Θ_{w}] by Φ.

The double table ‡‡^{θ_{w},Θ′_{w},Φ} and the tables †^{θ_{et},Θ′_{w}} and †^{θ_{vel},Θ′_{w}} are

\begin{aligned}θ & & 0 & 1 & 0 & 1 & H \\ & & 0 & 0 & 1 & 1 & W \\ 0 & 0 & 1 & 1 & 0 & 0 \\ 1 & 0 & 0 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 & 1 & 0 \\ 1 & 1 & 0 & 0 & 0 & 0 \\ R & S \end{aligned} \begin{matrix}R & S & θ_{et} \\ 0 & 0 & 0 \\ 1 & 0 & 0 \\ 0 & 1 & 0 \\ 1 & 1 & 0 \end{matrix} \begin{matrix}R & S & θ_{vel} \\ 0 & 0 & 1 \\ 1 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 1 & 0 \end{matrix}

Thus there is

— [θ_{et}, Θ′_{w}] = [0, {R, S}]

— [θ_{vel}, Θ′_{w}] = [¬(R ∧ S), {R, S}]

2.5 Conjuntive atom reduction

Summarized in an algorithm it is defined ⌜ Definition 2

Let [θ, Θ] be a theory and Φ a set of bit variables. The conjunctive atom reduction of [θ, Θ] by Φ is the theory

[θ′, Θ′] := conred(θ, Θ, Φ) where conred is a function defined by the following algorithm: Algorithm conred(θ, Θ, Φ)

begin

Θ′ := Θ \ Φ ; n := 2^{card(Θ′)} ; m := 2^{card(Φ)} ; Ω := {} ; for i := 0, ..., n − 1 do

   begin

ω_{i} := val(i, Θ′) ; θ_{i} := subst(θ, ω_{i}) ; if eval((∧ subst(θ_{i}, val(0, Φ)) ... subst(θ_{i}, val(m − 1, Φ)))) = 1 then Ω := Ω ∪ {ω_{i}} ;

   end ;

Ω is now {ω_{i_{0}}, ω_{i_{1}}, ..., ω_{i_{k−1}}}, so set θ′ := (∨ litconj(ω_{i_{0}}) litconj(ω_{i_{1}}) ... litconj(ω_{i_{k−1}})) ;

return [θ′, Θ′] ;
end.

⌟

2.6 Disjuntive atom reduction

In analogy to the conjunctive atom reduction it is defined ⌜ Definition 3 Let [θ, Θ] be a theory and Φ a set of bit variables. The disjunctive atom reduction of [θ, Θ] by Φ is the theory

[θ′, Θ′] := disred(θ, Θ, Φ) where disred is a function defined by the following algorithm: Algorithm disred(θ, Θ, Φ)

begin

Θ′ := Θ \ Φ ; n := 2^{card(Θ′)} ; m := 2^{card(Φ)} ; Ω := {} ; for i := 0, ..., n − 1 do

   begin

ω_{i} := val(i, Θ′) ; θ_{i} := subst(θ, ω_{i}) ; if eval((∨ subst(θ_{i}, val(0, Φ)) ... subst(θ_{i}, val(m − 1, Φ)))) = 1 then Ω := Ω ∪ {ω_{i}} ;

   end ;

Ω is now {ω_{i_{0}}, ω_{i_{1}}, ..., ω_{i_{k−1}}}, so set θ′ := (∨ litconj(ω_{i_{0}}) litconj(ω_{i_{1}}) ... litconj(ω_{i_{k−1}})) ;

return [θ′, Θ′] ;
end.

⌟

Theory intervals and vector schemes

3.1 The subvalence as an order relation

⌜ Lemma 4 Let Φ be a set of bit variables and T ⊆ T heoΦ. Then for all [α, Φ], [β, Φ], [γ, Φ] ∈ T the following properties of the subvalence hold:

— the reflexivity α ⇒ α

— the anti–symmetry if α ⇒ β and β ⇒ α, then α ⇔ β

— the transitivity

if α ⇒ β and β ⇒ γ, then α ⇒ γ

⌟

That means, that the subvalence ⇒ is an order relation on T , but which is in general not total (similar to the smaller–or–equal relation ≤ on the set of real numbers), but partial (similar to the ⊆–relation on sets of sets).

3.2 Relative and absolute minima and maxima

⌜ Definition 5 Let Φ be a set of bit variables, T ⊆ T heoΦ and [β, Φ] ∈ T , then [β, Φ] is called a

— relative minimum of T if there is no [α, Φ] ∈ T different from [β, Φ] with α ⇔ β

— absolute minimum of T if for all [γ, Φ] ∈ T holds β ⇒ γ

— relative maximum of T

if there is no [γ, Φ] ∈ T different from [β, Φ] with β ⇒ γ

— absolute maximum of T

if for all [α, Φ] ∈ T holds α ⇒ β

⌟

⌜ Lemma 6 For a set Φ of bit variables and T ⊆ the following holds:

— T can have several relative minimas and maximas, but no more than one absolute minimum and one absolute maximum.

— If [0, Φ] ∈ T , then [0, Φ] is the absolute minimum of T .

If [1, Φ] ∈ T , then [1, Φ] is the absolute maximum of T .

— If T is finite, thus especially if Φ is finite, relative minima and maxima do always exist. But an absolute minimum or maximum does not have to exist.

⌟

3.3 Theory intervals

⌜ Definition 7

For two theories [α, Φ] and [γ, Φ] with α ⇒ γ

T (α, γ, Φ) := {[β, Φ]|β ∈ F ormΦ and α ⇒ β and β ⇒ α} is called the theory interval from α to γ in Φ or from [α, Φ] to [γ, Φ]. ⌟

A set T ⊆ T heoΦ of theories can be expressed as a theory interval if and only if T has an absolute minimum and maximum. For theories [α, Φ], [β, Φ], and [γ, Φ] with α ⇒ γ there is

[β, Φ] ∈ T (α, γ, Φ) if and only if

Unitval(α, Φ) ⊆ Unitval(β, Φ) ⊆ Unitval(γ, Φ) From that the following lemma derives easily: ⌜ Lemma 8

For theories [α, Φ] and [γ, Φ] with α ⇒ γ and

k := card(Unitval(γ, Φ) \ Unitval(α, Φ)) there is

card(T (α, γ, Φ)) = 2^{k}.

⌟

3.4 Vector schemes

A theory interval can be well represented by a scheme. For example consider

Φ  α β γ
0 0 0 0 ∗ 1
1 0 0 0 0 0
0 1 0 1 1 1
1 1 0 0 ∗ 1
0 0 1 0 0 0
1 0 1 0 ∗ 1
0 1 1 0 0 0
1 1 1 1 1 1

Let [α, Φ], [β, Φ], [γ, Φ] be theories with α ⇒ γ and

[β, Φ] ∈ T (α, γ, Φ). By comparing the tables for α, β, and γ the following cases can be distinguished for the components †_{i}^{α},†_{i}^{β}, and †_{i}^{γ} where i = 0, 1, ..., 2^{card(Φ)} − 1:

— †_{i}^{α} = 0 and †_{i}^{γ} = 0 Then †_{i}^{β} has to be 0 as well.

— †_{i}^{α} = 1 and †_{i}^{γ} = 0 This case is impossible because α ⇒ γ is demanded.

— †_{i}^{α} = 0 and †_{i}^{γ} = 1 In this case †_{i}^{β} can be either 0 or 1. This is denoted by †_{i}^{β} = ∗.

— †_{i}^{α} = 1 and †_{i}^{γ} = 1 Then †_{i}^{β} has to be 1 as well.

So this results for given α and γ (or †^{α} and †^{γ} respectively) is a so–called vector scheme for all possible [β, Φ] of the interval T (α, γ, Φ), which not only includes 0 and 1 as components as the vector †^{β} does, but also might contain the sign ∗ as a component. Any theory [β, Φ] of the interval can then be constructed by substituting a 0 or 1 for any of the occurences of ∗. In this way the last lemma is well demonstrated: Let k be the number of occurences of the ∗ in the vector scheme for β, then

card(T (α, γ, Φ)) = 2^{k} A simple example:

— [α, Φ] = [A ∧ B, {A, B}]

— [γ, Φ] = [A ∨ B, {A, B}] It is α ⇒ γ and thus the theory interval is well defined:

T (A ∧ B, A ∨ B, {A, B}) The vectors for α and γ and the vector scheme for all possible [β, {A, B}] of the theory interval are

\begin{matrix}A & B & α & β & γ \\ 0 & 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & ∗ & 1 \\ 0 & 1 & 0 & ∗ & 1 \\ 1 & 1 & 1 & 1 & 1 \end{matrix}

The sign ∗ occurs twice, the theory interval has 2^{2} = 4 elements, and these are:

— [AB, {A, B}] = [α, {A, B}]

— [A\overline{B} ∨ AB, \{A, B\}] = [A, \{A, B\}] — [\overline{A}B ∨ AB, \{A, B\}] = [B, \{A, B\}]

— [A\overline{B} ∨ \overline{A}B ∨ AB, \{A, B\}] = [γ, \{A, B\}]

3.5 Intersection sets of theory intervals

A lemma which will be used later is the following ⌜ Lemma 9

Let Φ be a set of bit variables and α_{0}, α_{1}, β_{0}, β_{1} ∈ F ormΦ with α_{0} ⇒ α_{1} and β_{0} ⇒ β_{1}. Thus

— T_{α} := T (α_{0}, α_{1}, Φ) ∉ {}

— T_{β} := T (β_{0}, β_{1}, Φ) ∉ {} and

T_{γ} := T_{α} ∩ T_{β} = \{ \begin{matrix}T (α_{0} ∨ β_{0}, α_{1} ∧ β_{1}, Φ) & if α_{0} ∨ β_{0} ⇒ α_{1} ∧ β_{1} \\ \{\} & else. \end{matrix}

⌟

Proof For a theory [γ, Φ] there is

[γ, Φ] ∈ T_{γ} if and only if [γ, Φ] ∈ T_{α} and [γ, Φ] ∈ T_{β}

and that is the case if and only if

( α_{0} ⇒ γ and γ ⇒ α_{1} ) and ( β_{0} ⇒ γ and γ ⇒ β_{1} ) if and only if

( α_{0} ⇒ γ and β_{0} ⇒ γ ) and ( γ ⇒ α_{1} and γ ⇒ β_{1} ) Now there is

— α_{0} ⇒ γ and β_{0} ⇒ γ if and only if Unitval(α_{0}, Φ) ⊆ Unitval(γ, Φ) and Unitval(β_{0}, Φ) ⊆ Unitval(γ, Φ) if and only if Unitval(α_{0}, Φ) ∪ Unitval(β_{0}, Φ) ⊆ Unitval(γ, Φ) if and only if Unitval(α_{0} ∨ β_{0}, Φ) ⊆ Unitval(γ, Φ) if and only if α_{0} ∨ β_{0} ⇒ γ.

— γ ⇒ α_{1} and γ ⇒ β_{1} if and only if Unitval(γ, Φ) ⊆ Unitval(α_{1}, Φ) and Unitval(γ, Φ) ⊆ Unitval(β_{1}, Φ) if and only if Unitval(γ, Φ) ⊆ Unitval(α_{1}, Φ) ∩ Unitval(β_{1}, Φ) if and only if Unitval(γ, Φ) ⊆ Unitval(α_{1} ∧ β_{1}, Φ) if and only if γ ⇒ α_{1} ∧ β_{1}.

Combining this gives [γ, Φ] ∈ T_{γ} if and only if α_{0} ∨ β_{0} ⇒ γ and γ ⇒ α_{1} ∧ β_{1}

and thus

T_{γ} = \{ \begin{matrix}T (α_{0} ∨ β_{0}, α_{1} ∧ β_{1}, Φ) & if α_{0} ∨ β_{0} ⇒ α_{1} ∧ β_{1} \\ \{\} & else. \end{matrix}

End of Proof.

Opposition, verification, and definition

4.1 Basic concepts

4.1.1 Opposition

⌜ Definition 10 For any three sets Θ, Φ, and Φ′ the triple (Θ, Φ, Φ′) is a set opposition if and only if

— Φ ∪ Φ′ = Θ and

— Φ ∩ Φ′ = {}. In this case it is also said:

Φ and Φ′ are in opposition (according to Θ).

⌟

A set diagram of a set opposition demonstrates this definition

[figure: Φ; Φ′; Θ]

⌜ Definition 11 For any three formulas θ, φ, and μ the triple (θ, φ, μ) is a formula opposition if and only if there are sets Θ, Φ, and Φ′ of bit variables such that

— θ ∈ F ormΘ, φ ∈ F ormΦ, μ ∈ F ormΦ′ and

— (Θ, Φ, Φ′) is a set opposition. In this case it is also said:

φ and μ are in opposition (according to θ).

⌟

⌜ Lemma 12 For three formulas θ, φ, μ the triple (θ, φ, μ) is a formula opposition if and only if Atoms(φ) ∩ Atoms(μ) = {}. ⌟

Proof of Lemma 12 There are two different cases:

— If Atoms(φ) ∩ Atoms(μ) ≠ {}, there are no Φ and Φ′ with Φ ∩ Φ′ = {} so that φ ∈ F ormΦ and μ ∈ F ormΦ. So (θ, φ, μ) is not a formula opposition.

— If Atoms(φ) ∩ Atoms(μ) = {} let — Θ := Atoms(θ) ∪ Atoms(φ) ∪ Atoms(μ)

— Φ_{0} := Atoms(φ)

— Φ′_{0} := Atoms(μ)

— Θ′ := Θ \ (Φ_{0} ∪ Φ′_{0}) what is shown by the diagram

[figure: Θ; Θ′; Φ_{0}; Φ′_{0}]

Now let Φ and Φ′ be constructed out of Φ_{0} and Φ′_{0} by adding each element of Θ′ either to Φ_{0} or to Φ′_{0}. (For example set Φ := Φ_{0} and Φ′ := Φ′_{0} ∪ Θ′.) Then (Θ, Φ, Φ′) is a set opposition and thus (θ, φ, μ) is a formula opposition.

End of Proof.

⌜ Definition 13 For any three theories [θ, Θ], [φ, Φ], and [μ, Φ′] the tripel ([θ, Θ], [φ, Φ], [μ, Φ′]) is a theory opposition if and only if (Θ, Φ, Φ′) is a set opposition (and thus (θ, φ, μ) is a formula opposition). In this case it is also said:

[φ, Φ] and [μ, Φ′] are in opposition (according to [θ, Θ]).

⌟

⌜ Definiton 14 Let (x_{0}, x_{1}, x_{2}) be a set triple, a formula triple or a theory triple, then

opp(x_{0}, x_{1}, x_{2}) := \{ \begin{matrix}1 & if x_{1} and x_{2} are in opposition \\ & according to x_{0} \\ 0 & else. \end{matrix}
⌟

4.1.2 Verifications

⌜ Definition 15 For any three formulas θ, φ, and μ the triple (θ, φ, μ) is a formula verification, if the following conditions hold — the sub–supervalence:

θ ⇒ μ → φ

— the opposition:

Atoms(φ) ∩ Atoms(μ) = {}. In this case it is also said:

μ verifies φ in θ.

⌟

The following lemma (mostly called the deduction theorem) gives another formulation of the sub–supervalence: ⌜ Lemma 16

For θ, φ, μ ∈ F ormB holds:

θ ⇒ μ → φ if and only if θ ∧ μ ⇒ φ.

⌟

The proof is evident. ⌜ Definition 17

For any three theories [θ, Θ], [φ, Φ], and [μ, Φ′] the triple ([θ, Θ], [φ, Φ], [μ, Φ′]) is a theory verification if the following two conditions hold:

— the sub–supervalence:

θ ⇒ μ → φ

— the opposition:

opp(Θ, Φ, Φ′) = 1. In this case it is also said that

— [μ, Φ′] verifies [φ, Φ] in [θ, Θ] or

— [μ, Φ′] verifies [θ, Θ | φ, Φ].

⌟

⌜ Definition 18 Let (x_{0}, x_{1}, x_{2}) be a formula triple or a theory triple, then

verif(x_{0}, x_{1}, x_{2}) := \{ \begin{matrix}1 & if x_{2} verifies x_{1} in x_{0} \\ 0 & else. \end{matrix}

⌟

An implementation is given by

— verif(θ, φ, μ) := eval(taut(θ → (μ → φ)) ∧ opp(θ, φ, μ))

for formula triples and

— verif([θ, Θ], [φ, Φ], [μ, Φ′]) := eval(taut(θ → (μ → φ))and opp(Θ, Φ, Φ′)) for theory triples.

4.1.3 Definitions

⌜ Definition 19 For any three formulas θ, φ, and μ the triple (θ, φ, μ) is a formula definition if the following two conditions hold:

— the sub–equivalence:

θ ⇒ φ ↔ μ

— the opposition:

Atoms(φ) ∩ Atoms(μ) = {}.

In this case it is also said:

μ defines φ in θ.

⌟

⌜ Definition 20 For any three theories [θ, Θ], [φ, Φ], and [μ, Φ′] the triple ([θ, Θ], [φ, Φ], [μ, Φ′]) is a theory definition if the following two conditions hold:

— the sub–equivalence:

θ ⇒ φ ↔ μ

— the opposition:

opp(Θ, Φ, Φ′) = 1. In this case it is also said:

— [μ, Φ′] defines [φ, Φ] in [θ, Θ] or

— [μ, Φ′] defines [θ, Θ | φ, Φ].

⌟

⌜ Definition 21 Let (x_{0}, x_{1}, x_{2}) be a formula triple or a theory triple, then

defin(x_{0}, x_{1}, x_{2}) := \{ \begin{matrix}1 & if x_{2} defines x_{1} in x_{0} \\ 0 & else. \end{matrix}

⌟

An implementation is given by

— defin(θ, φ, μ) := eval(taut(θ → (φ ↔ μ)) ∧ opp(θ, φ, μ))

for formula triples and

— defin([θ, Θ], [φ, Φ], [μ, Φ′]) := eval(taut(θ → (φ ↔ μ)) ∧ opp(Θ, Φ, Φ′)) for theory triples.

4.2 Verification and definition theories

4.2.1 Introduction

The rest of this chapter 4 is concerned with the systematic answer to the following question:

Given two theories [θ, Θ] and [φ, Φ]. When and how can a theory [μ, Φ′] be constructed which verifies or which defines [φ, Φ] in [θ, Θ]?

Without mentioning it, it will be supposed furthermore that the theories are finite. The methods which will be developed are computable alltogether, even if the algorithms are very naive and much too inefficient most of the times. Nevertheless the results can easily transferred to the infinite case.

4.2.2 Verification and definition theories

⌜ Definition 22 Let [θ, Θ] and [φ, Φ] be two theories. In other words: let [θ, Θ | φ, Φ] be a message. Then

— V erifT heo[θ, Θ | φ, Φ] := V erifT heo([θ, Θ], [φ, Φ])

:= {[μ, Φ′]|Φ′ ⊆ B, μ ∈ F ormΦ′, verif([θ, Θ], [φ, Φ], [μ, Φ′]) = 1} is the set of verification theories for [θ, Θ | φ, Φ] or for [φ, Φ] in [θ, Θ] and

— DefinT heo[θ, Θ | φ, Φ] := DefinT heo([θ, Θ], [φ, Φ]) := {[μ, Φ′]|Φ′ ⊆ B, μ ∈ F ormΦ′, defin([θ, Θ], [φ, Φ], [μ, Φ′]) = 1} is the set of definition theories for [θ, Θ | φ, Φ] or for [φ, Φ] in [θ, Θ].

If V erifT heo[θ, Θ | φ, Φ] is not empty, it is said that — [θ, Θ | φ, Φ] is verifiable or

— [φ, Φ] is verifiable in [θ, Θ]. If DefinT heo[θ, Θ | φ, Φ] is not empty, it is said that — [θ, Θ | φ, Φ] is defineable or

— [φ, Φ] is defineable in [θ, Θ].

⌟

4.2.3 Each definition theory is a verification theory

⌜ Lemma 23

For any three formulas θ, φ, and μ there holds:

If θ ⇒ φ ↔ μ then θ ⇒ μ → φ.

⌟

The proof is evident. From this lemma the following one immediately derives: ⌜ Lemma 24

For any three theories [θ, Θ], [φ, Φ], and [μ, Φ′]

defin([θ, Θ], [φ, Φ], [μ, Φ′]) = 1 implies

verif([θ, Θ], [φ, Φ], [μ, Φ′]) = 0.

⌟

and so it is: ⌜ Lemma 25

For every message [θ, Θ | φ, Φ] there is

DefinT heo[θ, Θ | φ, Φ] ⊆ V erifT heo[θ, Θ | φ, Φ].

⌟

In short:

Each definition theory is a verification theory. The opposite is wrong in general.

4.2.4 Only assertions are verifiable and defineable

A necessary condition for both verification and definition is the opposition property. To hold

— verif([θ, Θ], [φ, Φ], [μ, Φ′]) = 1 or

— defin([θ, Θ], [φ, Φ], [μ, Φ′]) = 1 it is necessary that

opp([θ, Θ], [φ, Φ], [μ, Φ′]) = 1

and that says that

Θ = Φ ∪ Φ′ and {} = Φ ∩ Φ′ where Φ ⊆ Θ says exactly the same as the claim that [θ, Θ | φ, Φ] has to be an assertion. ⌜ Lemma 26

If a message is not an assertion, it is neither verifiable nor defineable. ⌟ ⌜ Lemma 27

For every assertion [θ, Θ | φ, Φ] with Φ′ := Θ \ Φ there is

— V erifT heo[θ, Θ | φ, Φ] ⊆ T heoΦ′

— DefinT heo[θ, Θ | φ, Φ] ⊆ T heoΦ′

⌟

Because if the first lemma the further investigations will be restricted to the only interesting case, namely that the messages are assertoric.

4.3 Numbers of verification and definition theories

4.3.1 Bounds

The last lemma shows immediately the bounds of the number of all possible verification and definition theories. ⌜ Lemma 28

For every assertion [θ, Θ | φ, Φ] with Φ′ := Θ \ Φ holds:

— 0 ≤ card(V erifT heo[θ, Θ | φ, Φ]) ≤ 2^{2^{card(Φ′)}}

— 0 ≤ card(DefinT heo[θ, Θ | φ, Φ]) ≤ 2^{2^{card(Φ′)}}

⌟

Because the questions about the existence (cardinality > 0) and the uniqueness (cardinality < 2) of this two sets are very important for the later argumentation, they shall be answered explicitely, before the possibilities to construct verification and definition theories will be investigated systematically.

4.3.2 The existence of verification theories

⌜ Lemma 29 For every assertion [θ, Θ | φ, Φ] a theory [μ, Φ′] exists, which verifies the assertion. ⌟

Because for Φ′ = Θ \ Φ and if μ is a contradiction, then [μ, Φ′] is always a verification theory.

4.3.3 The non–uniqueness of verification theories

⌜ Lemma 30 There are assertions [θ, Θ | φ, Φ] for which more than one verification theory [μ, Φ′] exists. ⌟

For example, if [θ_{w}, Θ_{w}] is the standard example theory and

[φ, Φ] := [H, {H}] then several verification theories

[μ, Φ′] := [μ, {R, S, W }] do exist, for instance if the theory formula is

— μ = R or

— μ = ¬S ∧ W or

— μ = R ∧ S.

4.3.4 The non–existence of definition theories

⌜ Lemma 31

There are assertions which are not defineable. ⌟ For the same example

[φ, Φ] := [H, {H}]

there are again 2^{2^{card(Φ′)}} = 256 different theories of the form

[μ, Φ′] = [μ, {R, S, W }] but none of them is a definition theory for [θ_{w}, Θ_{w} | φ, Φ]. (Later on a method will be given to proof this statement.)

4.3.5 The non–uniqueness of definition theories

⌜ Lemma 32 There are assertions [θ, Θ | φ, Φ] which have more than one definition theory. ⌟

If [θ_{w}, Θ_{w}] is the standard example and

[φ, Φ] := [R, {R}] then definition theories

[μ, Φ′] = [μ, {H, S, W }] are given for example for

— μ = ¬S ∧ W

— μ = W ∧ H

4.4 Criteria for verification

4.4.1 Construction of verification theories

A method to construct all the verification theories of a given assertion can be won in a very demonstrative way by investigating double tables. (See also the following example in 4.4.2.) The problem is designated again by:

— Given an assertion [θ, Θ | φ, Φ].

— Wanted a theory [μ, Φ′] which verifies [θ, Θ | φ, Φ]. Because the opposition is demanded there is

— Φ′ = Θ \ Φ

— Φ ∩ Φ′ = {}

— Φ ∪ Φ′ = Θ Now construct the three double tables of θ, φ, and μ, each according to Φ′ and Φ. These (their matrices) are denoted by ‡‡^{θ}, ‡‡^{φ}, and ‡‡^{μ}. The matrices ‡‡^{θ} and ‡‡^{φ} are uniquely given by the assertion [θ, Θ | φ, Φ], the components of ‡‡^{μ} are still unknown so far.

\begin{matrix}θ & & Φ \\ ‡ & ‡ & θ \\ Φ′ \end{matrix}  \begin{matrix}φ & & Φ \\ ‡ & ‡ & φ \\ Φ′ \end{matrix}  \begin{matrix}μ & & Φ \\ ‡ & ‡ & μ \\ Φ′ \end{matrix}

The criterion that constitutes ‡‡^{μ} states:

[μ, Φ′] shall verify [θ, Θ | φ, Φ]. That says, for μ the following two conditons have to hold:

1. the sub–supervalence: θ ⇒ μ → φ

2. the opposition: μ ∈ F ormΦ′.

For ‡‡^{μ} this says:

1. For every i = 0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 the bit value ‡‡_{i,j}^{μ} has to fulfil the condition

eval(‡‡_{i,j}^{θ} → (‡‡_{i,j}^{μ} → ‡‡_{i,j}^{φ})) = 1

and thus

‡‡_{i,j}^{μ} = \{ \begin{matrix}0 & if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 0 \\ ∗ & else \end{matrix}

where ∗ stands for “any bit value 0 or 1”.

2. μ ∈ F ormΦ′ includes for ‡‡^{μ}, that in each row of the matrix all components have to be identic.

From this an algorithm can be derived to construct a vector scheme †^{μ,Φ′} for the input of ‡‡^{θ} and ‡‡^{φ}. And from that vector scheme all verification theories and the set of all verification theories as a theory interval can be read. Algorithm verifconstr(‡‡^{θ,Φ′,Φ}, ‡‡^{φ,Φ′,Φ})

begin

1. For each i = 0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 set

‡‡_{i,j}^{μ,Φ′,Φ} := \{ \begin{matrix}0 & if ‡‡_{i,j}^{θ,Φ′,Φ} = 1 and ‡‡_{i,j}^{φ,Φ′,Φ} = 0 \\ ∗ & else \end{matrix}

(The result ‡‡^{μ,Φ′,Φ} of this first step is not a matrix, because it contains not only bit values (in this case 0 only) but also the sign ∗. So ‡‡^{μ,Φ′,Φ} is called a matrices scheme.)

2. In each row or the matrices scheme make all signs identic in the following way:

(i) If at least one 0 occurs in the row, set all the components of this row to 0. (ii) If only ∗ occurs in the row, nothing has to be changed.

2’. From ‡‡^{μ,Φ′,Φ} the vector scheme †^{μ,Φ′} can easily be constructed by:

For each i = 0, ..., 2^{card(Φ′)} − 1 set †_{i}^{μ,Φ′} := ‡‡_{i,0}^{μ,Φ′,Φ}.

return †^{μ,Φ′}.
end.

4.4.2 An example

It shall be asked for the verification theories of the assertion

[θ_{w}, {H, R, S, W } | H, {H}] The double tables ‡‡^{θ_{w}}, ‡‡^{φ}, and ‡‡^{μ} according to (R, S, W) and (H) are

\begin{aligned}& θ_{w} & & & 0 & 1 & H \\ 0 & & 0 & 0 & 1 & 1 \\ 1 & & 0 & 0 & 0 & 0 \\ 0 & & 1 & 0 & 0 & 0 \\ 1 & & 1 & 0 & 0 & 0 \\ 0 & & 0 & 1 & 0 & 0 \\ 1 & & 0 & 1 & 0 & 1 \\ 0 & & 1 & 1 & 1 & 0 \\ 1 & & 1 & 1 & 0 & 0 \\ R & & S & W \end{aligned} \begin{matrix}φ = H & & 0 & 1 & H \\ 0 & 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 & 1 \\ 1 & 1 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 & 1 \\ 1 & 0 & 1 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 \\ 1 & 1 & 1 & 0 & 1 \\ R & S & W \end{matrix} \begin{aligned}& μ & & & 0 & 1 & H \\ 0 & & 0 & 0 \\ 1 & & 0 & 0 \\ 0 & & 1 & 0 \\ 1 & & 1 & 0 \\ 0 & & 0 & 1 \\ 1 & & 0 & 1 \\ 0 & & 1 & 1 \\ 1 & & 1 & 1 \\ R & & S & W \end{aligned}

The matrices scheme ‡‡^{μ} results from applying the algorithm:

\begin{matrix}step 1 \\ μ & & 0 & 1 & H \\ 0 & 0 & 0 & 0 & ∗ \\ 1 & 0 & 0 & ∗ & ∗ \\ 0 & 1 & 0 & ∗ & ∗ \\ 1 & 1 & 0 & ∗ & ∗ \\ 0 & 0 & 1 & ∗ & ∗ \\ 1 & 0 & 1 & ∗ & ∗ \\ 0 & 1 & 1 & 0 & ∗ \\ 1 & 1 & 1 & ∗ & ∗ \\ R & S & W \end{matrix} \begin{matrix}step 2 \\ μ & & 0 & 1 & H \\ 0 & 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & ∗ & ∗ \\ 0 & 1 & 0 & ∗ & ∗ \\ 1 & 1 & 0 & ∗ & ∗ \\ 0 & 0 & 1 & ∗ & ∗ \\ 1 & 0 & 1 & ∗ & ∗ \\ 0 & 1 & 1 & 0 & 0 \\ 1 & 1 & 1 & ∗ & ∗ \\ R & S & W \end{matrix} \begin{matrix}step 2’ \\ R & S & W & μ \\ 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & ∗ \\ 0 & 1 & 0 & ∗ \\ 1 & 1 & 0 & ∗ \\ 0 & 0 & 1 & ∗ \\ 1 & 0 & 1 & ∗ \\ 0 & 1 & 1 & 0 \\ 1 & 1 & 1 & ∗ \end{matrix}

From this vector scheme with 6 occurences of the sign ∗, all the 2^{6} = 64 verification theories con be read off, depending on which bit value is chosen for a ∗ each. Possible μ ∈ F orm{R, S, H} such that [μ, {R, S, W }] is a verification theory are for example

— μ = R

— μ = 0

— μ = ¬S ∧ W because the vector of each of the theories [μ, {R, S, W }] fits into the vector scheme. Written as a theory interval, the set of all verification theories is given by:

V erifT heo[θ_{w}, {H, R, S, W } | H, {H}]

= T (0, R\overline{S}\overline{W} ∨ \overline{R}S\overline{W} ∨ RS\overline{W} ∨ \overline{R}\overline{S}W ∨ R\overline{S}W ∨ RSW, \{R, S, W \})

4.4.3 Minimal and maximal verification theories

If the vector scheme for †^{μ} includes the sign ∗ k–times, 2^{k} verification theories exist. Such exist always, as it is confirmed again. Besides it shows, that the set of all verification theories is always a theory interval. It’s (absolute) minimum and maximum shall be called the minimal and maximal verifiction theory. These are the theories that arise by replacing a 0 (or a 1) for each ∗ of the vector scheme. ⌜ Lemma and Definition 33

For any assertion [θ, Θ | φ, Φ] holds:

— There is exactly one so–called minimal verification theory

minverif[θ, Θ | φ, Φ] = [μ_{min}, Φ′] ∈ V erifT heo[θ, Θ | φ, Φ] such that μ_{min} ⇒ μ for all [μ, Φ′] ∈ V erifT heo[θ, Θ | φ, Φ].

— There is exactly one so–called maximal verification theory

maxverif[θ, Θ | φ, Φ] = [μ_{max}, Φ′] ∈ V erifT heo[θ, Θ | φ, Φ] such that μ ⇒ μ_{max} for all [μ, Φ′] ∈ V erifT heo[θ, Θ | φ, Φ].

⌟

The direct construction for the minimal verification theory is trivial: all components of †^{μ} are 0. ⌜ Lemma 34

For an assertion [θ, Θ | φ, Φ] and Φ′ := Θ \ Φ minverif[θ, Θ | φ, Φ] = [0, Φ′].

⌟

A direct construction procedure for the maximal verification theory is given by a special modification of the algorithm verifconstr:

1. For each i = 0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 set

‡‡_{i,j}^{μ} := \{ \begin{matrix}0 & if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 0 \\ 1 & else \end{matrix}

2. In each row of ‡‡^{μ} make all components identic by:

(i) set all components to 0 if at least one 0 occurs in the row (ii) leave the row as it is, if all the components are 1.

Read the vector †^{μ,Φ′} and the theory maxverif[θ, Θ | φ, Φ] off the matrix.

In other words:

1. Construct ‡‡^{θ→ϕ} out of ‡‡^{θ} and ‡‡^{φ}

2. Construct the conjunctive atom reduction of [θ → φ, Θ] by Φ.

In that way a direct construction procedure is won: ⌜ Lemma 35

For every assertion [θ, Θ | φ, Φ]

maxverif[θ, Θ | φ, Φ] = conred(θ → φ, Θ, Φ).

⌟

4.4.4 The main lemma of verification

The results of the question for the verification theories of a given assertion shall be summarized in the ⌜ Lemma 36 (main lemma of verification)

For every assertion [θ, Θ | φ, Φ] and Φ′ := Θ \ Φ

— minverif[θ, Θ | φ, Φ] = [0, Φ′]

— maxverif[θ, Θ | φ, Φ] = conred(θ → φ, Θ, Φ) =: [μ_{1}, Φ′] and

V erifT heo[θ, Θ | φ, Φ] = T (0, μ_{1}, Φ′)
⌟

The reader may apply this result again to the example in 4.4.2.

4.5 Criteria for definition

4.5.1 Construction of definition theories

Again the investigation of double tables will lead to this method. (See also the following examples in 4.5.2.) The designations remain the same, so again the three double tables are

\begin{matrix}θ & & Φ \\ ‡ & ‡ & θ \\ Φ′ \end{matrix}  \begin{matrix}φ & & Φ \\ ‡ & ‡ & φ \\ Φ′ \end{matrix}  \begin{matrix}μ & & Φ \\ ‡ & ‡ & μ \\ Φ′ \end{matrix}

and again the matrices ‡‡^{θ} and ‡‡^{φ} are unambiguously given by the assertion [θ, Θ | φ, Φ] and ‡‡^{μ} is unknown at this stage. The criterion that constiutes ‡‡^{μ} states:

[μ, Φ′] shall verify [θ, Θ | φ, Φ]. That says, for μ the following two conditions have to hold:

1. the sub–equivalence: θ ⇒ φ ↔ μ

2. the opposition: μ ∈ F ormΦ′.

For ‡‡^{μ} this says:

1. For every i = 0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 the bit value ‡‡_{i,j}^{μ} has to fulfil the condition

eval(‡‡_{i,j}^{θ} → (‡‡_{i,j}^{φ} ↔ ‡‡_{i,j}^{μ})) = 1 and thus

‡‡_{i,j}^{μ} = \{ \begin{matrix}0 & if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 0 \\ 1 & if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 1 \\ ∗ & if ‡‡_{i,j}^{θ} = 0 \end{matrix}

where ∗ again stands for “any bit value 0 or 1”.

2. μ ∈ F ormΦ′ includes for ‡‡^{μ} that in each row or the matrix all components have to be identic.

From this an algorithm can be derived to construct a vector scheme †^{μ,Φ′} by the input of ‡‡^{θ} and ‡‡^{φ}. Algorithm definconstr(‡‡^{θ,Φ′,Φ}, ‡‡^{φ,Φ′,Φ})

begin

1. For each i = 0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 set

‡‡_{i,j}^{μ,Φ′,Φ} := \{ \begin{matrix}0 & if ‡‡_{i,j}^{θ,Φ′,Φ} = 1 and ‡‡_{i,j}^{φ,Φ′,Φ} = 0 \\ 1 & if ‡‡_{i,j}^{θ,Φ′,Φ} = 1 and ‡‡_{i,j}^{φ,Φ′,Φ} = 1 \\ ∗ & if ‡‡_{i,j}^{θ,Φ′,Φ} = 0 \end{matrix}

2. In each row of the matrices scheme ‡‡^{μ,Φ′,Φ} make all signs identic by doing the following in each of the four different possible cases:

(i) If at least one 0 and for the rest only ∗ occur in the row, set all components of the row to 0. (ii) If at least one 1 and for the rest only ∗ occur in the row, set all components of the row to 1. (iii) If only ∗ occurs in the row, nothing is changed. (iv) If the row contains at least one 0 and one 1 at the same time, the components can not be made identic. So if and only if this case occurs, no definition theory does exist. For the matrices scheme the sign • shall be introduced and the algorithm continues as follows: If the row contains at least one 0 and one 1 at the same time, set all components of this column to •.

2’. From ‡‡^{μ,Φ′,Φ} the vector scheme †^{μ,Φ′} can easily be constructed by:

For each i = 0, ..., 2^{card(Φ′)} − 1 set †_{i}^{μ,Φ′} := ‡‡_{i,0}^{μ,Φ′,Φ}.

return †^{μ,Φ′}.
end.

The output †^{μ,Φ′} shows whether [θ, Θ | φ, Φ] is defineable. This is the case if and only if the sign • does not occur in †^{μ,Φ′}. If it is defineable, the set of all definition theories is determined by †^{μ,Φ′} as a theory interval.

4.5.2 Two examples

The algorithm is now applied to two examples: to a not defineable and to a defineable assertion. First it shall be asked for the definition theories of the assertion

[θ_{w}, {H, R, S, W } | H, {H}] The double tables ‡‡^{θ_{w}}, ‡‡^{φ}, and ‡‡^{μ} according to (R, S, W) and (H) are

\begin{aligned}& θ_{w} & & & 0 & 1 & H \\ 0 & & 0 & 0 & 1 & 1 \\ 1 & & 0 & 0 & 0 & 0 \\ 0 & & 1 & 0 & 0 & 0 \\ 1 & & 1 & 0 & 0 & 0 \\ 0 & & 0 & 1 & 0 & 0 \\ 1 & & 0 & 1 & 0 & 1 \\ 0 & & 1 & 1 & 1 & 0 \\ 1 & & 1 & 1 & 0 & 0 \\ R & & S & W \end{aligned} \begin{matrix}φ = H & & 0 & 1 & H \\ 0 & 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 & 1 \\ 1 & 1 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 & 1 \\ 1 & 0 & 1 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 \\ 1 & 1 & 1 & 0 & 1 \\ R & S & W \end{matrix} \begin{aligned}& μ & & & 0 & 1 & H \\ 0 & & 0 & 0 \\ 1 & & 0 & 0 \\ 0 & & 1 & 0 \\ 1 & & 1 & 0 \\ 0 & & 0 & 1 \\ 1 & & 0 & 1 \\ 0 & & 1 & 1 \\ 1 & & 1 & 1 \\ R & & S & W \end{aligned}

and the algorithm constructs the matrices scheme ‡‡^{μ} and the vector scheme †^{μ,Φ′} as follows

\begin{matrix}step 1 \\ μ & & 0 & 1 & H \\ 0 & 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & ∗ & ∗ \\ 0 & 1 & 0 & ∗ & ∗ \\ 1 & 1 & 0 & ∗ & ∗ \\ 0 & 0 & 1 & ∗ & ∗ \\ 1 & 0 & 1 & ∗ & 1 \\ 0 & 1 & 1 & 0 & ∗ \\ 1 & 1 & 1 & ∗ & ∗ \\ R & S & W \end{matrix} \begin{matrix}step 2 \\ μ & & 0 & 1 & H \\ 0 & 0 & 0 & • & • \\ 1 & 0 & 0 & ∗ & ∗ \\ 0 & 1 & 0 & ∗ & ∗ \\ 1 & 1 & 0 & ∗ & ∗ \\ 0 & 0 & 1 & ∗ & ∗ \\ 1 & 0 & 1 & 1 & 1 \\ 0 & 1 & 1 & 0 & 0 \\ 1 & 1 & 1 & ∗ & ∗ \\ R & S & W \end{matrix} \begin{matrix}step 2’ \\ R & S & W & μ \\ 0 & 0 & 0 & • \\ 1 & 0 & 0 & ∗ \\ 0 & 1 & 0 & ∗ \\ 1 & 1 & 0 & ∗ \\ 0 & 0 & 1 & ∗ \\ 1 & 0 & 1 & 1 \\ 0 & 1 & 1 & 0 \\ 1 & 1 & 1 & ∗ \end{matrix}

The sign • occurs in the vector scheme †^{μ,Φ′}:

[H, {H}] is not defineable in [θ_{w}, {H, R, S, W }]. The second example is

[θ_{w}, {H, R, S, W } | R, {R}] The double tables ‡‡^{θ_{w}}, ‡‡^{φ}, and ‡‡^{μ} according to (H, S, W) and (R) are

\begin{aligned}& θ_{w} & & & 0 & 1 & R \\ 0 & & 0 & 0 & 1 & 0 \\ 1 & & 0 & 0 & 1 & 0 \\ 0 & & 1 & 0 & 0 & 0 \\ 1 & & 1 & 0 & 0 & 0 \\ 0 & & 0 & 1 & 0 & 0 \\ 1 & & 0 & 1 & 0 & 1 \\ 0 & & 1 & 1 & 1 & 0 \\ 1 & & 1 & 1 & 0 & 0 \\ H & & S & W \end{aligned} \begin{matrix}φ = R & & 0 & 1 & R \\ 0 & 0 & 0 & 0 & 1 \\ 1 & 0 & 0 & 0 & 1 \\ 0 & 1 & 0 & 0 & 1 \\ 1 & 1 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 & 1 \\ 1 & 0 & 1 & 0 & 1 \\ 0 & 1 & 1 & 0 & 1 \\ 1 & 1 & 1 & 0 & 1 \\ H & S & W \end{matrix} \begin{aligned}& μ & & & 0 & 1 & R \\ 0 & & 0 & 0 \\ 1 & & 0 & 0 \\ 0 & & 1 & 0 \\ 1 & & 1 & 0 \\ 0 & & 0 & 1 \\ 1 & & 0 & 1 \\ 0 & & 1 & 1 \\ 1 & & 1 & 1 \\ H & & S & W \end{aligned}

Applying the algorithm gives

\begin{matrix}step 1 \\ μ & & 0 & 1 & R \\ 0 & 0 & 0 & 0 & ∗ \\ 1 & 0 & 0 & 0 & ∗ \\ 0 & 1 & 0 & ∗ & ∗ \\ 1 & 1 & 0 & ∗ & ∗ \\ 0 & 0 & 1 & ∗ & ∗ \\ 1 & 0 & 1 & ∗ & 1 \\ 0 & 1 & 1 & 0 & ∗ \\ 1 & 1 & 1 & ∗ & ∗ \\ H & S & W \end{matrix} \begin{matrix}step 2 \\ μ & & 0 & 1 & H \\ 0 & 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 0 & 0 \\ 0 & 1 & 0 & ∗ & ∗ \\ 1 & 1 & 0 & ∗ & ∗ \\ 0 & 0 & 1 & ∗ & ∗ \\ 1 & 0 & 1 & 1 & 1 \\ 0 & 1 & 1 & 0 & 0 \\ 1 & 1 & 1 & ∗ & ∗ \\ H & S & W \end{matrix} \begin{matrix}step 2’ \\ H & S & W & μ \\ 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & ∗ \\ 1 & 1 & 0 & ∗ \\ 0 & 0 & 1 & ∗ \\ 1 & 0 & 1 & 1 \\ 0 & 1 & 1 & 0 \\ 1 & 1 & 1 & ∗ \end{matrix}

The sign • does not occur in †^{μ,Φ′}:

[R, {R}] is defineable in [θ_{w}, {H, R, S, W }].

And because the sign ∗ occurs 4 times in †^{μ,Φ′}, there are 2^{4} = 16 different definition theories of the form [μ, {H, S, W }], for instance for

— μ = H ∧ ¬S ∧ W (each ∗ is set to 0)

— μ = (S ∧ ¬W) ∨ (¬S ∧ W) ∨ (H ∧ S ∧ W) (each ∗ is set to 1)

— μ = ¬S ∧ W etc. It is

DefinT heo[θ_{w}, {H, R, S, W } | R, {R}] =
T (H\overline{S}W, \overline{H}S\overline{W} ∨ HS\overline{W} ∨ \overline{H}\overline{S}W ∨ H\overline{S}W ∨ HSW, \{H, S, W \}).

4.5.3 Minimal and maximal definition theories and a criterion for defineability

Similar to the verification the construction method for definition theories shows as well that the set of definition theories is a theory interval — presupposed that the assertion is defineable at all. ⌜ Lemma and Definition 37

For any defineable assertion [θ, Θ | φ, Φ] holds:

— There is exactly one so-called minimal definition theory

mindefin[θ, Θ | φ, Φ] = [μ_{min}, Φ′] ∈ DefinT heo[θ, Θ | φ, Φ] such that μ_{min} ⇒ μ for all [μ, Φ′] ∈ DefinT heo[θ, Θ | φ, Φ].

— There is exactly one so-called maximal definition theory

maxdefin[θ, Θ | φ, Φ] = [μ_{max}, Φ′] ∈ DefinT heo[θ, Θ | φ, Φ] such that μ ⇒ μ_{max} for all [μ, Φ′] ∈ DefinT heo[θ, Θ | φ, Φ].

⌟

A direct construction of the minimal and maximal definition theory is given by the following ⌜ Lemma 38

For every defineable assertion [θ, Θ | φ, Φ] holds:

— mindefin[θ, Θ | φ, Φ] = disred(θ ∧ φ, Θ, Φ)

— maxdefin[θ, Θ | φ, Φ] = conred(θ → φ, Θ, Φ)

⌟

The expressions disred(θ ∧φ, Θ, Φ) and conred(θ → φ, Θ, Φ) do even more than just being direct constructions for minimal and maximal definition theories of defineable assertions. They provide a criterion to decide whether an assertion is defineable at all. ⌜ Lemma 39

Let [θ, Θ | φ, Φ] be an assertion and

— [μ_{0}, Φ′] := disred(θ ∧ φ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ)

Then [θ, Θ | φ, Φ] is defineable if and only if μ_{0} ⇒ μ_{1}. ⌟ Proof of Lemma 38 and Lemma 39 Given ‡‡^{θ} := ‡‡^{θ,Φ′,Φ} and ‡‡^{φ} := ‡‡^{φ,Φ′,Φ} uniquely determined by [θ, Θ | φ, Φ]. The vector scheme †^{μ} := †^{μ,Φ′} and the vectors †^{μ_{0}} := †^{μ_{0},Φ′} and †^{μ_{1}} := †^{μ_{1},Φ′} shall be constructed and compared. The result is shown in table 1. (Step 2 and 2’ in definconstr are combined here in one step.) There are two different situations:

— The assertion is defineable: That means, the case 2.(iv) does not occur and thus there is never †_{i}^{μ_{0}} = 1 and †_{i}^{μ_{1}} = 0. Hence μ_{0} ⇒ μ_{1}. Besides †_{i}^{μ} = 0 always includes †_{i}^{μ_{0}} = 0 and †_{i}^{μ_{1}} = 1 so that μ_{0} and μ_{1} are theory formulas for the minimal and maximal definition theory.

— The assertion is defineable: That means, the case 2.(iv) occurs at least once with †_{i}^{μ_{0}} = 1 and †_{i}^{μ_{1}} = 0 and μ_{0} ⇒ μ_{1} does not hold.

End of Proof.

4.5.4 The main lemma of definition

A summary of the results is the ⌜ Lemma 40 (main lemma of definition)

For every assertion [θ, Θ | φ, Φ] and

— [μ_{0}, Φ′] := disred(θ ∧ φ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ)

holds:

definconstr(‡‡^{θ}, ‡‡^{φ})  disred(θ ∧ φ, Θ, Φ)  conred(θ → φ, Θ, Φ)
1.  For each i  =

0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 set ‡‡_{i,j}^{μ} :=

0 if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 0
1 if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 1
∗ if ‡‡_{i,j}^{θ} = 0

1.  For each i  =

0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1 set ‡‡_{i,j}^{μ_{0}} :=

0 if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 0
1 if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 1
0 if ‡‡_{i,j}^{θ} = 0

1.  For each i  =
0, ..., 2^{card(Φ′)} − 1 and j =
0, ..., 2^{card(Φ)} − 1 set ‡‡_{i,j}^{μ_{1}} :=
0 if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 0
1 if ‡‡_{i,j}^{θ} = 1 and ‡‡_{i,j}^{φ} = 1
1 if ‡‡_{i,j}^{θ} = 0

2.(i) The i–th row of ‡‡^{μ} has at least one 0 and further only ∗. So †_{i}^{μ} := 0 2.(i) In this case the i–th row of ‡‡^{μ_{0}} has only 0 as components. The disjunction of the components gives †_{i}^{μ_{0}} := 0 2.(i) In this case the i–th row of ‡‡^{μ_{1}} has at least one 0 and further only 1. The conjunction gives †_{i}^{μ_{1}} := 0

2.(ii) The i–th row of ‡‡^{μ} has at least one 1 and further only ∗. So †_{i}^{μ} := 1 2.(ii) In this case the i–th row of ‡‡^{μ_{0}} has at least one 1 and further only 0 as components. The disjunction gives †_{i}^{μ_{0}} := 1 2.(ii) In this case the i–th row of ‡‡^{μ_{1}} has only 1 as components. The conjunction gives †_{i}^{μ_{1}} := 1

2.(iii) The i–th row of ‡‡^{μ} has only ∗. So †_{i}^{μ} := ∗ 2.(iii) In this case the i–th row of ‡‡^{μ_{0}} has only 0 as components. The disjunction gives †_{i}^{μ_{0}} := 0 2.(iii) In this case the i–th row of ‡‡^{μ_{1}} has only 1 as components. The conjunction gives †_{i}^{μ_{1}} := 1

2.(iv) The i–th row of ‡‡^{μ} has at least one 0 and one 1 at the same time. So †_{i}^{μ} := • 2.(iv) In this case the i–th row of ‡‡^{μ_{0}} has at least one 0 and one 1 at the same time. The disjunction gives †_{i}^{μ_{0}} := 1 2.(iv) In this case the i–th row of ‡‡^{μ_{1}} has at least one 0 and one 1 at the same time. The conjunction gives †_{i}^{μ_{1}} := 0

Table 1

[θ, Θ | φ, Φ] is defineable if and only if μ_{0} ⇒ μ_{1}. In that case there is

— mindefin[θ, Θ | φ, Φ] = [μ_{0}, Φ′]

— maxdefin[θ, Θ | φ, Φ] = [μ_{1}, Φ′]

— DefinT heo[θ, Θ | φ, Φ] = T (μ_{0}, μ_{1}, Φ′)

⌟

The reader may visualize this result again by applying it to the two examples of 4.5.2.

Meaning

5.1 Meaning functions

⌜ Definition 41 (the fundamental principle of the meaning concept)

A meaning function is a function of the form

meaning : Assert∞ ⟶ T heo∞ and it is demanded that for every assertion [θ, Θ | φ, Φ] with

[μ, Φ′] = meaning[θ, Θ | φ, Φ] the message [θ, Θ | μ, Φ′] must be assertoric too. [μ, Φ′] is called the meaning of [θ, Θ | φ, Φ] or the meaning of [φ, Φ] in [θ, Θ]. ⌟

Of course the most of this meaning functions do not provide a reasonable concept of meaning. A useful meaning function should also satisfy some other principles such as the so–called verification principle, demanding that the meaning verifies the given assertion. In this way two promising meaning functions shall be worked out:

— the so–called true meaning function and

— the so–called absolute satisfying meaning function.

5.2 The true meaning function

5.2.1 The true meaning function

⌜ Theorem 42 For every assertion [θ, Θ | φ, Φ] the set of all theories [μ, Φ′] which satisfy the conditions Π_{opp}, Π_{verif}, and Π_{defin}has exactly one absolute maximum [μ_{true}, Φ′]. And there is

— Π_{opp}the opposition principle: Φ′ = Θ \ Φ.

— Π_{verif}the verification principle:

[μ, Φ′] verifies [θ, Θ | φ, Φ].

— Π_{defin}the definition principle:

If [θ, Θ | φ, Φ] is defineable, [μ, Φ′] is a definition theory.

⌟

⌜ Corollary 43

Besides this theory [μ_{true}, Φ′] satisfies Π_{truemean}the principle of embedding the truth into the meaning concept: taut(μ_{true}) = truth[θ, Θ | φ, Φ]

⌟

This corollary motivates the terminology of the following ⌜ Definition 44

The function that assigns to every assertion [θ, Θ | φ, Φ] this well–defined theory [μ_{true}, Φ′] of the theorem, is called the true meaning function, written

truemean[θ, Θ | φ, Φ] := [μ_{true}, Φ′] and [μ_{true}, Φ′] is called the true meaning of [θ, Θ | φ, Φ] or of [φ, Φ] in [θ, Θ]. ⌟

⌜ Corollary 45

For every assertion [θ, Θ | φ, Φ]

truemean[θ, Θ | φ, Φ] = conred(θ → φ, Θ, Φ)

⌟

The next chapter presents the proof of the theorem and the two corollaries. The following chapter shows a list of examples of true meanings for the standard example.

5.2.2 Proofs

Proof of theorem 42 and corollary 45 Given an assertion [θ, Θ | φ, Φ] and Φ′ := Θ \ Φ. Besides μ_{0} and μ_{1} are given by — [μ_{0}, Φ′] := disred(θ ∧ φ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ) Let T_{opp} be the set of all thories fulfilling the opposition principle Π_{opp}. So

T_{opp} = T heoΦ′ Let T_{verif} be the set of all theories fulfilling the verification principle Π_{verif}. According to the main lemma of verification

T_{verif} = T (0, μ_{1}, Φ′) Let T_{defin} be the set of all theories fulfilling the definition principle Π_{defin}. According to the main lemma of definition

T_{defin} = T (μ_{0}, μ_{1}, Φ′) if μ_{0} ⇒ μ_{1}. Let T_{true} be the set of all theories fulfilling all three principles Π_{opp}, Π_{verif}, and Π_{defin}. So

T_{true} = \{ \begin{matrix}T_{opp} ∩ T_{verif} ∩ T_{defin} & if μ_{0} ⇒ μ_{1} \\ T_{opp} ∩ T_{verif} & else. \end{matrix}

Now there is

T_{verif} = T (0, μ_{1}, Φ′) ⊆ T heoΦ′ = T_{opp} and in case μ_{0} ⇒ μ_{1} there is also

T_{defin} = T (μ_{0}, μ_{1}, Φ′) ⊆ T (0, μ_{1}, Φ′) = T_{verif}. So there is

T_{opp} ∩ T_{verif} ∩ T_{defin} = T_{defin} if μ_{0} ⇒ μ_{1} and

T_{opp} ∩ T_{verif} = T_{verif}.

And so

T_{true} = \{ \begin{matrix}T (μ_{0}, μ_{1}, Φ′) & if μ_{0} ⇒ μ_{1} \\ T (0, μ_{1}, Φ′) & else. \end{matrix}

Thus an absolute maximum of T_{true} does exist and it is, no matter of [θ, Θ | φ, Φ] is defineable or not, the theory [μ, Φ′]. This proofs the theorem and corollary 45. End of Proof. Proof of corollary 43 Let

[μ_{true}, Φ′] = conred(θ → φ, Θ, Φ)

then there is

taut(μ_{true}) = 1 if and only if for all i = 0, ..., 2^{card(Φ′)} − 1

†^{μ_{true},Φ′} = 1 if and only if for all i = 0, ..., 2^{card(Φ′)} − 1 and j = 0, ..., 2^{card(Φ)} − 1

‡‡_{i,j}^{θ→φ,Φ′,Φ} = 1 if and only if

θ ⇒ φ if and only if

truth[θ, Θ | φ, Φ] = 1. Thus

taut(μ_{true}) = 1 if and only if truth[θ, Θ | φ, Φ] = 1.

End of Proof.

5.2.3 Examples

List 1 shows a list of examples for true meanings for the standard example. In each case there is

[μ_{true}, Φ′] := truemean[θ, Θ | φ, Φ] and the true meaning is computed via

[μ_{true}, Φ′] := conred(θ → φ, Θ, Φ) so that μ_{true} is a CDNF. Most of the time, the CDNF is not the most readable theory formula and a more intuitive, atom reduced form μ′_{true} with [μ_{true}, Φ′] = [μ′_{true}, Φ′] is given in a separate column.

List 1^{\begin{matrix}Φ & φ & Φ′ & μ_{true} & μ′_{true} & ⇒ \\ \{\} & 0 & \{H, R, S, W \} & \overline{H}R\overline{S}\overline{W} ∨ HR\overline{S}\overline{W} ∨ ; \overline{H}\overline{R}S\overline{W} ∨ H\overline{R}S\overline{W} ∨ ; \overline{H}RS\overline{W} ∨ HRS\overline{W} ∨ ; \overline{H}\overline{R}\overline{S}W ∨ H\overline{R}\overline{S}W ∨ ; \overline{H}R\overline{S}W ∨ H\overline{R}SW ∨ ; \overline{H}RSW ∨ HRSW & ¬θ_{w} & 0 \\ \{\} & 1 & \{H, R, S, W \} & \overline{H}\overline{R}\overline{S}\overline{W} ∨ H\overline{R}\overline{S}\overline{W} ∨ ; \overline{H}R\overline{S}\overline{W} ∨ HR\overline{S}\overline{W} ∨ ; \overline{H}\overline{R}S\overline{W} ∨ H\overline{R}S\overline{W} ∨ ; \overline{H}RS\overline{W} ∨ HRS\overline{W} ∨ ; \overline{H}\overline{R}\overline{S}W ∨ H\overline{R}\overline{S}W ∨ ; \overline{H}R\overline{S}W ∨ HR\overline{S}W ∨ ; \overline{H}\overline{R}SW ∨ H\overline{R}SW ∨ ; \overline{H}RSW ∨ HRSW & 1 & 1 \\ \{H\} & H & \{R, S, W \} & {R\overline{S}\overline{W} ∨ \overline{R}S\overline{W} ∨ \atop RS\overline{W} ∨H\overline{S}W ∨RSW} & R ∨ S\overline{W} ∨ \overline{S}W & 0 \\ \{R\} & R & \{H, S, W \} & \overline{H}S\overline{W} ∨ HS\overline{W} ∨ ; \overline{H}\overline{S}W ∨ H\overline{S}W ∨ ; HSW & HS ∨ S\overline{W} ∨ \overline{S}W & 0 \\ \{S\} & S & \{H, R, W \} & \overline{H}R\overline{W} ∨ HR\overline{W} ∨ ; \overline{H}\overline{R}W ∨ H\overline{R}W ∨ ; \overline{H}RW & \overline{H}R∨R\overline{W} ∨\overline{R}W & 0 \\ \{W \} & W & \{H, R, S\} & {\overline{H}R\overline{S}∨HR\overline{S}∨\overline{H}\overline{R}S∨ \atop H\overline{R}S ∨ \overline{H}RS ∨ HRS} & R ∨ S & 0 \\ \{R, S\} & R ∨ S & \{H, W \} & \overline{H}W ∨ HW & W & 0 \\ \{R, S\} & R ∧ S & \{H, W \} & (∨) & 0 & 0 \\ \{R, S\} & ¬(R ∧ S) & \{H, W \} & {\overline{H}\overline{W} ∨ H\overline{W} ∨ \overline{H}W ∨ \atop HW} & 1 & 1 \\ \{H, S\} & ¬(H ∧ S) & \{R, W \} & {\overline{R}\overline{W} ∨ R\overline{W} ∨ \overline{R}W ∨ \atop RW} & 1 & 1 \\ \{R, W \} & R → W & \{H, S\} & \overline{H}\overline{S} ∨ H\overline{S} ∨ \overline{H}S ∨ HS & 1 & 1 \\ \{R, W \} & R ∧ W & \{H, S\} & HS & H ∧ S & 0 \\ \{R, W \} & R ∨ W & \{H, S\} & \overline{H}S ∨ HS & S & 0 \\ \{R, S\} & ¬R ∨ ¬S & \{H, W \} & {\overline{H}\overline{W} ∨ H\overline{W} ∨ \overline{H}W ∨ \atop HW} & 1 & 1 \\ \{S, W \} & S ∧ W & \{H, R\} & \overline{H}R & ¬H ∧ R & 0 \\ \{R, S, W \} & R → W ∧ ¬S & \{H\} & \overline{H} ∨ H & 1 & 1 \\ \{R, S, W \} & R ∨ S → W & \{H\} & \overline{H} ∨ H & 1 & 1 \\ \{R, S, W \} & W ↔ S ∨ R & \{H\} & \overline{H} ∨ H & 1 & 1 \\ \{R, S, W \} & R ↔ ¬S ∧ W & \{H\} & \overline{H} ∨ H & 1 & 1 \\ \{R, S, W \} & R ↔ ¬S ∨ W & \{H\} & (∨) & 1 & 0 \\ \{R, S, W \} & R ∨ S ∨ ¬W & \{H\} & \overline{H} ∨ H & 1 & 1 \\ \{H, R, S, W \} & H ∧ R ∧ ¬S ∧ W & \{\} & (∨) & 0 & 0 \\ \{H, R, S, W \} & ¬H∧R∧S∧¬W & \{\} & (∨) & 0 & 0 \\ \{H, R, S, W \} & H ∨ R ∨ S ∨ ¬W & \{\} & (∨ (∧)) & 1 & 1 \\ \{H, R, S, W \} & {¬H ∨ ¬R ∨ ¬S ∨ \atop ¬W} & \{\} & (∨) & 0 & 0 \\ \{H, R, S, W \} & θ_{w} & \{\} & (∨ (∧)) & 1 & 1 \\ \{H, R, S, W \} & ¬θ_{w} & \{\} & (∨) & 0 & 0 \end{matrix}}

53 The last column (⇒) indicates if θ_{w} ⇒ φ by showing the result of subval(θ_{w}, φ) to check corollary 43:

taut(μ_{true}) = 1 (and so μ′_{true} = 1) if and only if truth[θ_{w}, {H, R, S, W } | φ, Φ] = 1 (that is subval(θ_{w}, φ) = 1).

5.3 The absolute satisfying meaning function

5.3.1 The absolute satisfying meaning function

⌜ Theorem 46 For every assertion [θ, Θ | φ, Φ] the set of all theorie [μ, Φ′] which satisfy the conditions Π_{opp}, Π_{verif}, Π_{defin}, and Π_{abssat}has exactly one absolute maximum [μ_{abssat}, Φ′]. And there is

— Π_{opp}the opposition principle:

Φ′ = Θ \ Φ.

— Π_{verif}the verification principle:

[μ, Φ′] verifies [θ, Θ | φ, Φ].

— Π_{defin}the definition principle:

If [θ, Θ | φ, Φ] is defineable, [μ, Φ′] is a definition theory.

— Π_{abssat}the principle of absolute satisfiability:

[θ, Θ | μ, Φ′] is absolute satisfiable.

⌟

⌜ Definition 47 The function that assigns to every assertion [θ, Θ | φ, Φ] this well–defined theory [μ_{absssat}, Φ′] of the theorem, is called the absolute satisfying meaning function, written as

abssatmean[θ, Θ | φ, Φ] := [μ_{abssat}, Φ′] and [μ_{abssat}, Φ′] is called the absolute satisfying meaning of [θ, Θ | φ, Φ] or of [φ, Φ] in [θ, Θ]. ⌟

⌜ Corollary 48 For every assertion [θ, Θ | φ, Φ] and

— [μ_{θ}, Φ′] := disred(θ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ) there is

abssatmean[θ, Θ | φ, Φ] = [μ_{θ} ∧ μ_{1}, Φ′].

⌟

⌜ Corollary 49 For every assertion [θ, Θ | φ, Φ] and

— [μ_{0}, Φ′] := disred(θ ∧ φ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ) there is

abssatmean[θ, Θ | φ, Φ] = [μ_{0} ∧ μ_{1}, Φ′].

⌟

5.3.2 Proofs

The following lemma is used to proof theorem 46 and corollary 48. ⌜ Lemma 50

Let [θ, Θ | μ, Φ′] be an assertion and Φ := Θ\Φ′. The assertion is absolute satisfiable if and only if

[μ, Φ′] ∈ T (0, μ_{θ}, Φ′) with

[μ_{θ}, Φ′] := disred(θ, Θ, Φ).
⌟

Proof To demand the absolute satisfiability of [θ, Θ | μ, Φ′] says for ‡‡^{θ} := ‡‡^{θ,Φ′,Φ} and †^{μ} := †^{μ,Φ′} that for all i = 0, ..., 2^{card(Φ′)} − 1 holds:

if †_{i}^{μ} = 1 then a 1 must occur in the i–th row of ‡‡^{θ}. The i–th row of ‡‡^{θ} includes at least one 1 if and only if †_{i}^{μ_{θ}} = 1. So the absolute satisfiability demands for every i = 0, ..., 2^{card(Φ′)} − 1:

if †_{i}^{μ} = 1 then †_{i}^{μ_{θ}} = 1 and that is

μ ⇒ μ_{θ} and so

[μ, Φ′] ∈ T (0, μ_{θ}, Φ′).

End of Proof.

Proof of theorem 46 and corollary 48 So let [θ, Θ | φ, Φ] be an assertion and Φ′ := Θ \ Φ. Furthermore let μ_{0}, μ_{θ}, μ_{1} ∈ F ormΦ′ be defined by

— [μ_{0}, Φ′] := disred(θ ∧ φ, Θ, Φ)

— [μ_{θ}, Φ′] := disred(θ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ) The proof of theorem 42 has already shown that the set T_{true} of all theories satisfying the principles Π_{opp}, Π_{verif}, and Π_{defin}is given by

T_{true} := \{ \begin{matrix}T (μ_{0}, μ_{1}, Φ′) & if μ_{0} ⇒ μ_{1} \\ T (0, μ_{1}, Φ′) & else \end{matrix}

Let T_{abssat} denote the set of all theories fulfilling the principle Π_{abssat}of absolute satisfiability, then

T_{abssat} = T (0, μ_{θ}, Φ′) according to lemma 50. Finally let T_{four} be the set of all theories satisfying all of the four demanded principles Π_{opp}, Π_{verif}, Π_{defin}, and Π_{abssat}. So

T_{four} = T_{true} ∩ T_{abssat} and thus

T_{four} = \{ \begin{matrix}T (μ_{0}, μ_{1}, Φ′) ∩ T (0, μ_{θ}, Φ′) & if μ_{0} ⇒ μ_{1} \\ T (0, μ_{1}, Φ′) ∩ T (0, μ_{θ}, Φ′) & else \end{matrix}

and by applying lemma 9 to both cases:

T_{four}

= \{ \begin{matrix}\{ & T (μ_{0} ∨ 0, μ_{1} ∧ μ_{θ}, Φ′) if μ_{0} ⇒ μ_{1} and μ_{0} ∨ 0 ⇒ μ_{1} ∧ μ_{θ} \{\}  if μ_{0} ⇒ μ_{1} and not μ_{0} ∨ 0 ⇒ μ_{1} ∧ μ_{θ} \\ \{ & T (0 ∨ 0, μ_{1} ∧ μ_{0}, Φ′) if not μ_{0} ⇒ μ_{1} and 0 ∨ 0 ⇒ μ_{1} ∧ μ_{θ} \{\}  if not μ_{0} ⇒ μ_{1} and not 0 ∨ 0 ⇒ μ_{1} ∧ μ_{θ} \end{matrix}

= \{ \begin{matrix}(i) & T (μ_{0}, μ_{1} ∧ μ_{θ}, Φ′) & if μ_{0} ⇒ μ_{1} and μ_{0} ⇒ μ_{1} ∧ μ_{θ} \\ (ii) & \{\} & if μ_{0} ⇒ μ_{1} and not μ_{0} ⇒ μ_{1} ∧ μ_{θ} \\ (iii) & T (0, μ_{1} ∧ μ_{θ}, Φ′) & if not μ_{0} ⇒ μ_{1} and 0 ⇒ μ_{1} ∧ μ_{θ} \\ (iv) & \{\} & if not μ_{0} ⇒ μ_{1} and not 0 ⇒ μ_{1} ∧ μ_{θ} \end{matrix}

But now there holds:

— Case (ii) never occurs:

This is because θ ∧ φ ⇒ θ holds for any two formulas θ and φ and so, as it can be shown easily, for the formulas μ_{0} and μ_{θ} which are the disjunctive atom reductions of θ ∧ φ and θ, the subvalence μ_{0} ⇒ μ_{θ} holds. It follows that μ_{0} ∧ μ_{θ} ⇔ μ_{0}. So if μ_{0} ⇒ μ_{1} and thus μ_{0} ∧ μ_{θ} ⇒ μ_{1} ∧ μ_{θ} hold, μ_{0} ⇒ μ_{1} ∧μ_{θ} is the case too. The case that μ_{0} ⇒ μ_{1} and not μ_{0} ⇒ μ_{1} ∧μ_{θ} hold at the same time, can not occur.

— The case (iv) is impossible, too. Because for every formula, especially for μ_{1} ∧ μ_{θ}, 0 ⇒ μ_{1} ∧ μ_{θ} is always the case.

So the cases (ii) and (iv) disappear and it remains

T_{four} = \{ \begin{matrix}T (μ_{0}, μ_{1} ∧ μ_{θ}, Φ′) & if μ_{0} ⇒ μ_{1} \\ T (0, μ_{1} ∧ μ_{θ}, Φ′) & else \end{matrix}

T_{four} is never empty and has the same absolute maximum [μ_{1} ∧ μ_{θ}, Φ′] in both cases. This closes the proof of theorem 46 and corollary 48. End of Proof. Proof of corollary 49 Corollary 48 states that abssatmean[θ, Θ | φ, Φ] = [μ_{θ} ∧ μ_{1}, Φ′]. So it is sufficient to show that μ_{θ} ∧ μ_{1} ⇔ μ_{0} ∧ μ_{1}. This proof shall be demonstrated by contradiction: Suppose μ_{θ} ∧ μ_{1} and μ_{0} ∧ μ_{1} are not equivalent. Then the vectors of these two formulas must differ in at least one component. So there must be an i ∈ {0, ..., 2^{card(Φ′)} − 1} such that †_{i}^{μ_{θ}∧μ_{1}} ≠ †_{i}^{μ_{0}∧μ_{1}} (where both vectors are according to Φ′). If †_{i}^{μ_{1}} = 0 then †_{i}^{μ_{θ}∧μ_{1}} = †_{i}^{μ_{0}∧μ_{1}} = 0. So †_{i}^{μ_{1}} = 1 must hold. Under this condition there are two alternatives so that †_{i}^{μ_{θ}∧μ_{1}} ≠ †_{i}^{μ_{0}∧μ_{1}}: First †_{i}^{μ_{θ}} = 0 and †_{i}^{μ_{0}} = 1 and second †_{i}^{μ_{θ}} = 1 and †_{i}^{μ_{0}} = 0. Thet first alternative discards because for all j: ‡‡_{i,j}^{θ,Φ′,Φ} = 0 includes ‡‡_{i,j}^{θ∧φ,Φ′,Φ} = 0 as well and thus †_{i}^{μ_{θ}} = 0 includes †_{i}^{μ_{0}} = 0. Only the second alternative †_{i}^{μ_{θ}} = 1, †_{i}^{μ_{0}} = 0, and †_{i}^{μ_{1}} = 1 is left. †_{i}^{μ_{0}} = 0 includes ‡‡_{i,j}^{θ∧φ,Φ′,Φ} = 0 for all j ∈ {0, ..., 2^{card(Φ)} −1} and so for all these

j holds: ‡‡_{i,j}^{θ,Φ′,Φ} = 0 or ‡‡_{i,j}^{φ,Φ′,Φ} = 0.

†_{i}^{μ_{1}} = 1 includes ‡‡_{i,j}^{θ→φ,Φ′,Φ} = 1 for all j ∈ {0, ..., 2^{card(Φ)} − 1}, so there cannot

be a j such that ‡‡_{i,j}^{θ,Φ′,Φ} = 1 and ‡‡_{i,j}^{φ,Φ′,Φ} = 0.

\begin{matrix}Φ & φ & Φ′ & μ_{abssat} & μ′_{abssat} \\ \{\} & 0 & \{H, R, S, W \} & (∨) & 0 \\ \{\} & 1 & \{H, R, S, W \} & {\overline{H}\overline{R}\overline{S}\overline{W} ∨ H\overline{R}\overline{S}\overline{W} ∨ \atop HR\overline{S}W ∨ \overline{H}\overline{R}SW} & θ_{w} \\ \{H\} & H & \{R, S, W \} & R\overline{S}W & R ∧ ¬S ∧ W \\ \{R\} & R & \{H, S, W \} & H\overline{S}W & H ∧ ¬S ∧ W \\ \{S\} & S & \{H, R, W \} & \overline{H}\overline{R}W & ¬H ∧ ¬R ∧ W \\ \{W \} & W & \{H, R, S\} & HR\overline{S} ∨ \overline{H}\overline{R}S & HR\overline{S} ∨ \overline{H}\overline{R}S \\ \{R, S\} & R ∨ S & \{H, W \} & \overline{H}W ∨ HW & W \\ \{R, S\} & R ∧ S & \{H, W \} & (∨) & 0 \\ \{R, S\} & ¬(R ∧ S) & \{H, W \} & {\overline{H}\overline{W} ∨ H\overline{W} ∨ \overline{H}W ∨ \atop HW} & 1 \\ \{H, S\} & ¬(H ∧ S) & \{R, W \} & \overline{R}\overline{W} ∨ \overline{R}W ∨ RW & ¬R ∨ W \\ \{R, W \} & R → W & \{H, S\} & \overline{H}\overline{S} ∨ H\overline{S} ∨ \overline{H}S & H ∨ ¬S \\ \{R, W \} & R ∧ W & \{H, S\} & (∨) & 0 \\ \{R, W \} & R ∨ W & \{H, S\} & \overline{H}S & ¬H ∧ S \\ \{R, S\} & ¬R ∨ ¬S & \{H, W \} & {\overline{H}\overline{W} ∨ H\overline{W} ∨ \overline{H}W ∨ \atop HW} & 1 \\ \{S, W \} & S ∧ W & \{H, R\} & (∨) & 0 \\ \{R, S, W \} & R → W ∧ ¬S & \{H\} & \overline{H} ∨ H & 1 \\ \{R, S, W \} & R ∨ S → W & \{H\} & \overline{H} ∨ H & 1 \\ \{R, S, W \} & W ↔ S ∨ R & \{H\} & \overline{H} ∨ H & 1 \\ \{R, S, W \} & R ↔ ¬S ∧ W & \{H\} & \overline{H} ∨ H & 1 \\ \{R, S, W \} & R ↔ ¬S ∨ W & \{H\} & (∨) & 0 \\ \{R, S, W \} & R ∨ S ∨ ¬W & \{H\} & \overline{H} ∨ H & 1 \\ \{H, R, S, W \} & H ∧ R ∧ ¬S ∧ W & \{\} & (∨) & 0 \\ \{H, R, S, W \} & ¬H ∧ R ∧ S ∧ ¬W & \{\} & (∨) & 0 \\ \{H, R, S, W \} & H ∨ R ∨ S ∨ ¬W & \{\} & (∨ (∧)) & 1 \\ \{H, R, S, W \} & ¬H ∨ ¬R ∨ ¬S ∨ ¬W & \{\} & (∨) & 0 \\ \{H, R, S, W \} & θ_{w} & \{\} & (∨ (∧)) & 1 \\ \{H, R, S, W \} & ¬θ_{w} & \{\} & (∨) & 0 \end{matrix} List 2

So from †_{i}^{μ_{0}} = 0 and †_{i}^{μ_{1}} = 1 follows for all j ∈ {0, ..., 2^{card(Φ)} − 1} that ‡‡_{i,j}^{θ,Φ′,Φ} = 0. But that would include †_{i}^{μ_{θ}} = 0 in contradiction to the assumption †_{i}^{μ_{θ}} = 1. Thus there is no assertion [θ, Θ | φ, Φ] such that μ_{θ} ∧ μ_{1} and μ_{0} ∧ μ_{1} are not equivalent. End of Proof.

5.3.3 Examples

List 2 is similar to list 1 and contains the same examples, this time for

[μ_{abssat}, Φ′] := abssatmean[θ, Θ | φ, Φ] where [μ_{abssat}, Φ′] is computed by

— [μ_{0}, Φ′] := disred(θ ∧ φ, Θ, Φ)

— [μ_{1}, Φ′] := conred(θ → φ, Θ, Φ)

— [μ_{abssat}, Φ′] := [cdnf(μ_{0} ∧ μ_{1}), Φ′] And again, μ′_{abssat} is a more readable, atom reduced, equivalent form of μ_{abssat}.

5.4 Meaning functions on messages

Meaning functions were introduced for assertions as arguments. But a meaning function meaning can be easily expanded to a function meaning′ allowing arbitrary messages as arguments. Let meaning be a meaning function and [θ, Θ | φ, Φ] a message. The expansion meaning′ of meaning is then defined by

meaning′[θ, Θ | φ, Φ] := meaning[θ, Θ ∪ Φ | φ, Φ] If [θ, Θ | φ, Φ] is a message, [θ, Θ ∪ Φ | φ, Φ] is an assertion and meaning[θ, Θ | φ, Φ] is well defined. The principles and results can be easily modified to fit for the expanded meaning function.