Semantics — Read

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Editorial

This chapter collects definitions for semantics for intuitionistic logic. So far only Kripke and topological semantics are covered. There are no examples yet, either of how models make formulas true or of proofs that formulas are valid.

Introduction

No logic is satisfactorily described without a semantics, and intuitionistic logic is no exception. Whereas for classical logic, the semantics based on valuations is canonical, there are several competing semantics for intuitionistic logic. None of them are completely satisfactory in the sense that they give an intuitionistically acceptable account of the meanings of the connectives.

The semantics based on relational models, similar to the semantics for modal logics, is perhaps the most popular one. In this semantics, propositional variables are assigned to worlds, and these worlds are related by an accessibility relation. That relation is always a partial order, i.e., it is reflexive, antisymmetric, and transitive.

Intuitively, you might think of these worlds as states of knowledge or “evidentiary situations.” A state $w'$ source is accessible from $w$ source iff, for all we know, $w'$ source is a possible (future) state of knowledge, i.e., one that is compatible with what's known at $w$ source. Once a proposition is known, it can't become un-known, i.e., whenever $!A$ source is known at $w$ source and $Rww'$ source, $!A$ source is known at $w'$ source as well. So “knowledge” is monotonic with respect to the accessibility relation.

If we define “ $!A$ source is known” as in epistemic logic as “true in all epistemic alternatives,” then $!A \land !B$ source is known at $w$ source if in all epistemic alternatives, both $!A$ source and $!B$ source are known. But since knowledge is monotonic and $R$ source is reflexive, that means that $!A \land !B$ source is known at $w$ source iff $!A$ source and $!B$ source are known at $w$ source. For the same reason, $!A \lor !B$ source is known at $w$ source iff at least one of them is known. So for $\land$ source and $\lor$ source, the truth conditions of the connectives coincide with those in classical logic.

The truth conditions for the conditional, however, differ from classical logic. $!A \lif !B$ source is known at $w$ source iff at no $w'$ source with $Rww'$ source, $!A$ source is known without $!B$ source also being known. This is not the same as the condition that $!A$ source is unknown or $!B$ source is known at $w$ source. For if we know neither $!A$ source nor $!B$ source at $w$ source, there might be a future epistemic state $w'$ source with $Rww'$ source such that at $w'$ source, $!A$ source is known without also coming to know $!B$ source.

We know $\lnot !A$ source only if there is no possible future epistemic state in which we know $!A$ source. Here the idea is that if $!A$ source were knowable, then in some possible future epistemic state $!A$ source becomes known. Since we can't know $\lfalse$ source, in that future epistemic state, we would know $!A$ source but not know $\lfalse$ source.

On this interpretation the principle of excluded middle fails. For there are some $!A$ source which we don't yet know, but which we might come to know. For such a formula $!A$ source, both $!A$ source and $\lnot !A$ source are unknown, so $!A \lor \lnot !A$ source is not known. But we do know, e.g., that $\lnot(!A \land \lnot !A)$ source. For no future state in which we know both $!A$ source and $\lnot !A$ source is possible, and we know this independently of whether or not we know $!A$ source or $\lnot !A$ source.

Relational models are not the only available semantics for intuitionistic logic. The topological semantics is another: here propositions are interpreted as open sets in a topological space, and the connectives are interpreted as operations on these sets (e.g., $\land$ source corresponds to intersection).

relational model

In order to give a precise semantics for intuitionistic propositional logic, we have to give a definition of what counts as a model relative to which we can evaluate formulas. On the basis of such a definition it is then also possible to define semantics notions such as validity and entailment. One such semantics is given by relational models.

Definition of an intuitionistic relational model

A relational model for intuitionistic propositional logic is a triple $\mModel{M} = \tuple{W, R, V}$ source, where

$W$ source is a non-empty set,
$R$ source is a partial order (i.e., a reflexive, antisymmetric, and transitive binary relation) on $W$ source, and
$V$ source is a function assigning to each propositional variable $p$ source a subset of $W$ source, such that
$V$ source is monotone with respect to $R$ source, i.e., if $w \in V(p)$ source and $Rww'$ source, then $w' \in V(p)$ source.

Inductive definition of truth at a world

We define the notion of $!A$ source being true at $w$ source in $\mModel{M}$ source, $\mSat{M}{!A}[w]$ source, inductively as follows:

