Intuitionistic Logic

Semantics

Equation form expr-005518057817a68d

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-006636c39b123d81

i∈Ii \in I

Read as: i belongs to I

Means: i belongs to I

1 occurrence in this chapter

Equation form expr-01208e159d2aec8c

∧\land

Read as: conjunction

Means: conjunction

2 occurrences in this chapter

Equation form expr-0235b08a7368ce73

U∩VU \cap V

Read as: the intersection of U and V

Means: the intersection of U and V

1 occurrence in this chapter

Equation form expr-0436bbc5b893fd10

X\mModel{X}

Read as: topological model X

Means: topological model X

1 occurrence in this chapter

Equation form expr-0ab83730c263f0b7

⊨A\Entails !A

Read as: A is valid

Means: A is valid

1 occurrence in this chapter

Equation form expr-141a788a845573ec

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

Read as: model M satisfies the formula in the current induction case at world w

Means: model M satisfies the formula in the current induction case at world w

6 occurrences in this chapter

Equation form expr-148de9c5a7a44d19

pp

Read as: p

Means: p

1 occurrence in this chapter

Equation form expr-1a86e9ba6619464b

⟦A→B⟧X∩⟦A⟧X⊂⟦B⟧X\Prop{X}{!A \lif !B} \cap \Prop{X}{!A} \subset \Prop{X}{!B}

Read as: the intersection of the proposition for if A then B and the proposition for A is a proper subset of the proposition for B

Means: the intersection of the proposition for if A then B and the proposition for A is a proper subset of the proposition for B

1 occurrence in this chapter

Equation form expr-1abadd9c71f59bdc

⟦A∧B⟧X=⟦A⟧X∩⟦B⟧X\Prop{X}{!A \land !B} = \Prop{X}{!A} \cap \Prop{X}{!B}

Read as: the proposition for A and B in X equals the intersection of the proposition for A and the proposition for B

Means: the proposition for A and B in X equals the intersection of the proposition for A and the proposition for B

1 occurrence 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-2083afb38a285ef8

⊥⊢A\lfalse \Proves !A

Read as: A is derivable from falsity

Means: A is derivable from falsity

1 occurrence in this chapter

Equation form expr-238b57dc11e17be1

A⊢B!A \Proves !B

Read as: B is derivable from A

Means: B is derivable from A

1 occurrence in this chapter

Equation form expr-240381337f804e9f

A→B!A \lif !B

Read as: if A, then B

Means: if A, then B

3 occurrences in this chapter

Equation form expr-2532eb1524bb44ec

X∈OX \in \Top{O}

Read as: X belongs to script O

Means: X belongs to script O

1 occurrence in this chapter

Equation form expr-25979b28f8b02c3b

Ww={u∈W:Rwu},Rw=R∩(Ww)2, andVw(p)=V(p)∩Ww.W_w & = \Setabs{u \in W}{Rwu},\\ R_w & = R \cap (W_w)^2, \text{ and}\\ V_w(p) & = V(p) \cap W_w.

Read as: Restriction components. W subscript w is the set of u in W such that u is accessible from w. R subscript w is R intersected with the Cartesian square of W subscript w. V subscript w of p is V of p intersected with W subscript w. End components.

Means: Restriction components. W subscript w is the set of u in W such that u is accessible from w. R subscript w is R intersected with the Cartesian square of W subscript w. V subscript w of p is V of p intersected with W subscript w. End components.

1 occurrence in this chapter

Equation form expr-2b7c9ae1acc76455

⟦B∧C⟧X⊆⟦B⟧X\Prop{X}{!B \land !C} \subseteq \Prop{X}{!B}

Read as: the proposition for B and C is a subset of the proposition for B

Means: the proposition for B and C is a subset of the proposition for B

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

6 occurrences in this chapter

Equation form expr-303d52c8d005ab48

B∈Γ!B \in \Gamma

Read as: B belongs to Gamma

Means: B belongs to Gamma

2 occurrences in this chapter

Equation form expr-30cd47a4d9142c09

V⊆XV \subseteq X

Read as: V is a subset of X

Means: V is a subset of X

