Intuitionistic Logic

Intuitionistic Tableaux

Equation form expr-007dac77de886d9f

σFA\sFmla{\False}{!A}[\sigma]

Read as: signed false A at prefix sigma

Means: signed false A at prefix sigma

1 occurrence in this chapter

Equation form expr-01208e159d2aec8c

∧\land

Read as: conjunction

Means: conjunction

3 occurrences in this chapter

Equation form expr-07e4058091995bcc

σ.*FA\sFmla{\False}{!A}[\sigma.{*}]

Read as: signed false A at prefix sigma dot star

Means: signed false A at prefix sigma dot star

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-0c9d36851e5eca4a

σ.n∉P(Γ)\sigma.n \notin P(\Gamma)

Read as: prefix sigma dot n is not a member of P of Gamma

Means: prefix sigma dot n is not a member of P of Gamma

1 occurrence in this chapter

Equation form expr-123f1c3159574353

σ.n1.⋯.nk\sigma.n_1.\cdots.n_k

Read as: prefix sigma dot n sub one, continuing through dot n sub k

Means: prefix sigma dot n sub one, continuing through dot n sub k

1 occurrence in this chapter

Equation form expr-13068b6c2dfe8ad1

FB∨C∈Γ\sFmla{\False}{!B \lor !C} \in \Gamma

Read as: signed false, B or C, is a member of Gamma

Means: signed false, B or C, is a member of Gamma

1 occurrence in this chapter

Equation form expr-176ac74c18155191

1.2.1.31.2.1.3

Read as: prefix one dot two dot one dot three

Means: prefix one dot two dot one dot three

1 occurrence in this chapter

Equation form expr-18069020c5e029eb

∨F\TRule{\False}{\lor}

Read as: the signed-false disjunction rule

Means: the signed-false disjunction rule

1 occurrence in this chapter

Equation form expr-19086e05fd052ff5

σSA∈Γ\sFmla{S}{!A}[\sigma] \in \Gamma

Read as: signed A with sign S at prefix sigma is a member of Gamma

Means: signed A with sign S at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: n

2 occurrences in this chapter

Equation form expr-1fcb2a117f1a4fa5

Γ0={B1,…,Bn}⊆Γ\Gamma_0 = \{!B_1, \dots, !B_n\} \subseteq \Gamma

Read as: Gamma sub zero equals the finite set containing B sub one through B sub n, and is a subset of Gamma

Means: Gamma sub zero equals the finite set containing B sub one through B sub n, and is a subset of Gamma

1 occurrence in this chapter

Equation form expr-20732e65a0b29eb1

B1,…,Bn⊨A!B_1, \dots, !B_n \Entails !A

Read as: B sub one through B sub n entail A

Means: B sub one through B sub n entail A

1 occurrence in this chapter

Equation form expr-213b22437e14fef7

∧F\TRule{\False}{\land}

Read as: the signed-false conjunction rule

Means: the signed-false conjunction rule

1 occurrence in this chapter

Equation form expr-23787e9916d65124

B1,…,Bn⊢A!B_1, \dots, !B_n \Proves !A

Read as: B sub one through B sub n prove A

Means: B sub one through B sub n prove A

1 occurrence in this chapter

Equation form expr-2502333f01ab0743

σFAandσ.*TA\sFmla{\False}{!A}[\sigma] \quad\text{and}\quad \sFmla{\True}{!A}[\sigma.{*}]

Read as: signed false A at prefix sigma, and signed true A at an accessible prefix sigma dot star

Means: signed false A at prefix sigma, and signed true A at an accessible prefix sigma dot star

1 occurrence in this chapter

Equation form expr-252f10c83610ebca

ff

Read as: f

Means: f

11 occurrences in this chapter

Equation form expr-254a38182e07f78b

σ.*FB\sFmla{\False}{!B}[\sigma.{*}]

Read as: signed false B at prefix sigma dot star

Means: signed false B at prefix sigma dot star

2 occurrences in this chapter

Equation form expr-27d5651e66d95235

TA or FA.\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.

Read as: signed true A, or signed false A

Means: signed true A, or signed false A

1 occurrence in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: negation

Means: negation

2 occurrences in this chapter

Equation form expr-28d64e1be2f9dba1

σ.n1.n2\sigma.n_1.n_2

Read as: prefix sigma dot n sub one dot n sub two

Means: prefix sigma dot n sub one dot n sub two

1 occurrence in this chapter

Equation form expr-2ccf4ae99ead0f50

M⊮⊥[f(σ)]\mSat/{M}{\lfalse}[f(\sigma)]

Read as: in model capital M at the world f of sigma, falsity is not satisfied

Means: in model capital M at the world f of sigma, falsity is not satisfied

1 occurrence in this chapter

Equation form expr-2d9c017ce04cb9be

Rf(σ)f(σ.n)Rf(\sigma)f(\sigma.n)

Read as: f of sigma bears R to f of sigma dot n

Means: f of sigma bears R to f of sigma dot n

1 occurrence in this chapter

Equation form expr-2f4583c8b7c73ba0

f′f'

Read as: f prime

Means: f prime

2 occurrences in this chapter

Equation form expr-319b49b17c38d247

Bn∈Γ!B_n \in \Gamma

Read as: B sub n is a member of Gamma

Means: B sub n is a member of Gamma

1 occurrence in this chapter

Equation form expr-333bf014c1cf8aa6

σFC\sFmla{\False}{!C}[\sigma]

