Kripke frames are a tool discovered in the late 1950s by Saul Kripke
to describe a semantics for modal logic – those logics with
modal operators, typically □, read as
necessarily, and ◇, read as
possibly. In this semantics, we have a set \(\mathcal{W}\) which we call the
set of worlds, and a binary relation \(\mathcal{R}\), called the
accessibility relation, on \(\mathcal{W}\), which is meant to denote a
notion of potentiality between worlds – to say of \(\mathrm{w}_1, \mathrm{w}_2 \in
\mathcal{W}\) that \(\mathrm{w}_1
\mathcal{R}\mathrm{w}_2\) can be intuitively read as saying that
\(\mathrm{w}_2\) has more information
than \(\mathrm{w}_1\), or that it is at
a later stage of development. We then have semantics for the modal
operators that read something like:
□ Pis true at worldwifPis true at every world accessible fromw◇ Pis true at worldwifPis true at some world accessible fromw
There is a vast panoply of different systems of modal logics with
names like S4, S5, K etc.1. From the model-theoretic point of
view, these correspond to different ordering structures \(\mathcal{R}\) gives to \(\mathcal{W}\), e.g. for S4 we
have that \(\mathcal{R}\) is a
pre-order, whereas for S5 we want \(\mathcal{R}\) to be an equivalence
relation.
As a result of this observation, Kripke realized that such an information order gives an interpretation of intuitionistic logic. One aspect Brouwer emphasized in his account of intuitionism is the way in which mathematical knowledge unfolds over time, in a state of becoming. This was one way in which Brouwer rejected the law of excluded middle, since at any given moment our knowledge may not be sufficient to either affirm or refute a given proposition. Kripke’s observation was also influenced by earlier work of Gödel, McKinsey and Tarski, who came up with a translation from intuitionistic to modal logic:
\[\begin{aligned} t(v) &= \Box v \qquad \text{[var } v\text{]} \\ t(\bot) &= \bot \\ t(A \wedge B) &= t(A) \wedge t(B) \\ t(A \vee B) &= t(A) \vee t(B) \\ t(A \to B) &= \Box\bigl(t(A) \to t(B)\bigr) \end{aligned}\]
Here we think of \(\Box\) as a modality akin to “provability”. The important clauses then say that a primitive variable is true if it is true in all worlds, and an implication is true if in any future world in which \(A\) becomes true, \(B\) must also become true. We note that this means negation doesn’t behave like classical negation since it is a worldly notion – if we prove the negation of \(\mathcal{P}\), then \(\mathcal{P}\) cannot be true in any accessible world – we can hence read the truth of a negation as constituting a proof of a refutation.
Let us see how we can develop some of these ideas in
lean:
Syntax
We will develop our semantics for intuitionistic propositional logic, and so we have the following type of terms:
inductive Tm : Type where
| var : ℕ → Tm
| and : Tm → Tm → Tm
| or : Tm → Tm → Tm
| imp : Tm → Tm → Tm
| tt : Tm
| ff : TmNote: we use \(\mathbb{N}\) for variables, which is merely for the sake of convenience.
We also add some standard infix abbreviations so we can, for example,
write ∧ for and, ∨ for
or etc. For us, a proof context2 is
nothing but a list of terms3:
We then use a standard natural-deduction-style proof theory:
inductive Pf : (Γ : Ctxt) → Tm → Prop where
| assume : ∀ {Γ : Ctxt} {P : Tm} , Pf (P :: Γ ) P
| wk : ∀ {Γ Δ : Ctxt} {P : Tm}, Γ ≤ Δ → Pf Γ P → Pf Δ P
| and_I : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ P → Pf Γ Q → Pf Γ (P ∧ Q)
| and_E₁ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ (P ∧ Q) → Pf Γ P
| and_E₂ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ (P ∧ Q) → Pf Γ Q
| or_I₁ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ P → Pf Γ (P ∨ Q)
| or_I₂ : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ Q → Pf Γ (P ∨ Q)
| or_E : ∀ {Γ : Ctxt} {P Q C : Tm}, Pf Γ (P ∨ Q) → Pf (P :: Γ) C → Pf (Q :: Γ) C → Pf Γ C
| imp_I : ∀ {Γ : Ctxt} {P Q : Tm}, Pf (P :: Γ) Q → Pf Γ (P ⇒ Q)
| imp_E : ∀ {Γ : Ctxt} {P Q : Tm}, Pf Γ (P ⇒ Q) → Pf Γ P → Pf Γ Q
| ff_E : ∀ {Γ : Ctxt}{P : Tm}, Pf Γ ff → Pf Γ P
| tt_I : ∀ {Γ : Ctxt}, Pf Γ ttAs an example, here is how a simple proof looks:
def example1 : Pf [] ((var 0 ⇒ var 1) ∧ var 0 ⇒ var 1) := by
apply Pf.imp_I
apply Pf.imp_Ea.P⊢ Tm
· apply Pf.and_E₁a.a.Q⊢ Tm
apply Pf.assume
· apply Pf.and_E₂a.a.P⊢ Tm
apply Pf.assumeWe make pervasive use of three elementary syntactic results on
admissibility. The first is a multi-cut principle which
says that if we have a proof of P from one context
Δ, and from another context Γ, we can prove
each formula in Δ, then we can prove P using
Γ. This is a rather wordy way of stating that
substitution of contexts acts on terms:
theorem multicut {Δ : Ctxt} {P : Tm} (h : Pf Δ P) :
∀ {Γ : Ctxt}, (∀ Q ∈ Δ, Pf Γ Q) → Pf Γ P := by
induction h with
| assume =>
intro Γ hΓ
exact hΓ _ (by simp)
| wk hΔ hP ih =>
intro Γ hΓ
apply ih
intro Q hQ
exact hΓ Q (hΔ.sublist.subset hQ)
| and_I hP hQ ihP ihQ =>
intro Γ hΓ
exact Pf.and_I (ihP hΓ) (ihQ hΓ)
| and_E₁ hPQ ih =>
intro Γ hΓ
exact Pf.and_E₁ (ih hΓ)
| and_E₂ hPQ ih =>
intro Γ hΓ
exact Pf.and_E₂ (ih hΓ)
| or_I₁ hP ih =>
intro Γ hΓ
exact Pf.or_I₁ (ih hΓ)
| or_I₂ hQ ih =>
intro Γ hΓ
exact Pf.or_I₂ (ih hΓ)
| or_E hPQ hPC hQC ihPQ ihPC ihQC =>or_E
intro Γ hΓor_E
exact Pf.or_E (ihPQ hΓ)
(ihPC (Γ := _ :: Γ) (fun R hR => by
simp at hR
rcases hR with rfl | hRinlinr
·inl exact Pf.assume
·inr exact Pf.wk (List.suffix_cons _ Γ) (hΓ R hR)))
(ihQC (Γ := _ :: Γ) (fun R hR => by
simp at hR
rcases hR with rfl | hRinlinr
·inl exact Pf.assume
·inr exact Pf.wk (List.suffix_cons _ Γ) (hΓ R hR)))
| imp_I hPQ ih =>
intro Γ hΓ
exact Pf.imp_I (ih (Γ := _ :: Γ) (fun R hR => by
simp at hR
rcases hR with rfl | hRinl
· exact Pf.assume
· exact Pf.wk (List.suffix_cons _ Γ) (hΓ R hR)))
| imp_E hPQ hP ihPQ ihP =>
intro Γ hΓ
exact Pf.imp_E (ihPQ hΓ) (ihP hΓ)
| ff_E hff ih =>
intro Γ hΓ
exact Pf.ff_E (ih hΓ)
| tt_I =>
intro Γ hΓ
exact Pf.tt_IThe second is a generalized assumption rule, stating that if a term is a member of the context, then it can be proven:
theorem of_mem {Γ : Ctxt} {P : Tm} (h : P ∈ Γ) : Pf Γ P := by
induction Γ with
| nil =>
cases h
| cons Q Γ ih =>
simp at h
rcases h with rfl | h
· exact Pf.assume
· exact Pf.wk (List.suffix_cons Q Γ) (ih h)The third is a generalized weakening principle stating that if one context is a sub-sequence of another, then anything provable using the first context is provable with respect to the second:
theorem monotone_mem (Γ Δ : Ctxt) {P : Tm} (hmem : ∀ Q ∈ Γ, Q ∈ Δ) :
Pf Γ P → Pf Δ P := by
intro hP
exact hP.multicut (fun Q hQ => of_mem (hmem Q hQ))Kripke Semantics
Our semantics take values in a structure called Kripke Frame, just
the same as is used for the model theory of S4 modal logic. This means
we require a set W which has the structure of a
Preorder, and we supply a valuation telling us which worlds
\(\mathrm{w}\) each of the atomic
propositions (variables) \(\mathcal{P}\) is true at4,
which we denote \(\mathrm{w}\vDash_{\mathcal{W}}
\mathcal{P}\). Finally, we have a functoriality
constraint our valuation must satisfy: if we have \(\mathrm{w}\vDash_{\mathcal{W}}
\mathcal{P}\), and \(\mathrm{v}\) is accessible from \(\mathrm{w}\), i.e. \(\mathrm{w}\leq \mathrm{v}\), then \(\mathrm{v}\vDash_{\mathcal{W}}
\mathcal{P}\). The categorist will note that this constraint
means we can think of val as a Prop-valued
functor on the preorder W considered as a category. In some
of what is to follow, it would be more natural if we were instead to set
things up so val is a contravariant functor on
W, or in other words, we were to consider the inverse
information order where \(\mathrm{w}\leq
\mathrm{v}\) can be intuitively read as stating that \(\mathrm{w}\) is more informative than \(\mathrm{v}\). Alas, we stick to the
logicians’ convention. Here is how we encode this in
lean:
class Frame (W : Type u) extends Preorder W where
val : W → ℕ → Prop
le_val : ∀ {w w' : W}{i : ℕ}, w ≤ w' → val w i → val w' iNow we have to extend the valuation to give the forcing conditions for when a general term holds at a given world:
def at_world {W : Type u} [Frame W] (w : W) (tm : Tm) : Prop :=
match tm with
| var v => val w v
| Tm.and p q => at_world w p ∧ at_world w q
| Tm.or p q => at_world w p ∨ at_world w q
| imp p q => ∀ (w' : W), w ≤ w' → at_world w' p → at_world w' q
| tt => True
| ff => FalseAs discussed previously, the interesting case for us is implication. We take this to be necessary implication and so, if the antecedent is true at any accessible world, then the consequent must also be true at that world.
We then need to prove a standard monotonicity lemma, extending our
functoriality condition on val from variables to all of
Tm:
def mono_at {W : Type u} [Frame W] {w w' : W} {t : Tm} (le : w ≤ w') (t_at_w : at_world w t)
: at_world w' t :=
match t with
| var _n => le_val le t_at_w
| Tm.and _p _q => ⟨mono_at le t_at_w.1, mono_at le t_at_w.2⟩
| Tm.or _p _q => match t_at_w with
| Or.inl l => Or.inl (mono_at le l)
| Or.inr r => Or.inr (mono_at le r)
| Tm.imp _p _q => fun w'' w'_le_w'' p_at_w'' => t_at_w w'' (le_trans le w'_le_w'') p_at_w''
| tt => trivial
| ff => False.elim t_at_wNext, since we want to semantically interpret not just terms, but our proof judgments, we have to say what it means for a proof context to be forced at a given world – \(\mathrm{w}\vDash_{\mathcal{W}} \Gamma\). This is nothing but the conjunction of the truth of each term at the given world:
def all_at_world {W : Type u} [Frame W] (w : W) : Ctxt → Prop
| [] => True
| (t :: ts) => at_world w t ∧ all_at_world w tsWe then similarly have a monotonicity theorem for contexts:
def mono_all {W : Type u} [Frame W] {w w' : W} {Γ : Ctxt} (w_le_w' : w ≤ w')
(Γ_at_w : all_at_world w Γ) : all_at_world w' Γ :=
match Γ, Γ_at_w with
| [], _ => trivial
| _ :: _, ⟨h, t⟩ => ⟨mono_at w_le_w' h, mono_all w_le_w' t⟩Now that we have what it means for a term or context to be forced at a particular world, we can say what it means for a judgment to be true – \(\Gamma \vDash_{\mathcal{W}} \mathcal{P}\). This is the case precisely if in all the worlds where the premises (i.e. context) are true, the conclusion is true:
def Entails (W : Type u) [Frame W] (Γ : Ctxt) (t : Tm) : Prop :=
∀ (w : W), all_at_world w Γ → at_world w tFinally, we can state what it means that a term holds semantically by quantifying over all frames – \(\Gamma \vDash_{\mathrm{Kripke}} \mathcal{P}\):
def SemEntails (Γ : Ctxt) (t : Tm) : Prop :=
∀ (W : Type u) [Frame W] (w : W), all_at_world w Γ → at_world w tSoundness for Kripke Frames
It is fairly easy for us to show that each of our natural deduction rules holds in our semantics:
def assumption : Entails W (p :: Γ) p := fun _w all => all.1 def wk : Γ ≤ Δ → Entails W Γ t → Entails W Δ t :=
fun hΓΔ Γ_to_t w all => Γ_to_t w (all_at_of_suffix hΓΔ all) def and_I : Entails W Γ p → Entails W Γ q → Entails W Γ (p ∧ q) :=
fun p_holds q_holds w all => ⟨p_holds w all, q_holds w all⟩ def or_E : Entails W Γ (p ∨ q) → Entails W (p :: Γ) c → Entails W (q :: Γ) c → Entails W Γ c :=
fun p_or_q c_ass_p c_ass_q w all => match p_or_q w all with
| Or.inl p_at_w => c_ass_p w ⟨p_at_w, all⟩
| Or.inr q_at_w => c_ass_q w ⟨q_at_w, all⟩ def imp_I : Entails W (p :: Γ) q → Entails W Γ (p ⇒ q) :=
fun q_ass_p _w all w' w_le_w' p_at_w' =>
q_ass_p w' ⟨p_at_w', mono_all w_le_w' all⟩ def imp_E : Entails W Γ (p ⇒ q) → Entails W Γ p → Entails W Γ q :=
fun q_if_p p_holds w all =>
q_if_p w all w (le_refl w) (p_holds w all)This allows us to prove soundness by rule induction on the proof term:
def soundness {W : Type u}[Frame W] {Γ : Ctxt}{tm : Tm} : Pf Γ tm → Entails W Γ tm
| Pf.assume => by
apply Semantics.assumption
| Pf.wk h pf => by
exact Semantics.wk (Γ := _) (Δ := _) (t := _) h (soundness pf)
| Pf.and_I p q => by
apply Semantics.and_Ia
apply soundness p
apply soundness q
| Pf.and_E₁ p => by
apply Semantics.and_E₁a
apply soundness p
| Pf.and_E₂ p => by
apply Semantics.and_E₂a
apply soundness p
| or_I₁ p => by
apply Semantics.or_I₁
apply soundness p
| or_I₂ q => by
apply Semantics.or_I₂
apply soundness q
| or_E p_or_q c_ass_p c_ass_q => by
apply Semantics.or_EaW : Type uaW : Type uaW : Type u
apply soundness p_or_qaW : Type u
apply soundness c_ass_p
apply soundness c_ass_q
| Pf.imp_I p => by
apply Semantics.imp_I
apply soundness p
| Pf.imp_E p q => by
apply Semantics.imp_Eaa
apply soundness p
apply soundness q
| Pf.tt_I => fun _ _ => trivial
| Pf.ff_E p => by
exact Semantics.ff_E (Γ := _) (p := _) (soundness p)Soundness gives us a means to show what terms are not
provable in our proof theory. For instance, if we were to take a model
with a single world, we would be unable to prove False at
this world, and thus we can show that our proof theory doesn’t prove
ff – in other words, this gives us consistency for this
version of constructive logic5:
open TrivIn just the same way, we can also show that certain classical principles do not hold by constructing models in which they fail. For instance, we can construct a Kripke frame where one world splits into two to show that excluded middle cannot be derived constructively:
/-- A Kripke frame that refutes the Law of Excluded Middle.
w1 [P]
/
/
w0 []
\
\
w2 [¬P]
-/
inductive EMFrame where
| w0 | w1 | w2instance : LE EMFrame where
le x y := match x, y with
| .w0, _ => True
| .w1, .w1 => True
| .w2, .w2 => True
| _, _ => Falseinstance : Preorder EMFrame where
le_refl x := by cases xw0w1w2 <;>w0w1w2 simp [LE.le]
le_trans x y z := by
cases x <;> cases y <;> cases zw2.w2.w0w2.w2.w1w2.w2.w2 <;>w0.w0.w0w0.w0.w1w0.w0.w2w0.w1.w0w0.w1.w1w0.w1.w2w0.w2.w0w0.w2.w1w0.w2.w2w1.w0.w0w1.w0.w1w1.w0.w2w1.w1.w0w1.w1.w1w1.w1.w2w1.w2.w0w1.w2.w1w1.w2.w2w2.w0.w0w2.w0.w1w2.w0.w2w2.w1.w0w2.w1.w1w2.w1.w2w2.w2.w0w2.w2.w1w2.w2.w2 simp [LE.le]instance : Frame EMFrame where
val w i := match w, i with
| .w1, 0 => True
| _, _ => False
le_val := by⊢ ∀ {w w' : EMFrame} {i : ℕ},
w ≤ w' →
(match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False
intro w w'⊢ ∀ {i : ℕ},
w ≤ w' →
(match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False i⊢ w ≤ w' →
(match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False hle⊢ (match w, i with
| EMFrame.w1, 0 => True
| x, x_1 => False) →
match w', i with
| EMFrame.w1, 0 => True
| x, x_1 => False hval
cases ww0w1w2 <;>w0w1w2 cases w'w2.w0w2.w1w2.w2 <;>w0.w0w0.w1w0.w2w1.w0w1.w1w1.w2w2.w0w2.w1w2.w2 simp [LE.le] at *
exact hvalopen Tmopen EMFrametheorem em_not_provable : ¬ Pf [] (var 0 ∨ (var 0 ⇒ ff)) := by
intro h
-- EM for P := var 0, is neither probable nor refutable at w0
let EM_pf_at_w := soundness (W := EMFrame) h w0 (by simp [all_at_world])
simp [at_world] at EM_pf_at_w
rcases EM_pf_at_w with pf_p | pf_not_p
· -- case 1: w0 forced at p,
-- But by def of val it is not forced here
simp [Frame.val] at pf_p
· -- Case 2: w0 forces p -> ⊥
-- At every world accessible from w0, if p is true, then ⊥ is true.
-- But w1 is accessible from w0, and p is true at w1 while ⊥ is never true.
have w0_le_w1 : w0 ≤ w1 := by simp [LE.le]
have p_at_w1 : at_world w1 (var 0) := by simp [at_world, Frame.val]
exact pf_not_p w1 w0_le_w1 p_at_w1Completeness for Kripke Frames
As well as soundness, we can also prove completeness for Kripke
frames, but the details, as is typical for completeness proofs, are
significantly more intricate. The proof is standard, and similar to
proofs of the completeness of truth tables for classical logic6. Since we are working classically,
we don’t give a direct argument that if a term is true in all models,
then we can reconstruct a derivation for it. Instead, we give a proof by
contradiction. Let us suppose then that we have a term A
for which we cannot give a derivation: \(\neg
\Gamma \vdash \mathcal{A}\). The idea of our proof is to
construct, from this assumption that we cannot prove A, a
bespoke Kripke frame which contradicts that \(\mathcal{A}\) holds in all models. In such
a frame, the collection of worlds is taken to be certain
theories – that is, sets of terms – which are:
- Deductively closed: anything you can prove from the theory is already in the theory
- Consistent: the theory doesn’t prove
ff - Avoid
A: The theory also doesn’t proveA - Prime/Irreducible: If the theory proves a term
P ∨ Q, then the theory proves eitherPorQ
structure World where
carrier : Theory
closed : Closed carrier
consistent : Consistent carrier
prime : Prime carrierWe will not cover the precise details of the proof here7,
but we shall give an outline of the main ideas. If we have some theory
T from which we can’t prove A, then we may
gradually extend the theory so that at each point we maintain both the
invariant that the theory still doesn’t prove A, and the
invariant that the theory is still consistent. To begin with, we can
take the (deductive) closure of T and show that this is
consistent and still doesn’t prove A. We may then consider
the set of all such theories satisfying these properties and show, using
Zorn’s lemma, that we may construct a maximal such closed theory. We
then show that such a maximal admissible theory is prime.
With such a theory in hand, we may then show the main technical result –
the truth lemma8:
theorem truth_lemma (w : World) : ∀ φ : Tm, at_world w φ ↔ φ ∈ w.carrier
| Tm.var i => Iff.rfl
| Tm.and φ ψ => by
constructor
· intro at_w_and
have hφ : φ ∈ w.carrier := by
rw [<- truth_lemma w φ]
apply And.left
apply at_w_and
have hψ : ψ ∈ w.carrier := by
rw [<- truth_lemma w ψ]
apply And.right
apply at_w_and
-- use that w is deductively closed
apply w.closed
exists [φ, ψ]
constructormp.a.left
· aesop
· have hφmem : φ ∈ [φ, ψ] := by simp
have hψmem : ψ ∈ [φ, ψ] := by simp
exact Pf.and_I (Pf.of_mem hφmem) (Pf.of_mem hψmem)
· intro both_in_w
constructor
· rw [truth_lemma w φ]
apply w.closed
exists [φ ∧ ψ]
constructormpr.left.a.left
· simpa using both_in_w
· have hmem : (φ ∧ ψ) ∈ [φ ∧ ψ] := by simp
exact Pf.and_E₁ (Pf.of_mem hmem)
· rw [truth_lemma w ψ]
apply w.closed
exists [φ ∧ ψ]
constructormpr.right.a.left
· simpa using both_in_w
· have hmem : (φ ∧ ψ) ∈ [φ ∧ ψ] := by simp
exact Pf.and_E₂ (Pf.of_mem hmem)
| Tm.or φ ψ => by
constructor
· intro or_at_w
rcases or_at_w with φ_at_w | ψ_at_w
· apply w.closed
exists [φ]
constructor
· simp
rw [<- truth_lemma w φ]
exact φ_at_w
· have hmem : φ ∈ [φ] := by simp
exact Pf.or_I₁ (Pf.of_mem hmem)
· apply w.closed
exists [ψ]
constructor
· simp
rw [<- truth_lemma w ψ]
exact ψ_at_w
· have hmem : ψ ∈ [ψ] := by simp
exact Pf.or_I₂ (Pf.of_mem hmem)
· intro or_in_w
rcases w.prime or_in_w with φ_in_w | ψ_in_w
· simp
rw [truth_lemma w φ]
apply Or.inl
assumption
· simp
rw [truth_lemma w ψ]
apply Or.inr
assumption
| Tm.imp φ ψ => by
constructor
· intro imp_at_w
by_contra imp_not_in_w
have ψ_not_in_clos : ψ ∉ closure (Set.insert φ w.carrier) := by
intro ψ_in_clos
apply imp_not_in_w
apply closure_insert_impT_closed
apply w.closed
exact ψ_in_clos
have w'_consistent : Consistent (closure (Set.insert φ w.carrier)) := by
intro ff_in_w'
have not_φ_in_w : (φ ⇒ Tm.ff) ∈ w.carrier :=
closure_insert_imp w.closed ff_in_w'
apply imp_not_in_w
apply w.closed
exists
[φ ⇒ Tm.ff]
constructora.left
· simpa using not_φ_in_w
· exact Pf.quodlibet φ ψ
-- construct a world containing w and φ, which extends w, and where
-- φ holds but ψ doesn't
obtain ⟨T, T_adm, T_prime⟩ :=
prime_extension_avoiding (closure_closed _) w'_consistent ψ_not_in_clos
let v : World :=
⟨T, T_adm.closed, T_adm.consistent, T_prime⟩
have w_le_v : w ≤ v := by
intro χ hχ
exact T_adm.base (subset_closure (Or.inr hχ))
have φ_at_v : at_world v φ := by
apply (truth_lemma v φ).2
exact T_adm.base (subset_closure (Or.inl rfl))
have not_ψ_at_v : ¬ at_world v ψ := by
intro hψv⊢ False
exact T_adm.avoids ((truth_lemma v ψ).1 hψv)
apply not_ψ_at_vmp
apply imp_at_w v w_le_v φ_at_v
· intro imp_in_w v w_le_v φ_at_v
have imp_in_v : (φ ⇒ ψ) ∈ v.carrier := w_le_v imp_in_w
have φ_in_v : φ ∈ v.carrier := by
rw [<- truth_lemma v φ]
exact φ_at_v
have ψ_in_v : ψ ∈ v.carrier := by
apply v.closed
exists [φ ⇒ ψ, φ]
constructora.left
· intro tm tm_in_ctx
simp at tm_in_ctx
rcases tm_in_ctx with rfl | rfla.left.inl
· exact imp_in_v
· exact φ_in_v
· have imp_mem : (φ ⇒ ψ) ∈ [φ ⇒ ψ, φ] := by simp
have φ_mem: φ ∈ [φ ⇒ ψ, φ] := by simp
exact Pf.imp_E (Pf.of_mem imp_mem) (Pf.of_mem φ_mem)
rw [truth_lemma v ψ]
exact ψ_in_v
| Tm.tt => by
constructor
· intro _
exact w.closed ⟨[], by simp, Pf.tt_I⟩
· aesop
| Tm.ff => by
constructor
· intro ff_at_w
exact False.elim ff_at_w
· intro ff_in_w
exfalso
exact w.consistent ff_in_wIt is then easy to use this to construct a countermodel in this
Kripke frame assuming we can’t give a deduction of A:
theorem countermodel {Γ : Ctxt} {tm : Tm} (neg_pf : ¬ Pf Γ tm) :
¬ Kripke.SemEntails.{0} Γ tm := by
have tm_avoids_T : tm ∉ theoryOf Γ := by
intro htm
apply neg_pf
rw [<- mem_theoryOf]
assumption
have ΓT_Cons : Consistent (theoryOf Γ) := by
intro hff
apply neg_pf
apply Pf.ff_E
rw [<- mem_theoryOf]
assumption
obtain ⟨T, T_admissible, T_prime⟩ :=
prime_extension_avoiding (closure_closed _) ΓT_Cons tm_avoids_T
let w : World := ⟨T, T_admissible.closed, T_admissible.consistent, T_prime⟩
have all_in_T : ∀ Δ : Ctxt, (∀ φ ∈ Δ, φ ∈ T) → all_at_world w Δ := by
intro Δ hΔ
induction Δ with
| nil =>nil
simp
| cons φ Δ ih =>cons
constructorcons.leftcons.right
·cons.left rw [truth_lemma w φ]cons.left
apply hΔ φcons.left
simp
·cons.right apply ihcons.right
intro ψ hψcons.right
apply hΔ ψcons.right
simp [hψ]
have all_at_Γ : all_at_world w Γ := by
apply all_in_T Γ
intro φ φ_in_Γ
apply T_admissible.base (contextSet_mem φ_in_Γ)
have not_tm_at_w : ¬ at_world w tm := by
intro tm_at_w⊢ False
apply T_admissible.avoids
rw [<- truth_lemma w tm]
apply tm_at_w
intro sem_tm⊢ False
apply not_tm_at_w
apply sem_tma
apply all_at_ΓWe then use the countermodel to give a proof by contradiction of completeness:
theorem completeness {Γ : Ctxt} {tm : Tm} : Kripke.SemEntails.{0} Γ tm → Pf Γ tm := by
contrapose!
exact countermodelBeth Semantics
Traditionally Beth semantics arose from Beth’s work seeking to explain and unify Brouwer’s account of choice sequences, along with his notion that the fan theorem gives a constructively acceptable compactness result in intuitionistic mathematics. In particular, for the theory of choice sequences, Brouwer emphasized that we are to think of a sequence \(\mathrm{f}: \mathbb{N} \rightarrow \mathbb{N}\) as something perhaps unconstrained or un-law-like which is unfolding over time, or actively in a state of becoming as our knowledge proceeds. As such, those properties of sequences that are intuitionistically acceptable are the ones we can verify within finite time, or in other words, those which can be checked on some initial sub-sequence of \(\mathrm{f}\). Classically, this means that instead of considering all set-theoretical properties \(\phi : \mathbb{N}^{\mathbb{N}} \rightarrow \mathbb{2}\), we consider only those that are continuous with respect to the product topology9.
Inspired by these considerations, Beth studied abstract trees,
i.e. sets of finite sequences (in this case with values drawn from \(\mathbb{N}\)), which are closed under
taking prefixes. If we have a node in such a tree \(\mathcal{T}= \langle t_1,\ldots, t_n
\rangle\) – which we might think of as denoting a path
in the tree recording each of the prior nodes – then we can think of
this as a description of the initial segment of how a choice sequence
has unfolded thus far, and hence we can think of descendant nodes of
\(\mathcal{T}\) as the potential future
unfoldings of the choice sequence. Because of these considerations, it
was typical that the trees Beth studied were
finitely-branching – meaning each tree node has only
finitely many children – and pruned – meaning every node
always has at least one child node.
If we are to prove an intuitionistically acceptable property of such a sequence represented as a given node, then Beth considered the principle whereby we prove that the property holds for a subset which bars the given node, meaning every path proceeding from the given node eventually hits the given subset. If we can prove a property holds for such a bar, and that the property is stable under immediate prefixes10, then we can show that it holds for the given sequence. This reasoning principle is called bar induction. Beth used this idea to give an interpretation of constructive logic in which the nodes of the tree were labelled by sets of formulas, and where the branching of the tree essentially followed the rules of semantic tableaux.
Rather than focus too closely on Beth’s particular example of
abstract trees with bar induction, we would like to
emphasize that we can take a more abstract view that places
(generalized) Beth semantics as a direct topological generalization of
Kripke frames – topological in just the sense that spaces generalize
sets, or that sheaf categories generalize presheaf categories. In what
follows, then, we will want to think of the structure provided by the
bars in a Beth tree as a kind of topological structure on the tree, and
the induction principle as a kind of sheaf property. For
this to make sense, we need to take a brief detour into Grothendieck
topologies.
Grothendieck Topologies
A Grothendieck topology is a certain kind of structure one can place upon a category. Many have remarked that it is something of a misnomer to call it a topology – suggesting it generalizes the notion of a topology on a space – and that we’d be better off with a name like a coverage, since it really abstracts the concept of a collection of open sets covering another set. We will therefore follow this naming in our actual development.
In our setting, we only contend with defining coverages for preorders
considered as a category, minimizing some of the difficulties of the
theory. We start with the idea of a sieve11.
Given a preorder \(\mathcal{P}\) and
\(\mathrm{p}\in \mathcal{P}\), a
sieve on p is a sub-functor of \(\operatorname{Hom}(\mathrm{p}, -)\) – in
other words, it is an upward closed set which is bounded below by \(\mathrm{p}\):
structure Sieve {P : Type u}[Preorder P] (p : P) : Type u where
carrier : Set P
bounded : ∀ {q : P}, q ∈ carrier → p ≤ q
upward_closed : ∀ {q r : P}, (r ∈ carrier) → r ≤ q → q ∈ carrierWe note that the principal upward closed set \(\uparrow \mathrm{p}:= \{\mathrm{q}| \mathrm{p}\leq \mathrm{q}\}\) always gives us a sieve:
def maximal_sieve [Preorder.{u} P] (p : P) : Sieve p := by
refine {carrier := ?_, bounded := ?_, upward_closed := ?_}
· exact {q | p ≤ q}
· intro q h; exact h
· intro q r hgr hqr
exact le_trans hgr hqrAlso, if we are given a sieve \(\mathcal{S}\) on \(\mathrm{p}\) and we have \(\mathrm{p}\leq \mathrm{q}\), then we can consider the subset of the sieve that is greater than \(\mathrm{q}\): \(\; \mathcal{S}\uparrow \mathrm{q}:= \{ \mathrm{r}\; | \; \mathrm{r}\in \mathcal{S}, \mathrm{q}\leq \mathrm{r}\}\) – and this gives us a sieve on \(\mathrm{q}\). We call this, rather dubiously, the pullback12:
-- We use the terminology pullback even though this goes forward in our set up
def pullback [Preorder P] {p q : P} (_h : p ≤ q) (S : Sieve p) : Sieve q where
carrier := {r | r ∈ S.carrier ∧ q ≤ r}
bounded := fun ⟨_, hr⟩ => hr
upward_closed := fun ⟨r'_in_S, q_le_r' ⟩ r'_le_r => ⟨S.upward_closed r'_in_S r'_le_r, le_trans q_le_r' r'_le_r⟩A coverage (Grothendieck topology) on \(\mathcal{P}\) is then, for each \(\mathrm{p}: \mathcal{P}\), a collection of sieves on \(\mathrm{p}\) which abstractly “cover” \(\mathrm{p}\). In particular, a coverage satisfies the axioms:
- maximality: The maximal sieve covers \(\mathrm{p}\)
- stability: If \(\mathcal{S}\) covers \(\mathrm{p}\), and \(\mathrm{p}\leq \mathrm{q}\), then the pullback of \(\mathcal{S}\) covers \(\mathrm{q}\)
- transitivity: If we have two sieves \(\mathcal{S}, \mathcal{S}'\) on \(\mathrm{p}\), and we have that \(\mathcal{S}\) is a covering sieve, and for each \(\mathrm{q}\in \mathcal{S}\) we have that the pullback of \(\mathcal{S}'\) to \(\mathrm{q}\) is a covering sieve, then \(\mathcal{S}'\) is also a covering sieve on \(\mathrm{p}\).
We can read stability as stating that covers can be
‘restricted’ to a sub-object, and transitivity as stating
that if a sieve is locally covering with respect to another cover, then
it itself is covering. Here is how it looks in lean:
structure Coverage (P : Type u) [Preorder P] : Type u where
covers : (p : P) → Set (Sieve p)
maximal : ∀ (p : P), covers p (maximal_sieve p)
transitive : ∀ (p : P) (U V : Sieve p), covers p U → (∀ (q : U.carrier),
(covers (q : P) (pullback (U.bounded q.property) V))) -> covers p V
stability : ∀ {p q : P} {U : Sieve p} (_U_Cov : covers p U) (p_le_q : p ≤ q), covers q (pullback p_le_q U)Beth Frames
A Beth frame, our terminology13, is an extension of a
Kripke frame, where we ask that we have a Coverage on the
underlying preorder W, and that the valuation now satisfies
the sheaf condition with respect to it. This says that if
we have a world w with a covering sieve S on
w, and a variable v is true on the covering
sieve, i.e. true for each world in the covering sieve, then the variable
must be true at w. We might think, as an intuitionist, that
this condition is giving an account not of the usual BHK semantics, but
instead is a semantics of assertibility. We think of \(\mathcal{S}\) as giving a “bar” of the
current world – meaning any of the future ways in which the present
world might develop will be through one of the worlds in \(\mathcal{S}\) – and think of this condition
as stating that we will in finite time be able to verify the truth of a
given atomic proposition P, and thus that we are already
justified in asserting P.
We also require that each of the covering sieves is non-empty. This
is analogous to the pruning condition, requiring that each bar is
non-empty. The reason this is necessary is that if we have a world with
an empty cover, then we can use the sheaf condition on this cover to
prove False at this world. For an ordinary topological
space, the only set that has an empty cover is the empty set, and so we
can think of this as requiring that our semantics is only on non-empty
open domains.
class BethFrame (W : Type u) extends HasCoverage W, Kripke.Frame W where
sheaf_condition : ∀ {i : ℕ} {w : W} {S : Sieve w} (_S_covers : covers w S), (∀ q ∈ S , val q i) → val w i
nonempty_covers : ∀ {w : W} {S : Sieve w}, covers w S → Nonempty S.carrierThe semantical clauses for truth, or assertibility, at a world, in a
Beth frame, are almost identical to those for Kripke frames except for
the account they give of disjunction. To say that a disjunction
P ∨ Q is assertible is not to say that we know the truth of
either component of the disjunction at the present world, but that we
have a cover upon which we will be able to verify either that
P holds or that Q holds:
def at_world {W : Type u} [BethFrame W] (w : W) (tm : Tm) : Prop :=
match tm with
| var v => val w v
| Tm.and p q => at_world w p ∧ at_world w q
| Tm.or p q =>
∃ (S : Sieve w), covers w S ∧ (∀ w' ∈ S, at_world w' p ∨ at_world w' q)
| imp p q => ∀ (w' : W), w ≤ w' → at_world w' p → at_world w' q
| tt => True
| ff => FalseOur clauses for entailment and semantic entailment are then identical to those for Kripke frames:
def Entails (W : Type u) [BethFrame W] (Γ : Ctxt) (t : Tm) : Prop :=
∀ (w : W), all_at_world w Γ → at_world w tdef SemEntails (Γ : Ctxt) (t : Tm) : Prop :=
∀ (W : Type u) [BethFrame W] (w : W), all_at_world w Γ → at_world w tA final twist is that just as we showed a monotonicity lemma – that
extending val to the evaluation of all formulas at a world
remains monotonic with respect to accessibility – in Beth semantics we
also need to show that the sheaf condition on atomic
propositions extends to all terms:
def sheaf_term {W : Type u} [BethFrame W] {w : W} {S : Sieve w} (S_covers : covers w S) (tm : Tm) : (∀ w' ∈ S , at_world w' tm) → at_world w tm :=
match tm with
| var n => sheaf_condition S_covers
| Tm.and p q => by
intro pq_on_S
constructorleftW : Type uw : W
· apply sheaf_term S_covers p
intro s s_in_S
exact (pq_on_S s s_in_S).1
· apply sheaf_term S_covers q
intro s s_in_S
exact (pq_on_S s s_in_S).2
| Tm.or p q => by
intro p_or_q_on_S
have h_ex (w' : S.carrier) : ∃ (S' : Sieve (w' : W)), covers (w' : W) S' ∧
(∀ v ∈ S', at_world v p ∨ at_world v q) := p_or_q_on_S w' w'.property
choose f_sieve f_spec using h_ex
let S_gl := glue_sieves S f_sieve
simp
exists S_gl
constructorleft
· apply covers_glue f_sieve S_covers (fun q => (f_spec q).1)
· intro v hv
let ⟨q, hgv⟩ := hv
exact (f_spec q).2 v hgv
| Tm.imp p q => by
intro hS w' w_le_w' p_at_w'
have pullback_covers : covers w' (pullback w_le_w' S) := by
apply covers_stable
exact S_covers
apply sheaf_term pullback_covers q
intro w'' hw''
simp [pullback] at hw''W : Type uw : Ww' : Ww'' : W
apply hS w'' hw''.1 w'' (le_refl w'')W : Type uw : Ww' : Ww'' : W
apply mono_at hw''.2 p_at_w'
| tt => by
intro _
trivial
| ff => by
intro ff_on_S
obtain ⟨⟨w', hw'⟩⟩ := nonempty_covers S_covers
exact ff_on_S w' hw'Kripke Frames as Beth Frames
Although Beth frames give a generalization of Kripke frames, we can define a discrete coverage for any preorder in which the covers are just the maximal sieves:
def maximalSieveCoverage (W : Type u) [Preorder W] : Coverage W where
covers w S := S.carrier = (maximal_sieve w).carrier
maximal _w := rfl
transitive := by⊢ ∀ (p : W) (U V : Sieve p),
U.carrier = (maximal_sieve p).carrier →
(∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier
intro p U⊢ ∀ (V : Sieve p),
U.carrier = (maximal_sieve p).carrier →
(∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier V⊢ U.carrier = (maximal_sieve p).carrier →
(∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier hUP : Type uW : Type up : W⊢ (∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier hVP : Type uW : Type up : W
have p_in_U : p ∈ U.carrier := by⊢ ∀ (p : W) (U V : Sieve p),
U.carrier = (maximal_sieve p).carrier →
(∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier rw [hU]P : Type uW : Type up : W; exact le_refl p
have pullback_maximal := hV ⟨p, p_in_U⟩P : Type uW : Type up : W
ext shP : Type uW : Type up : Ws : W
simp only [maximal_sieve, Set.mem_setOf_eq]hP : Type uW : Type up : Ws : W
constructorh.mpP : Type uW : Type up : Ws : Wh.mprP : Type uW : Type up : Ws : W
·h.mpP : Type uW : Type up : Ws : W intro hrh.mpP : Type uW : Type up : Ws : W; exact V.bounded hr
·h.mprP : Type uW : Type up : Ws : W intro hrh.mprP : Type uW : Type up : Ws : W
have hmem : s ∈ (pullback (U.bounded p_in_U) V).carrier := by⊢ ∀ (p : W) (U V : Sieve p),
U.carrier = (maximal_sieve p).carrier →
(∀ (q : ↑U.carrier), (pullback ⋯ V).carrier = (maximal_sieve ↑q).carrier) → V.carrier = (maximal_sieve p).carrier
rw [pullback_maximal]P : Type uW : Type up : Ws : W; assumption
simp only [pullback, Set.mem_setOf_eq] at hmemh.mprP : Type uW : Type up : Ws : W
exact hmem.1
stability := by
intro p q U⊢ U.carrier = (maximal_sieve p).carrier → ∀ (p_le_q : p ≤ q), (pullback p_le_q U).carrier = (maximal_sieve q).carrier hUP : Type uW : Type up : Wq : W hP : Type uW : Type up : Wq : W
ext rhP : Type uW : Type up : Wq : Wr : W
simp only [pullback, maximal_sieve, Set.mem_setOf_eq]
constructorh.mpP : Type uW : Type up : Wq : Wr : W
· rintro ⟨_, hr⟩; exact hr
· intro hr
exact ⟨by rw [hU]P : Type uW : Type up : Wq : Wr : W; exact le_trans h hr, hr⟩We can then construe any Kripke frame as a discrete Beth frame:
instance bethFrameOfKripke (W : Type u) [F : Kripke.Frame W] : BethFrame W where
coverage := maximalSieveCoverage W
val := F.val
le_val := F.le_val
sheaf_condition := byW : Type u⊢ ∀ {i : ℕ} {w : W} {S : Sieve w}, covers w S → (∀ q ∈ S, Kripke.Frame.val q i) → Kripke.Frame.val w i
intro i w S hS hvalW : Type uw : W
apply hval wW : Type uw : W
show w ∈ S.carrierW : Type uw : W
rw [hS]W : Type uw : W; exact le_refl w
nonempty_covers := byW : Type u
intro w S hS
exact ⟨⟨w, by rw [hS]; exact le_refl w⟩⟩It is easy to see that in this case, Beth semantics reduces to the
previous Kripke semantics. For example, suppose P ∨ Q holds
at w. We then must have a cover S on which
either P holds or on which Q holds. But the
only cover is maximal, which includes w itself, and thus we
have that either P holds at w or
Q does.
Soundness for Beth Frames
Just as for Kripke semantics, it is straightforward to show that each of the proof rules preserves validity in a Beth frame:
def assumption : Entails W (p :: Γ) p := fun _ all => all.1 def wk : Γ ≤ Δ → Entails W Γ t → Entails W Δ t :=
fun hΓΔ Γ_to_t w all => Γ_to_t w (all_at_of_suffix hΓΔ all) def and_I : Entails W Γ p → Entails W Γ q → Entails W Γ (p ∧ q) :=
fun p_holds q_holds w' all => ⟨p_holds w' all, q_holds w' all⟩ def or_I₁ : Entails W Γ p → Entails W Γ (p ∨ q) := by
intro p_holds w' all_w'
simp
exists maximal_sieve w'W : Type uw' : W
constructorleftW : Type uw' : W
·leftW : Type uw' : W apply covers_maximal
· intro v hv
have le : w' ≤ v := hv
left
apply p_holds vright.hW : Type uw' : Wv : W
apply mono_all le all_w' def or_I₂ : Entails W Γ q → Entails W Γ (p ∨ q) := by
intro q_holds w' all_w'
simp
exists maximal_sieve w'W : Type uw' : W
constructorleftW : Type uw' : W
·leftW : Type uw' : W apply covers_maximal
· intro v hv
have le : w' ≤ v := hv
right
apply q_holds vright.hW : Type uw' : Wv : W
apply mono_all le all_w' def or_E : Entails W Γ (p ∨ q) → Entails W (p :: Γ) c → Entails W (q :: Γ) c → Entails W Γ c := by
intro p_or_q c_ass_p c_ass_q w' all_w'
let ⟨S, S_cov, pq_sem⟩ := p_or_q w' all_w'
apply sheaf_term S_cov
intro v hv
let le : w' ≤ v := S.bounded hvaW : Type uw' : Wv : W
match pq_sem v hv with
| Or.inl p_holds =>W : Type uw' : Wv : W
apply c_ass_p vW : Type uw' : Wv : W
constructorleftW : Type uw' : Wv : WrightW : Type uw' : Wv : W
·leftW : Type uw' : Wv : W exact p_holds
·rightW : Type uw' : Wv : W exact (mono_all le all_w')
| Or.inr q_holds =>W : Type uw' : Wv : W
apply c_ass_q vW : Type uw' : Wv : W
constructorleftW : Type uw' : Wv : WrightW : Type uw' : Wv : W
·leftW : Type uw' : Wv : W exact q_holds
·rightW : Type uw' : Wv : W exact (mono_all le all_w') def imp_I : Entails W (p :: Γ) q → Entails W Γ (p ⇒ q) :=
fun q_ass_p _w' all_w' v w_le_v p_at_v =>
q_ass_p v ⟨p_at_v, mono_all w_le_v all_w'⟩ def imp_E : Entails W Γ (p ⇒ q) → Entails W Γ p → Entails W Γ q :=
fun q_if_p p_holds w' all_w' =>
q_if_p w' all_w' w' (le_refl w') (p_holds w' all_w')The only cases of interest are those of or, where for
or-introduction we choose the maximal sieve to witness that
if P is true, then P ∨ Q is true, and in the
or-elimination principle we have to make use of the sheaf
property for terms.
With these proof rules having been shown, the proof of soundness is identical to that for Kripke frames:
def soundness {W : Type u}[BethFrame W] {Γ : Ctxt}{tm : Tm} : Pf Γ tm → Entails W Γ tm
| Pf.assume => by
apply Semantics.assumption
| Pf.wk le pf => by
apply Semantics.wkaa
exact le
apply soundness pf
| Pf.and_I p q => by
apply Semantics.and_Ia
apply soundness p
apply soundness q
| Pf.and_E₁ p => by
apply Semantics.and_E₁a
apply soundness p
| Pf.and_E₂ p => by
apply Semantics.and_E₂a
apply soundness p
| or_I₁ p => by
apply Semantics.or_I₁
apply soundness p
| or_I₂ q => by
apply Semantics.or_I₂
apply soundness q
| or_E p_or_q c_ass_p c_ass_q => by
apply Semantics.or_EaW : Type uaW : Type uaW : Type u
apply soundness p_or_qaW : Type u
apply soundness c_ass_p
apply soundness c_ass_q
| Pf.imp_I p => by
apply Semantics.imp_I
apply soundness p
| Pf.imp_E p q => by
apply Semantics.imp_Eaa
apply soundness p
apply soundness q
| Pf.tt_I => fun _ _ => trivial
| Pf.ff_E pf => by
apply Semantics.ff_E
apply soundness pfCompleteness for Beth Frames
Since Kripke frames are already complete for constructive logic, and each gives rise to a Beth frame, we already have a proof of completeness for Beth frames. However, one thing that is pleasing about this approach is that we can use the coverage of the frame to give a particularly elegant construction of countermodels. In particular, for our frame we now consider as worlds all contexts which are consistent:
What makes us no longer need to consider prime theories
is that we make use of a “Beth” topology, which gives us the
truth lemma for disjunctions. Suppose we have a context
\(\Gamma\), a term \(\mathrm{L}= \mathcal{P}_1 \lor \ldots \lor
\mathcal{P}_{\mathrm{n}}\), and suppose further that we have a
derivation \(\Gamma \vdash \mathcal{P}_1 \lor
\ldots \lor \mathcal{P}_{\mathrm{n}}\); we then consider the
coverage freely generated by the sets which decide which particular
disjunct we have proven \(\{\Gamma :
\mathcal{P}_{\mathrm{i}} \}_{i \in I}\).
We first give a way to construct generalized disjunctions:
def mk_disjunction : Ctxt → Tm
| [] => Tm.ff
| t :: ts => Tm.or t (mk_disjunction ts)We also prove that the corresponding introduction and elimination rules for such generalized disjunctions are admissible in our proof theory:
theorem disjunction_intro {t : Tm} {Γ Δ : Ctxt}
(t_in : t ∈ Δ) (pf : Pf Γ t) : Pf Γ (mk_disjunction Δ) := by
induction Δ with
| nil =>
cases t_in
| cons a Δ ih =>
simp at t_in
rcases t_in with rfl | htcons.inl
· exact Pf.or_I₁ pf
· simpa [mk_disjunction] using Pf.or_I₂ (ih ht)theorem disjunction_elim {p : Tm} {Γ : Ctxt} (Δ : Ctxt) :
(∀ {t : Tm}, t ∈ Δ → Pf (t :: Γ) p) →
Pf Γ (mk_disjunction Δ) → Pf Γ p := by
intro htcase hΔ
induction Δ generalizing Γ with
| nil =>
simp [mk_disjunction] at hΔ
exact Pf.ff_E hΔ
| cons a Δ ih =>
simp [mk_disjunction] at hΔ
apply Pf.or_E hΔcons.a
· exact htcase (by simp)
· have htail : ∀ {t : Tm}, t ∈ Δ → Pf (t :: mk_disjunction Δ :: Γ) p := by
intro t ht
apply Syntax.Pf.monotone_mem (Γ := t :: Γ)
(Δ := t :: mk_disjunction Δ :: Γ) (P := p)hmem
· intro Q hQ
have : Q = t ∨ Q ∈ Γ := by simpa using hQ
rcases this with rfl | hmemhmem.inl
· simp
· simp [hmem]
· exact htcase (by simpa using Or.inr ht)
exact ih htail Pf.assumetheorem disjunction_two {Γ : Ctxt} {φ ψ : Tm} :
Pf Γ (Tm.or φ ψ) → Pf Γ (mk_disjunction [φ, ψ]) := by
intro h
simp [mk_disjunction]
apply Pf.or_E h
· exact Pf.or_I₁ Pf.assume
· exact Pf.or_I₂ (Pf.or_I₁ Pf.assume)Here is how we encode covering sieves proving one of the disjuncts
(where we give the disjuncts as a list of proof terms
L):
def context_sieve (Γ : World) (L : List Tm) : Sieve Γ where
carrier := { Δ : World | (Γ.carrier ≤ Δ.carrier) ∧ (∃ A ∈ L, Pf Δ.carrier A) }
bounded := by
intro Δ hΔ
exact hΔ.1
upward_closed := by
intro Δ Θ hΔ hle
constructorleft
· exact List.IsSuffix.trans hΔ.1 hle
· rcases hΔ.2 with ⟨A, hA, hPf⟩
exact ⟨A, hA, Pf.wk hle hPf⟩Our coverage is then freely generated, under the closure conditions for a coverage, by these generating disjunction sieves:
inductive ContextCovers : (Γ : World) → Sieve Γ → Prop where
| basic (Γ : World) (L : List Tm) {S : Sieve Γ} :
Pf Γ.carrier (mk_disjunction L) →
(context_sieve Γ L).carrier ⊆ S.carrier →
ContextCovers Γ S
| maximal (Γ : World) :
ContextCovers Γ (maximal_sieve Γ)
| trans (Γ : World) (U V : Sieve Γ) :
ContextCovers Γ U →
(∀ q : U.carrier, ContextCovers (q : World) (pullback (U.bounded q.property) V)) →
ContextCovers Γ VWe note that we don’t build in stability, as this already follows from the given closure conditions:
theorem ContextCovers.stable {Γ Δ : World} {U : Sieve Γ} (h : Γ ≤ Δ) :
ContextCovers Γ U → ContextCovers Δ (pullback h U) := by
intro hU
induction hU with
| basic Γ L hpf hsub =>
apply ContextCovers.basic Δ Lbasic.a
· exact Pf.wk h hpf
· intro Θ hΘ
constructorbasic.a.left
· apply hsub
constructorbasic.a.left.a.left
· exact List.IsSuffix.trans h hΘ.1
· exact hΘ.2
· exact hΘ.1
| maximal Γ =>maximal
have hEq : pullback h (maximal_sieve Γ) = maximal_sieve Δ := by
apply Sieve.ext
funext Θ
apply propext
constructorh.h.a.mp
· intro hΘ
exact hΘ.2
· intro hΘ
constructorh.h.a.mpr.left
· exact List.IsSuffix.trans h hΘ
· exact hΘ
simpa [hEq] using ContextCovers.maximal Δ
| trans Γ U V hU hV ihU ihV =>trans
apply ContextCovers.trans Δ (pullback h U)trans.atrans.a
·trans.a exact ihU h
·trans.a intro qtrans.a
have hq : (q : World) ∈ U.carrier := q.property.1trans.a
have q_le : Δ ≤ q := q.property.2trans.a
have hEq :
pullback ((pullback h U).bounded q.property) (pullback h V) =
pullback (U.bounded hq) V := by
apply Sieve.exth
funext rh.h
apply propexth.h.a
constructorh.h.a.mph.h.a.mpr
·h.h.a.mp intro hrh.h.a.mp
exact ⟨hr.1.1, hr.2⟩
·h.h.a.mpr intro hrh.h.a.mpr
simp [pullback] at hrh.h.a.mpr
constructorh.h.a.mpr.lefth.h.a.mpr.right
·h.h.a.mpr.left simp [pullback]h.h.a.mpr.left
exact ⟨hr.1, List.IsSuffix.trans q_le hr.2⟩
·h.h.a.mpr.right exact hr.2
simpa [hEq] using hV ⟨(q : World), hq⟩Hence we get a coverage on our worlds:
def contextCoverage : Coverage World where
covers := ContextCovers
maximal := ContextCovers.maximal
transitive := by⊢ ∀ (p : World) (U V : Sieve p),
ContextCovers p U → (∀ (q : ↑U.carrier), ContextCovers (↑q) (pullback ⋯ V)) → ContextCovers p V
intro p U⊢ ∀ (V : Sieve p), ContextCovers p U → (∀ (q : ↑U.carrier), ContextCovers (↑q) (pullback ⋯ V)) → ContextCovers p V V hU hV
exact ContextCovers.trans p U V hU hV
stability := by⊢ ∀ {p q : World} {U : Sieve p}, ContextCovers p U → ∀ (p_le_q : p ≤ q), ContextCovers q (pullback p_le_q U)
intro p q U hU hpq
exact ContextCovers.stable hpq hUThe key lemma we then show is that if we have a covering sieve \(\mathcal{S}\) of \(\Gamma\), and for each context in the covering sieve we can prove some particular formula, then we can prove the formula at \(\Gamma\). In other words, provability forms a sheaf with respect to this model:
theorem pf_sheaf {Γ : World} {S : Sieve Γ} {r : Tm} :
ContextCovers Γ S →
(∀ Δ ∈ S.carrier, Pf Δ.carrier r) →
Pf Γ.carrier r := by
intro hCov hS
induction hCovbasicmaximaltrans
case basic Γ0 L S0 hPf hSub =>
refine disjunction_elim (Γ := Γ0.carrier) L ?_ hPf
intro t ht
by_cases hff : Pf (t :: Γ0.carrier) Tm.ffpos
· exact Pf.ff_E hff
· let Δ : World := ⟨t :: Γ0.carrier, hff⟩neg
have hin : Δ ∈ (context_sieve Γ0 L).carrier := by
constructorleftright
·left exact List.suffix_cons t Γ0.carrier
·right exact ⟨t, ht, Pf.assume⟩
exact hS Δ (hSub hin)
case maximal Γ =>
exact hS Γ (show Γ ≤ Γ from le_rfl)
case trans Γ U V hU hV ihU ihV =>
apply ihU
intro Δ hΔ
exact ihV ⟨Δ, hΔ⟩ (fun Θ hΘ => hS Θ hΘ.1)With that, we can then again prove the corresponding
truth lemma by induction on the term:
theorem truth_lemma (w : World) : ∀ φ : Tm, at_world w φ ↔ Pf w.carrier φ
| Tm.var i => by
rfl
| Tm.and φ ψ => by
constructor
· intro h
exact Pf.and_I ((truth_lemma w φ).1 h.1) ((truth_lemma w ψ).1 h.2)
· intro h
constructor
· rw [truth_lemma w φ]
exact Pf.and_E₁ h
· rw [truth_lemma w ψ]
exact Pf.and_E₂ h
| Tm.or φ ψ => by
constructor
· intro h
rcases h with ⟨S, hS, hLocal⟩
change ContextCovers w S at hS
apply pf_sheaf hS
intro Δ hΔ
rcases hLocal Δ hΔ with hφ | hψmp.inl
· apply Pf.or_I₁
rw [<- truth_lemma Δ φ]
exact hφ
· apply Pf.or_I₂
rw [<- truth_lemma Δ ψ]
exact hψ
· intro h
refine ⟨context_sieve w [φ, ψ], ?_, ?_⟩
· change ContextCovers w (context_sieve w [φ, ψ])
apply ContextCovers.basic w [φ, ψ]
· exact disjunction_two h
· apply subset_rfl
· intro Δ hΔ
rcases hΔ.2 with ⟨A, hA, hPf⟩
simp at hA
rcases hA with hA | hAmpr.refine_2.inl
· subst A
apply Or.inl
rw [truth_lemma Δ φ]
exact hPf
· subst A
apply Or.inr
rw [truth_lemma Δ ψ]
exact hPf
| Tm.imp φ ψ => by
constructor
· intro hImp
by_cases hff : Pf (φ :: w.carrier) Tm.ffpos
· exact Pf.imp_I (Pf.ff_E hff)
· let v : World := ⟨φ :: w.carrier, hff⟩
have hwv : w ≤ v := List.suffix_cons φ w.carrier
have hφv : at_world v φ := (truth_lemma v φ).2 Pf.assume
have hψv : at_world v ψ := hImp v hwv hφv
exact Pf.imp_I ((truth_lemma v ψ).1 hψv)
· intro hImp v hwv hφv
have hImpv : Pf v.carrier (Tm.imp φ ψ) := Pf.wk hwv hImp
have hφp : Pf v.carrier φ := (truth_lemma v φ).1 hφv
exact (truth_lemma v ψ).2 (Pf.imp_E hImpv hφp)
| Tm.tt => by
constructor
· intro _
exact Pf.tt_I
· intro _
trivial
| Tm.ff => by
constructor
· intro h
exact False.elim h
· intro h
exact False.elim (w.consistent h)Now, suppose we cannot prove \(\Gamma
\vdash \mathcal{P}\), but we have that \(\mathcal{P}\) holds in all Beth frames
\(\Gamma \Vdash_{\mathrm{Beth}}
\mathcal{P}\). We can then take \(\Gamma\) as our world, noting that if it
doesn’t prove \(\mathcal{P}\), then it
must be consistent. So, in order to get a contradiction, we only need to
show that all the terms in \(\Gamma\)
hold at \(\Gamma\), which readily
follows by applying the truth lemma:
theorem all_at_world_self : ∀ w : World, all_at_world w w.carrier := by
intro w
cases w with
| mk carrier consistent =>
induction carrier with
| nil =>
simp
| cons φ Γ ih =>
have htail : ¬ Pf Γ Tm.ff := by
intro hff
exact consistent (Pf.wk (List.suffix_cons φ Γ) hff)
constructor
· rw [truth_lemma ⟨φ :: Γ, consistent⟩ φ]
apply Pf.assume
· have Γ_le : Γ ≤ φ :: Γ := by
apply List.suffix_cons
have w_le : (⟨Γ, htail⟩ : World) ≤ ⟨(φ :: Γ), consistent⟩ := by
exact Γ_le
apply mono_all w_le
apply ih htailIn our proof of completeness, we then split on whether \(\Gamma\) is consistent. As we noted, if it
is not consistent, then we can use false elimination to immediately
prove \(\mathcal{P}\), which is a
contradiction. Otherwise, we may assume that \(\Gamma\) is consistent and so use our model
at world \(\Gamma\). In this world we
have that each of the premises hold by all_at_world_self,
and so we have that \(\mathcal{P}\) is
forced at this world. But then the truth lemma shows that
\(\mathcal{P}\) must be provable:
theorem completeness {Γ : Ctxt} {P : Tm} : Beth.SemEntails.{0} Γ P → Pf Γ P := by
intro hsem
by_cases hff : Pf Γ Tm.ff
· exact Pf.ff_E hff
· let w : World := ⟨Γ, hff⟩
have hΓ : all_at_world w Γ := all_at_world_self w
have hP : at_world w P := hsem World w hΓ
rw [<- truth_lemma w P]
exact hPRevisiting Beth Trees
Let us lastly return to show that Beth trees can be given the structure of a Beth frame, with a topology generated by bars. We encode the conditions for a Beth tree as follows:
structure BethTree (α : Type u) where
tree_node : SnocList α → Prop
root : tree_node .nil
prefix_closed : ∀ l a, tree_node (l :> a) → tree_node l
pruned : ∀ l, tree_node l → ∃ a, tree_node (l :> a)In order to define the notion of a bar, we first need a preliminary definition for the initial segment of a choice sequence:
A bar of a tree node T is then an intensional subset
(i.e. a subset given as a property) whereby any choice sequence
extending our given node eventually hits the bar:
def IsBar {α : Type u} (T : BethTree α) (l : SnocList α) (S : SnocList α → Prop) : Prop :=
∀ f : ℕ → α,
T.tree_node l →
(∀ n, T.tree_node (l ++ initial f n)) →
∃ n, S (l ++ initial f n)This then allows us to define a coverage on Beth trees:
def BethTreeCoverage {α : Type u} (T : BethTree α) :
Coverage {l : SnocList α // T.tree_node l} where
covers w S := IsBar T w.1 (nodeBar S)
maximal := by
intro ⟨l, hl⟩ f hl' hpaths
refine ⟨0, ?_⟩
simp only [initial, SnocList.append_nil, nodeBar, maximal_sieve, Set.mem_setOf_eq]
exact ⟨hl', le_refl _⟩
stability := by
intro ⟨ps, hps⟩ ⟨qs, hqs⟩ S bar_in_S p_le_q f_qsα : Type u in_Tα : Type u f_in_Tα : Type u
haveI : Nonempty α := T.nonemptyα : Type u
obtain ⟨f_ps, n_ps, rfl⟩ := le_init ps qs p_le_qα : Type u
let f_total (i : ℕ) := if h : i < n_ps then f_ps i else f_qs (i - n_ps)α : Type u
have f_total_low : ∀ i < n_ps, f_total i = f_ps i := fun i hi => byα : Type u simp [f_total, hi]
have f_total_high : ∀ i, f_total (n_ps + i) = f_qs i := fun i => byα : Type u
simp [f_total, show ¬ (n_ps + i < n_ps) from Nat.not_lt_of_le (Nat.le_add_right _ _)]
have h_total_init : ∀ m ≤ n_ps, initial f_total m = initial f_ps m := fun m hm =>
initial_eq_of_agree (fun i hi => f_total_low i (Nat.lt_of_lt_of_le hi hm))α : Type u
have h_total_split : initial f_total n_ps = initial f_ps n_ps :=
h_total_init n_ps (le_refl _)α : Type u
have hpath_total : ∀ n, T.tree_node (ps ++ initial f_total n) := by
intro nα : Type u
by_cases h : n ≤ n_psposα : Type unegα : Type u
·posα : Type u rw [h_total_init n h]posα : Type u
exact T.prefix_closed' (SnocList.le_of_initial_le ps h) in_T
·negα : Type u push Not at hnegα : Type u
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.le_of_lt h)negα : Type u
rw [initial_add, ← SnocList.append_assoc, h_total_split,
initial_eq_of_agree (fun i _ => f_total_high i)]negα : Type u
exact f_in_T k
obtain ⟨m, hm_bar⟩ := bar_in_S f_total hps hpath_totalα : Type u
obtain ⟨hm_node, hm_mem⟩ := hm_barα : Type u
by_cases hmle : n_ps ≤ mposα : Type unegα : Type u
·posα : Type u obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmleposα : Type u
refine ⟨k, ?_⟩posα : Type u
simp only [nodeBar, pullback, Set.mem_setOf_eq]posα : Type u
have heq : ps ++ initial f_total (n_ps + k) =
ps ++ initial f_ps n_ps ++ initial f_qs k := by
rw [initial_add, ← SnocList.append_assoc, h_total_split,
initial_eq_of_agree (fun i _ => f_total_high i)]
have hm_node' : T.tree_node (ps ++ initial f_ps n_ps ++ initial f_qs k) := heq ▸ hm_nodeposα : Type u
have helem : (⟨ps ++ initial f_total (n_ps + k), hm_node⟩ : {l : SnocList α // T.tree_node l}) =
⟨ps ++ initial f_ps n_ps ++ initial f_qs k, hm_node'⟩ := Subtype.ext heqposα : Type u
exact ⟨hm_node', helem ▸ hm_mem, SnocList.is_prefix_append _ _⟩
·negα : Type u push Not at hmlenegα : Type u
refine ⟨0, ?_⟩negα : Type u
simp only [initial, SnocList.append_nil, nodeBar, pullback, Set.mem_setOf_eq]negα : Type u
have hm_le : m ≤ n_ps := Nat.le_of_lt hmlenegα : Type u
have hle_qs : ps ++ initial f_total m ≤ ps ++ initial f_ps n_ps := by
rw [h_total_init m hm_le]α : Type u; exact SnocList.le_of_initial_le ps hm_le
exact ⟨hqs, S.upward_closed hm_mem hle_qs, le_refl _⟩
transitive := by
intro ⟨l, hl⟩ U V bar_in_U h_UV fα : Type u in_Tα : Type u f_in_Tα : Type u
obtain ⟨n1, hn1_bar⟩ := bar_in_U f hl f_in_Tα : Type u
obtain ⟨hn1_node, hn1_mem⟩ := hn1_barα : Type u
let q := l ++ initial f n1α : Type u
let f_tail (i : ℕ) := f (n1 + i)α : Type u
have f_tail_in_T : ∀ n, T.tree_node (q ++ initial f_tail n) := fun n => byα : Type u
simpa [q, f_tail, initial_add, SnocList.append_assoc] using f_in_T (n1 + n)
have h_cov_q := h_UV ⟨⟨q, hn1_node⟩, hn1_mem⟩α : Type u
obtain ⟨n2, hn2_bar⟩ := h_cov_q f_tail hn1_node f_tail_in_Tα : Type u
obtain ⟨hn2_node, hn2_mem⟩ := hn2_barα : Type u
simp only [pullback, Set.mem_setOf_eq] at hn2_memα : Type u
refine ⟨n1 + n2, ?_⟩α : Type u
simp only [nodeBar]α : Type u
have heq : q ++ initial f_tail n2 = l ++ initial f (n1 + n2) := by
simp [q, f_tail, initial_add, SnocList.append_assoc]
have hn2_node' : T.tree_node (l ++ initial f (n1 + n2)) := heq ▸ hn2_node
have helem : (⟨q ++ initial f_tail n2, hn2_node⟩ : {l : SnocList α // T.tree_node l}) =
⟨l ++ initial f (n1 + n2), hn2_node'⟩ := Subtype.ext heq
exact ⟨hn2_node', helem ▸ hn2_mem.1⟩We can then finally construct a concrete example of the full binary
bit tree as a Beth frame. In our valuation we have that the variable
\(\mathcal{P}:= \mathrm{var}\; 0\) is
forced on the left false branch, and \(\mathcal{Q}:= \mathrm{var}\; 1\) is forced
on the right true branch. As such, unlike Kripke semantics,
we have that \(\mathcal{P}\lor
\mathcal{Q}\) is forced at the root, by the bar of depth 1,
despite neither \(\mathcal{P}\) nor
\(\mathcal{Q}\) being forced at the
root:
def fullBinaryTree : BethTree Bool where
tree_node _ := True
root := trivial
prefix_closed _ _ _ := trivial
pruned _l _ := ⟨false, trivial⟩def binaryBranchVal : BethVal fullBinaryTree where
val l i := match i with
| 0 => (SnocList.nil :> false) ≤ l
| 1 => (SnocList.nil :> true) ≤ l
| _ => False
mono_val := by
intro l m i hle _ hval
match i with
| 0 => exact SnocList.is_prefix_trans hval hle
| 1 => exact SnocList.is_prefix_trans hval hle
| _ + 2 => exact hval.elim
sheaf_val := by
intro l i _ hbar
match i with
| 0 =>
by_contra h
simp at h
simp at hbar
-- If ¬ εₛ :> ff ≤ l, then the l ++ initial (fun _ => tt) is not barred
obtain ⟨n, hn⟩ := hbar (fun _ => true) trivial (fun _ => trivial)
apply not_prefix_false_of_const_true l n h hn
| 1 =>
by_contra h
simp at h
simp at hbar
-- If ¬ εₛ :> tt ≤ l, then the l ++ initial (fun _ => ff) is not barred
obtain ⟨n, hn⟩ := hbar (fun _ => false) trivial (fun _ => trivial)
exact not_prefix_true_of_const_false l n h hn
| i + 2 =>
simp at hbar
obtain ⟨_, hm, _⟩ := IsBar.nonempty fullBinaryTree hbar trivial
exact hm.eliminstance fullBinaryBethFrame : BethFrame {l : SnocList Bool // fullBinaryTree.tree_node l} :=
BethTreeFrame fullBinaryTree binaryBranchValexample : at_world root (Tm.or (Tm.var 0) (Tm.var 1)) := by
simp only [at_world]
let S : Sieve root := {
carrier := {w | (εₛ :> false : SnocList Bool) ≤ w.1 ∨
(εₛ :> true : SnocList Bool) ≤ w.1},
bounded := fun _ => nil_prefix _,
upward_closed := by
intro q r hmem r_le_q
simp at hmem
apply hmem.impf
· exact (fun h => SnocList.is_prefix_trans h r_le_q)
· exact (fun h => SnocList.is_prefix_trans h r_le_q)
}
refine ⟨S, ?_, ?_⟩refine_1
· -- The sieve is a bar at nil: at depth 1, f 0 is false or true.
intro f _ _
refine ⟨1, trivial, ?_⟩
-- Reduce nil ++ initial f 1 = nil :> f 0 and unfold set membership
simp only [initial, SnocList.append_snoc, SnocList.append_nil]
-- Goal: nil :> false ≤ nil :> f 0 ∨ nil :> true ≤ nil :> f 0
simp [S]
exact Bool.casesOn (f 0) (Or.inl (Or.inl rfl)) (Or.inr (Or.inl rfl))
· -- Every element of the sieve forces var 0 or var 1.
intro ⟨m, _⟩ hm
rcases hm with h | h
· exact Or.inl h
· exact Or.inr hOne sometimes wonders which governmental agency is responsible for such names↩︎
Analogous to a typing context↩︎
We would be better off in a more long-lived implementation using a snoc-list here to fit with our typical spatial intuitions for contexts growing on the right↩︎
We sometimes say the variable is forced at that world, because of the tight connection with Cohen’s use of forcing in set theory↩︎
This is only consistency with respect to the background theory, in this case the type theory of
lean↩︎Both are fundamentally connected to the compactness theorem and thus to the concept of ultrafilters↩︎
They can be perused in all their details here for those who are curious↩︎
One will note that we require our world to be
prime, precisely in order to prove the∨case of thetruth lemma↩︎This is typically called The Baire Space↩︎
meaning that if it holds of a sequence, then it holds of its parent node↩︎
As noted above, we would be better off using the dual preorder, and so throughout this section our terminology is regrettably non-standard. What we call a sieve is more typically now called a co-sieve. Similarly, we will later use the term
pullbackfor something that evidently goes in the wrong direction.↩︎As noted, if we were considering sub-functors of \(\operatorname{Hom}(-, \mathcal{A})\) – and so set up our semantics as contravariant functors – as is much more typical in the literature on Grothendieck topologies, then this is indeed a kind of pullback↩︎
I learned of this concept from Jeremy Avigad’s excellent book Mathematical Logic and Computation, but he calls this concept a “generalized Beth model”↩︎