Many-valued logics

Syntax and Semantics

Equation form expr-01208e159d2aec8c

∧\land

Read as: conjunction

Means: conjunction

8 occurrences in this chapter

Equation form expr-09500e18cee3ef58

F∉V+\False \notin V^+

Read as: false is not in the set of designated values V plus

Means: false is not in the set of designated values V plus

2 occurrences in this chapter

Equation form expr-0d4cbaecc5a93859

⊥~=F\tf{\lfalse} = \False

Read as: the truth value of the falsity constant is false

Means: the truth value of the falsity constant is false

1 occurrence in this chapter

Equation form expr-0db163baa438d48a

v⊭LA\pSat/{v}{!A}[\Log L]

Read as: valuation v does not satisfy A in logic L

Means: valuation v does not satisfy A in logic L

1 occurrence in this chapter

Equation form expr-0fd6d107a43b1f02

⊨L⊆⊨C{\Entails[\Log L]} \subseteq {\Entails[\LogCL]}

Read as: the consequence relation of logic L is included in the consequence relation of classical logic

Means: the consequence relation of logic L is included in the consequence relation of classical logic

1 occurrence in this chapter

Equation form expr-1006d5203d6c3047

Γ⊨LA\Gamma \Entails[\Log L] !A

Read as: Gamma entails A in logic L

Means: Gamma entails A in logic L

1 occurrence in this chapter

Equation form expr-10460c48f54fe957

v¯(⋆(A1,…,An))=⋆~L(v¯(A1),…,v¯(An)).\pValue{v}(\star(!A_1, \dots, !A_n)) = \tf{\star}[\Log L] (\pValue{v}(!A_1), \dots, \pValue{v}(!A_n)).

Read as: The value under v of star applied to A subscript one through A subscript n equals the truth function for star in logic L applied, in that order, to the values under v of A subscript one through A subscript n.

Means: The value under v of star applied to A subscript one through A subscript n equals the truth function for star in logic L applied, in that order, to the values under v of A subscript one through A subscript n.

1 occurrence in this chapter

Equation form expr-10db6ea11a3cf0e4

Δ⊨A\Delta \Entails !A

Read as: Delta entails A

Means: Delta entails A

1 occurrence in this chapter

Equation form expr-116e1578d14c7fb7

x=Fx = \False

Read as: x equals false

Means: x equals false

1 occurrence in this chapter

Equation form expr-11fbd48b42c71e9f

v¯C(A)=T\pValue v[\LogCL](!A) = \True

Read as: the value of A under v in classical logic equals true

Means: the value of A under v in classical logic equals true

1 occurrence in this chapter

Equation form expr-1239e63d5cfacbb7

¬~L(x)=¬~C(x)\tf{\lnot}[\Log L](x) = \tf{\lnot}[\LogCL](x)

Read as: the negation truth function of logic L at x equals the classical negation truth function at x

Means: the negation truth function of logic L at x equals the classical negation truth function at x

2 occurrences in this chapter

Equation form expr-12943ee36d2b0173

v⊭LB\pAssign v \Entails/[\Log L] !B

Read as: valuation v does not satisfy B in logic L

Means: valuation v does not satisfy B in logic L

1 occurrence in this chapter

Equation form expr-139c7c04318de35e

n=0n = 0

Read as: n equals zero

Means: n equals zero

1 occurrence in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

1 occurrence in this chapter

Equation form expr-15371170798ae4ac

C\LogCL

Read as: C

Means: C

2 occurrences in this chapter

Equation form expr-1a087d4e7e64e44d

{T,F}\{\True, \False\}

Read as: the set containing true and false

Means: the set containing true and false

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

5 occurrences in this chapter

Equation form expr-1b50ab81bf0add5e

Γ⊨A→B\Gamma \Entails !A \lif !B

Read as: Gamma entails the conditional if A then B

Means: Gamma entails the conditional if A then B

2 occurrences in this chapter

Equation form expr-1ee7a629a82cb64c

x,y∈{T,F}x, y \in \{\True, \False\}

Read as: x and y both belong to the set containing true and false

Means: x and y both belong to the set containing true and false