Read as: signed false C at prefix sigma

Means: signed false C at prefix sigma

2 occurrences in this chapter

Equation form expr-34c12198e3393e14

¬A∨¬B⊢¬(A∧B)\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)

Read as: not A or not B proves not both A and B

Means: not A or not B proves not both A and B

1 occurrence in this chapter

Equation form expr-3762bf925b6f0e5b

i=1i=1

Read as: i equals one

Means: i equals one

2 occurrences in this chapter

Equation form expr-3ab205095a2faa4e

M⊩Bi[w]\mSat{M}{!B_i}[w]

Read as: in model capital M at world w, B sub i is satisfied

Means: in model capital M at world w, B sub i is satisfied

2 occurrences in this chapter

Equation form expr-3bbeed026b312599

→T\TRule{\True}{\lif}

Read as: the signed-true conditional rule

Means: the signed-true conditional rule

1 occurrence in this chapter

Equation form expr-3c365a42cee7c749

σ.nFC\sFmla{\False}{!C}[\sigma.n]

Read as: signed false C at prefix sigma dot n

Means: signed false C at prefix sigma dot n

1 occurrence in this chapter

Equation form expr-3e5b27e999bd94b2

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

Read as: in model capital M at the world f of sigma, B is satisfied

Means: in model capital M at the world f of sigma, B is satisfied

1 occurrence in this chapter

Equation form expr-3eecfd3e618a0fe1

f(σ.*)f(\sigma.{*})

Read as: f of prefix sigma dot star

Means: f of prefix sigma dot star

1 occurrence in this chapter

Equation form expr-4363d711b46caeda

σFB→C∈Γ\sFmla{\False}{!B \lif !C}[\sigma] \in \Gamma

Read as: signed false, if B then C, at prefix sigma is a member of Gamma

Means: signed false, if B then C, at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-4414cf0c52ecc4b0

σTB∨C∈Γ\sFmla{\True}{!B \lor !C}[\sigma] \in \Gamma

Read as: signed true, B or C, at prefix sigma is a member of Gamma

Means: signed true, B or C, at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-4579bd19edd91c98

M⊮A[f(σ)]\mSat/{M}{!A}[f(\sigma)]

Read as: in model capital M at the world f of sigma, A is not satisfied

Means: in model capital M at the world f of sigma, A is not satisfied

1 occurrence in this chapter

Equation form expr-4877305150ddd9db

∨T\TRule{\True}{\lor}

Read as: the signed-true disjunction rule

Means: the signed-true disjunction rule

1 occurrence in this chapter

Equation form expr-48c22ac377d7a0e2

σ.*\sigma.{*}

Read as: prefix sigma dot star

Means: prefix sigma dot star

4 occurrences in this chapter

Equation form expr-49e7273bd7309be4

¬F\TRule{\False}{\lnot}

Read as: the signed-false negation rule

Means: the signed-false negation rule

1 occurrence in this chapter

Equation form expr-4e255303de2156b9

T→\TRule{\lif}{\True}

Read as: the signed-true conditional rule

Means: the signed-true conditional rule

1 occurrence in this chapter

Equation form expr-4ee8e8397c9dba08

σFA→B\sFmla{\False}{!A \lif !B}[\sigma]

Read as: signed false, if A then B, at prefix sigma

Means: signed false, if A then B, at prefix sigma

1 occurrence in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: w

Means: w

3 occurrences in this chapter

Equation form expr-513e83da52aa90cf

M,f′\mModel{M}, f'

Read as: model capital M together with interpretation f prime

Means: model capital M together with interpretation f prime

1 occurrence in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: disjunction

Means: disjunction

3 occurrences in this chapter

Equation form expr-52a1eb2402f22a50

P(Γ)P(\Gamma)

Read as: P of Gamma, the set of prefixes occurring in Gamma

Means: P of Gamma, the set of prefixes occurring in Gamma

5 occurrences in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

14 occurrences in this chapter

Equation form expr-57a641fd810b5a91

⊢\Proves

Read as: proves

Means: proves

1 occurrence in this chapter

Equation form expr-5810793836dd180c

1TB1,…,1TBn,1FA.\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1].

Read as: signed true B sub one through signed true B sub n at prefix one, followed by signed false A at prefix one

Means: signed true B sub one through signed true B sub n at prefix one, followed by signed false A at prefix one

1 occurrence in this chapter

Equation form expr-59cf7cd4fdb9ff5b

T\True

Read as: true

Means: true

2 occurrences in this chapter

Equation form expr-5c62e091b8c0565f

PP

Read as: P

Means: P

4 occurrences in this chapter

Equation form expr-5ce29c3c24488728

→F\TRule{\False}{\lif}

Read as: the signed-false conditional rule

Means: the signed-false conditional rule

1 occurrence in this chapter

Equation form expr-5f5e6fc357a6dae4

σSA\sFmla{S}{!A}[\sigma]

Read as: signed A with sign S at prefix sigma

Means: signed A with sign S at prefix sigma

1 occurrence in this chapter

Equation form expr-64d171b37eb4e274

F→\TRule{\lif}{\False}

Read as: the signed-false conditional rule

Means: the signed-false conditional rule

1 occurrence in this chapter

Equation form expr-684888c0ebb17f37

**

Read as: star

Means: star

1 occurrence in this chapter

Equation form expr-6b86b273ff34fce1

11

Read as: one

Means: one

1 occurrence in this chapter