Case: $!A \ident p$ source
$\mSat{M}{\indfrm}[w]$ source iff $w \in V(p)$ source.
Case: $!A \ident \lfalse$ source
not $\mSat{M}{\indfrm}[w]$ source.
Case: $!A \ident \lnot !B$ source
$\mSat{M}{\indfrm}[w]$ source iff for no $w'$ source such that $Rww'$ source, $\mSat{M}{!B}[w']$ source.
Case: $!A \ident !B \land !C$ source
$\mSat{M}{\indfrm}[w]$ source iff $\mSat{M}{!B}[w]$ source and $\mSat{M}{!C}[w]$ source.
Case: $!A \ident !B \lor !C$ source
$\mSat{M}{\indfrm}[w]$ source iff $\mSat{M}{!B}[w]$ source or $\mSat{M}{!C}[w]$ source (or both).
Case: $!A \ident !B \lif !C$ source
$\mSat{M}{\indfrm}[w]$ source iff for every $w'$ source such that $Rww'$ source, not $\mSat{M}{!B}[w']$ source or $\mSat{M}{!C}[w']$ source (or both).

We write $\mSat/{M}{!A}[w]$ source if not $\mSat{M}{!A}[w]$ source. If $\Gamma$ source is a set of formulas, $\mSat{M}{\Gamma}[w]$ source means $\mSat{M}{!B}[w]$ source for all $!B \in \Gamma$ source.

Exercise relating negation to a conditional

Show that according to the definition of truth at a world, $\mSat{M}{\lnot !A}[w]$ source iff $\mSat{M}{!A \lif \lfalse}[w]$ source.

Proposition that truth is monotone

Truth at worlds is monotonic with respect to $R$ source, i.e., if $\mSat{M}{!A}[w]$ source and $Rww'$ source, then $\mSat{M}{!A}[w']$ source.

Proof

Exercise.

Exercise proving truth monotonicity

Prove the proposition that truth at worlds is monotone.

Semantic Notions

Definition of global truth, validity, and entailment

We say $!A$ source is true in the model $\mModel{M} = \tuple{W,R,V}$ source, $\mSat{M}{!A}$ source, iff $\mSat{M}{!A}[w]$ source for all $w \in W$ source. $!A$ source is valid, $\Entails !A$ source, iff it is true in all models. We say a set of formulas $\Gamma$ source entails $!A$ source, $\Gamma \Entails !A$ source, iff for every model $\mModel{M}$ source and every $w$ source such that $\mSat{M}{\Gamma}[w]$ source, $\mSat{M}{!A}[w]$ source.

Two consequences of entailment

If $\mSat{M}{\Gamma}[w]$ source and $\Gamma \Entails !A$ source, then $\mSat{M}{!A}[w]$ source.
If $\mSat{M}{\Gamma}$ source and $\Gamma \Entails !A$ source, then $\mSat{M}{!A}$ source.

Proof

Suppose $\mSat{M}{\Gamma}$ source. Since $\Gamma \Entails !A$ source, we know that if $\mSat{M}{\Gamma}[w]$ source, then $\mSat{M}{!A}[w]$ source. Since $\mSat{M}{\Gamma}[u]$ source for all every $u \in W$ source, $\mSat{M}{\Gamma}[w]$ source. Hence $\mSat{M}{!A}[w]$ source.
Follows immediately from the first part of the proposition relating satisfaction and entailment.

Definition of a model restricted to a world

Suppose $\mModel{M}$ source is a relational model and $w \in W$ source. The restriction $\mModel{M}_w=\tuple{W_w, R_w, V_w}$ source of $\mModel{M}$ source to $w$ source is given by:

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

source

Proposition characterizing restriction

$\mSat{M}{!A}[w]$ source iff $\mSat{M_w}{!A}$ source.

Exercise proving the restriction proposition

Prove the proposition characterizing restriction to a world.

Proposition deriving local entailment from global model truth

Suppose for every model $\mModel{M}$ source such that $\mSat{M}{\Gamma}$ source, $\mSat{M}{!A}$ source. Then $\Gamma \Entails !A$ source.

Proof

Suppose that $\mSat{M}{\Gamma}[w]$ source. By the the proposition characterizing restriction to a world applied to every $!B \in \Gamma$ source, we have $\mSat{M_w}{\Gamma}$ source. By the assumption, we have $\mSat{M_w}{!A}$ source. By the proposition characterizing restriction to a world again, we get $\mSat{M}{!A}[w]$ source.

Topological Semantics

Another way to provide a semantics for intuitionistic logic is using the mathematical concept of a topology.

Definition of a topology

Let $X$ source be a set. A topology on $X$ source is a set $\Top{O} \subseteq \Pow{X}$ source that satisfies the properties below. The elements of $\Top{O}$ source are called the open sets of the topology. The set $X$ source together with $\Top{O}$ source is called a topological space.

The empty set and the entire space are open: $\emptyset$ source, $X \in \Top{O}$ source.
Open sets are closed under finite intersections: if $U$ source, $V \in \Top{O}$ source then $U \cap V \in \Top{O}$ source
Open sets are closed under arbitrary unions: if $U_i \in \Top{O}$ source for all $i \in I$ source, then $\bigcup \Setabs{U_i}{i \in I} \in \Top{O}$ source.

We may write $X$ source for a topology if the collection of open sets can be inferred from the context; note that, still, only after $X$ source is endowed with open sets can it be called a topology.

Definition of a topological model and its propositions

A topological model of intuitionistic propositional logic is a triple $\mModel{X} = \tuple{X, \Top{O}, V}$ source where $\Top{O}$ source is a topology on $X$ source and $V$ source is a function assigning an open set in $\Top{O}$ source to each propositional variable.