2 occurrences in this chapter

Equation form expr-23fac266c08cc34b

pi\Obj p_i

Read as: p subscript i

Means: p subscript i

1 occurrence in this chapter

Equation form expr-240313d5e995741c

v\pAssign{v}

Read as: v

Means: v

13 occurrences in this chapter

Equation form expr-2657355be2d06c9e

Γ∪{A}⊨B\Gamma \cup \{!A\} \Entails !B

Read as: Gamma together with A entails B

Means: Gamma together with A entails B

1 occurrence in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: negation

Means: negation

6 occurrences in this chapter

Equation form expr-2a3e00fd37391fac

∧~\tf{\land}

Read as: the conjunction truth function

Means: the conjunction truth function

1 occurrence in this chapter

Equation form expr-2b79c20bfbb7a12e

x=Tx = \True

Read as: x equals true

Means: x equals true

1 occurrence in this chapter

Equation form expr-362138992adfe804

⋆\star

Read as: star

Means: star

8 occurrences in this chapter

Equation form expr-3634fd48a2326f78

V={T,F}V = \{\True, \False\}

Read as: V equals the set containing true and false

Means: V equals the set containing true and false

2 occurrences in this chapter

Equation form expr-37b22a86c093d68f

V+V^+

Read as: V plus

Means: V plus

2 occurrences in this chapter

Equation form expr-382ee137aedcf4de

A≡p!A \ident p

Read as: A, namely p,

Means: A, namely p,

1 occurrence in this chapter

Equation form expr-38a6461e5f88ab3d

△\triangle

Read as: triangle

Means: triangle

2 occurrences in this chapter

Equation form expr-3a8d1bfa3b0e045f

v¯C(B)=F\pValue v[\LogCL](!B) = \False

Read as: the value of B under v in classical logic equals false

Means: the value of B under v in classical logic equals false

1 occurrence in this chapter

Equation form expr-3d43654da81a83f1

∅⊨A\emptyset \Entails !A

Read as: the empty set of premises entails A

Means: the empty set of premises entails A

1 occurrence in this chapter

Equation form expr-3f2322dc8cdd4156

⋆~\tf{\star}

Read as: the truth function for star

Means: the truth function for star

1 occurrence in this chapter

Equation form expr-400048a76f6a5014

L0\Lang{L_0}

Read as: L subscript zero

Means: L subscript zero

1 occurrence in this chapter

Equation form expr-44016824161fd23f

{T,F}\{\True,\False\}

Read as: the set containing true and false

Means: the set containing true and false

1 occurrence in this chapter

Equation form expr-472cdb090aa87ad0

⋆(A1)\star(!A_1)

Read as: star applied to A subscript one

Means: star applied to A subscript one

1 occurrence in this chapter

Equation form expr-4c94485e0c21ae6c

vv

Read as: v

Means: v

1 occurrence in this chapter

Equation form expr-4feaf0824cc8e0d1

⊨\Entails

Read as: semantic entailment

Means: semantic entailment

1 occurrence in this chapter

Equation form expr-5280c8f9e471df51

⊤\ltrue

Read as: the truth constant

Means: the truth constant

1 occurrence in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: disjunction

Means: disjunction

7 occurrences in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

9 occurrences in this chapter

Equation form expr-581559724ec1bd25

v¯L(A)∈V+\pValue{v}(!A)[\Log L] \in V^+

Read as: the value of A under v in logic L belongs to the set of designated values V plus

Means: the value of A under v in logic L belongs to the set of designated values V plus

2 occurrences in this chapter

Equation form expr-58197ff8ca27696b

¬~\tf{\lnot}

Read as: the negation truth function

Means: the negation truth function

1 occurrence in this chapter

Equation form expr-5978b1f1bab524d4

→~L(x,y)=→~C(x,y)\tf{\lif}[\Log L](x,y) = \tf{\lif}[\LogCL](x,y)

Read as: the conditional truth function of logic L at x and y equals the classical conditional truth function at x and y

Means: the conditional truth function of logic L at x and y equals the classical conditional truth function at x and y

1 occurrence in this chapter

Equation form expr-599dfb6065696bc6