Equation form expr-7039112fb3d40070

T⊥\sFmla{\True}{\lfalse}

Read as: signed true falsity

Means: signed true falsity

1 occurrence in this chapter

Equation form expr-7404a48e4996fc8c

σT¬Aσ.*FA signed-true negationσF¬Aσ.nTA signed-false negationσTA→Bσ.*FA signed-true conditionalσFA→Bσ.nTA signed-false conditional\def\arraystretch{3}\begin{array}{|c|c|} \hline \AxiomC{\sFmla{\True}{\lnot !A}[\sigma]} \RightLabel{\TRule{\True}{\lnot}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma.{*}]$} \DisplayProof & \AxiomC{\sFmla{\False}{\lnot !A}[\sigma]} \RightLabel{\TRule{\False}{\lnot}} \UnaryInfC{\sFmla{\True}{!A}[\sigma.n]} \DisplayProof \\[1ex] \text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\ \hline \AxiomC{\sFmla{\True}{!A \lif !B}[\sigma]} \RightLabel{\TRule{\True}{\lif}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma.{*}] \quad \mid \quad \sFmla{\True}{!B}[\sigma.{*}]$} \DisplayProof & \AxiomC{\sFmla{\False}{!A \lif !B}[\sigma]} \RightLabel{\TRule{\False}{\lif}} \UnaryInfC{\sFmla{\True}{!A}[\sigma.n]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma.n]} \DisplayProof \\[1ex] \text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\ \hline \end{array}

Read as: Four prefixed tableau rules, read across each source row. Row one left, signed true not A at sigma yields signed false A at used accessible prefix sigma dot star. Row one right, signed false not A at sigma yields signed true A at a new prefix sigma dot n. Row two left, signed true if A then B at sigma branches to signed false A or signed true B at a used accessible prefix sigma dot star. Row two right, signed false if A then B at sigma yields signed true A and then signed false B at a new prefix sigma dot n. End of rule table.

Means: Four prefixed tableau rules, read across each source row. Row one left, signed true not A at sigma yields signed false A at used accessible prefix sigma dot star. Row one right, signed false not A at sigma yields signed true A at a new prefix sigma dot n. Row two left, signed true if A then B at sigma branches to signed false A or signed true B at a used accessible prefix sigma dot star. Row two right, signed false if A then B at sigma yields signed true A and then signed false B at a new prefix sigma dot n. End of rule table.

1 occurrence in this chapter

Equation form expr-78046105f9332890

f′(σ)=f(σ)f'(\sigma) = f(\sigma)

Read as: f prime of sigma equals f of sigma

Means: f prime of sigma equals f of sigma

1 occurrence in this chapter

Equation form expr-7a24e0bf2f531ed6

Γ∪{σ.nFB→C}\Gamma \cup \{\sFmla{\False}{!B \lif !C}[\sigma.n]\}

Read as: Gamma union the singleton containing signed false, if B then C, at prefix sigma dot n

Means: Gamma union the singleton containing signed false, if B then C, at prefix sigma dot n

2 occurrences in this chapter

Equation form expr-7aac21b858f44550

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

Read as: model capital M satisfies Gamma with respect to f

Means: model capital M satisfies Gamma with respect to f

6 occurrences in this chapter

Equation form expr-7ac880016e9f5b71

P(Δ)P(\Delta)

Read as: P of Delta, the set of prefixes occurring in Delta

Means: P of Delta, the set of prefixes occurring in Delta

1 occurrence in this chapter

Equation form expr-7cc21a3bda17828d

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

Read as: in model capital M at world w, B is satisfied

Means: in model capital M at world w, B is satisfied

1 occurrence in this chapter

Equation form expr-7d9f8feedfb757f6

σT¬B∈Γ\sFmla{\True}{\lnot !B}[\sigma] \in \Gamma

Read as: signed true not B at prefix sigma is a member of Gamma

Means: signed true not B at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

5 occurrences in this chapter

Equation form expr-8353b5c6cd768adf

σTC\sFmla{\True}{!C}[\sigma]

Read as: signed true C at prefix sigma

Means: signed true C at prefix sigma

2 occurrences in this chapter

Equation form expr-83e2071a842d5098

¬T\TRule{\True}{\lnot}

Read as: the signed-true negation rule

Means: the signed-true negation rule

1 occurrence in this chapter

Equation form expr-864bfe3788faaaf3

σTAandσ.*FA\sFmla{\True}{!A}[\sigma] \quad\text{and}\quad \sFmla{\False}{!A}[\sigma.{*}]

Read as: signed true A at prefix sigma, and signed false A at an accessible prefix sigma dot star

Means: signed true A at prefix sigma, and signed false A at an accessible prefix sigma dot star

1 occurrence in this chapter

Equation form expr-88af22d0eaf50e97

Γ∪{σ.*FB}\Gamma \cup \{\sFmla{\False}{!B}[\sigma.{*}]\}

Read as: Gamma union the singleton containing signed false B at prefix sigma dot star

Means: Gamma union the singleton containing signed false B at prefix sigma dot star

1 occurrence in this chapter

Equation form expr-89383b4fbde3a8bf

f′(σ.n)=wf'(\sigma.n) = w

Read as: f prime of sigma dot n equals w

Means: f prime of sigma dot n equals w

1 occurrence in this chapter

Equation form expr-8986c9fb12676f69

Rf′(σ)f′(σ.n)Rf'(\sigma)f'(\sigma.n)