1 occurrence in this chapter

Equation form expr-325aa01e8967ab79

A⊨B!A \Entails !B

Read as: A entails B

Means: A entails B

1 occurrence in this chapter

Equation form expr-39f31b3a2b9e52da

O\Top{O}

Read as: script O

Means: script O

5 occurrences 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

2 occurrences in this chapter

Equation form expr-3b92e69960699487

Mw⊩Γ\mSat{M_w}{\Gamma}

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

Means: every formula in Gamma is true throughout model M subscript w

1 occurrence in this chapter

Equation form expr-3e1687df1d18403c

U⊆WU \subseteq W

Read as: U is a subset of W

Means: U is a subset of W

1 occurrence in this chapter

Equation form expr-445d41d6171b4475

B∧C⊢B!B \land !C \Proves !B

Read as: B is derivable from B and C

Means: B is derivable from B and C

1 occurrence in this chapter

Equation form expr-4745d6ca3b38fdf9

B∧C!B \land !C

Read as: B and C

Means: B and C

1 occurrence in this chapter

Equation form expr-47dc669a0d5860e9

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

Read as: B or C is derivable from C

Means: B or C is derivable from C

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: X

Means: X

8 occurrences in this chapter

Equation form expr-4f7440b4f48ff3f9

⟦A∨B⟧X=⟦A⟧X∪⟦B⟧X\Prop{X}{!A \lor !B} = \Prop{X}{!A} \cup \Prop{X}{!B}

Read as: the proposition for A or B in X equals the union of the proposition for A and the proposition for B

Means: the proposition for A or B in X equals the union of the proposition for A and the proposition for B

1 occurrence in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: w

Means: w

13 occurrences in this chapter

Equation form expr-5182ca231867dc3e

⟦A⟧X⊂⟦B⟧X\Prop{X}{!A} \subset \Prop{X}{!B}

Read as: the proposition for A in X is a proper subset of the proposition for B in X

Means: the proposition for A in X is a proper subset of the proposition for B in X

1 occurrence in this chapter

Equation form expr-529ad2daacd7efcb

∨\lor

Read as: disjunction

Means: disjunction

1 occurrence in this chapter

Equation form expr-53e526f39cf9e52d

M⊩A→⊥[w]\mSat{M}{!A \lif \lfalse}[w]

Read as: model M satisfies the conditional from A to falsity at world w

Means: model M satisfies the conditional from A to falsity at world w

1 occurrence in this chapter

Equation form expr-57885e4c75965b23

Γ\Gamma

Read as: Gamma

Means: Gamma

2 occurrences in this chapter

Equation form expr-5fa9465a39bf5723

W⊆UW \subseteq U

Read as: W is a subset of U

Means: W is a subset of U

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

3 occurrences in this chapter

Equation form expr-6455b29833af2b9b

U∪VU \cup V

Read as: the union of U and V

Means: the union of U and V

1 occurrence in this chapter

Equation form expr-69ef9ee2c45eb3b7

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

Read as: model M satisfies A at world w prime

Means: model M satisfies A at world w prime

1 occurrence in this chapter

Equation form expr-6fbaf12cc9c1efea

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

Read as: B or C is derivable from B

Means: B or C is derivable from B

1 occurrence in this chapter

Equation form expr-779b8a0a9b3ba932

w′∈V(p)w' \in V(p)

Read as: w prime belongs to V of p

Means: w prime belongs to V of p

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

7 occurrences in this chapter

Equation form expr-7a4d8f136fcb8fd2

⟦A→B⟧X=Int((X∖⟦A⟧X)∪⟦B⟧X)\Prop{X}{!A \lif !B} = \Interior{(X \setminus \Prop{X}{!A}) \cup \Prop{X}{!B}}

Read as: the proposition for if A then B in X equals the interior of the union of X minus the proposition for A and the proposition for B

Means: the proposition for if A then B in X equals the interior of the union of X minus the proposition for A and the proposition for B

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

3 occurrences in this chapter

Equation form expr-7e2285d936d514c3

⟦A→B⟧X\Prop{X}{!A \lif !B}

Read as: the proposition for if A then B in X