A≡¬B!A \ident \lnot B

Read as: A is the negation of B

Means: A is the negation of B

1 occurrence in this chapter

Equation form expr-59afe76b65ca4bdd

v¯(A)\pValue{v}(!A)

Read as: of A under v

Means: of A under v

3 occurrences in this chapter

Equation form expr-59cf7cd4fdb9ff5b

T\True

Read as: true

Means: true

21 occurrences in this chapter

Equation form expr-5b5a153da39a5ae2

⋆A1\star !A_1

Read as: star followed by A subscript one

Means: star followed by A subscript one

1 occurrence in this chapter

Equation form expr-5e585fb8dfd9f7c9

Γ⊆Δ\Gamma \subseteq \Delta

Read as: Gamma is a subset of Delta

Means: Gamma is a subset of Delta

1 occurrence in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: zero

5 occurrences in this chapter

Equation form expr-65fc0961f49725f0

v⊨A\pSat{v}{!A}

Read as: valuation v satisfies A

Means: valuation v satisfies A

5 occurrences in this chapter

Equation form expr-66061714160e100b

∧~L(x,y)=∧~C(x,y)\tf{\land}[\Log L](x,y) = \tf{\land}[\LogCL](x,y)

Read as: the conjunction truth function of logic L at x and y equals the classical conjunction truth function at x and y

Means: the conjunction truth function of logic L at x and y equals the classical conjunction truth function at x and y

1 occurrence in this chapter

Equation form expr-66635912032d5f86

⋆~:Vn→V\tf{\star} : V^n \to V

Read as: for star, from ordered n tuples of values in V to V

Means: for star, from ordered n tuples of values in V to V

1 occurrence in this chapter

Equation form expr-6899c2c078115d7c

v¯L(A)=¬~L(v¯L(B))by the evaluation definition=¬~L(v¯C(B))by inductive hypothesis=¬~C(v¯C(B))by assumption the assumption that negation agrees on true and false,since v¯C(B)∈{T,F},=v¯C(A)by the evaluation definition.\pValue v[\Log L](!A) & = \tf{\lnot}[\Log L](\pValue v[\Log L](!B)) & &\text{by \olref[val]{defn:pValue}}\\ & = \tf{\lnot}[\Log L](\pValue v[\LogCL](!B)) && \text{by inductive hypothesis}\\ & = \tf{\lnot}[\LogCL](\pValue v[\LogCL](!B)) &&\text{by assumption \olref{prop:not},}\\ &&&\text{since $\pValue v[\LogCL](!B) \in \{\True, \False\}$,}\\ & = \pValue v[\LogCL](!A) &&\text{by \olref[val]{defn:pValue}}.

Read as: Equality chain for negation. The value of A under v in logic L equals the L negation truth function applied to the L value of B, by the evaluation definition. This equals that same truth function applied to the classical value of B, by the inductive hypothesis. This equals the classical negation truth function applied to the classical value of B, by the assumption that negation agrees on true and false, since the classical value of B is either true or false. Finally this equals the classical value of A under v, by the evaluation definition. End of equality chain.

Means: Equality chain for negation. The value of A under v in logic L equals the L negation truth function applied to the L value of B, by the evaluation definition. This equals that same truth function applied to the classical value of B, by the inductive hypothesis. This equals the classical negation truth function applied to the classical value of B, by the assumption that negation agrees on true and false, since the classical value of B is either true or false. Finally this equals the classical value of A under v, by the evaluation definition. End of equality chain.

1 occurrence in this chapter

Equation form expr-6b86b273ff34fce1

11

Read as: one

Means: one

7 occurrences in this chapter

Equation form expr-6da11151a32fddba

Γ⊭CB\Gamma \Entails/[\LogCL] !B

Read as: Gamma does not entail B in classical logic

Means: Gamma does not entail B in classical logic

1 occurrence in this chapter

Equation form expr-720edbf3808e1a0a

Γ⊭LB\Gamma \Entails/[\Log L] !B

Read as: Gamma does not entail B in logic L

Means: Gamma does not entail B in logic L

1 occurrence in this chapter

Equation form expr-77728d3a75d300bb