Read as: f prime of sigma bears R to f prime of sigma dot n

Means: f prime of sigma bears R to f prime of sigma dot n

1 occurrence in this chapter

Equation form expr-89937f947333635b

σF¬B∈Γ\sFmla{\False}{\lnot !B}[\sigma] \in \Gamma

Read as: signed false not B at prefix sigma is a member of Gamma

Means: signed false not B at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-8a5886ea8729e9d1

σ=1.2.1\sigma = 1.2.1

Read as: sigma equals prefix one dot two dot one

Means: sigma equals prefix one dot two dot one

1 occurrence in this chapter

Equation form expr-8b73294bb700d439

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

Read as: in model capital M at the world f of sigma, A is satisfied

Means: in model capital M at the world f of sigma, A is satisfied

4 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: R

1 occurrence in this chapter

Equation form expr-8c4e80ab09662b57

σT⊥\sFmla{\True}{\bot}[\sigma]

Read as: signed true falsity at prefix sigma

Means: signed true falsity at prefix sigma

1 occurrence in this chapter

Equation form expr-8cd273e85fd60c89

f:P→Wf\colon P \to W

Read as: f is a function from the prefix set P to the world set W

Means: f is a function from the prefix set P to the world set W

1 occurrence in this chapter

Equation form expr-8dc500341e756846

σ.nTA\sFmla{\True}{!A}[\sigma.n]

Read as: signed true A at prefix sigma dot n

Means: signed true A at prefix sigma dot n

1 occurrence in this chapter

Equation form expr-8f9aaf394ef17b96

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

Read as: in model capital M at the world f of sigma, C is satisfied

Means: in model capital M at the world f of sigma, C is satisfied

1 occurrence in this chapter

Equation form expr-9838b89d557550b4

σFB\sFmla{\False}{!B}[\sigma]

Read as: signed false B at prefix sigma

Means: signed false B at prefix sigma

3 occurrences in this chapter

Equation form expr-99444ba051d2abdc

⊢A→(B→A)\Proves !A \lif (!B \lif !A)

Read as: proves if A then if B then A

Means: proves if A then if B then A

1 occurrence in this chapter

Equation form expr-9c3245dfb4ac54c1

σ\sigma

Read as: sigma

Means: sigma

18 occurrences in this chapter

Equation form expr-9cc49755e722fb91

σTA\sFmla{\True}{!A}[\sigma]

Read as: signed true A at prefix sigma

Means: signed true A at prefix sigma

3 occurrences in this chapter

Equation form expr-9db90411d96a9f72

M⊮B→C[f(σ)]\mSat/{M}{!B \lif !C}[f(\sigma)]

Read as: in model capital M at the world f of sigma, if B then C is not satisfied

Means: in model capital M at the world f of sigma, if B then C is not satisfied

2 occurrences in this chapter

Equation form expr-9ed185d202e0b9ca

⟨⟩\tuple{\ }

Read as: angle-bracket sequence notation

Means: angle-bracket sequence notation

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-a5bf061e48c501d7

σ.3\sigma.3

Read as: prefix sigma dot three

Means: prefix sigma dot three

1 occurrence in this chapter

Equation form expr-a743b31cd8da60de

σT⊥\sFmla{\True}{\lfalse}[\sigma]

Read as: signed true falsity at prefix sigma

Means: signed true falsity at prefix sigma

1 occurrence in this chapter

Equation form expr-a97850b19ac36f58

1TB1,…,1TBn,1FA\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1]

Read as: signed true B sub one through signed true B sub n at prefix one, followed by signed false A at prefix one

Means: signed true B sub one through signed true B sub n at prefix one, followed by signed false A at prefix one

1 occurrence in this chapter

Equation form expr-aa8f4af5c142c59a

f(1)=wf(1) = w

Read as: f of one equals w

Means: f of one equals w

1 occurrence in this chapter

Equation form expr-ab733e02bed54e75

Γ⊨A\Gamma \Entails !A

Read as: Gamma entails A

Means: Gamma entails A

2 occurrences in this chapter

Equation form expr-ae839bfc37daea0a

M⊮B[f(σ)]\mSat/{M}{!B}[f(\sigma)]

Read as: in model capital M at the world f of sigma, B is not satisfied

Means: in model capital M at the world f of sigma, B is not satisfied

1 occurrence in this chapter

Equation form expr-b0c0b42f7e1a7499

M⊩¬B[f(σ)]\mSat{M}{\lnot !B}[f(\sigma)]

Read as: in model capital M at the world f of sigma, not B is satisfied

Means: in model capital M at the world f of sigma, not B is satisfied

1 occurrence in this chapter

Equation form expr-b41a0604521df0b9

σTA∧BσTA signed-true conjunctionσFA∧BσFA signed-false conjunctionσTA∨BσTA signed-true disjunctionσFA∨BσFA signed-false disjunction\def\arraystretch{3}\begin{array}{|c|c|} \hline \AxiomC{\sFmla{\True}{!A \land !B}[\sigma]} \RightLabel{\TRule{\True}{\land}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\True}{!B}[\sigma]} \DisplayProof & \AxiomC{\sFmla{\False}{!A \land !B}[\sigma]} \RightLabel{\TRule{\False}{\land}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad \sFmla{\False}{!B}[\sigma]$} \DisplayProof \\[2ex] \hline \AxiomC{\sFmla{\True}{!A \lor !B}[\sigma]} \RightLabel{\TRule{\True}{\lor}} \UnaryInfC{$\sFmla{\True}{!A}[\sigma] \quad \mid \quad \sFmla{\True}{!B}[\sigma]$} \DisplayProof & \AxiomC{\sFmla{\False}{!A \lor !B}[\sigma]} \RightLabel{\TRule{\False}{\lor}} \UnaryInfC{\sFmla{\False}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma]} \DisplayProof \\[2ex] \hline \end{array}