Means: the proposition for if A then B in X

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

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: A

Means: A

28 occurrences in this chapter

Equation form expr-8c2574892063f995

RR

Read as: R

Means: R

4 occurrences in this chapter

Equation form expr-8d2cacefc75ba038

∅\emptyset

Read as: the empty set

Means: the empty set

1 occurrence in this chapter

Equation form expr-8f61ac75ac98e885

V⊆WV \subseteq W

Read as: V is a subset of W

Means: V is a subset of W

1 occurrence in this chapter

Equation form expr-90ece2639769ff97

⟦C⟧X⊆⟦B∨C⟧X\Prop{X}{!C} \subseteq \Prop{X}{!B \lor !C}

Read as: the proposition for C is a subset of the proposition for B or C

Means: the proposition for C is a subset of the proposition for B or C

1 occurrence in this chapter

Equation form expr-9456de63da768541

⟦⊥⟧X=∅\Prop{X}{\lfalse} = \emptyset

Read as: the open-set proposition for falsity in X equals the empty set

Means: the open-set proposition for falsity in X equals the empty set

2 occurrences in this chapter

Equation form expr-98cffa21524a6bed

Int(V)\Interior{V}

Read as: the interior of V

Means: the interior of V

1 occurrence in this chapter

Equation form expr-992accb9917efeb5

C!C

Read as: C

Means: C

1 occurrence in this chapter

Equation form expr-9d67dc827f7ab049

⟦A⟧X⊆⟦B⟧X\Prop{X}{!A} \subseteq \Prop{X}{!B}

Read as: the proposition for A in X is a subset of the proposition for B in X

Means: the proposition for A in X is a subset of the proposition for B in X

1 occurrence 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

2 occurrences in this chapter

Equation form expr-9ee8b55474e825e4

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

Read as: B is derivable from the conditional from A to B together with A

Means: B is derivable from the conditional from A to B together with A

1 occurrence in this chapter

Equation form expr-a25513c7e0f6eaa8

UU

Read as: U

Means: U

2 occurrences in this chapter

Equation form expr-a948d9553e25da4a

∅⊆U\emptyset \subseteq U

Read as: the empty set is a subset of U

Means: the empty set is a subset of U

1 occurrence in this chapter

Equation form expr-a9702afa0cf8d7ec

B∨C!B \lor !C

Read as: B or C

Means: B or C

1 occurrence in this chapter

Equation form expr-a9af67e71b538e29

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

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

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

1 occurrence in this chapter

Equation form expr-ab733e02bed54e75

Γ⊨A\Gamma \Entails !A

Read as: Gamma entails A

Means: Gamma entails A

5 occurrences in this chapter

Equation form expr-ace91093efeab72e

Int(V)=⋃{U:U⊆V and U∈O}.\Interior{V} = \bigcup \Setabs{U}{U \subseteq V \text{ and } U \in \Top{O}}.

Read as: the interior of V equals the union of all U such that U is a subset of V and U belongs to script O

Means: the interior of V equals the union of all U such that U is a subset of V and U belongs to script O

1 occurrence in this chapter

Equation form expr-ae34411c1dacd818

Ui∈OU_i \in \Top{O}

Read as: U subscript i belongs to script O

Means: U subscript i belongs to script O

1 occurrence in this chapter

Equation form expr-b299a756fe5b9f2c

A∨B!A \lor !B

Read as: A or B

Means: A or B

1 occurrence in this chapter

Equation form expr-b455f29de9a8eccc

O⊆℘(X)\Top{O} \subseteq \Pow{X}

Read as: script O is a subset of the power set of X

Means: script O is a subset of the power set of X

1 occurrence 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

10 occurrences in this chapter

Equation form expr-b99d2e5f37ae7e17

w′w'

Read as: w prime

Means: w prime

8 occurrences in this chapter

Equation form expr-b9a6014877617b03

⟦B∧C⟧X⊆⟦C⟧X\Prop{X}{!B \land !C} \subseteq \Prop{X}{!C}

Read as: the proposition for B and C is a subset of the proposition for C

Means: the proposition for B and C is a subset of the proposition for C