p1→(p1∧¬p2)\Obj p_1 \lif (\Obj p_1 \land \lnot \Obj p_2)

Read as: the conditional with antecedent p subscript one and consequent the conjunction of p subscript one with not p subscript two

Means: the conditional with antecedent p subscript one and consequent the conjunction of p subscript one with not p subscript two

1 occurrence in this chapter

Equation form expr-788a697792410816

v⊨LA\pSat{v}{!A}[\Log L]

Read as: valuation v satisfies A in logic L

Means: valuation v satisfies A in logic L

4 occurrences in this chapter

Equation form expr-7cf5134707ebdb1c

v⊨LΓ\pAssign v \Entails[\Log L] \Gamma

Read as: valuation v satisfies every formula in Gamma in logic L

Means: valuation v satisfies every formula in Gamma in logic L

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

10 occurrences in this chapter

Equation form expr-847b1bb0075410b8

Γ⊨LB\Gamma \Entails[\Log L] !B

Read as: Gamma entails B in logic L

Means: Gamma entails B in logic L

1 occurrence in this chapter

Equation form expr-86550a5a2241a81a

p1→(p1⊙¬p2)\Obj p_1 \lif (\Obj p_1 \odot \lnot \Obj p_2)

Read as: the conditional with antecedent p subscript one and consequent the product conjunction of p subscript one with not p subscript two

Means: the conditional with antecedent p subscript one and consequent the product conjunction of p subscript one with not p subscript two

1 occurrence in this chapter

Equation form expr-87ccc6412302e179

Γ∪Δ⊨B\Gamma \cup \Delta \Entails !B

Read as: the union of Gamma and Delta entails B

Means: the union of Gamma and Delta entails B

1 occurrence in this chapter

Equation form expr-886721686ccc2e5b

A≡(B∨C)!A \ident (!B \lor !C)

Read as: A is the disjunction of B and C

Means: A is the disjunction of B and C

1 occurrence in this chapter

Equation form expr-889336cffefbfda1

V+={T}V^+ = \{\True\}

Read as: V plus is the singleton set containing true

Means: V plus is the singleton set containing true

1 occurrence in this chapter

Equation form expr-8a18a44f16986562

Γ⊨CB\Gamma \Entails[\LogCL] !B

Read as: Gamma entails B in classical logic

Means: Gamma entails B in classical logic

1 occurrence in this chapter

Equation form expr-8a1b602e33a8fdfb

T∈V+\True \in V^+

Read as: true belongs to the set of designated values V plus

Means: true belongs to the set of designated values V plus

2 occurrences in this chapter

Equation form expr-8cbb20bde1281f6c

Δ∪{A}⊨B\Delta \cup \{ !A\} \Entails !B

Read as: Delta together with A entails B

Means: Delta together with A entails B

1 occurrence in this chapter

Equation form expr-8d699c420d03f5ec

v⊨Γ\pSat{v}{\Gamma}

Read as: valuation v satisfies every formula in Gamma

Means: valuation v satisfies every formula in Gamma

2 occurrences in this chapter

Equation form expr-8da0d4f1e054b243

⊨LA\Entails[\Log L] !A

Read as: A is a tautology of logic L

Means: A is a tautology of logic L

1 occurrence in this chapter

Equation form expr-8e62c3a6292cd2ea

L\Log L

Read as: L

Means: L

9 occurrences in this chapter

Equation form expr-94893319a56fcba0

v:At0→{T,F}\pAssign v\colon \PVar \to \{\True, \False\}

Read as: v, mapping the propositional variables to the set containing true and false,

Means: v, mapping the propositional variables to the set containing true and false,

1 occurrence in this chapter

Equation form expr-958561a3f86a9f76

Γ⊨B\Gamma \Entails !B

Read as: Gamma entails B

Means: Gamma entails B

1 occurrence in this chapter

Equation form expr-990896f9cdb651ff

T,F∈V\True, \False \in V

Read as: true and false both belong to V

Means: true and false both belong to V

2 occurrences in this chapter

Equation form expr-a036e66d4b3c3e9c

v¯:Frm(L)→V\pValue{v} \colon \Frm[L] \to V