Read as: Four prefixed propositional tableau rules, read across each source row. Row one left, signed true A and B at sigma yields signed true A and then signed true B at sigma. Row one right, signed false A and B at sigma branches to signed false A or signed false B at sigma. Row two left, signed true A or B at sigma branches to signed true A or signed true B at sigma. Row two right, signed false A or B at sigma yields signed false A and then signed false B at sigma. End of rule table.

Means: Four prefixed propositional tableau rules, read across each source row. Row one left, signed true A and B at sigma yields signed true A and then signed true B at sigma. Row one right, signed false A and B at sigma branches to signed false A or signed false B at sigma. Row two left, signed true A or B at sigma branches to signed true A or signed true B at sigma. Row two right, signed false A or B at sigma yields signed false A and then signed false B at sigma. End of rule table.

1 occurrence in this chapter

Equation form expr-b4236f414ba063d4

σFB∧C∈Γ\sFmla{\False}{!B \land !C}[\sigma] \in \Gamma

Read as: signed false, B and C, at prefix sigma is a member of Gamma

Means: signed false, B and C, at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-b5b446abb4d0323b

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

Read as: in model capital M at world w, A is satisfied

Means: in model capital M at world w, A is satisfied

1 occurrence in this chapter

Equation form expr-bb67dd931d26c8e1

{FA,TB1,…,TBn}.\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.

Read as: the set containing signed false A and signed true B sub one through signed true B sub n

Means: the set containing signed false A and signed true B sub one through signed true B sub n

1 occurrence in this chapter

Equation form expr-bc4648182536ef6a

⊢¬(A∧¬A)\Proves \lnot(!A \land \lnot !A)

Read as: proves not both A and not A

Means: proves not both A and not A

1 occurrence in this chapter

Equation form expr-bcdbfaccac910427

M,f\mModel{M}, f

Read as: model capital M together with interpretation f

Means: model capital M together with interpretation f

2 occurrences in this chapter

Equation form expr-bd914fc29ad24536

σTA→B\sFmla{\True}{!A \lif !B}[\sigma]

Read as: signed true, if A then B, at prefix sigma

Means: signed true, if A then B, at prefix sigma

1 occurrence in this chapter

Equation form expr-bf13f30556ae5738

Rf(σ)wRf(\sigma)w

Read as: f of sigma bears R to w

Means: f of sigma bears R to w

3 occurrences in this chapter

Equation form expr-bf1df883a744abb3

A∧B!A \land !B

Read as: A and B

Means: A and B

1 occurrence in this chapter

Equation form expr-c0dd9ea36e822d4b

Rf(σ)(σ.*)Rf(\sigma)(\sigma.{*})

Read as: f of sigma bears R to prefix sigma dot star

Means: f of sigma bears R to prefix sigma dot star

1 occurrence in this chapter

Equation form expr-c372d99f1f0b2736

σ.nTB\sFmla{\True}{!B}[\sigma.n]

Read as: signed true B at prefix sigma dot n

Means: signed true B at prefix sigma dot n

1 occurrence in this chapter

Equation form expr-c4e49a40ff2bb1f0

P⊆(Z+)*∖{Λ}P \subseteq (\PosInt)^* \setminus \{\emptyseq\}

Read as: P is a subset of the nonempty finite sequences of positive integers

Means: P is a subset of the nonempty finite sequences of positive integers

1 occurrence in this chapter

Equation form expr-c5ada008cc655003

FA\sFmla{\False}{!A}

Read as: signed false A

Means: signed false 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-c7521b58633df856

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

Read as: in model capital M at world w, C is not satisfied

Means: in model capital M at world w, C is not satisfied

1 occurrence in this chapter

Equation form expr-c7d083471edaf049

⊢A\Proves !A

Read as: proves A

Means: proves A

1 occurrence in this chapter

Equation form expr-c847fdbaa302c769

