Knowledge is justified true belief

Helper Lemmas

theorem Error.involved_not_have_before_of_not_have_after {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (C : Call) (σ : List Call) (a : Agent) (o : maxOne (C :: σ)) (r_in : roleOfIn a C ≠ Role.Other) (a_has_no_k : (b, k) ∉ S⌈⟨C :: σ, o⟩⌉a) (a_has_no_not_k : (b, !k) ∉ S⌈⟨C :: σ, o⟩⌉a) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉a

If a is in C and has neither value of b after call C, then before the call they also cannot have had the real value.

theorem Error.errFree_resultSet_correct {n : ℕ} (c : Agent) (S : Dist) (σ : Sequence) (o : maxOne σ) (h : errFree σ) (j : Agent) (d : Bool) (mem : (j, d) ∈ S⌈⟨σ, o⟩⌉c) : d = S j

For errFree sequences, all values in the result set are correct.

theorem Error.errFree_resultSet_dist_independent {n : ℕ} (c j : Agent) (S T : Dist) (σ : Sequence) (o : maxOne σ) (h : errFree σ) (mem : (j, S j) ∈ S⌈⟨σ, o⟩⌉c) : (j, T j) ∈ T⌈⟨σ, o⟩⌉c

If σ is errFree and after σ agent c has the real value (j, S j), then for any other initial distribution T we also have that after σ agent c has the real value (j, T j).

theorem Error.resultSet_switch_invert_errFree {n : ℕ} (b c : Agent) (S : Dist) (σ : Sequence) (o : maxOne σ) (h : errFree σ) : invert b (S⌈⟨σ, o⟩⌉c) = (Dist.switch b S)⌈⟨σ, o⟩⌉c

theorem Error.caller_real_value_not_before {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (κ : Call) (σ : List Call) (a : Agent) (o : maxOne (κ :: σ)) (ra : roleOfIn a κ = Role.Caller) (a_has_no_k : (b, k) ∉ S⌈⟨κ :: σ, o⟩⌉a) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉a

If a is the Caller, S b = k, and (b,k) is NOT in a's result set after the call, then (b,k) was NOT in a's result set before the call either. This is because the true value can never be refused or deleted.

theorem Error.callee_real_value_not_in_normal {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (a : Agent) (c : { b : Agent // b ≠ a }) (σ : List Call) (o : maxOne (⌜a c⌝ :: σ)) (a_has_no_k : (b, k) ∉ S⌈⟨⌜a c⌝ :: σ, o⟩⌉a) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉↑c

Extract callee not having (b,k) from caller not having (b,k) after normal call.

theorem Error.callee_real_value_not_in_fstE {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (a e : Agent) (c : { b : Agent // b ≠ a }) (σ : List Call) (o : maxOne (⌜a^e c⌝ :: σ)) (a_has_no_k : (b, k) ∉ S⌈⟨⌜a^e c⌝ :: σ, o⟩⌉a) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉↑c

Extract callee not having (b,k) from caller not having (b,k) after fstE call.

theorem Error.callee_real_value_not_before {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (κ : Call) (σ : List Call) (a : Agent) (o : maxOne (κ :: σ)) (ra : roleOfIn a κ = Role.Callee) (a_has_no_k : (b, k) ∉ S⌈⟨κ :: σ, o⟩⌉a) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉a

If a is the Callee, S b = k, and (b,k) is NOT in a's result set after the call, then (b,k) was NOT in a's result set before the call either.

theorem Error.caller_real_value_not_in_normal {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (a : Agent) (c : { b : Agent // b ≠ a }) (σ : List Call) (o : maxOne (⌜a c⌝ :: σ)) (c_has_no_k : (b, k) ∉ S⌈⟨⌜a c⌝ :: σ, o⟩⌉↑c) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉a

Extract caller not having (b,k) from callee not having (b,k) after normal call.

theorem Error.caller_real_value_not_in_fstE {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (a e : Agent) (ne : e ≠ b) (c : { b : Agent // b ≠ a }) (σ : List Call) (o : maxOne (⌜a^e c⌝ :: σ)) (c_has_no_k : (b, k) ∉ S⌈⟨⌜a^e c⌝ :: σ, o⟩⌉↑c) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉a

Extract caller not having (b,k) from callee not having (b,k) after fstE call with e ≠ b.

theorem Error.caller_real_value_not_in_sndE {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (a e : Agent) (c : { b : Agent // b ≠ a }) (σ : List Call) (o : maxOne (⌜a c^e⌝ :: σ)) (c_has_no_k : (b, k) ∉ S⌈⟨⌜a c^e⌝ :: σ, o⟩⌉↑c) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉a

Extract caller not having (b,k) from callee not having (b,k) after sndE call.

theorem Error.callee_real_value_not_in_sndE {n : ℕ} {b : Agent} {S : Dist} {k : Bool} (is_k : S b = k) (a e : Agent) (ne : e ≠ b) (c : { b : Agent // b ≠ a }) (σ : List Call) (o : maxOne (⌜a c^e⌝ :: σ)) (a_has_no_k : (b, k) ∉ S⌈⟨⌜a c^e⌝ :: σ, o⟩⌉a) : (b, k) ∉ S⌈⟨σ, ⋯⟩⌉↑c

Extract callee not having (b,k) from caller not having (b,k) after sndE call with e ≠ b.

theorem Error.consider_corrected_caller {n : ℕ} (a b : Agent) {S : Dist} {k : Bool} (real_b_is_k : S b = k) (κ : Call) (σ : List Call) (o : maxOne (κ :: σ)) (a_has_no_b_k : (b, k) ∉ S⌈⟨κ :: σ, o⟩⌉a) (role_def : roleOfIn a κ = Role.Caller) (IH : ∀ (c : Agent), (b, k) ∉ S⌈⟨σ, ⋯⟩⌉c → equiv c (S, ⟨⟨σ, ⋯⟩, ⋯⟩) (Dist.switch b S, ⟨⟨cor b σ, ⋯⟩, ⋯⟩)) : equiv a (S, ⟨⟨κ :: σ, o⟩, ⋯⟩) (Dist.switch b S, ⟨⟨Call.cor b κ :: cor b σ, ⋯⟩, ⋯⟩)

Helper for the Caller case of consider_corrected.

theorem Error.consider_corrected_callee {n : ℕ} (a b : Agent) {S : Dist} {k : Bool} (real_b_is_k : S b = k) (κ : Call) (σ : List Call) (o : maxOne (κ :: σ)) (a_has_no_b_k : (b, k) ∉ S⌈⟨κ :: σ, o⟩⌉a) (role_def : roleOfIn a κ = Role.Callee) (IH : ∀ (c : Agent), (b, k) ∉ S⌈⟨σ, ⋯⟩⌉c → equiv c (S, ⟨⟨σ, ⋯⟩, ⋯⟩) (Dist.switch b S, ⟨⟨cor b σ, ⋯⟩, ⋯⟩)) : equiv a (S, ⟨⟨κ :: σ, o⟩, ⋯⟩) (Dist.switch b S, ⟨⟨Call.cor b κ :: cor b σ, ⋯⟩, ⋯⟩)

Helper for the Callee case of consider_corrected.

@[irreducible]

theorem Error.consider_corrected {n : ℕ} (a b : Agent) {S : Dist} {σ : OSequence} {k : Bool} (real_b_is_k : S b = k) (a_has_no_b_k : (b, k) ∉ S⌈σ⌉a) : equiv a (S, ⟨σ, ⋯⟩) (Dist.switch b S, ⟨⟨cor b ↑σ, ⋯⟩, ⋯⟩)

Key Lemma 12 that helps to show knowledge_implies_correct_belief. If the actual values of b is k, but agent a does not yet have it, then agent a considers possible the b-switched distribution with the b-correction of the actual sequence.

Lemmas about Keeping and Rejecting

theorem Error.callee_keeps_known_value {n : ℕ} {a b : Agent} {k : Bool} (C : Call) (ra : roleOfIn a C = Role.Callee) (S : Dist) (σ : Sequence) (o : maxOne (C :: σ)) (know_before : S⌈⟨σ, ⋯⟩⌉ ⊧ Form.K a ((b, k)@b)) (had_before : S⌈⟨σ, ⋯⟩⌉ ⊧ (b, k)@a) : S⌈⟨C :: σ, o⟩⌉ ⊧ (b, k)@a

theorem Error.callee_rejects_opposite_of_known_value {n : ℕ} {a b : Agent} {k : Bool} (C : Call) (ra : roleOfIn a C = Role.Callee) (S : Dist) (σ : Sequence) (o : maxOne (C :: σ)) (know_before : S⌈⟨σ, ⋯⟩⌉ ⊧ Form.K a ((b, k)@b)) : S⌈⟨C :: σ, o⟩⌉ ⊧ ( ¬'(b, !k)@a)

theorem Error.callee_rejects_opposite_of_afterwards_known_value {n : ℕ} {a b : Agent} {k : Bool} (C : Call) (ra : roleOfIn a C = Role.Callee) (S : Dist) (σ : List Call) (o : maxOne (C :: σ)) (know_after : S⌈⟨C :: σ, o⟩⌉ ⊧ Form.K a ((b, k)@b)) : S⌈⟨C :: σ, o⟩⌉ ⊧ ( ¬'(b, !k)@a)

Main Result

theorem Error.knowledge_implies_correct_belief {n : ℕ} {a b : Agent} {k : Bool} : ⊨ ( ¬'( ¬' ¬'Form.K a ((b, k)@b) ⋀ ¬'((b, k)@b ⋀ (b, k)@a ⋀ ¬'(b, !k)@a)))

Proposition 13. Parts (i) and (ii) are given by different k values.

theorem Error.knowledge_is_justified_true_belief {k : Bool} {n : ℕ} {a b : Agent} : ⊨ ( ¬'( ¬' ¬'Form.K a ((b, k)@b) ⋀ ¬'Form.K a ((b, k)@b ⋀ (b, k)@a ⋀ ¬'(b, !k)@a)) ⋀ ¬'( ¬' ¬'Form.K a ((b, k)@b ⋀ (b, k)@a ⋀ ¬'(b, !k)@a) ⋀ ¬'Form.K a ((b, k)@b)))

Corollary 14.