Read as: determined by v, from formulas of language L to values in V,

Means: determined by v, from formulas of language L to values in V,

1 occurrence in this chapter

Equation form expr-a34910944de266ad

⊙\odot

Read as: the circled dot conjunction symbol

Means: the circled dot conjunction symbol

1 occurrence in this chapter

Equation form expr-a37bce9779209494

v¯(A)=T\pValue{v}(!A) = \True

Read as: the value of A under v equals true

Means: the value of A under v equals true

2 occurrences in this chapter

Equation form expr-a4292733bf8c1b64

v¯L(B)=F\pValue v[\Log L](!B) = \False

Read as: the value of B under v in logic L equals false

Means: the value of B under v in logic L equals false

1 occurrence in this chapter

Equation form expr-a79afee06e758d4a

→~\tf{\lif}

Read as: the conditional truth function

Means: the conditional truth function

2 occurrences in this chapter

Equation form expr-ab733e02bed54e75

Γ⊨A\Gamma \Entails !A

Read as: Gamma entails A

Means: Gamma entails A

4 occurrences in this chapter

Equation form expr-af53acca4667f7cb

∨~\tf{\lor}

Read as: the disjunction truth function

Means: the disjunction truth function

1 occurrence in this chapter

Equation form expr-b0ae2a05722e43c9

(A1⋆A2)(!A_1 \star !A_2)

Read as: A subscript one, star, A subscript two, enclosed together in parentheses

Means: A subscript one, star, A subscript two, enclosed together in parentheses

1 occurrence in this chapter

Equation form expr-b105a3b312f4d49e

⋆(A1,A2)\star(!A_1,!A_2)

Read as: star applied to A subscript one and A subscript two in that order

Means: star applied to A subscript one and A subscript two in that order

1 occurrence in this chapter

Equation form expr-b24c2720089cdd3e

↔\liff

Read as: biconditional

Means: biconditional

2 occurrences in this chapter

Equation form expr-b50bb8940da5b931

L\Lang{L}

Read as: L

Means: L

1 occurrence in this chapter

Equation form expr-bc9367794d2761fe

A∈Γ!A \in \Gamma

Read as: A in Gamma

Means: A in Gamma

3 occurrences in this chapter

Equation form expr-bdcb7192fe841cb0

v\pAssign v

Read as: v

Means: v

2 occurrences in this chapter

Equation form expr-c3173025e5d9bcd9

A≡(B∧C)!A \ident (!B \land !C)

Read as: A is the conjunction of B and C

Means: A is the conjunction of B and C

1 occurrence in this chapter

Equation form expr-c528968600380362

∨~L(x,y)=∨~C(x,y)\tf{\lor}[\Log L](x,y) = \tf{\lor}[\LogCL](x,y)

Read as: the disjunction truth function of logic L at x and y equals the classical disjunction truth function at x and y

Means: the disjunction truth function of logic L at x and y equals the classical disjunction truth function at x and y

1 occurrence in this chapter

Equation form expr-c80da6054830a65a

v¯(pn)=v(pn)\pValue{v}(\Obj p_n) = \pAssign{v}(\Obj p_n)

Read as: the value of p subscript n under the evaluation function determined by v equals the value assigned to p subscript n by v

Means: the value of p subscript n under the evaluation function determined by v equals the value assigned to p subscript n by v

1 occurrence in this chapter

Equation form expr-c8259cf25517cbba

V+⊆VV^+ \subseteq V

Read as: V plus, which is a subset of V,

Means: V plus, which is a subset of V,

1 occurrence in this chapter

Equation form expr-cbb77dc5e1515d21

V≠∅V \neq \emptyset

Read as: V, which is nonempty,

Means: V, which is nonempty,

1 occurrence in this chapter

Equation form expr-cdc2ed7d3b3d72c2

⊥\lfalse

Read as: the falsity constant

Means: the falsity constant

4 occurrences in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: conditional

Means: conditional

8 occurrences in this chapter

Equation form expr-d4735e3a265e16ee

22

Read as: two

Means: two

5 occurrences in this chapter