M⊩B[f′(σ.n)]\mSat{M}{!B}[f'(\sigma.n)]

Read as: in model capital M at the world f prime of sigma dot n, B is satisfied

Means: in model capital M at the world f prime of sigma dot n, B is satisfied

1 occurrence in this chapter

Equation form expr-cad706b77aef949a

σTB∧C∈Γ\sFmla{\True}{!B \land !C}[\sigma] \in \Gamma

Read as: signed true, B and C, at prefix sigma is a member of Gamma

Means: signed true, B and C, at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-cb8b58c892b5e758

M⊮C[f(σ)]\mSat/{M}{!C}[f(\sigma)]

Read as: in model capital M at the world f of sigma, C is not satisfied

Means: in model capital M at the world f of sigma, C is not satisfied

1 occurrence in this chapter

Equation form expr-cbbba670a3f47b53

Γ⊢A\Gamma \Proves !A

Read as: Gamma proves A

Means: Gamma proves A

4 occurrences in this chapter

Equation form expr-cdb4ee2aea69cc6a

..

Read as: a dot

Means: a dot

1 occurrence in this chapter

Equation form expr-ce6122780bbe9210

σ.*TA\sFmla{\True}{!A}[\sigma.{*}]

Read as: signed true A at prefix sigma dot star

Means: signed true A at prefix sigma dot star

1 occurrence in this chapter

Equation form expr-d01fe6b0ab557c74

M⊮B∧C[f(σ)]\mSat/{M}{!B \land !C}[f(\sigma)]

Read as: in model capital M at the world f of sigma, B and C is not satisfied

Means: in model capital M at the world f of sigma, B and C is not satisfied

1 occurrence in this chapter

Equation form expr-d03502c43d74a30b

,,

Read as: a comma

Means: a comma

1 occurrence in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: conditional

Means: conditional

2 occurrences in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: B

Means: B

1 occurrence in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model capital M

Means: model capital M

16 occurrences in this chapter

Equation form expr-d148fb86b1972296

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

Read as: in model capital M at world w, A is not satisfied

Means: in model capital M at world w, A is not satisfied

1 occurrence in this chapter

Equation form expr-d16b73ce79fc2dfd

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

Read as: in model capital M at world w, B is not satisfied

Means: in model capital M at world w, B is not satisfied

1 occurrence in this chapter

Equation form expr-d1d2852fa31bffef

A→(B→C)⊢(A∧B)→C!A \lif (!B \lif !C) \Proves (!A \land !B) \lif !C

Read as: if A then if B then C proves if both A and B then C

Means: if A then if B then C proves if both A and B then C

1 occurrence in this chapter

Equation form expr-d2da161508eebc66

w∈Ww \in W

Read as: w is a member of W

Means: w is a member of W

1 occurrence in this chapter

Equation form expr-d4657b8da2e75a37

TA\sFmla{\True}{!A}

Read as: signed true A

Means: signed true A

1 occurrence in this chapter

Equation form expr-d4a789297665f2d5

(A∧B)→C⊢A→(B→C)(!A \land !B) \lif !C \Proves !A \lif (!B \lif !C)

Read as: if both A and B then C proves if A then if B then C

Means: if both A and B then C proves if A then if B then C

1 occurrence in this chapter

Equation form expr-da528f74f8845ade

σ.n\sigma.n

Read as: prefix sigma dot n

Means: prefix sigma dot n

5 occurrences in this chapter

Equation form expr-db8757ba1b5fc53f

σ′∈P(Γ)\sigma' \in P(\Gamma)

Read as: sigma prime is a member of P of Gamma

Means: sigma prime is a member of P of Gamma

1 occurrence in this chapter

Equation form expr-dbcb6ec19cfc80e5

Δ={1FA,1TB1,…,1TBn}\Delta = \{\sFmla{\False}{!A}[1], \sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1]\}

Read as: Delta equals the set containing signed false A and signed true B sub one through B sub n, all at prefix one

Means: Delta equals the set containing signed false A and signed true B sub one through B sub n, all at prefix one

1 occurrence in this chapter

Equation form expr-dd5ced94250ee670

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

Read as: model capital M satisfies Gamma with respect to f prime

Means: model capital M satisfies Gamma with respect to f prime

1 occurrence in this chapter

Equation form expr-df72b35e73c5e0d4

σ.n1\sigma.n_1

Read as: prefix sigma dot n sub one

Means: prefix sigma dot n sub one

1 occurrence in this chapter

Equation form expr-dfa8611240a5318d

M⊮A[f(σ.*)]\mSat/{M}{!A}[f(\sigma.{*})]

Read as: in model capital M at the world f of sigma dot star, A is not satisfied

Means: in model capital M at the world f of sigma dot star, A is not satisfied

1 occurrence in this chapter

Equation form expr-e020d400b4633dcc

σ.nFB\sFmla{\False}{!B}[\sigma.n]

Read as: signed false B at prefix sigma dot n

Means: signed false B at prefix sigma dot n

1 occurrence in this chapter

Equation form expr-e326e8acffeafb82