Given a topological model $\mModel{X}$ source, we can define $\Prop{X}{!A}$ source inductively as follows:

$\Prop{X}{\lfalse} = \emptyset$ source
$\Prop{X}{p} = V(p)$ source
$\Prop{X}{!A \land !B} = \Prop{X}{!A} \cap \Prop{X}{!B}$ source
$\Prop{X}{!A \lor !B} = \Prop{X}{!A} \cup \Prop{X}{!B}$ source
$\Prop{X}{!A \lif !B} = \Interior{(X \setminus \Prop{X}{!A}) \cup \Prop{X}{!B}}$ source

Here, $\Interior{V}$ source is the function that maps a set $V \subseteq X$ source to its interior, that is, the union of all open sets it contains. In other words,

\Interior{V} = \bigcup \Setabs{U}{U \subseteq V \text{ and } U \in \Top{O}}.

source

Note that the interior of any set is always open, since it is a union of open sets. Thus, $\Prop{X}{!A}$ source is always an open set.

Although topological semantics is highly abstract, there are ways to think about it that might motivate it. Suppose that the elements, or “points,” of $X$ source are points at which statements can be evaluated. The set of all points where $!A$ source is true is the proposition expressed by $!A$ source. Not every set of points is a potential proposition; only the elements of $\Top{O}$ source are. $!A \Entails !B$ source iff $!B$ source is true at every point at which $!A$ source is true, i.e., $\Prop{X}{!A} \subseteq \Prop{X}{!B}$ source, for all $X$ source. The absurd statement $\lfalse$ source is never true, so $\Prop{X}{\lfalse} = \emptyset$ source.

How must the propositions expressed by $!B \land !C$ source, $!B \lor !C$ source, and $!B \lif !C$ source be related to those expressed by $!B$ source and $!C$ source for the intuitionistically valid laws to hold, i.e., so that $!A \Proves !B$ source iff $\Prop{X}{!A} \subset \Prop{X}{!B}$ source? We require $\lfalse \Proves !A$ source for any $!A$ source, which is satisfied because $\emptyset \subseteq U$ source for all $U$ source. Since $!B \land !C \Proves !B$ source, we require that $\Prop{X}{!B \land !C} \subseteq \Prop{X}{!B}$ source, and similarly $\Prop{X}{!B \land !C} \subseteq \Prop{X}{!C}$ source. The largest set satisfying $W \subseteq U$ source and $W \subseteq V$ source is $U \cap V$ source. Conversely, $!B \Proves !B \lor !C$ source and $!C \Proves !B \lor !C$ source, and so we require that $\Prop{X}{!B} \subseteq \Prop{X}{!B \lor !C}$ source and $\Prop{X}{!C} \subseteq \Prop{X}{!B \lor !C}$ source. The smallest set $W$ source such that $U \subseteq W$ source and $V \subseteq W$ source is $U \cup V$ source.

The definition for $\lif$ source is tricky: $!A \lif !B$ source expresses the weakest proposition that, combined with $!A$ source, entails $!B$ source. That $!A \lif !B$ source combined with $!A$ source entails $!B$ source is clear from $(!A \lif !B) \land !A \Proves !B$ source. So $\Prop{X}{!A \lif !B}$ source should be the greatest open set such that $\Prop{X}{!A \lif !B} \cap \Prop{X}{!A} \subset \Prop{X}{!B}$ source, leading to our definition.

Source disclosures

TR060-SAR-001: Source caveat. The first numbered proof paragraph assumes global truth of Gamma and concludes truth of A at an arbitrary world, while the proposition's first item has a local premise at one world. The next paragraph says the second item follows from the first. The printed numbering and argument are retained without silently swapping the paragraphs. source
TR060-SAR-002: Source caveat. The phrase for all every is retained as a source wording error; the mathematical formula u belongs to W is unchanged. source
TR060-SAR-003: Source caveat. These two displayed semantic conditions use the strict-subset symbol, whereas the surrounding order conditions predominantly use subset-or-equal. The edition preserves and speaks strict subset at the two printed occurrences. source

Reading preferences

Source file content/intuitionistic-logic/semantics/semantics.tex

Editorial

Source file content/intuitionistic-logic/semantics/introduction.tex

Introduction

Source file content/intuitionistic-logic/semantics/relational-models.tex

relational model

Definition of an intuitionistic relational model

Inductive definition of truth at a world

Exercise relating negation to a conditional

Proposition that truth is monotone

Proof

Exercise proving truth monotonicity

Source file content/intuitionistic-logic/semantics/semantic-notions.tex

Semantic Notions

Definition of global truth, validity, and entailment

Two consequences of entailment

Proof

Definition of a model restricted to a world

Proposition characterizing restriction

Exercise proving the restriction proposition

Proposition deriving local entailment from global model truth

Proof

Source file content/intuitionistic-logic/semantics/topological-semantics.tex

Topological Semantics

Definition of a topology

Definition of a topological model and its propositions

Source disclosures