Intuitionistic Logic

Soundness and Completeness

Equation form expr-01208e159d2aec8c

∧\land

Read as: conjunction

Means: conjunction

2 occurrences in this chapter

Equation form expr-01cadf2075e66b6d

Ak!A_k

Read as: A subscript k

Means: A subscript k

1 occurrence in this chapter

Equation form expr-02d8e5067e7026bc

Δ(σ)⊬A\Delta(\sigma) \Proves/ \indfrm

Read as: falsity is not derivable from Delta of sigma

Means: falsity is not derivable from Delta of sigma

1 occurrence in this chapter

Equation form expr-03569cbd604e9e67

Γ*\Gamma^*

Read as: Gamma star

Means: Gamma star

9 occurrences in this chapter

Equation form expr-03a9b09b35d993ff

n=0n=0

Read as: n equals zero

Means: n equals zero

1 occurrence in this chapter

Equation form expr-044e9e04f38b168d

M(Γ*)⊩B[Λ]\mSat{M(\Gamma^*)}{!B}[\emptyseq]

Read as: model M of Gamma star satisfies B at the empty sequence

Means: model M of Gamma star satisfies B at the empty sequence

1 occurrence in this chapter

Equation form expr-045a331a4f222a61

Γ*⊢B\Gamma^* \Proves !B

Read as: B is derivable from Gamma star

Means: B is derivable from Gamma star

2 occurrences in this chapter

Equation form expr-04c00f1bed4b874f

∨Elim\Elim{\lor}

Read as: disjunction elimination

Means: disjunction elimination

1 occurrence in this chapter

Equation form expr-053b7f536648f530

Δ1∪{B}\Delta_1 \cup \{!B\}

Read as: Delta subscript one union the singleton containing B

Means: Delta subscript one union the singleton containing B

1 occurrence in this chapter

Equation form expr-0906c36ab520717a

A→⊥!A \lif \lfalse

Read as: if A then falsity

Means: if A then falsity

1 occurrence in this chapter

Equation form expr-0910149deb8ef09f

Cj∉Γn!C_j \notin \Gamma_n

Read as: C subscript j does not belong to Gamma subscript n

Means: C subscript j does not belong to Gamma subscript n

1 occurrence in this chapter

Equation form expr-09ec6b541bb75970

k<nk<n

Read as: k is less than n

Means: k is less than n

1 occurrence in this chapter

Equation form expr-0ab83730c263f0b7

⊨A\Entails !A

Read as: A is valid

Means: A is valid

2 occurrences in this chapter

Equation form expr-0bf143354ca3b931

Γ*⊢B∨B\Gamma^* \Proves !B \lor !B

Read as: B or B is derivable from Gamma star

Means: B or B is derivable from Gamma star

2 occurrences in this chapter

Equation form expr-0c1c2c37af5d5e96

M⊩D[w]\mSat{M}{!D}[w]

Read as: model M satisfies D at world w

Means: model M satisfies D at world w

3 occurrences in this chapter

Equation form expr-0c6212743a3cab96

Δ(σ)⊢B→C\Delta(\sigma) \Proves !B \lif !C

Read as: the conditional from B to C is derivable from Delta of sigma

Means: the conditional from B to C is derivable from Delta of sigma

1 occurrence in this chapter

Equation form expr-0ef817c3f243f4b9

M⊩B[w]\mSat{M}{!B}[w]

Read as: model M satisfies B at world w

Means: model M satisfies B at world w

1 occurrence in this chapter

Equation form expr-11c90ef513ea18a1