M⊮C[f′(σ.n)]\mSat/{M}{!C}[f'(\sigma.n)]

Read as: in model capital M at the world f prime of sigma dot n, C is not satisfied

Means: in model capital M at the world f prime of sigma dot n, C is not satisfied

1 occurrence in this chapter

Equation form expr-e399ad4bf2412ea8

1.2TA→(B→C)\sFmla{\True}{!A \lif (!B \lif !C)}[1.2]

Read as: signed true, if A then if B then C, at prefix one dot two

Means: signed true, if A then if B then C, at prefix one dot two

1 occurrence in this chapter

Equation form expr-e4692cb2e04e41ec

f(σ′)=f′(σ′)f(\sigma') = f'(\sigma')

Read as: f of sigma prime equals f prime of sigma prime

Means: f of sigma prime equals f prime of sigma prime

1 occurrence in this chapter

Equation form expr-e8acd579b14893cc

σ∈(Z+)*∖{Λ}\sigma \in (\PosInt)^* \setminus \{\emptyseq\}

Read as: sigma is a nonempty finite sequence of positive integers

Means: sigma is a nonempty finite sequence of positive integers

1 occurrence in this chapter

Equation form expr-ebfa11e38546e384

Rf(σ)f(σ.*)Rf(\sigma)f(\sigma.{*})

Read as: f of sigma bears R to f of prefix sigma dot star

Means: f of sigma bears R to f of prefix sigma dot star

1 occurrence in this chapter

Equation form expr-ef2e8f6fac20e974

σTB\sFmla{\True}{!B}[\sigma]

Read as: signed true B at prefix sigma

Means: signed true B at prefix sigma

2 occurrences in this chapter

Equation form expr-f1941b975ffcc891

Δ\Delta

Read as: Delta

Means: Delta

2 occurrences in this chapter

Equation form expr-f9baaf9f77711629

F\False

Read as: false

Means: false

2 occurrences in this chapter

Equation form expr-fae0e8eec6e2c400

∧T\TRule{\True}{\land}

Read as: the signed-true conjunction rule

Means: the signed-true conjunction rule

1 occurrence in this chapter

Equation form expr-fbd3e9ce9e6e8f31

M⊩B∧C[f(σ)]\mSat{M}{!B \land !C}[f(\sigma)]

Read as: in model capital M at the world f of sigma, B and C is satisfied

Means: in model capital M at the world f of sigma, B and C is satisfied

1 occurrence in this chapter

Equation form expr-fc0a9fb41d713e25

P(Γ)∪{σ.n}P(\Gamma) \cup \{\sigma.n\}

Read as: P of Gamma union the singleton containing prefix sigma dot n

Means: P of Gamma union the singleton containing prefix sigma dot n

2 occurrences in this chapter

Equation form expr-fc3b784d15c23d3f

σ.*\sigma.*

Read as: prefix sigma dot star

Means: prefix sigma dot star

2 occurrences in this chapter

Equation form expr-fe655a6b4f57748d

σTB→C∈Γ\sFmla{\True}{!B \lif !C}[\sigma] \in \Gamma

Read as: signed true, if B then C, at prefix sigma is a member of Gamma

Means: signed true, if B then C, at prefix sigma is a member of Gamma

1 occurrence in this chapter

Equation form expr-ff0ef5c23edbf7bf

B1!B_1

Read as: B sub one

Means: B sub one

1 occurrence in this chapter

Prefixed conjunction and disjunction rule table

A two-by-two source table gives the signed true and signed false prefixed tableau rules for conjunction and disjunction. Each embedded rule proof is structurally recorded in source order.

Source

Signed true conjunction rule

From signed true A and B at sigma, continue the same branch with signed true A and signed true B at sigma.

Source

Signed false conjunction rule

From signed false A and B at sigma, split into a branch with signed false A and a branch with signed false B at sigma.

Source

Signed true disjunction rule

From signed true A or B at sigma, split into a branch with signed true A and a branch with signed true B at sigma.

Source

Signed false disjunction rule

From signed false A or B at sigma, continue the same branch with signed false A and signed false B at sigma.

Source

Prefixed negation and conditional rule table

A two-by-two source table gives the signed true and signed false prefixed rules for negation and the conditional, including used-prefix and new-prefix side conditions.

Source

Signed true negation rule

From signed true not A at sigma, add signed false A at an already used accessible prefix sigma dot star.

Source

Signed false negation rule

From signed false not A at sigma, add signed true A at a new prefix sigma dot n.

Source

Signed true conditional rule

From signed true if A then B at sigma, branch to signed false A or signed true B at an already used accessible prefix sigma dot star.

Source

Signed false conditional rule

From signed false if A then B at sigma, add signed true A and signed false B on the same branch at a new prefix sigma dot n.

Source

Example closed intuitionistic tableau

A worked closed tableau derives if A then if B then C from if both A and B then C. The enclosed tableau is read node by node with prefixes, rules, branches, and closure witnesses.

Source

Closed tableau for conditional currying

Ten prefixed signed-formula nodes form three closed branches. False-conditional and true-conditional rules introduce successive prefixes one dot one and one dot one dot one.

Source

Exercise constructing four intuitionistic tableaux

Find closed intuitionistic tableaux for four listed sequents concerning weakening, noncontradiction, uncurrying, and a De Morgan direction. No solutions are supplied.

Source

Definition of an interpretation of prefixes

An interpretation maps a set of nonempty finite positive-integer prefixes into model worlds and respects R whenever both a prefix and its one-step extension occur. It also defines satisfaction of signed true and signed false formulas.

Source

Definition of satisfiable prefixed formulas

A model satisfies a set Gamma of prefixed formulas relative to an interpretation f when it satisfies every member; Gamma is satisfiable when such a model and interpretation exist.

Source

Closure configurations are unsatisfiable

A set is unsatisfiable if it contains signed true A at sigma and signed false A at an accessible extension, or contains signed true falsity.

Source

Soundness theorem for intuitionistic tableaux

If Gamma has a closed intuitionistic tableau, then Gamma is unsatisfiable.

Source

Exercise completing the tableau soundness proof

Complete the omitted signed-false negation, signed-false disjunction, signed-true disjunction, and signed-true conditional cases of the soundness proof. No solution is supplied.

Source

Soundness corollary for provability and entailment

If Gamma proves A by a closed intuitionistic tableau, then Gamma entails A.

Source

Weak soundness corollary

If A is provable by a closed intuitionistic tableau, then A is true in every model.

Source

Cross-reference reference-001159

the prefixed conjunction and disjunction rule table

Source occurrence

Cross-reference reference-001160

the prefixed negation and conditional rule table

Source occurrence

Cross-reference reference-001161

the earlier proposition that intuitionistic truth persists along accessibility

Source occurrence

Cross-reference reference-001162

the intuitionistic tableau soundness theorem

Source occurrence

Cross-reference reference-001163

the intuitionistic tableau soundness theorem

Source occurrence

Source disclosures

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

1T(A∧B)→C\pFmla{\True}{(\formula{A} \land \formula{B}) \lif \formula{C}}{1}

Read as: signed true, if both A and B then C, at prefix one

Read in context source

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

1FA→(B→C)\pFmla{\False}{\formula{A} \lif (\formula{B} \lif \formula{C})}{1}

Read as: signed false, if A then if B then C, at prefix one

Read in context source

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

1.1TA\pFmla{\True}{\formula{A}}{1.1}

Read as: signed true A at prefix one dot one

Read in context source

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

1.1FB→C\pFmla{\False}{\formula{B} \lif \formula{C}}{1.1}

Read as: signed false, if B then C, at prefix one dot one

Read in context source

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

1.1.1TB\pFmla{\True}{\formula{B}}{1.1.1}

Read as: signed true B at prefix one dot one dot one

Read in context source

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

1.1.1FC\pFmla{\False}{\formula{C}}{1.1.1}

Read as: signed false C at prefix one dot one dot one

Read in context source

Source-generated case expression tr062-source-macro-0007

1.1.1FA∧B\pFmla{\False}{\formula{A} \land \formula{B}}{1.1.1}

Read as: signed false, A and B, at prefix one dot one dot one

Read in context source

Source-generated case expression tr062-source-macro-0008

1.1.1FA\pFmla{\False}{\formula{A}}{1.1.1}

Read as: signed false A at prefix one dot one dot one

Read in context source

Source-generated case expression tr062-source-macro-0009

1.1.1FB\pFmla{\False}{\formula{B}}{1.1.1}

Read as: signed false B at prefix one dot one dot one

Read in context source

Source-generated case expression tr062-source-macro-0010

1.1.1TC\pFmla{\True}{\formula{C}}{1.1.1}

Read as: signed true C at prefix one dot one dot one

Read in context source

Ordered structures

Prefixed conjunction and disjunction rule table

Structure: table.

Four prefixed propositional tableau rules, read across each source row. Row one left, signed true A and B at sigma yields signed true A and then signed true B at sigma. Row one right, signed false A and B at sigma branches to signed false A or signed false B at sigma. Row two left, signed true A or B at sigma branches to signed true A or signed true B at sigma. Row two right, signed false A or B at sigma yields signed false A and then signed false B at sigma. End of rule table. Caption connective labels, in source order: conjunction, then disjunction. End of table.

Read the source-bound structure in context

Signed true conjunction rule

Structure: proof tree.

Signed-true conjunction rule. From signed true A and B at sigma, continue the same branch with signed true A at sigma and signed true B at sigma.

Read the source-bound structure in context

Signed false conjunction rule

Structure: proof tree.

Signed-false conjunction rule. From signed false A and B at sigma, split into a left branch containing signed false A at sigma and a right branch containing signed false B at sigma.

Read the source-bound structure in context

Signed true disjunction rule

Structure: proof tree.

Signed-true disjunction rule. From signed true A or B at sigma, split into a left branch containing signed true A at sigma and a right branch containing signed true B at sigma.

Read the source-bound structure in context

Signed false disjunction rule

Structure: proof tree.

Signed-false disjunction rule. From signed false A or B at sigma, continue the same branch with signed false A at sigma and signed false B at sigma.

Read the source-bound structure in context

Prefixed negation and conditional rule table

Structure: table.

Four prefixed tableau rules, read across each source row. Row one left, signed true not A at sigma yields signed false A at used accessible prefix sigma dot star. Row one right, signed false not A at sigma yields signed true A at a new prefix sigma dot n. Row two left, signed true if A then B at sigma branches to signed false A or signed true B at a used accessible prefix sigma dot star. Row two right, signed false if A then B at sigma yields signed true A and then signed false B at a new prefix sigma dot n. End of rule table. Caption connective labels, in source order: negation, then conditional. End of table.

Read the source-bound structure in context

Signed true negation rule

Structure: proof tree.

Signed-true negation rule. From signed true not A at sigma, add signed false A at an already used accessible prefix sigma dot star.

Read the source-bound structure in context

Signed true conditional rule

Structure: proof tree.

Signed-true conditional rule. From signed true if A then B at sigma, split at an already used accessible prefix sigma dot star: left signed false A, right signed true B.

Read the source-bound structure in context

Signed false conditional rule

Structure: proof tree.

Signed-false conditional rule. From signed false if A then B at sigma, continue the same branch at a new prefix sigma dot n with signed true A and signed false B.

Read the source-bound structure in context

Closed tableau for conditional currying

Structure: tableau.

Closed tableau. Assumption one: signed true, if both A and B then C, at prefix one. Assumption two: signed false, if A then if B then C, at prefix one. By the signed-false conditional rule on node two: signed true A at prefix one dot one, then signed false, if B then C, at prefix one dot one. By the signed-false conditional rule on node four: signed true B at prefix one dot one dot one, then signed false C at prefix one dot one dot one. The signed-true conditional rule on node one splits from node six. One continuation is signed false, A and B, at prefix one dot one dot one, which branches by the signed-false conjunction rule on node four to signed false A at prefix one dot one dot one, closing against node three, or signed false B at prefix one dot one dot one, closing against node five. The other continuation is signed true C at prefix one dot one dot one, closing against node six. All three branches are closed. End of tableau.

Read the source-bound structure in context