Visser, A. (1998) Preliminary Notes on Interpretability Logic

The notes can be downloaded from here.

1. Definitions

$⟨ K, b, R, {S_{x} : x \in K}⟩$ is a Veltman Prestructure if:
1. $K \neq = \emptyset$
2. $b \in K \land \forall_{x \in K} x = b \lor b R x$
3. $R$ is binary relations
4. $S_{x}$ are binary relations on $K$ s.t. $\forall_{x, y, z \in K} y S_{x} z \to x R y$
  - $S [x] := S_{x}$
$A ▹ B$ iff $T + A$ is (relatively) interpretable in $T + B$ , (it is axiomatised in the construction of BIL)
- for $T + A := {φ : \exists_{φ_{1}, ..., φ_{n} \in T} \exists_{ψ_{1}, ..., ψ_{m} \in A} {φ_{1}, ..., φ_{n}, ψ_{1}, ..., ψ_{m}} ⊢ φ}$ , if theories are meant to be inferentially closed, otherwise, $T + A := T \cup A$ .
for $K \neq = \emptyset$ and $L$ the language, $⊩$ is a relation between $K$ and $L$ with the "usual clauses", together with:
- for $x \in K$ , $A, B$ theories, $(x ⊩ A ▹ B) \leftrightarrow (\forall_{y \in K} ((x R y \land y ⊩ A) \to \exists_{z \in K} (y S_{x} z \land z ⊩ B)))$
for $V$ a Veltman prestructure, $⊩$ a forcing relation on $V$ , $⟨ V, ⊩ ⟩$ is a Veltman Premodel
for $W, W^{'}$ two Veltman Premodels, $β$ is a bisimulation if:
1. $β$ is a relation between $K$ and $K^{'}$
2. $b β b^{'}$
3. $\forall_{x \in K} \forall_{x^{'} \in K^{'}} x β x^{'} \to (\forall_{y \in K} (x R y \to \exists_{y^{'} \in K^{'}} (y β y^{'} \land x^{'} R y^{'} \land \forall_{z^{'} \in K^{'}} (y^{'} S_{x} z^{'} \to \exists_{z \in K} (z β z^{'} \land y S_{x} z))))$
4. $\forall_{x \in K} \forall_{x^{'} \in K^{'}} x β x^{'} \to (\forall_{y^{'} \in K^{'}} (x^{'} R y^{'} \to \exists_{y^{'} \in K^{'}} (y β y^{'} \land x R y \land \forall_{z \in K} (y S_{x^{'}} z \to \exists_{z^{'} \in K^{'}} (z^{'} β z \land y^{'} S_{x^{'}} z^{'}))))$
5. $\forall_{x \in K} \forall_{x^{'} \in K^{'}} x β x^{'} \to (x ⊩ p \leftrightarrow x^{'} ⊩ p)$ for all atoms $p$
- cf. 3. Expressive Power and Invariance

2. Facts

(i) bisimulating is an equivalence relation
(ii) for $β$ a bisimulation between $W, W^{'}$ and $x \in K$ , $x^{'} \in K^{'}$ s.t. $x β x^{'}$ , then for any theory $A$ of the language $x ⊩ A \Leftrightarrow x^{'} ⊩^{'} A$ .
- corresponds to J4, K1, K2.

3. Some Principles & Correspondences for Veltman Prestructures

see 4. Frame Correspondence. These principles show the strong similarities between " $▹$ " and " $\to$ ".

$⊢ □ (A \to B) \to A ▹ B$ , (J1)
- corresponds to: $x R y \to y S_{x} y$
$⊢ (A ▹ B \land B ▹ C) \to A ▹ C$ , (J2)
- Transitivity
- corresponds to: for all $x \in K$ , $S_{x}$ is transitive and $y S_{x} z \to x R z$
- if we consider structures with (ii), J2 corresponds to (i).
$⊢ (A ▹ C \land B ▹ C) \to (A \lor B) ▹ C$ , (J3)
$⊢ A ▹ B \to (◊ A \to ◊ B)$ , (J4)
- corresponds to (ii)
$⊢ (A ▹ B \land □ (B \to C)) \to A ▹ C$ , (K1)
- corresponds to (ii)
$⊢ (A ▹ B \land B ▹ ⊥) \to A ▹ ⊥$ , (K2)
- corresponds to (ii)
$⊢ ◊ A ▹ A$ , (J5)
- corresponds to: $x R y \land y R z \to y S_{x} z$

4. More Definitions

$⟨ K, b, R, {S_{x} : x \in K}⟩$ is a Veltman Structure if:
1. $K \neq = \emptyset$
2. $b \in K \land \forall_{x \in K} x = b \lor b R x$
3. $R$ is binary relations
4. $S_{x}$ are transitive and reflexive binary relations ${y \in K : x R y}$ ( $=: x R$ )
5. $\forall_{x, y, z \in K} (x R y \land y R z) \to y S_{x} z$ (equivalently $R ∣_{x R} \subseteq S_{x}$ )
  - 4. & 5. imply that $R$ is transitive

5. Basic Interpretability Logic

$⊢ A \Rightarrow⊢ □ A$ (L1)
$□ (A \to B) \to (□ A \to □ B)$ , (L2)
$□ A \to □□ A$ , (L3)
$□ (□ A \to A) \to □ A$ , (L4)
BIL is Prop. Modal Logic with L1-4 & J1-5
- L3 is derived by L4 but also by J4-5

6. Some Facts about BIL

a Veltman Structure is upwards well-founded if $R$ is upwards well-founded.
if a Veltman Structure is upwards well-founded, then BIL is valid.
$B I L ⊢ A \Leftrightarrow$ for all (finite) upwards well-founded Veltman Models $W$ and all $k$ of $W$ , $k ⊩ A$ (Completeness Theorem, De Jongh, Veltman)

7. Some Derivations in BIL

$A \equiv B := A ▹ B \land B ▹ A$
$□^{+} A := A \land □ A$
$⊢ □^{+} (C \leftrightarrow D) \to (A C \leftrightarrow A D)$ , (K3)
- what is AC?
- derived from J1, J2
$⊢ A \equiv (A \lor ◊ A)$ , (K4)
- derived from J1, J3, J5
$ϕ A := A \lor ◊ A$
$ψ A := A \land □ \neg A$
(K5) is made from
1. $⊢ ϕ A \leftrightarrow ϕϕ A$
2. $⊢ A \leftrightarrow ϕ ψ A$
3. $⊢ ψ A \leftrightarrow ψψ A$
4. $⊢ ψ A \leftrightarrow ψ ϕ A$
$⊢ A ▹ (A \land □ \neg A)$ , (K6)
- it is an alternative for J5.
$⊢ A \equiv (A \land □ \neg A)$ , (K7)
$⊢ A ▹ ⊥ \to □ \neg A$ , (K8)
- derived from J4
$⊢ ◊ A \to \neg (A ▹ ◊ A)$ , (K9, Feferman Principle)
- this is not derivable in BIL
$⊢ ◊ A ▹ \neg (A ▹ ◊ A)$ , (K10)
- is a weakening of K9 that is derivable in BIL

🪴 Quartz 4.0

Explorer

Visser, A. (1998) Preliminary Notes on Interpretability Logic

1. Definitions

2. Facts

3. Some Principles & Correspondences for Veltman Prestructures

4. More Definitions

5. Basic Interpretability Logic

6. Some Facts about BIL

7. Some Derivations in BIL

Graph View

Backlinks