Δ(σ)⊆Δ(σ′)\Delta(\sigma) \subseteq \Delta(\sigma')

Read as: Delta of sigma is a subset of or equal to Delta of sigma prime

Means: Delta of sigma is a subset of or equal to Delta of sigma prime

2 occurrences in this chapter

Equation form expr-13244e796db0683e

Δ(σ′)⊢B\Delta(\sigma') \Proves !B

Read as: B is derivable from Delta of sigma prime

Means: B is derivable from Delta of sigma prime

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-13f75e1a99fec552

M′\mModel{M'}

Read as: model M prime

Means: model M prime

1 occurrence in this chapter

Equation form expr-14ed0589cdf1c70f

Γ*⊇Γ\Gamma^* \supseteq \Gamma

Read as: Gamma star contains Gamma

Means: Gamma star contains Gamma

3 occurrences in this chapter

Equation form expr-1539f8a44f846db9

⊩\mSat{{}}{}

Read as: the satisfaction relation

Means: the satisfaction relation

1 occurrence in this chapter

Equation form expr-15deb173e058476c

Γn+1=Γn∪{Ci}⊢A\Gamma_{n+1} = \Gamma_n \cup \{!C_i\} \Proves !A

Read as: Gamma subscript n plus one equals Gamma subscript n together with C subscript i proves A

Means: Gamma subscript n plus one equals Gamma subscript n together with C subscript i proves A

1 occurrence in this chapter

Equation form expr-16a06475eaa6b41e

⟨B,C⟩\tuple{!B, !C}

Read as: the ordered pair B, C

Means: the ordered pair B, C

1 occurrence in this chapter

Equation form expr-1705de07fe24b5b5

σ∈V(p)\sigma \in V(p)

Read as: prefix sigma belongs to V of p

Means: prefix sigma belongs to V of p

1 occurrence in this chapter

Equation form expr-1715f249a73b8f0b

⊥I\FalseInt

Read as: intuitionistic absurdity, or explosion

Means: intuitionistic absurdity, or explosion

1 occurrence in this chapter

Equation form expr-17f86e1dd437c551

Λ∈ℕ*\emptyseq \in \Nat^*

Read as: the empty sequence belongs to the set of finite sequences of natural numbers

Means: the empty sequence belongs to the set of finite sequences of natural numbers

1 occurrence in this chapter

Equation form expr-18eeb803e2e29220

Bj∨Cj!B_j \lor !C_j

Read as: B subscript j or C subscript j

Means: B subscript j or C subscript j

2 occurrences in this chapter

Equation form expr-1a2c0b459511a696

→Intro\Intro{\lif}

Read as: conditional introduction

Means: conditional introduction

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

7 occurrences in this chapter

Equation form expr-1c0c874bae60ea7d

M⊩¬A[w]\mSat{M}{\lnot !A}[w]

Read as: model M satisfies not A at world w

Means: model M satisfies not A at world w

1 occurrence in this chapter

Equation form expr-1c0cafa7d7d4b3cd

Δ(σ)⊢A\Delta(\sigma) \Proves \indfrm

Read as: p is derivable from Delta of sigma

Means: p is derivable from Delta of sigma

3 occurrences in this chapter

Equation form expr-1ef5584f3cf54f8c

ℕ*\Nat^*

Read as: the set of finite sequences of natural numbers

Means: the set of finite sequences of natural numbers

3 occurrences in this chapter

Equation form expr-2070eac4ccbf9ca2

[w]={p∈P:w∈V(p)}[w] = \Setabs{p \in P}{w \in V(p)}

Read as: bracket w is the set of p in P such that w belongs to V of p

Means: bracket w is the set of p in P such that w belongs to V of p

1 occurrence in this chapter

Equation form expr-217a55dfbbd95edd

Γ⊢⊥\Gamma \Proves \lfalse

Read as: falsity is derivable from Gamma

Means: falsity is derivable from Gamma

1 occurrence in this chapter

Equation form expr-22140e8c4f1f5522

M⊩An[w′]\mSat{M}{!A_n}[w']

Read as: model M satisfies A subscript n at world w prime

Means: model M satisfies A subscript n at world w prime

1 occurrence in this chapter

Equation form expr-254d8bb613e146bb

M(Δ)⊩B[σ.n]\mSat{M(\Delta)}{!B}[\sigma.n]

Read as: model M of Delta satisfies B at prefix sigma dot n

Means: model M of Delta satisfies B at prefix sigma dot n

1 occurrence in this chapter

Equation form expr-25c5ad037040251f

Γn\Gamma_n

Read as: Gamma subscript n

Means: Gamma subscript n

4 occurrences in this chapter

Equation form expr-25e613a2af020f23

M⊩B∨C[w]\mSat{M}{!B \lor !C}[w]

Read as: model M satisfies the disjunction B or C at world w

Means: model M satisfies the disjunction B or C at world w

2 occurrences in this chapter

Equation form expr-27fd4929a01bf510

Δ1∪{B}⊨D\Delta_1 \cup \{!B\} \Entails !D

Read as: Delta subscript one together with B entails D

Means: Delta subscript one together with B entails D

1 occurrence in this chapter

Equation form expr-291498894ee291c0

{(Δ(σ)∪{Bn})*if Δ(σ)∪{Bn}⊬CnΔ(σ)otherwise\begin{cases} (\Delta(\sigma) \cup \{!B_n\})^* & \text{if $\Delta(\sigma) \cup \{!B_n\} \Proves/ !C_n$} \\ \Delta(\sigma) & \text{otherwise} \end{cases}

Read as: Cases. The prime extension of Delta of sigma together with B subscript n, if C subscript n is not derivable from Delta of sigma together with B subscript n. Otherwise, Delta of sigma. End cases.

Means: Cases. The prime extension of Delta of sigma together with B subscript n, if C subscript n is not derivable from Delta of sigma together with B subscript n. Otherwise, Delta of sigma. End cases.

1 occurrence in this chapter

Equation form expr-2a542a673cb39794

B1∨C1!B_1 \lor !C_1

Read as: B subscript one or C subscript one

Means: B subscript one or C subscript one

1 occurrence in this chapter

Equation form expr-2a58106bd308afaa

Γ*⊢A\Gamma^* \Proves !A

Read as: A is derivable from Gamma star

Means: A is derivable from Gamma star

1 occurrence in this chapter

Equation form expr-2ce645896979733b

M⊩Ai→An[w]\mSat{M}{!A_i \lif !A_n}[w]

Read as: model M satisfies the conditional from A subscript i to A subscript n at world w

Means: model M satisfies the conditional from A subscript i to A subscript n at world w

1 occurrence in this chapter

Equation form expr-2ddab0dfcc14b817

Δ(σ.n)⊬Cn\Delta(\sigma.n) \Proves/ !C_n

Read as: C subscript n is not derivable from Delta of sigma dot n

Means: C subscript n is not derivable from Delta of sigma dot n

1 occurrence in this chapter

Equation form expr-2e5011e124677f3b

M⊩Γ[w]\mSat{M}{\Gamma}[w]

Read as: model M satisfies every formula in Gamma at world w

Means: model M satisfies every formula in Gamma at world w

8 occurrences in this chapter

Equation form expr-2ef9dc622c8da076

Γn⊢A\Gamma_n \Proves !A

Read as: A is derivable from Gamma subscript n

Means: A is derivable from Gamma subscript n

2 occurrences in this chapter

Equation form expr-2f882aebbe54fba5

Δ(σ)⊢A\Delta(\sigma) \Proves !A

Read as: A is derivable from Delta of sigma

Means: A is derivable from Delta of sigma

1 occurrence in this chapter

Equation form expr-303d52c8d005ab48

B∈Γ!B \in \Gamma

Read as: B belongs to Gamma

Means: B belongs to Gamma

3 occurrences in this chapter

Equation form expr-32724dbf37258533

Γn+1=Γn∪{Bi}\Gamma_{n+1} = \Gamma_n \cup \{!B_i\}

Read as: Gamma subscript n plus one equals Gamma subscript n union the singleton containing B subscript i

Means: Gamma subscript n plus one equals Gamma subscript n union the singleton containing B subscript i

1 occurrence in this chapter

Equation form expr-356d1b40a1edd9f6

¬Intro\Intro\lnot

Read as: negation introduction

Means: negation introduction

2 occurrences in this chapter

Equation form expr-35bfed6fdc8fb75c

σ′=σ⌢σ′′\sigma' = \sigma \concat \sigma''

Read as: sigma prime equals sigma concatenated with sigma double prime

Means: sigma prime equals sigma concatenated with sigma double prime

1 occurrence in this chapter

Equation form expr-362a4e418110a6e8

M2⊮B\mSat/{M_2}{!B}

Read as: B is not true throughout model M subscript two

Means: B is not true throughout model M subscript two

1 occurrence in this chapter

Equation form expr-3777d9e2253f8a7c

M⊩Γ∪Δ[w]\mSat{M}{\Gamma \cup \Delta}[w]

Read as: model M satisfies every formula in Gamma union Delta at world w

Means: model M satisfies every formula in Gamma union Delta at world w

1 occurrence in this chapter

Equation form expr-380e522790172853

(Δ(σ)∪{Bn})*(\Delta(\sigma) \cup \{!B_n\})^*

Read as: the prime extension of Delta of sigma union the singleton containing B subscript n

Means: the prime extension of Delta of sigma union the singleton containing B subscript n

1 occurrence in this chapter

Equation form expr-3b33d126d8a95f0b

Ci∉Γn!C_i \notin \Gamma_n

Read as: C subscript i does not belong to Gamma subscript n

Means: C subscript i does not belong to Gamma subscript n

1 occurrence in this chapter

Equation form expr-3b524d8b1a1063d9

M⊩C[w]\mSat{M}{!C}[w]

Read as: model M satisfies C at world w

Means: model M satisfies C at world w

4 occurrences in this chapter

Equation form expr-3cad68311bf136e9

M(Δ)⊩B[σ]\mSat{M(\Delta)}{!B}[\sigma]

Read as: model M of Delta satisfies B at prefix sigma

Means: model M of Delta satisfies B at prefix sigma

3 occurrences in this chapter

Equation form expr-3f17e4788bc62bd7

Γ⊬⊥\Gamma \Proves/ \lfalse

Read as: falsity is not derivable from Gamma

Means: falsity is not derivable from Gamma

1 occurrence in this chapter

Equation form expr-405d524d374352c9

i=i(n)i = i(n)

Read as: i equals i of n

Means: i equals i of n

1 occurrence in this chapter

Equation form expr-40900c8edfc68b47

Δ(Λ)=Δ\Delta(\emptyseq) = \Delta

Read as: Delta of the empty sequence equals Delta

Means: Delta of the empty sequence equals Delta

1 occurrence in this chapter

Equation form expr-40de564437b5f1ea

B∨C∈Γ*!B \lor !C \in \Gamma^*

Read as: B or C belongs to Gamma star

Means: B or C belongs to Gamma star

1 occurrence in this chapter

Equation form expr-41b1f3903cb48eab

M⊩B→C[w]\mSat{M}{!B \lif !C}[w]

Read as: model M satisfies the conditional from B to C at world w

Means: model M satisfies the conditional from B to C at world w

1 occurrence in this chapter

Equation form expr-425393b0e0f6fcc7

M⊮A∨B\mSat/{M}{!A \lor !B}

Read as: A or B is not true throughout model M

Means: A or B is not true throughout model M

1 occurrence in this chapter

Equation form expr-42f8aa27075f2231

Γn∪{Bi}⊢A\Gamma_n \cup \{!B_i\} \Proves !A

Read as: A is derivable from Gamma subscript n together with B subscript i

Means: A is derivable from Gamma subscript n together with B subscript i

2 occurrences in this chapter

Equation form expr-457d4e8341a8e696

Γ⊭A\Gamma \Entails/ !A

Read as: Gamma does not entail A

Means: Gamma does not entail A

3 occurrences in this chapter

Equation form expr-497391c6d2b267da

Γ⊨Ai\Gamma \Entails !A_i

Read as: Gamma entails A subscript i

Means: Gamma entails A subscript i

2 occurrences in this chapter

Equation form expr-4a5272f008033c77

A⊢A!A \Proves !A

Read as: A is derivable from A

Means: A is derivable from A

1 occurrence in this chapter

Equation form expr-4e05a221f5bdd448

Δ(σ.n)=(Δ(σ)∪{B})*\Delta(\sigma.n) = (\Delta(\sigma) \cup \{!B\})^*

Read as: Delta of sigma dot n equals the prime extension of Delta of sigma together with B

Means: Delta of sigma dot n equals the prime extension of Delta of sigma together with B

1 occurrence in this chapter

Equation form expr-4fa56fe7efb19d17

Γ⊨An\Gamma \Entails !A_n

Read as: Gamma entails A subscript n

Means: Gamma entails A subscript n

2 occurrences in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: world w

Means: world w

4 occurrences in this chapter

Equation form expr-5242c333af44f123

Γi⊆Γn\Gamma_i \subseteq \Gamma_n

Read as: Gamma subscript i is a subset of or equal to Gamma subscript n

Means: Gamma subscript i is a subset of or equal to Gamma subscript n

1 occurrence in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: disjunction

Means: disjunction

2 occurrences in this chapter

Equation form expr-52d7448aebc51481

M⊩⊥[w]\mSat{M}{\lfalse}[w]

Read as: model M satisfies falsity at world w

Means: model M satisfies falsity at world w

1 occurrence in this chapter

Equation form expr-570dae66767ddcda

C∈Γn!C \in \Gamma_n

Read as: C belongs to Gamma subscript n

Means: C belongs to Gamma subscript n

1 occurrence in this chapter

Equation form expr-574f101c1fa8529b

Cn!C_n

Read as: C subscript n

Means: C subscript n

1 occurrence in this chapter

Equation form expr-5757d5082cda4415

Γ′⊆Γn\Gamma' \subseteq \Gamma_n

Read as: Gamma prime is a subset of or equal to Gamma subscript n

Means: Gamma prime is a subset of or equal to Gamma subscript n

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

13 occurrences in this chapter

Equation form expr-585084ba93c40384

Γ*⊬A\Gamma^* \Proves/ !A

Read as: A is not derivable from Gamma star

Means: A is not derivable from Gamma star

4 occurrences in this chapter

Equation form expr-594d512d5abfe81f

C∉Γ*!C \notin \Gamma^*

Read as: C does not belong to Gamma star

Means: C does not belong to Gamma star

2 occurrences in this chapter

Equation form expr-599236d580dbb47e

⊢¬¬A\Proves \lnot\lnot !A

Read as: double negation of A is derivable without assumptions

Means: double negation of A is derivable without assumptions

1 occurrence in this chapter

Equation form expr-5994ad045eed3d28

M′=⟨W′,R′,V′⟩\mModel{M'}=\tuple{W', R', V'}

Read as: model M prime is the ordered triple W prime, R prime, V prime

Means: model M prime is the ordered triple W prime, R prime, V prime

1 occurrence in this chapter

Equation form expr-59ef5b40f8e49d63

V′(p)={[w]:p∈[w]}V'(p)=\Setabs{[w]}{p \in [w]}

Read as: V prime of p is the set of equivalence classes bracket w such that p belongs to bracket w

Means: V prime of p is the set of equivalence classes bracket w such that p belongs to bracket w

1 occurrence in this chapter

Equation form expr-5af8757737968e0f

¬A\lnot!A

Read as: not A

Means: not A

1 occurrence in this chapter

Equation form expr-5afa20230f875253

n∈ℕn \in \Nat

Read as: n is a natural number

Means: n is a natural number

1 occurrence in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: P

3 occurrences in this chapter

Equation form expr-5c66900b6f67d94b

Γ∪{B}⊢C\Gamma \cup \{!B\} \Proves !C

Read as: C is derivable from Gamma together with B

Means: C is derivable from Gamma together with B

1 occurrence in this chapter

Equation form expr-5cac6a4cc9ae3d59

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

Read as: Gamma entails the conditional from B to C

Means: Gamma entails the conditional from B to C

3 occurrences in this chapter

Equation form expr-5cfd30b34ee68f31

Γ*⊢A∨¬A\Gamma^* \Proves !A \lor \lnot !A

Read as: A or not A is derivable from Gamma star

Means: A or not A is derivable from Gamma star

1 occurrence in this chapter

Equation form expr-5e507845b7921a19

Δ⊨B\Delta \Entails !B

Read as: Delta entails B

Means: Delta entails B

2 occurrences in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: zero

1 occurrence in this chapter

Equation form expr-60cc6dd7ee76fcfa

Δ(σ.n)⊢Bn\Delta(\sigma.n) \Proves !B_n

Read as: B subscript n is derivable from Delta of sigma dot n

Means: B subscript n is derivable from Delta of sigma dot n

1 occurrence in this chapter

Equation form expr-60d7cf1347fb4435

Γn+1\Gamma_{n+1}

Read as: Gamma subscript n plus one

Means: Gamma subscript n plus one

1 occurrence in this chapter

Equation form expr-60e05a2ad14219d7

Bj∉Γn!B_j \notin \Gamma_n

Read as: B subscript j does not belong to Gamma subscript n

Means: B subscript j does not belong to Gamma subscript n

1 occurrence in this chapter

Equation form expr-623fc0387a93ef39

M⊮⊥[w]\mSat/{M}{\lfalse}[w]

Read as: model M does not satisfy falsity at world w

Means: model M does not satisfy falsity at world w

1 occurrence in this chapter

Equation form expr-62c66a7a5dd70c31

mm

Read as: m

Means: m

1 occurrence in this chapter

Equation form expr-63713d1f6d4dc4ed

M⊩A\mSat{M}{!A}

Read as: A is true throughout model M

Means: A is true throughout model M

1 occurrence in this chapter

Equation form expr-639880e55e3d8094

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

Read as: Gamma together with B entails C

Means: Gamma together with B entails C

2 occurrences in this chapter

Equation form expr-64bc1e6b75a8cf78

Γ⊨Ai→An\Gamma \Entails !A_i \lif !A_n

Read as: Gamma entails the conditional from A subscript i to A subscript n

Means: Gamma entails the conditional from A subscript i to A subscript n

2 occurrences in this chapter

Equation form expr-65fb0d7eff50b8e8

Ai!A_i

Read as: A subscript i

Means: A subscript i

2 occurrences in this chapter

Equation form expr-67500429cdd36beb

n>0n>0

Read as: n is greater than zero

Means: n is greater than zero

1 occurrence in this chapter

Equation form expr-678d3e4c910641d6

Γ*=⋃n=0∞Γn\Gamma^* = \bigcup_{n=0}^\infty \Gamma_n

Read as: Gamma star equals the union of Gamma subscript n over all n from zero to infinity

Means: Gamma star equals the union of Gamma subscript n over all n from zero to infinity

1 occurrence in this chapter

Equation form expr-695bb7aa320c3174

σ′′\sigma''

Read as: sigma double prime

Means: sigma double prime

1 occurrence in this chapter

Equation form expr-6b31c1588cc84289

(A→B∨C)→((A→B)∨(A→C))(!A \lif !B \lor !C) \lif \bigl((!A \lif !B)\lor(!A \lif !C)\bigr)

Read as: if the conditional from A to the disjunction B or C holds, then either the conditional from A to B or the conditional from A to C holds

Means: if the conditional from A to the disjunction B or C holds, then either the conditional from A to B or the conditional from A to C holds

1 occurrence in this chapter

Equation form expr-6d0e429ffad83270

Γ⊨⊥\Gamma \Entails \lfalse

Read as: Gamma entails falsity

Means: Gamma entails falsity

2 occurrences in this chapter

Equation form expr-6f403fc157741a30

Γn+1⊢A\Gamma_{n+1} \Proves !A

Read as: A is derivable from Gamma subscript n plus one

Means: A is derivable from Gamma subscript n plus one

1 occurrence in this chapter

Equation form expr-6fa0962229722669

M(Γ*)⊮A[Λ]\mSat/{M(\Gamma^*)}{!A}[\emptyseq]

Read as: model M of Gamma star does not satisfy A at the empty sequence

Means: model M of Gamma star does not satisfy A at the empty sequence

1 occurrence in this chapter

Equation form expr-709815d5b5fc853c

j=i(m)j = i(m)

Read as: j equals i of m

Means: j equals i of m

1 occurrence in this chapter

Equation form expr-7161e1e96d5245fb

M⊩An[w]\mSat{M}{!A_n}[w]

Read as: model M satisfies A subscript n at world w

Means: model M satisfies A subscript n at world w

1 occurrence in this chapter

Equation form expr-72f88f0828fbb3d8

V(p)={σ:p∈Δ(σ)}V(p) = \Setabs{\sigma}{p \in \Delta(\sigma)}

Read as: V of p equals the set of sigma such that p belongs to Delta of sigma

Means: V of p equals the set of sigma such that p belongs to Delta of sigma

1 occurrence in this chapter

Equation form expr-737ddddd6ce598de

Γ⊨B∨C\Gamma \Entails !B \lor !C

Read as: Gamma entails the disjunction B or C

Means: Gamma entails the disjunction B or C

3 occurrences in this chapter

Equation form expr-76d1ed9a6f874be1

Γ′⊢A\Gamma' \Proves !A

Read as: A is derivable from Gamma prime

Means: A is derivable from Gamma prime

1 occurrence in this chapter

Equation form expr-7782d37180602968

Γ⊬⊥\Gamma \Proves/ \bot

Read as: falsity is not derivable from Gamma

Means: falsity is not derivable from Gamma

1 occurrence in this chapter

Equation form expr-7792a119fb074690

Aj!A_j

Read as: A subscript j

Means: A subscript j

1 occurrence in this chapter

Equation form expr-786aa0b01b2874ad

Rww′Rww'

Read as: world w prime is accessible from world w

Means: world w prime is accessible from world w

6 occurrences in this chapter

Equation form expr-7a138e1688b77dc4

Γ⊢B∨C\Gamma \Proves !B \lor !C

Read as: the disjunction B or C is derivable from Gamma

Means: the disjunction B or C is derivable from Gamma

1 occurrence in this chapter

Equation form expr-7c29e188c7b58eff

Δ⊢B\Delta \Proves !B

Read as: B is derivable from Delta

Means: B is derivable from Delta

1 occurrence in this chapter

Equation form expr-7cc21a3bda17828d

M⊩B[w]\mSat{M}{!B}[w]

Read as: model M satisfies B at world w

Means: model M satisfies B at world w

4 occurrences in this chapter

Equation form expr-7cd52a4ebb2a38b0

Aj≡Ai→An!A_j \ident !A_i \lif !A_n

Read as: A subscript j is identical to the conditional from A subscript i to A subscript n

Means: A subscript j is identical to the conditional from A subscript i to A subscript n

1 occurrence in this chapter

Equation form expr-7dbeca9691fabdb8

Δ2∪{C}⊨D\Delta_2 \cup \{!C\} \Entails !D

Read as: Delta subscript two together with C entails D

Means: Delta subscript two together with C entails D

1 occurrence in this chapter

Equation form expr-7e408d5b1c28df47

⟨Bn,Cn⟩\tuple{!B_n, !C_n}

Read as: the ordered pair B subscript n, C subscript n

Means: the ordered pair B subscript n, C subscript n

1 occurrence in this chapter

Equation form expr-81e18febf3859412

M⊩C[w′]\mSat{M}{!C}[w']

Read as: model M satisfies C at world w prime

Means: model M satisfies C at world w prime

3 occurrences in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

13 occurrences in this chapter

Equation form expr-83d4a511903443cd

Rσσ′R\sigma\sigma'

Read as: sigma prime is accessible from sigma under R

Means: sigma prime is accessible from sigma under R

5 occurrences in this chapter

Equation form expr-86a75837774c5ce4

→Elim\Elim{\lif}

Read as: conditional elimination

Means: conditional elimination

1 occurrence in this chapter

Equation form expr-8bc5cd4701c6816e

Γ0=Γ\Gamma_0 = \Gamma

Read as: Gamma subscript zero equals Gamma

Means: Gamma subscript zero equals Gamma

1 occurrence in this chapter

Equation form expr-8c2574892063f995

RR

Read as: accessibility relation R

Means: accessibility relation R

4 occurrences in this chapter

Equation form expr-8dd92d4879197137

Δ(σ.n)⊢B\Delta(\sigma.n) \Proves !B

Read as: B is derivable from Delta of sigma dot n

Means: B is derivable from Delta of sigma dot n

1 occurrence in this chapter

Equation form expr-8ee6543553b5a116

D∈Γ′!D \in \Gamma'

Read as: D belongs to Gamma prime

Means: D belongs to Gamma prime

1 occurrence in this chapter

Equation form expr-9051726a87762a5f

M(Δ)\mModel{M(\Delta)}

Read as: canonical model M of Delta

Means: canonical model M of Delta

1 occurrence in this chapter

Equation form expr-9110182faebe4be8

Γ∪{B}\Gamma \cup \{!B\}

Read as: Gamma union the singleton containing B

Means: Gamma union the singleton containing B

1 occurrence in this chapter

Equation form expr-911698b8731a940d

M′,[w]⊩A\mSat{M',[w]}{!A}

Read as: model M prime at equivalence class bracket w satisfies A

Means: model M prime at equivalence class bracket w satisfies A

1 occurrence in this chapter

Equation form expr-91199d874a8cc8df

Γ*(Λ)=Γ*\Gamma^*(\emptyseq) = \Gamma^*

Read as: Gamma star of the empty sequence equals Gamma star

Means: Gamma star of the empty sequence equals Gamma star

1 occurrence in this chapter

Equation form expr-92b59bb8de3808b7

Bi!B_i

Read as: B subscript i

Means: B subscript i

2 occurrences in this chapter

Equation form expr-94fd0bf2e7c5f741

M⊩A[w] iff M′⊩A[[w]]\mSat{M}{!A}[w] \text{ iff } \mSat{M'}{!A}[{[w]}]

Read as: model M satisfies A at w if and only if model M prime satisfies A at equivalence class bracket w

Means: model M satisfies A at w if and only if model M prime satisfies A at equivalence class bracket w

1 occurrence in this chapter

Equation form expr-9522bbe05d3dbd7f

W′={[w]:w∈W}W' = \Setabs{[w]}{w \in W}

Read as: W prime is the set of equivalence classes bracket w for w in W

Means: W prime is the set of equivalence classes bracket w for w in W

1 occurrence in this chapter

Equation form expr-958561a3f86a9f76

Γ⊨B\Gamma \Entails !B

Read as: Gamma entails B

Means: Gamma entails B

2 occurrences in this chapter

Equation form expr-96ecda2504700f21

Γn⊢Bi∨Ci\Gamma_n \Proves !B_i \lor !C_i

Read as: B subscript i or C subscript i is derivable from Gamma subscript n

Means: B subscript i or C subscript i is derivable from Gamma subscript n

1 occurrence in this chapter

Equation form expr-992accb9917efeb5

C!C

Read as: C

Means: C

4 occurrences in this chapter

Equation form expr-9a1aa907db88fe1f

M(Δ)⊩C[σ]\mSat{M(\Delta)}{!C}[\sigma]

Read as: model M of Delta satisfies C at prefix sigma

Means: model M of Delta satisfies C at prefix sigma

2 occurrences in this chapter

Equation form expr-9c3245dfb4ac54c1

σ\sigma

Read as: prefix sigma

Means: prefix sigma

5 occurrences in this chapter

Equation form expr-9dd4e4b646218a71

M⊩B[w′]\mSat{M}{!B}[w']

Read as: model M satisfies B at world w prime

Means: model M satisfies B at world w prime

3 occurrences in this chapter

Equation form expr-9fb4a85a312442ad

An∈Γ!A_n \in \Gamma

Read as: A subscript n belongs to Gamma

Means: A subscript n belongs to Gamma

1 occurrence in this chapter

Equation form expr-9fc431041d4c363b

M⊩\mSat{M}{}

Read as: satisfaction in model M

Means: satisfaction in model M

1 occurrence in this chapter

Equation form expr-a069349528cb819f

Δ(σ)∪{Bn}⊬Cn\Delta(\sigma) \cup \{!B_n\} \Proves/ !C_n

Read as: C subscript n is not derivable from Delta of sigma together with B subscript n

Means: C subscript n is not derivable from Delta of sigma together with B subscript n

1 occurrence in this chapter

Equation form expr-a0a5c24281bb132c

M1⊮A\mSat/{M_1}{!A}

Read as: A is not true throughout model M subscript one

Means: A is not true throughout model M subscript one

1 occurrence in this chapter

Equation form expr-a14ec3f38238b4d6

Rσ(σ.n)R\sigma(\sigma.n)

Read as: prefix sigma dot n is accessible from sigma under R

Means: prefix sigma dot n is accessible from sigma under R

1 occurrence in this chapter

Equation form expr-a180a3d7b6af53e6

Γn⊬A\Gamma_n \Proves/ !A

Read as: A is not derivable from Gamma subscript n

Means: A is not derivable from Gamma subscript n

3 occurrences in this chapter

Equation form expr-a374f128563b6def

M(Δ)⊩A[σ]\mSat{M(\Delta)}{!A}[\sigma]

Read as: model M of Delta satisfies A at prefix sigma

Means: model M of Delta satisfies A at prefix sigma

1 occurrence in this chapter

Equation form expr-a53a25ad7fa765d7

σ⌢⟨n⟩\sigma \concat \tuple{n}

Read as: prefix sigma concatenated with the one-element sequence n

Means: prefix sigma concatenated with the one-element sequence n

1 occurrence in this chapter

Equation form expr-a59de263cbef3d23

M⊩Ai[w]\mSat{M}{!A_i}[w]

Read as: model M satisfies A subscript i at world w

Means: model M satisfies A subscript i at world w

2 occurrences in this chapter

Equation form expr-a669a34fed7cec18

Δ(σ′)⊬B\Delta(\sigma') \Proves/ !B

Read as: B is not derivable from Delta of sigma prime

Means: B is not derivable from Delta of sigma prime

1 occurrence in this chapter

Equation form expr-a70f5d877ba66dcf

B→C!B\lif !C

Read as: if B then C

Means: if B then C

1 occurrence in this chapter

Equation form expr-a751e143a18fd48e

W=ℕ*W = \Nat^*

Read as: W equals the set of finite sequences of natural numbers

Means: W equals the set of finite sequences of natural numbers

1 occurrence in this chapter

Equation form expr-a759389a7a2d29f7

Δ1∪{B}⊨D\Delta_1 \cup \{!B\} \Entails !D

Read as: Delta subscript one together with B entails D

Means: Delta subscript one together with B entails D

1 occurrence in this chapter

Equation form expr-a7d4cd3f5eeccbce

M⊩Δ[w]\mSat{M}{\Delta}[w]

Read as: model M satisfies every formula in Delta at world w

Means: model M satisfies every formula in Delta at world w

1 occurrence in this chapter

Equation form expr-a84959a753d82ca7

M⊮A\mSat/{M}{!A}

Read as: A is not true throughout model M

Means: A is not true throughout model M

2 occurrences in this chapter

Equation form expr-a8ad7a00dff62e39

Γ⊢B\Gamma \Proves !B

Read as: B is derivable from Gamma

Means: B is derivable from Gamma

1 occurrence in this chapter

Equation form expr-a9702afa0cf8d7ec

B∨C!B \lor !C

Read as: B or C

Means: B or C

3 occurrences in this chapter

Equation form expr-aa293e77094504f5

Δ(σ)∪{B}⊬C\Delta(\sigma) \cup \{!B\} \Proves/ !C

Read as: C is not derivable from Delta of sigma together with B

Means: C is not derivable from Delta of sigma together with B

1 occurrence in this chapter

Equation form expr-aab8fa51f5b66206

σ⌢σ′\sigma \concat \sigma'

Read as: sigma concatenated with sigma prime

Means: sigma concatenated with sigma prime

1 occurrence in this chapter

Equation form expr-aabc6d88cbd006dc

R′R'

Read as: R prime

Means: R prime

1 occurrence in this chapter

Equation form expr-ab733e02bed54e75

Γ⊨A\Gamma \Entails !A

Read as: Gamma entails A

Means: Gamma entails A

8 occurrences in this chapter

Equation form expr-ab7caf0e56db2de6

Δ(σ.n)⊬C\Delta(\sigma.n) \Proves/ !C

Read as: C is not derivable from Delta of sigma dot n

Means: C is not derivable from Delta of sigma dot n

1 occurrence in this chapter

Equation form expr-ac1af1a7d106aafd

Δ(σ)⊢B\Delta(\sigma) \Proves !B

Read as: B is derivable from Delta of sigma

Means: B is derivable from Delta of sigma

3 occurrences in this chapter

Equation form expr-ac5217203ef7dcda

Γ′⊆Γ*\Gamma' \subseteq \Gamma^*

Read as: Gamma prime is a subset of or equal to Gamma star

Means: Gamma prime is a subset of or equal to Gamma star

1 occurrence in this chapter

Equation form expr-ad9293b54c2b636f

(A→B)∨(B→A)(!A \lif !B) \lor (!B \lif !A)

Read as: either if A then B, or if B then A

Means: either if A then B, or if B then A

1 occurrence in this chapter

Equation form expr-adb65e21934cb042

Δ(σ′)⊢C\Delta(\sigma') \Proves !C

Read as: C is derivable from Delta of sigma prime

Means: C is derivable from Delta of sigma prime

2 occurrences in this chapter

Equation form expr-adfbb17667a0b11e

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

Read as: Gamma union Delta entails C

Means: Gamma union Delta entails C

1 occurrence in this chapter

Equation form expr-ae5e7e88468f5d1b

Δ2∪{C}⊢D\Delta_2 \cup \{!C\} \Proves !D

Read as: D is derivable from Delta subscript two together with C

Means: D is derivable from Delta subscript two together with C

1 occurrence in this chapter

Equation form expr-af05a6f63b3b3e91

M⊩Δ2∪{C}[w]\mSat{M}{\Delta_2 \cup \{!C\}}[w]

Read as: model M satisfies every formula in Delta subscript two together with C at world w

Means: model M satisfies every formula in Delta subscript two together with C at world w

1 occurrence in this chapter

Equation form expr-b13bda3683a204e3

B∈Γ*!B \in \Gamma^*

Read as: B belongs to Gamma star

Means: B belongs to Gamma star

2 occurrences in this chapter

Equation form expr-b252e0975c6d0f59

B∈Γm+1!B \in \Gamma_{m+1}

Read as: B belongs to Gamma subscript m plus one

Means: B belongs to Gamma subscript m plus one

1 occurrence in this chapter

Equation form expr-b267c5398f313b52

Bi∉Γn!B_i \notin \Gamma_n

Read as: B subscript i does not belong to Gamma subscript n

Means: B subscript i does not belong to Gamma subscript n

1 occurrence in this chapter

Equation form expr-b293e692bb1be807

Γn⊢B∨C\Gamma_n \Proves !B \lor !C

Read as: B or C is derivable from Gamma subscript n

Means: B or C is derivable from Gamma subscript n

2 occurrences in this chapter

Equation form expr-b2f4990d4c4a7b47

Γn+1=Γn∪{Ci}\Gamma_{n+1} = \Gamma_n \cup \{!C_i\}

Read as: Gamma subscript n plus one equals Gamma subscript n union the singleton containing C subscript i

Means: Gamma subscript n plus one equals Gamma subscript n union the singleton containing C subscript i

2 occurrences in this chapter

Equation form expr-b402eecb8617d377

Δ2∪{C}\Delta_2 \cup \{!C\}

Read as: Delta subscript two union the singleton containing C

Means: Delta subscript two union the singleton containing C

1 occurrence in this chapter

Equation form expr-b499649b30456ffe

Γn⊢Bi∨Ci\Gamma _n \Proves !B_i \lor !C_i

Read as: B subscript i or C subscript i is derivable from Gamma subscript n

Means: B subscript i or C subscript i is derivable from Gamma subscript n

1 occurrence in this chapter

Equation form expr-b4dc54da3b693380

Γn+1=Γn\Gamma_{n+1} = \Gamma_n

Read as: Gamma subscript n plus one equals Gamma subscript n

Means: Gamma subscript n plus one equals Gamma subscript n

2 occurrences in this chapter

Equation form expr-b5b446abb4d0323b

M⊩A[w]\mSat{M}{!A}[w]

Read as: model M satisfies A at world w

Means: model M satisfies A at world w

2 occurrences in this chapter

Equation form expr-b61fb3db87e3950f

C∈Γm+1!C \in \Gamma_{m+1}

Read as: C belongs to Gamma subscript m plus one

Means: C belongs to Gamma subscript m plus one

1 occurrence in this chapter

Equation form expr-b8a1bf1bab77ec11

σ′\sigma'

Read as: sigma prime

Means: sigma prime

3 occurrences in this chapter

Equation form expr-b8faeff0e554be8a

C∈Γ*!C \in \Gamma^*

Read as: C belongs to Gamma star

Means: C belongs to Gamma star

1 occurrence in this chapter

Equation form expr-b963a987ed5b348c

Γn⊢Bj∨Cj\Gamma_n \Proves !B_j \lor !C_j

Read as: B subscript j or C subscript j is derivable from Gamma subscript n

Means: B subscript j or C subscript j is derivable from Gamma subscript n

1 occurrence in this chapter

Equation form expr-b99d2e5f37ae7e17

w′w'

Read as: world w prime

Means: world w prime

5 occurrences in this chapter

Equation form expr-bc9367794d2761fe

A∈Γ!A \in \Gamma

Read as: A belongs to Gamma

Means: A belongs to Gamma

2 occurrences in this chapter

Equation form expr-bebf1d022c494084

M⊩An[w]\mSat{M}{!A_n}[w]

Read as: model M satisfies A subscript n at world w

Means: model M satisfies A subscript n at world w

2 occurrences in this chapter

Equation form expr-bfd30497e63abb96

M,w⊩A\mSat{M,w}{!A}

Read as: model M at world w satisfies A

Means: model M at world w satisfies A

1 occurrence in this chapter

Equation form expr-c1e084fc9d3910aa

σ.n∈ℕ*\sigma.n \in \Nat^*

Read as: prefix sigma dot n belongs to the set of finite sequences of natural numbers

Means: prefix sigma dot n belongs to the set of finite sequences of natural numbers

1 occurrence in this chapter

Equation form expr-c1f1076deacc2bb4

∨Intro\Intro{\lor}

Read as: disjunction introduction

Means: disjunction introduction

1 occurrence in this chapter

Equation form expr-c3d4c7172226e1d9

M⊩Γ[w′]\mSat{M}{\Gamma}[w']

Read as: model M satisfies every formula in Gamma at world w prime

Means: model M satisfies every formula in Gamma at world w prime

1 occurrence in this chapter

Equation form expr-c555b1902ac29ff7

A⊨A!A \Entails !A

Read as: A entails A

Means: A entails A

1 occurrence in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not A

Means: not A

1 occurrence in this chapter

Equation form expr-c65e09c6283798e2

∧Intro\Intro{\land}

Read as: conjunction introduction

Means: conjunction introduction

1 occurrence in this chapter

Equation form expr-c6738fb70298a21f

B2∨C2!B_2 \lor !C_2

Read as: B subscript two or C subscript two

Means: B subscript two or C subscript two

1 occurrence in this chapter

Equation form expr-c6f4c1035772ac1e

Γn∪{Bi}⊬A\Gamma_n \cup \{!B_i\} \Proves/ !A

Read as: A is not derivable from Gamma subscript n together with B subscript i

Means: A is not derivable from Gamma subscript n together with B subscript i

2 occurrences in this chapter

Equation form expr-c7d083471edaf049

⊢A\Proves !A

Read as: A is derivable without assumptions

Means: A is derivable without assumptions

2 occurrences in this chapter

Equation form expr-c87721b01028b385

⊢B\Proves !B

Read as: B is derivable without assumptions

Means: B is derivable without assumptions

1 occurrence in this chapter

Equation form expr-cb8d8ab6c0ba65cc

¬Elim\Elim\lnot

Read as: negation elimination

Means: negation elimination

2 occurrences in this chapter

Equation form expr-cbbba670a3f47b53

Γ⊢A\Gamma \Proves !A

Read as: A is derivable from Gamma

Means: A is derivable from Gamma

6 occurrences in this chapter

Equation form expr-ccd2040af9c3689f

M(Γ*)\mModel{M(\Gamma^*)}

Read as: canonical model M of Gamma star

Means: canonical model M of Gamma star

1 occurrence in this chapter

Equation form expr-ccf32749a1e0e16a

Γ⊨C\Gamma \Entails !C

Read as: Gamma entails C

Means: Gamma entails C

1 occurrence in this chapter

Equation form expr-ccf8e514cc3908ad

σ∈ℕ*\sigma \in \Nat^*

Read as: sigma is a finite sequence of natural numbers

Means: sigma is a finite sequence of natural numbers

2 occurrences in this chapter

Equation form expr-cdc2ed7d3b3d72c2

⊥\lfalse

Read as: falsity

Means: falsity

1 occurrence in this chapter

Equation form expr-cdc7d84a7a25b566

Δ(σ)⊆Δ(σ.n)\Delta(\sigma) \subseteq \Delta(\sigma.n)

Read as: Delta of sigma is a subset of or equal to Delta of sigma dot n

Means: Delta of sigma is a subset of or equal to Delta of sigma dot n

2 occurrences in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: conditional

Means: conditional

1 occurrence in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: B

Means: B

3 occurrences in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model M

Means: model M

6 occurrences in this chapter

Equation form expr-d0acf6650c13e298

∧Elim\Elim{\land}

Read as: conjunction elimination

Means: conjunction elimination

1 occurrence in this chapter

Equation form expr-d148fb86b1972296

M⊮A[w]\mSat/{M}{!A}[w]

Read as: model M does not satisfy A at world w

Means: model M does not satisfy A at world w

1 occurrence in this chapter

Equation form expr-d44e11b041ae1e79

M(Δ)⊩A[σ]\mSat{M(\Delta)}{\indfrm}[\sigma]

Read as: model M of Delta satisfies p at prefix sigma

Means: model M of Delta satisfies p at prefix sigma

4 occurrences in this chapter

Equation form expr-d44f243b657ba50b

Γ⊢B→C\Gamma \Proves !B \lif !C

Read as: the conditional from B to C is derivable from Gamma

Means: the conditional from B to C is derivable from Gamma

1 occurrence in this chapter

Equation form expr-d61252d38c5eba2f

B→C!B \lif !C

Read as: if B then C

Means: if B then C

1 occurrence in this chapter

Equation form expr-d629deeb0e872c5e

M(Δ)⊮B[σ′]\mSat/{M(\Delta)}{!B}[\sigma']

Read as: model M of Delta does not satisfy B at prefix sigma prime

Means: model M of Delta does not satisfy B at prefix sigma prime

1 occurrence in this chapter

Equation form expr-d826a37801d792cd

i≤ni \le n

Read as: i is less than or equal to n

Means: i is less than or equal to n

1 occurrence in this chapter

Equation form expr-d9fdc25f77cd713c

Bi∨Ci!B_i \lor !C_i

Read as: B subscript i or C subscript i

Means: B subscript i or C subscript i

2 occurrences in this chapter

Equation form expr-da528f74f8845ade

σ.n\sigma.n

Read as: prefix sigma dot n

Means: prefix sigma dot n

1 occurrence in this chapter

Equation form expr-dadf4fe02fa3ab32

Δ(σ)⊢C\Delta(\sigma) \Proves !C

Read as: C is derivable from Delta of sigma

Means: C is derivable from Delta of sigma

2 occurrences in this chapter

Equation form expr-db64a5fd648ba9f0

M⊩Γ\mSat{M}{\Gamma}

Read as: every formula in Gamma is true throughout model M

Means: every formula in Gamma is true throughout model M

1 occurrence in this chapter

Equation form expr-dd0e6303b263f726

Γn+1={Γn∪{Bi(n)}if Γn∪{Bi(n)}⊬AΓn∪{Ci(n)}otherwise\Gamma_{n+1} = \begin{cases} \Gamma_n \cup \{!B_{i(n)}\} & \text{if $\Gamma_n \cup \{!B_{i(n)}\} \Proves/ !A$} \\ \Gamma_n \cup \{!C_{i(n)}\} & \text{otherwise} \end{cases}

Read as: Gamma subscript n plus one is defined by cases. It is Gamma subscript n union the singleton containing B subscript i of n if A is not derivable from that union. Otherwise it is Gamma subscript n union the singleton containing C subscript i of n. End cases.

Means: Gamma subscript n plus one is defined by cases. It is Gamma subscript n union the singleton containing B subscript i of n if A is not derivable from that union. Otherwise it is Gamma subscript n union the singleton containing C subscript i of n. End cases.

1 occurrence in this chapter

Equation form expr-dd1b44f4a83297ba

Ci!C_i

Read as: C subscript i

Means: C subscript i

2 occurrences in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: V

Means: V

1 occurrence in this chapter

Equation form expr-de64372991421159

An!A_n

Read as: A subscript n

Means: A subscript n

4 occurrences in this chapter

Equation form expr-de7d1b721a1e0632

ii

Read as: i

Means: i

2 occurrences in this chapter

Equation form expr-dfb3201fe21c8bb6

Δ(σ)⊬B→C\Delta(\sigma) \Proves/ !B \lif !C

Read as: the conditional from B to C is not derivable from Delta of sigma

Means: the conditional from B to C is not derivable from Delta of sigma

1 occurrence in this chapter

Equation form expr-dffa227108b65500

A1!A_1

Read as: A subscript one

Means: A subscript one

5 occurrences in this chapter

Equation form expr-e255e0fa213e3afb

M(Δ)⊮C[σ.n]\mSat/{M(\Delta)}{!C}[\sigma.n]

Read as: model M of Delta does not satisfy C at prefix sigma dot n

Means: model M of Delta does not satisfy C at prefix sigma dot n

1 occurrence in this chapter

Equation form expr-e354ec04cb9d8bce

M⊩(A→B)∨(B→A)\mSat{M}{(!A \lif !B)\lor(!B \lif !A)}

Read as: either if A then B, or if B then A, is true throughout model M

Means: either if A then B, or if B then A, is true throughout model M

1 occurrence in this chapter

Equation form expr-e3629f8953fb2967

M′⊮A\mSat/{M'}{!A}

Read as: A is not true throughout finite model M prime

Means: A is not true throughout finite model M prime

1 occurrence in this chapter

Equation form expr-e37350b2027ef768

Δ1∪{B}⊢D\Delta_1 \cup \{!B\} \Proves !D

Read as: D is derivable from Delta subscript one together with B

Means: D is derivable from Delta subscript one together with B

1 occurrence in this chapter

Equation form expr-e39c1fa87191d1f2

(¬¬A→A)→(A∨¬A)(\lnot\lnot !A \lif !A) \lif (!A \lor \lnot !A)

Read as: if double-negation elimination for A holds, then A or not A

Means: if double-negation elimination for A holds, then A or not A

1 occurrence in this chapter

Equation form expr-e7202a171f80dada

B∉Γ*!B \notin \Gamma^*

Read as: B does not belong to Gamma star

Means: B does not belong to Gamma star

2 occurrences in this chapter

Equation form expr-e761965b76608775

M⊩Ai[w′]\mSat{M}{!A_i}[w']

Read as: model M satisfies A subscript i at world w prime

Means: model M satisfies A subscript i at world w prime

1 occurrence in this chapter

Equation form expr-e78a1414699d2dfc

A∨B∈Γ!A \lor !B \in \Gamma

Read as: A or B belongs to Gamma

Means: A or B belongs to Gamma

1 occurrence in this chapter

Equation form expr-e905db4f2fad9e7d

⟨B2,C2⟩\tuple{!B_2, !C_2}

Read as: the ordered pair B subscript two, C subscript two

Means: the ordered pair B subscript two, C subscript two

1 occurrence in this chapter

Equation form expr-e92416e84f8319bb

An=A!A_n = !A

Read as: A subscript n equals A

Means: A subscript n equals A

1 occurrence in this chapter

Equation form expr-e9fe8ee5ada9c8bf

W′W'

Read as: W prime

Means: W prime

1 occurrence in this chapter

Equation form expr-ea07ef0e7ec14325

Γi\Gamma_i

Read as: Gamma subscript i

Means: Gamma subscript i

1 occurrence in this chapter

Equation form expr-eb1061b2d2f3fd57

Δ(σ)∪{Bn}\Delta(\sigma) \cup \{!B_n\}

Read as: Delta of sigma union the singleton containing B subscript n

Means: Delta of sigma union the singleton containing B subscript n

1 occurrence in this chapter

Equation form expr-eb45097515077452

M(Δ)⊮A[σ]\mSat/{M(\Delta)}{\indfrm}[\sigma]

Read as: model M of Delta does not satisfy falsity at prefix sigma

Means: model M of Delta does not satisfy falsity at prefix sigma

2 occurrences in this chapter

Equation form expr-ec034bd143a43107

¬¬A→A\lnot\lnot!A \lif !A

Read as: if not not A then A

Means: if not not A then A

1 occurrence in this chapter

Equation form expr-ed2fe9718064afee

M(Δ)⊩C[σ′]\mSat{M(\Delta)}{!C}[\sigma']

Read as: model M of Delta satisfies C at prefix sigma prime

Means: model M of Delta satisfies C at prefix sigma prime

1 occurrence in this chapter

Equation form expr-f09406a1860d079f

Γn+1⊬A\Gamma_{n+1} \Proves/ !A

Read as: A is not derivable from Gamma subscript n plus one

Means: A is not derivable from Gamma subscript n plus one

2 occurrences in this chapter

Equation form expr-f1941b975ffcc891

Δ\Delta

Read as: Delta

Means: Delta

7 occurrences in this chapter

Equation form expr-f1d1e0d9bd2ea89c

B∈Γn!B \in \Gamma_n

Read as: B belongs to Gamma subscript n

Means: B belongs to Gamma subscript n

1 occurrence in this chapter

Equation form expr-f251123bc41bc566

Δ(σ.n)=\Delta(\sigma.n) = {}

Read as: Delta of sigma dot n equals the following case definition

Means: Delta of sigma dot n equals the following case definition

1 occurrence in this chapter

Equation form expr-f473936ed7153b0b

M⊩Γ∪Δ1∪Δ2[w]\mSat{M}{\Gamma \cup \Delta_1 \cup \Delta_2}[w]

Read as: model M satisfies every formula in Gamma union Delta subscript one union Delta subscript two at world w

Means: model M satisfies every formula in Gamma union Delta subscript one union Delta subscript two at world w

1 occurrence in this chapter

Equation form expr-f62e4e6ecfecdec8

⊢A∨B\Proves !A \lor !B

Read as: A or B is derivable without assumptions

Means: A or B is derivable without assumptions

1 occurrence in this chapter

Equation form expr-f65af037e8662390

⊭A\Entails/ !A

Read as: A is not valid

Means: A is not valid

2 occurrences in this chapter

Equation form expr-f6ac033cc1d1554a

Γ⊬A\Gamma \Proves/ !A

Read as: A is not derivable from Gamma

Means: A is not derivable from Gamma

5 occurrences in this chapter

Equation form expr-f85ee5c08ff2c1e4

⟨B1,C1⟩\tuple{!B_1, !C_1}

Read as: the ordered pair B subscript one, C subscript one

Means: the ordered pair B subscript one, C subscript one

1 occurrence in this chapter

Equation form expr-f888d2e33b66d0c5

D!D

Read as: D

Means: D

2 occurrences in this chapter

Equation form expr-f8ca812f941fa5c1

Γ∪Δ1∪Δ2⊨D\Gamma \cup \Delta_1 \cup \Delta_2 \Entails !D

Read as: Gamma union Delta subscript one union Delta subscript two entails D

Means: Gamma union Delta subscript one union Delta subscript two entails D

1 occurrence in this chapter

Equation form expr-f91177e936d06340

M=⟨W,R,V⟩\mModel{M}=\tuple{W, R, V}

Read as: model M is the ordered triple W, R, V

Means: model M is the ordered triple W, R, V

1 occurrence in this chapter

Equation form expr-f9905ead1264ffa3

Δ(σ)\Delta(\sigma)

Read as: Delta of sigma

Means: Delta of sigma

4 occurrences in this chapter

Equation form expr-f990b7cd8ce3541f

M⊩Δ1∪{B}[w]\mSat{M}{\Delta_1 \cup \{!B\}}[w]

Read as: model M satisfies every formula in Delta subscript one together with B at world w

Means: model M satisfies every formula in Delta subscript one together with B at world w

1 occurrence in this chapter

Equation form expr-fc0f2fcd9429191f

Δ2∪{C}⊨D\Delta_2 \cup \{!C\} \Entails !D

Read as: Delta subscript two together with C entails D

Means: Delta subscript two together with C entails D

1 occurrence in this chapter

Equation form expr-fce8bac50716d105

Γ*⊢B∨C\Gamma^* \Proves !B \lor !C

Read as: B or C is derivable from Gamma star

Means: B or C is derivable from Gamma star

4 occurrences in this chapter

Equation form expr-fd42867faff01db0

<n<n

Read as: less than n

Means: less than n

1 occurrence in this chapter

Equation form expr-fe4d2e411e036670

i(n)i(n)

Read as: i of n

Means: i of n

6 occurrences in this chapter

Soundness theorem for the intuitionistic axiomatic calculus

If A is derivable from Gamma in the intuitionistic axiomatic calculus, then Gamma entails A. The proof uses induction on derivation length and treats axioms, assumptions, and modus ponens. Its axiom case relies on the validity of all intuitionistic axioms, which the source editorial explicitly says still needs to be proved.

Source

Soundness theorem for intuitionistic natural deduction

If A is derivable from Gamma by intuitionistic natural deduction, then Gamma entails A. The proof proceeds by induction on the derivation. Under the frozen source profile, both conjunction cases and both negation cases are left as exercises rather than supplied proofs; the remaining active cases are retained as printed.

Source

Exercise completing the natural-deduction soundness proof

Complete the soundness proof for negation introduction and negation elimination using the direct semantic definition of not A, rather than defining not A as the conditional from A to falsity. No solution is supplied.

Source

Exercise giving three intuitionistic nonderivability results

Show that three displayed formulas are not derivable in intuitionistic logic: conditional comparability, a double-negation principle implying excluded middle, and distribution of a conditional over a disjunction. No solution is supplied.

Source

Definition of a prime set of formulas

A set Gamma is prime exactly when it is consistent, contains every formula derivable from it, and has the disjunction property: whenever A or B belongs to Gamma, at least one of A and B belongs to Gamma.

Source

Lindenbaum's Lemma for intuitionistic logic

If A is not derivable from Gamma, there is a prime superset Gamma star of Gamma from which A is still not derivable. The proof constructs an increasing sequence that resolves enumerated disjunctions while preserving nonderivability.

Source

Exercise relating nonderivability of falsity to classical consistency

Show that if falsity is not derivable from Gamma, then Gamma is classically consistent by finding a valuation that makes every formula in Gamma true. No solution is supplied.

Source

Definition of the canonical intuitionistic model

For a prime set Delta, the canonical model has finite sequences of natural numbers as worlds, the initial-segment relation as accessibility, and V of p equal to the prefixes sigma for which p belongs to Delta of sigma.

Source

Truth Lemma for the canonical model

For prime Delta, model M of Delta satisfies A at prefix sigma if and only if A is derivable from Delta of sigma. The source proves the falsity, atomic, conjunction, disjunction, and conditional cases by induction; its displayed negation case has an empty proof body and is preserved as unfinished.

Source

Completeness theorem for intuitionistic logic

If Gamma entails A, then A is derivable from Gamma. The contrapositive proof extends Gamma to a prime set, uses its canonical model, and applies the Truth Lemma to obtain a countermodel whenever A is not derivable.

Source

Exercise on formulas using only variables, disjunction, and conjunction

Show that a formula containing only propositional variables, disjunction, and conjunction is not valid, and use this to show that the conditional is not definable from disjunction and conjunction. No solution is supplied.

Source

Exercise proving the disjunction property

Use completeness to prove that if A or B is derivable, then A is derivable or B is derivable. The hint asks for a combined countermodel from separate countermodels to A and B. No solution is supplied.

Source

Exercise on linearly ordered relational models

Show that every relational model whose accessibility order is linear satisfies either the conditional from A to B or the conditional from B to A. No solution is supplied.

Source

Finite-countermodel theorem

If A is not valid, then A fails in a finite model. The source identifies worlds by their true propositional variables, orders the resulting profiles by inclusion, and leaves truth preservation to an exercise. That printed construction can add accessibility and does not in general preserve all intuitionistic formulas; it is retained with an explicit source caveat rather than silently replaced by a filtration proof.

Source

Exercise finishing the finite-countermodel proof

Finish the decidability theorem by proving that model M at w satisfies A exactly when model M prime at equivalence class bracket w satisfies A, for formulas using only variables from P. No solution is supplied.

Source

Cross-reference reference-001140

the earlier proposition that intuitionistic truth persists along accessibility

Source occurrence

Cross-reference reference-001141

the natural-deduction soundness theorem

Source occurrence

Cross-reference reference-001142

the definition of truth at a world

Source occurrence

Cross-reference reference-001143

the first condition selecting a disjunction

Source occurrence

Cross-reference reference-001144

the second condition selecting a disjunction

Source occurrence

Cross-reference reference-001145

the consistency condition in the definition of a prime set

Source occurrence

Cross-reference reference-001146

the deductive-closure condition in the definition of a prime set

Source occurrence

Cross-reference reference-001147

the disjunction condition in the definition of a prime set

Source occurrence

Cross-reference reference-001148

the definition of a prime set

Source occurrence

Cross-reference reference-001149

the consistency condition in the definition of a prime set

Source occurrence

Cross-reference reference-001150

the disjunction condition in the definition of a prime set

Source occurrence

Cross-reference reference-001151

the deductive-closure condition in the definition of a prime set

Source occurrence

Cross-reference reference-001152

the definition of a prime set

Source occurrence

Cross-reference reference-001153

Lindenbaum's Lemma

Source occurrence

Cross-reference reference-001154

Lindenbaum's Lemma

Source occurrence

Cross-reference reference-001155

the definition of the canonical model

Source occurrence

Cross-reference reference-001156

the Truth Lemma

Source occurrence

Cross-reference reference-001157

the finite-countermodel theorem

Source occurrence

Cross-reference reference-001158

the finite-countermodel theorem

Source occurrence

Source disclosures

Source-generated case expression tr061-source-macro-0001

A≡⊥!A \ident \lfalse

Read as: Case: A is falsity.

Read in context source

Source-generated case expression tr061-source-macro-0002

A≡p!A \ident p

Read as: Case: A is the propositional variable p.

Read in context source

Source-generated case expression tr061-source-macro-0003

A≡¬B!A \ident \lnot !B

Read as: Case: A is the negation of B.

Read in context source

Source-generated case expression tr061-source-macro-0004

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

Read as: Case: A is the conjunction of B and C.

Read in context source

Source-generated case expression tr061-source-macro-0005

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

Read as: Case: A is the disjunction of B and C.

Read in context source

Source-generated case expression tr061-source-macro-0006

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

Read as: Case: A is the conditional from B to C.

Read in context source