Popper
Difficulty: hard — 4 definitions, 0 abbreviations, 0 lemmas, 7 theorems, 0 examples.
Propositional logic gives Popper’s Basis III two different, clearly separate instances, depending on what “deducibility between two formulas” is taken to mean.
Semantic entailment holds between \(\varphi\) and \(\psi\) when every valuation making \(\varphi\) true also makes \(\psi\) true — a fact about truth tables, nothing else. Syntactic entailment holds between them when \(\varphi \to \psi\) is provable in the Hilbert system — a fact about derivations, nothing else. Basis III does not care which: reflexivity and transitivity are all it asks of a deducibility relation, and both notions have them.
Under the semantic instance, conjunction, disjunction, and negation satisfy Popper’s own characterizing properties for a conjunction, a disjunction, and a classical negation.
Propositional.Formula.SemanticEntails
Semantic entailment: every valuation making \(\varphi\) true also makes \(\psi\) true. Reflexive and transitive for free, which is exactly what a Popper.Basis3 needs.
Propositional.Formula.SemanticEntails {α : Type} (φ ψ : Propositional.Formula α) : Prop
Show details
fun {α} φ ψ => ∀ (v : Propositional.Valuation α), Propositional.Formula.val v φ = true → Propositional.Formula.val v ψ = true
Complexity: 41 (size of the value term)
Outer dependencies: Propositional.Formula
Inner dependencies: Propositional.Formula.val, Propositional.Valuation
Propositional.Formula.SemanticEntails.refl
Propositional.Formula.SemanticEntails.refl {α : Type} (φ : Propositional.Formula α) : φ.SemanticEntails φ
Show details
fun {α} φ x h => h
Complexity: 25 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.SemanticEntails
Proof dependencies: Propositional.Formula.val, Propositional.Valuation
Used by: Propositional.semanticBasis3
Propositional.Formula.SemanticEntails.trans
Propositional.Formula.SemanticEntails.trans {α : Type} {φ ψ χ : Propositional.Formula α} (h1 : φ.SemanticEntails ψ) (h2 : ψ.SemanticEntails χ) : φ.SemanticEntails χ
Show details
fun {α} {φ ψ χ} h1 h2 v h => h2 v (h1 v h)
Complexity: 57 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.SemanticEntails
Proof dependencies: Propositional.Formula.val, Propositional.Valuation
Propositional.semanticBasis3
Propositional formulas over \(\alpha\), with semantic entailment as the deducibility relation, form a Popper.Basis3. Every notion Basis III provides in general — the recovered many-premise deducibility, relative demonstrability, and Cut — applies here without any further proof.
Propositional.semanticBasis3 (α : Type) : Popper.Basis3
Show details
fun α => { Obj := Propositional.Formula α, Deduce := Propositional.Formula.SemanticEntails, refl := ⋯, trans := ⋯ }
Complexity: 37 (size of the value term)
Outer dependencies: Popper.Basis3
Propositional.Formula.SyntacticEntails
Syntactic entailment: \(\varphi \to \psi\) is provable in the Hilbert system. Reflexive (Propositional.Formula.provable_self_imp) and transitive (hypothetical syllogism, via the Deduction Theorem) — the same two closure conditions semantic entailment satisfies, just established by proof search instead of by truth tables.
Propositional.Formula.SyntacticEntails {α : Type} (φ ψ : Propositional.Formula α) : Prop
Show details
fun {α} φ ψ => (φ.imp ψ).Provable
Complexity: 21 (size of the value term)
Outer dependencies: Propositional.Formula
Inner dependencies: Propositional.Formula.Provable
Propositional.Formula.SyntacticEntails.refl
Propositional.Formula.SyntacticEntails.refl {α : Type} (φ : Propositional.Formula α) : φ.SyntacticEntails φ
Show details
fun {α} φ => Propositional.Formula.provable_self_imp φ
Complexity: 11 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.SyntacticEntails
Proof dependencies: Propositional.Formula.provable_self_imp
Used by: Propositional.syntacticBasis3
Propositional.Formula.SyntacticEntails.trans
Propositional.Formula.SyntacticEntails.trans {α : Type} {φ ψ χ : Propositional.Formula α} (h1 : φ.SyntacticEntails ψ) (h2 : ψ.SyntacticEntails χ) : φ.SyntacticEntails χ
Show details
fun {α} {φ ψ χ} h1 h2 => Propositional.Formula.Derivable.provable_of_nil (Propositional.Formula.Derivable.deduction (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax h2) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax h1) (Propositional.Formula.Derivable.assumption (List.mem_singleton_self φ)))))
Complexity: 183 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.SyntacticEntails
Proof dependencies: Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.provable_of_nil
Lean core dependencies: List.mem_singleton_self
Used by: Propositional.syntacticBasis3
Propositional.syntacticBasis3
Propositional formulas over \(\alpha\), with syntactic entailment as the deducibility relation, also form a Popper.Basis3 — a second, unrelated instance from Propositional.semanticBasis3, since Basis III only ever asks for reflexivity and transitivity.
Propositional.syntacticBasis3 (α : Type) : Popper.Basis3
Show details
fun α => { Obj := Propositional.Formula α, Deduce := Propositional.Formula.SyntacticEntails, refl := ⋯, trans := ⋯ }
Complexity: 37 (size of the value term)
Outer dependencies: Popper.Basis3
Propositional.Formula.and_isConjunction
Conjunction. The conjunction of \(\varphi\) and \(\psi\) satisfies Popper’s characterizing property for a conjunction of the two.
Propositional.Formula.and_isConjunction {α : Type} (φ ψ : Propositional.Formula α) : (Propositional.semanticBasis3 α).toBasis1.IsConjunction φ ψ (φ.and ψ)
Show details
fun {α} φ ψ => have key := fun D c => id { mp := fun h e he => h e fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce e _a) heq)) ((Propositional.Formula.entails_and_iff✝ e φ ψ).mpr ⟨he φ List.mem_cons_self, he ψ (List.mem_cons.mpr (Or.inr List.mem_cons_self))⟩)) fun ha => he a (List.mem_cons.mpr (Or.inr (List.mem_cons.mpr (Or.inr ha)))), mpr := fun h e he => h e fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce e _a) heq)) ((Propositional.Formula.entails_and_iff✝ e φ ψ).mp (he (φ.and ψ) List.mem_cons_self)).left) fun ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce e _a) heq)) ((Propositional.Formula.entails_and_iff✝ e φ ψ).mp (he (φ.and ψ) List.mem_cons_self)).right) fun ha => he a (List.mem_cons.mpr (Or.inr ha)) }; fun d => id (id { mp := fun h c D hD => (key D c).mp (h c D hD), mpr := fun h c D hD => (key D c).mpr (h c D hD) })
Complexity: 6288 (size of the value term)
Dependencies: Popper.Basis1.IsConjunction, Popper.Basis3.toBasis1, Propositional.Formula, Propositional.semanticBasis3
Proof dependencies: Popper.Basis1.Derive, Popper.Basis3.NDeduce, Popper.Basis3.ndeduce_rg, Popper.Basis3.ndeduce_tg, Propositional.Formula.SemanticEntails
Lean core dependencies: And, Eq, Eq.mpr, Iff, List, List.mem_cons, List.mem_cons_self, Or, congrArg, id
Used by: (none)
Propositional.Formula.or_isDisjunction
Disjunction. The disjunction of \(\varphi\) and \(\psi\) satisfies Popper’s characterizing property for a disjunction of the two.
Propositional.Formula.or_isDisjunction {α : Type} (φ ψ : Propositional.Formula α) : (Propositional.semanticBasis3 α).toBasis1.IsDisjunction φ ψ (φ.or ψ)
Show details
fun {α} φ ψ d => { mp := fun L c D hQ => have hφ := hQ φ (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self φ)) (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (φ = ψ)) List.not_mem_nil._simp_1) (or_false (φ = ψ))))) (true_or (φ = ψ))))); have hψ := hQ ψ (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (ψ = φ)) (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self ψ)) List.not_mem_nil._simp_1) (or_false True)))) (or_true (ψ = φ))))); L c D fun b hb => Eq.symm (Eq.mp (congrArg (fun _a => _a) (propext List.mem_singleton)) hb) ▸ fun e he => have hφD := fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.Formula.and e φ).SemanticEntails _a) heq)) (Propositional.Formula.and_entails_right✝ e φ)) fun ha => Propositional.Formula.SemanticEntails.trans (Propositional.Formula.and_entails_left✝ e φ) (he a (List.mem_cons.mpr (Or.inr ha))); have hψD := fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.Formula.and e ψ).SemanticEntails _a) heq)) (Propositional.Formula.and_entails_right✝ e ψ)) fun ha => Propositional.Formula.SemanticEntails.trans (Propositional.Formula.and_entails_left✝ e ψ) (he a (List.mem_cons.mpr (Or.inr ha))); have hc1 := hφ (Propositional.Formula.and e φ) hφD; have hc2 := hψ (Propositional.Formula.and e ψ) hψD; have hd := he (φ.or ψ) List.mem_cons_self; fun v hv => Or.casesOn (Bool.or_eq_true_iff.mp (Eq.mpr (id (Bool.or_eq_true (Propositional.Formula.val v φ) (Propositional.Formula.val v ψ))) (Eq.mp (Bool.or_eq_true (Propositional.Formula.val v φ) (Propositional.Formula.val v ψ)) (hd v hv)))) (fun hφv => hc1 v (of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and hv) hφv) (Bool.and_self true))) true) (eq_self true)))) fun hψv => hc2 v (of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and hv) hψv) (Bool.and_self true))) true) (eq_self true))), mpr := fun R c D hQ => have hj := hQ (φ.or ψ) (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self (φ.or ψ))) List.not_mem_nil._simp_1) (or_false True)))); R c D fun b hb => Or.casesOn (List.mem_cons.mp hb) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).toBasis1.Deduce (_a :: D) c) heq)) fun e he => hj e fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq2 => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce e _a) heq2)) (Propositional.Formula.SemanticEntails.trans (he φ List.mem_cons_self) (Propositional.Formula.or_entails_left✝ φ ψ))) fun ha => he a (List.mem_cons.mpr (Or.inr ha))) fun hb_1 => Eq.ndrec (motive := fun ψ => (Propositional.semanticBasis3 α).toBasis1.Derive [d] [φ, ψ] → (∀ b ∈ [φ.or ψ], (Propositional.semanticBasis3 α).toBasis1.Deduce (b :: D) c) → (Propositional.semanticBasis3 α).NDeduce (φ.or ψ :: D) c → b ∈ [φ, ψ] → (Propositional.semanticBasis3 α).toBasis1.Deduce (b :: D) c) (fun R hQ hj hb e he => hj e fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq2 => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce e _a) heq2)) (Propositional.Formula.SemanticEntails.trans (he b List.mem_cons_self) (Propositional.Formula.or_entails_right✝ φ b))) fun ha => he a (List.mem_cons.mpr (Or.inr ha))) (Eq.mp (congrArg (fun _a => _a) (propext List.mem_singleton)) hb_1) R hQ hj hb }
Complexity: 7985 (size of the value term)
Dependencies: Popper.Basis1.IsDisjunction, Popper.Basis3.toBasis1, Propositional.Formula, Propositional.semanticBasis3
Proof dependencies: Popper.Basis1.Derive, Popper.Basis3.NDeduce, Propositional.Formula.SemanticEntails, Propositional.Formula.SemanticEntails.trans, Propositional.Formula.val, Propositional.Valuation
Lean core dependencies: Bool, Bool.and, Bool.and_self, Bool.or, Bool.or_eq_true, Bool.or_eq_true_iff, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, List, List.mem_cons, List.mem_cons_self, List.mem_singleton, Or, True, congr, congrArg, congrFun', eq_self, id, of_eq_true, or_false, or_true, true_or
Used by: (none)
Propositional.Formula.neg_isClassicalNegation
Classical negation. The negation of \(\varphi\) satisfies Popper’s characterizing property for a classical negation of it.
Propositional.Formula.neg_isClassicalNegation {α : Type} (φ : Propositional.Formula α) : (Propositional.semanticBasis3 α).toBasis1.IsClassicalNegation φ φ.neg
Show details
fun {α} φ d q => { mp := fun L c D hQ => have hφ := hQ φ (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self φ)) (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (φ = q)) List.not_mem_nil._simp_1) (or_false (φ = q))))) (true_or (φ = q))))); have hq := hQ q (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (q = φ)) (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self q)) List.not_mem_nil._simp_1) (or_false True)))) (or_true (q = φ))))); have hL := L c D fun b hb => Eq.symm (List.mem_singleton.mp hb) ▸ hq; fun e he => have heD := he d List.mem_cons_self; have heCtx := fun a ha => he a (List.mem_cons.mpr (Or.inr ha)); have h1 := hL (Propositional.Formula.and e φ.neg) fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce (Propositional.Formula.and e φ.neg) _a) heq)) (Propositional.Formula.SemanticEntails.trans (Propositional.Formula.and_entails_left✝ e φ.neg) heD)) fun ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce (Propositional.Formula.and e φ.neg) _a) heq)) (Propositional.Formula.and_entails_right✝ e φ.neg)) fun ha => Propositional.Formula.SemanticEntails.trans (Propositional.Formula.and_entails_left✝ e φ.neg) (heCtx a ha); have h2 := hφ (Propositional.Formula.and e φ) fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce (Propositional.Formula.and e φ) _a) heq)) (Propositional.Formula.and_entails_right✝ e φ)) fun ha => Propositional.Formula.SemanticEntails.trans (Propositional.Formula.and_entails_left✝ e φ) (heCtx a ha); fun v hv => Bool.casesOn (motive := fun x => Propositional.Formula.val v φ = x → Propositional.Formula.val v c = true) (Propositional.Formula.val v φ) (fun hφv => h1 v (of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and hv) (Eq.trans (congrArg not hφv) Bool.not_false)) (Bool.and_self true))) true) (eq_self true)))) (fun hφv => h2 v (of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and hv) hφv) (Bool.and_self true))) true) (eq_self true)))) (Eq.refl (Propositional.Formula.val v φ)), mpr := fun R c D hq => have hq' := hq q (List.mem_singleton_self q); R c (φ.neg :: D) fun b hb => Or.casesOn (List.mem_cons.mp hb) (fun heq => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).toBasis1.Deduce (_a :: φ.neg :: D) c) heq)) fun e he => have h1 := he φ List.mem_cons_self; have h2 := he φ.neg (List.mem_cons.mpr (Or.inr List.mem_cons_self)); Propositional.Formula.entails_of_entails_neg_contra✝ h1 h2 c) fun hb => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).toBasis1.Deduce (_a :: φ.neg :: D) c) (Eq.mp (congrArg (fun _a => _a) (propext List.mem_singleton)) hb))) fun e he => hq' e fun a ha => Or.casesOn (List.mem_cons.mp ha) (fun heq2 => Eq.mpr (id (congrArg (fun _a => (Propositional.semanticBasis3 α).Deduce e _a) heq2)) (he q List.mem_cons_self)) fun ha => he a (List.mem_cons.mpr (Or.inr (List.mem_cons.mpr (Or.inr ha)))) }
Complexity: 7459 (size of the value term)
Dependencies: Popper.Basis1.IsClassicalNegation, Popper.Basis3.toBasis1, Propositional.Formula, Propositional.semanticBasis3
Proof dependencies: Popper.Basis1.Derive, Popper.Basis3.NDeduce, Propositional.Formula.SemanticEntails, Propositional.Formula.SemanticEntails.trans, Propositional.Formula.val, Propositional.Valuation
Lean core dependencies: Bool, Bool.and, Bool.and_self, Bool.not, Bool.not_false, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, List, List.append, List.mem_cons, List.mem_cons_self, List.mem_singleton, List.mem_singleton_self, Or, True, congr, congrArg, congrFun', eq_self, id, of_eq_true, or_false, or_true, true_or
Used by: (none)
Dependency diagram
Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.