Equation form expr-d6d1bcaf996d4843

⋆(A1,…,An)\star(!A_1, \dots, !A_n)

Read as: star applied to A subscript one through A subscript n in that order

Means: star applied to A subscript one through A subscript n in that order

1 occurrence in this chapter

Equation form expr-d71dfb8558fe1f64

v¯L(A)=v¯C(A)\pValue v[\Log L](!A) = \pValue v[\LogCL](!A)

Read as: the value of A under v in logic L equals its value under v in classical logic

Means: the value of A under v in logic L equals its value under v in classical logic

1 occurrence in this chapter

Equation form expr-d72c2cedf15e5fa4

L0\Lang L_0

Read as: L subscript zero

Means: L subscript zero

2 occurrences in this chapter

Equation form expr-d98fa5be5dbf0694

v⊨LΓ\pSat{v}{\Gamma}[\Log L]

Read as: valuation v satisfies every formula in Gamma in logic L

Means: valuation v satisfies every formula in Gamma in logic L

1 occurrence in this chapter

Equation form expr-dbb4db7f6958ecdf

⋆~L(x,y)=⋆~C(x,y)\tf{\star}[\Log L](x,y) = \tf{\star}[\LogCL](x,y)

Read as: the truth function for star in logic L at x and y equals the classical truth function for star at x and y

Means: the truth function for star in logic L at x and y equals the classical truth function for star at x and y

1 occurrence in this chapter

Equation form expr-dbf6c550baefcd9d

v¯L(A)=v(p)=v¯C(A)\pValue v[\Log L](!A) = \pAssign v(p) = \pValue v[\LogCL](!A)

Read as: the value of A under v in logic L equals the value assigned to p by v, which equals the value of A under v in classical logic

Means: the value of A under v in logic L equals the value assigned to p by v, which equals the value of A under v in classical logic

1 occurrence in this chapter

Equation form expr-ddac566cfba543b6

v¯L(A)\pValue{v}(!A)[\Log L]

Read as: of A under v in logic L

Means: of A under v in logic L

1 occurrence in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: V

Means: V

9 occurrences in this chapter

Equation form expr-de64372991421159

An!A_n

Read as: A subscript n

Means: A subscript n

1 occurrence in this chapter

Equation form expr-dffa227108b65500

A1!A_1

Read as: A subscript one

Means: A subscript one

1 occurrence in this chapter

Equation form expr-e0a9d97b3cbda796

v¯(A)∈V+\pValue{v}(!A) \in V^+

Read as: the value of A under v belongs to the set of designated values V plus

Means: the value of A under v belongs to the set of designated values V plus

1 occurrence in this chapter

Equation form expr-e20c2f8c01a8c965

△(p1∧p2)→(△p1∧△p2)\triangle (\Obj p_1 \land \Obj p_2) \lif (\triangle \Obj p_1 \land \triangle \Obj p_2)

Read as: the conditional whose antecedent is triangle applied to the conjunction of p subscript one and p subscript two, and whose consequent is the conjunction of triangle applied to p subscript one with triangle applied to p subscript two

Means: the conditional whose antecedent is triangle applied to the conjunction of p subscript one and p subscript two, and whose consequent is the conjunction of triangle applied to p subscript one with triangle applied to p subscript two

1 occurrence in this chapter

Equation form expr-e3611f411c5ab41d

v:At0→V\pAssign{v} \colon \PVar \to V

Read as: valuation v maps the propositional variables to V

Means: valuation v maps the propositional variables to V

1 occurrence in this chapter

Equation form expr-ef7e569f2c56662c

v¯L(A)=∧~L(v¯L(B),v¯L(C))by the evaluation definition=∧~L(v¯C(B),v¯C(C))by inductive hypothesis=∧~C(v¯C(B),v¯C(C))by assumption the assumption that conjunction agrees on true and false,since v¯C(B),v¯C(C)∈{T,F},=v¯C(A)by the evaluation definition.\pValue v[\Log L](!A) & = \tf{\land}[\Log L](\pValue v[\Log L](!B), \pValue v[\Log L](!C)) & &\text{by \olref[val]{defn:pValue}}\\ & = \tf{\land}[\Log L](\pValue v[\LogCL](!B),\pValue v[\LogCL](!C)) && \text{by inductive hypothesis}\\ & = \tf{\land}[\LogCL](\pValue v[\LogCL](!B),\pValue v[\LogCL](!C)) &&\text{by assumption \olref{prop:land},}\\ &&&\text{since $\pValue v[\LogCL](!B),\pValue v[\LogCL](!C) \in \{\True, \False\}$,}\\ & = \pValue v[\LogCL](!A) &&\text{by \olref[val]{defn:pValue}}.