1 occurrence in this chapter

Equation form expr-bf1df883a744abb3

A∧B!A \land !B

Read as: A and B

Means: A and B

2 occurrences in this chapter

Equation form expr-c63f9557f464c93a

¬A\lnot !A

Read as: not A

Means: not A

4 occurrences in this chapter

Equation form expr-cd37871db1ba340f

A∨¬A!A \lor \lnot !A

Read as: A or not A

Means: A or not A

1 occurrence in this chapter

Equation form expr-cdc2ed7d3b3d72c2

⊥\lfalse

Read as: falsity

Means: falsity

3 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

10 occurrences in this chapter

Equation form expr-d0a2b90b3d18abd7

M\mModel{M}

Read as: model M

Means: model M

5 occurrences 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-d2da161508eebc66

w∈Ww \in W

Read as: w belongs to W

Means: w belongs to W

2 occurrences in this chapter

Equation form expr-d35a0fd27c7d0fa1

Mw⊩A\mSat{M_w}{!A}

Read as: A is true throughout model M subscript w

Means: A is true throughout model M subscript w

2 occurrences in this chapter

Equation form expr-d46ab73eeeb08d63

⟦A⟧X\Prop{X}{!A}

Read as: the open-set proposition for A in X

Means: the open-set proposition for A in X

2 occurrences 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-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

3 occurrences in this chapter

Equation form expr-de5a6f78116eca62

VV

Read as: V

Means: V

3 occurrences in this chapter

Equation form expr-e7ae8b2a6b7ec6cd

W⊆VW \subseteq V

Read as: W is a subset of V

Means: W is a subset of V

1 occurrence in this chapter

Equation form expr-ecd644c37133283a

Mw=⟨Ww,Rw,Vw⟩\mModel{M}_w=\tuple{W_w, R_w, V_w}

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

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

1 occurrence in this chapter

Equation form expr-ecdc9a215e5b2dbf

U∩V∈OU \cap V \in \Top{O}

Read as: the intersection of U and V belongs to script O

Means: the intersection of U and V belongs to script O

1 occurrence in this chapter

Equation form expr-edaaa74605c36742

⟦p⟧X=V(p)\Prop{X}{p} = V(p)

Read as: the open-set proposition for p in X equals V of p

Means: the open-set proposition for p in X equals V of p

1 occurrence in this chapter

Equation form expr-ef0bc6a09eb9081d

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

Read as: not both A and not A

Means: not both A and not A

1 occurrence in this chapter

Equation form expr-f1e0bc1f27713edc

X=⟨X,O,V⟩\mModel{X} = \tuple{X, \Top{O}, V}

Read as: topological model X is the ordered triple X, script O, V

Means: topological model X is the ordered triple X, script O, V

1 occurrence in this chapter

Equation form expr-f5f89528d536c23d

⋃{Ui:i∈I}∈O\bigcup \Setabs{U_i}{i \in I} \in \Top{O}

Read as: the union of all U subscript i such that i belongs to I, belongs to script O

Means: the union of all U subscript i such that i belongs to I, belongs to script O

1 occurrence in this chapter

Equation form expr-f8dcd48388f1ed21

w∈V(p)w \in V(p)

Read as: w belongs to V of p

Means: w belongs to V of p

2 occurrences in this chapter

Equation form expr-f94f4fd31510eb59

⟦B⟧X⊆⟦B∨C⟧X\Prop{X}{!B} \subseteq \Prop{X}{!B \lor !C}

Read as: the proposition for B is a subset of the proposition for B or C

Means: the proposition for B is a subset of the proposition for B or C

1 occurrence in this chapter

Equation form expr-f9c6cbd6245f9917

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

u∈Wu \in W

Read as: u belongs to W

Means: u belongs to W

1 occurrence in this chapter

Equation form expr-fcb5f40df9be6bae

WW

Read as: W

Means: W

4 occurrences in this chapter

Equation form expr-ff38d507010dbb68

V∈OV \in \Top{O}

Read as: V belongs to script O

Means: V belongs to script O

1 occurrence in this chapter

Definition of an intuitionistic relational model