Read as: Equality chain for conjunction. The value of A under v in logic L equals the L conjunction truth function applied to the L values of B and C, by the evaluation definition. This equals that same truth function applied to the classical values of B and C, by the inductive hypothesis. This equals the classical conjunction truth function applied to the classical values of B and C, by the assumption that conjunction agrees on true and false, since both classical values belong to the set containing true and false. Finally this equals the classical value of A under v, by the evaluation definition. End of equality chain.

Means: Equality chain for conjunction. The value of A under v in logic L equals the L conjunction truth function applied to the L values of B and C, by the evaluation definition. This equals that same truth function applied to the classical values of B and C, by the inductive hypothesis. This equals the classical conjunction truth function applied to the classical values of B and C, by the assumption that conjunction agrees on true and false, since both classical values belong to the set containing true and false. Finally this equals the classical value of A under v, by the evaluation definition. End of equality chain.

1 occurrence in this chapter

Equation form expr-efa51acdf0e7c3c4

L\Lang L

Read as: L

Means: L

6 occurrences in this chapter

Equation form expr-f1a2eae4c2fee93d

v(p)∈{T,F}\pAssign v(p) \in \{\True,\False\}

Read as: the value assigned to p by v belongs to the set containing true and false

Means: the value assigned to p by v belongs to the set containing true and false

1 occurrence in this chapter

Equation form expr-f3a719fe207daf62

v¯L(A)=T\pValue v[\Log L](!A) = \True

Read as: the value of A under v in logic L equals true

Means: the value of A under v in logic L equals true

1 occurrence in this chapter

Equation form expr-f5743d4a4f5e2ff5

x∈{T,F}x \in \{\True, \False\}

Read as: x belongs to the set containing true and false

Means: x belongs to the set containing true and false

1 occurrence in this chapter

Equation form expr-f65f435afa981240

Frm(L)\Frm[L]

Read as: F R M of L

Means: F R M of L

1 occurrence in this chapter

Equation form expr-f6f03bcc85ea86d3

v¯(⋆)=⋆~L\pValue{v}(\star) = \tf{\star}[\Log L]

Read as: the value of the constant star under v equals the truth value assigned to that constant by the matrix of logic L

Means: the value of the constant star under v equals the truth value assigned to that constant by the matrix of logic L

1 occurrence in this chapter

Equation form expr-f7bd8f50661f608e

A≡(B→C)!A \ident (!B \lif !C)

Read as: A is the conditional if B then C

Means: A is the conditional if B then C

1 occurrence in this chapter

Equation form expr-f9baaf9f77711629

F\False

Read as: false

Means: false

16 occurrences in this chapter

Propositional languages and arities

A language is a set of connectives, each with an arity. Arity zero means a constant, arity one a unary connective, and arity two a binary connective.

Source

Standard propositional language and alternative operators

The standard language lists falsity with arity zero, negation with arity one, and conjunction, disjunction and conditional each with arity two. Product conjunction uses a circled dot; a unary triangle can be added as a determinateness operator.

Source

Inductive definition of formulas

Propositional variables and zero place connectives are atomic formulas. An n place connective applied to n formulas produces a formula. The source also specifies prefix notation and the corresponding infix notation for binary connectives.

Source

Examples of formulas in different languages

The examples distinguish ordinary conjunction from the product conjunction symbol and show triangle applied to a whole conjunction on the left of a conditional and separately to its two arguments on the right.

Source

Matrix for a many-valued logic

A matrix supplies a language, a nonempty set V of truth values, a designated subset V plus, and a truth function from ordered n tuples of values to V for each n place connective. For zero place connectives the interpretation is a single value.