An intuitionistic relational model is an ordered triple W, R, V. W is nonempty. R is a reflexive, antisymmetric, transitive partial order on W. V assigns each propositional variable a subset of W and is monotone: if w belongs to V of p and w prime is accessible from w, then w prime belongs to V of p.

Source

Inductive definition of truth at a world

Truth of A at world w in model M is defined by formula form. An atom p is true exactly when w belongs to V of p. Falsity is not true. Not B is true exactly when B is true at no world accessible from w. A conjunction is true exactly when both conjuncts are true at w. A disjunction is true exactly when either or both disjuncts are true at w. A conditional from B to C is true exactly when, at every accessible world, either B is not true or C is true, or both. The definition also introduces non-satisfaction and satisfaction of every member of Gamma.

Source

Exercise relating negation to a conditional

Show, using the preceding truth definition, that model M satisfies not A at w if and only if it satisfies the conditional from A to falsity at w. The source gives no solution.

Source

Proposition that truth is monotone

If model M satisfies A at w and w prime is accessible from w, then model M satisfies A at w prime. The source proof consists only of the word Exercise.

Source

Exercise proving truth monotonicity

Prove the preceding proposition that truth at worlds is monotone with respect to R. The exercise remains unsolved in the source.

Source

Definition of global truth, validity, and entailment

A is true in model M exactly when M satisfies A at every world in W. A is valid exactly when it is true in every model. Gamma entails A exactly when, for every model and world satisfying every member of Gamma, that world also satisfies A.

Source

Two consequences of entailment

First, if model M satisfies Gamma at w and Gamma entails A, then M satisfies A at w. Second, if every member of Gamma is true throughout M and Gamma entails A, then A is true throughout M. The printed proof treats the global case in its first numbered paragraph and then says the second follows from the first; that source ordering is preserved and disclosed separately.

Source

Definition of a model restricted to a world

For a relational model M and a world w, the restriction M subscript w has worlds exactly those u accessible from w, relation R restricted to those worlds, and valuations V of p intersected with that restricted world set.

Source

Three component equations for model restriction

W subscript w is the set of u in W accessible from w. R subscript w is R intersected with the Cartesian square of W subscript w. V subscript w of p is V of p intersected with W subscript w.

Source

Proposition characterizing restriction

Model M satisfies A at w if and only if A is true throughout the restricted model M subscript w.

Source

Exercise proving the restriction proposition

Prove the preceding proposition characterizing truth at a world by truth in the restricted model. The source supplies no solution.

Source

Proposition deriving local entailment from global model truth

Suppose that in every model where Gamma is globally true, A is globally true. Then Gamma entails A. The proof restricts a model to a world satisfying Gamma, applies the hypothesis in the restricted model, and transfers truth of A back to the original world.

Source

Definition of a topology

A topology script O on X is a subset of the power set of X. It contains the empty set and X, is closed under finite intersections, and is closed under arbitrary unions. Its members are the open sets, and X together with script O is a topological space.

Source

Definition of a topological model and its propositions

A topological model is an ordered triple X, script O, V, where script O is a topology on X and V assigns an open set to each propositional variable. Falsity denotes the empty set; an atom p denotes V of p; conjunction denotes intersection; disjunction denotes union; and a conditional from A to B denotes the interior of the union of X minus the proposition for A with the proposition for B. The interior of V is the union of all open subsets of V.

Source

Cross-reference reference-001134

the definition of truth at a world

Source occurrence

Cross-reference reference-001135

the proposition that truth at worlds is monotone

Source occurrence

Cross-reference reference-001136

the first part of the proposition relating satisfaction and entailment

Source occurrence

Cross-reference reference-001137

the proposition characterizing restriction to a world

Source occurrence

Cross-reference reference-001138

the proposition characterizing restriction to a world

Source occurrence

Cross-reference reference-001139

the proposition characterizing restriction to a world

Source occurrence

Source disclosures

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

A≡p!A \ident p

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

Read in context source

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

A≡⊥!A \ident \lfalse

Read as: Case: A is falsity.

Read in context source

Source-generated case expression tr060-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 tr060-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 tr060-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 tr060-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