Source

Classical logic as a many-valued matrix

The truth values are true and false, only true is designated, and the falsity constant has value false. Four tables give the negation, conjunction, disjunction and conditional truth functions in that order.

Source

Four truth functions of classical logic

The figure contains four separately linearized tables. The unary table pairs input with output; binary tables use the first argument as the row label and the second argument as the column label. True precedes false on each axis.

Source

Classical negation truth table

Input true gives false; input false gives true. The source places inputs in the first column and outputs in the second.

Source

Classical conjunction truth table

With column inputs true then false, the row for first input true has outputs true then false, and the row for first input false has outputs false then false.

Source

Classical disjunction truth table

With column inputs true then false, the row for first input true has outputs true then true, and the row for first input false has outputs true then false.

Source

Classical conditional truth table

Rows give the antecedent, columns the consequent. With consequent true then false, the true antecedent row gives true then false, and the false antecedent row gives true then true.

Source

Valuation into a truth value set

A valuation assigns an element of V to each propositional variable. Its domain is the propositional variables, not all formulas.

Source

Evaluation function on all formulas

Extend a valuation to all formulas. On a variable use the original assignment; on a constant use the matrix value; on a compound apply the relevant truth function to the values of its arguments in their source order.

Source

Satisfaction by designated values

A valuation satisfies a formula exactly when its value belongs to V plus. Satisfaction of a set requires satisfaction of every member; negated satisfaction means the particular valuation fails to satisfy the formula.

Source

Satisfiability, tautology and entailment

Satisfiability requires at least one satisfying valuation; tautology requires every valuation. Gamma entails A exactly when every valuation satisfying all of Gamma satisfies A. These quantifiers are not interchangeable.

Source

General facts about many-valued entailment

Tautologies are consequences of the empty set. Every finite subset of a satisfiable set is satisfiable. Entailment is monotone in the premise set and satisfies the stated transitivity property. The source leaves the proof as an exercise.

Source

Exercise on semantic facts

Prove the four preceding semantic facts. No solution is supplied.

Source

Agreement with classical evaluation on classical inputs

Assuming the displayed connectives agree with classical truth functions on true and false, the source argues by induction for equality of the many-valued and classical evaluations. Its displayed valuation hypothesis restricts only one variable p, while the conclusion concerns an arbitrary formula A; the induction needs the valuation restricted to true and false on every variable occurring in A, or on all propositional variables. The source also leaves language and constant qualifications implicit. The accompanying caveat preserves all of these limitations without changing the proposition.

Source

Inductive negation case

Four equal expressions connect the L value of the negated formula to its classical value. The links use evaluation, the inductive hypothesis, agreement of negation on classical inputs, and evaluation again.

Source

Inductive conjunction case

Four equal expressions connect the L value of the conjunction to its classical value. The inductive hypothesis is applied to both arguments in source order before using agreement of the conjunction truth functions.

Source

Consequence relation included in classical consequence

With true designated and false not designated, the stated agreement conditions make every L consequence a classical consequence. The proof transfers a classical countervaluation. Where a valuation is the left operand, the semantic relation means satisfaction by that valuation rather than consequence from a premise set.

Source

Cross-reference reference-000910

the figure of classical truth functions

Source occurrence

Cross-reference reference-000911

the proposition on the four general semantic facts

Source occurrence

Cross-reference reference-000912

the evaluation definition

Source occurrence

Cross-reference reference-000913

the assumption that negation agrees on true and false

Source occurrence

Cross-reference reference-000914

the evaluation definition

Source occurrence

Cross-reference reference-000915

the evaluation definition

Source occurrence

Cross-reference reference-000916

the assumption that conjunction agrees on true and false

Source occurrence

Cross-reference reference-000917

the evaluation definition

Source occurrence

Cross-reference reference-000918

the proposition on agreement with classical evaluation

Source occurrence

Cross-reference reference-000919

the proposition on agreement with classical evaluation

Source occurrence

Source disclosures

Source-generated mathematical component tr046-source-macro-0001

C\LogCL

Read as: C

Read in context source