Popper

Difficulty: hard — 2 definitions, 0 abbreviations, 18 lemmas, 4 theorems, 0 examples.

definition lemma theorem

legend

Propositional logic gives Popper’s Basis III two different, clearly separate instances, depending on what “deducibility between two formulas” is taken to mean.

Syntactic entailment holds between \(\varphi\) and \(\psi\) when \(\varphi \to \psi\) is provable in the Hilbert system — a fact about derivations, nothing else. Semantic entailment holds between them when every valuation making \(\varphi\) true also makes \(\psi\) true — a fact about truth tables, 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 each instance, conjunction, disjunction, and negation satisfy Popper’s own characterizing properties for a conjunction, a disjunction, and a classical negation — shown below for the syntactic instance first, then for the semantic one.

Syntax

NoteLogic.PropositionalLogic.Formula.SyntacticEntails

Syntactic entailment: \(\varphi \to \psi\) is provable in the Hilbert system.

def Logic.PropositionalLogic.Formula.SyntacticEntails {α : Type}
  (φ ψ : Logic.PropositionalLogic.Formula α) : Prop

Show details

| φ.SyntacticEntails ψ = (φ.imp ψ).Provable

Complexity: 21 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula

Inner dependencies: Logic.PropositionalLogic.Formula.Provable

Used by: Logic.PropositionalLogic.Formula.SyntacticEntails.refl, Logic.PropositionalLogic.Formula.SyntacticEntails.trans, Logic.PropositionalLogic.Formula.and_entails_left_syntactic, Logic.PropositionalLogic.Formula.and_entails_right_syntactic, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.or_entails_left_syntactic, Logic.PropositionalLogic.Formula.or_entails_right_syntactic, Logic.PropositionalLogic.syntacticBasis3, Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.SyntacticEntails.refl

Reflexivity of syntactic entailment: every formula implies itself (PropositionalLogic.Formula.provable_self_imp).

theorem Logic.PropositionalLogic.Formula.SyntacticEntails.refl {α : Type}
  (φ : Logic.PropositionalLogic.Formula α) : φ.SyntacticEntails φ

Show details

fun {α} φ => Logic.PropositionalLogic.Formula.provable_self_imp φ

Complexity: 11 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.provable_self_imp

Used by: Logic.PropositionalLogic.syntacticBasis3

TipLogic.PropositionalLogic.Formula.SyntacticEntails.trans

Transitivity of syntactic entailment: hypothetical syllogism, via the Deduction Theorem.

theorem Logic.PropositionalLogic.Formula.SyntacticEntails.trans {α : Type}
  {φ ψ χ : Logic.PropositionalLogic.Formula α} (h1 : φ.SyntacticEntails ψ)
  (h2 : ψ.SyntacticEntails χ) : φ.SyntacticEntails χ

Show details

fun {α} {φ ψ χ} h1 h2 =>
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax h2)
        (Logic.PropositionalLogic.Formula.Derivable.mp
          (Logic.PropositionalLogic.Formula.Derivable.ax h1)
          (Logic.PropositionalLogic.Formula.Derivable.assumption (List.mem_singleton_self φ)))))

Complexity: 183 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil

Lean core dependencies: List.mem_singleton_self

Used by: Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.syntacticBasis3, Logic.PropositionalLogic.syntacticConnectives

ImportantLogic.PropositionalLogic.syntacticBasis3

Propositional formulas over \(\alpha\), with syntactic 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.

instance Logic.PropositionalLogic.syntacticBasis3 (α : Type) :
  Logic.Popper.Basis3 (Logic.PropositionalLogic.Formula α)

Show details

| Logic.PropositionalLogic.syntacticBasis3 α =
  { Follows := Logic.PropositionalLogic.Formula.SyntacticEntails, refl := ⋯, trans := ⋯ }

Complexity: 37 (size of the value term)

Outer dependencies: Logic.Popper.Basis3, Logic.PropositionalLogic.Formula

Inner dependencies: Logic.PropositionalLogic.Formula.SyntacticEntails, Logic.PropositionalLogic.Formula.SyntacticEntails.refl, Logic.PropositionalLogic.Formula.SyntacticEntails.trans

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic, Logic.PropositionalLogic.Formula.syntactic_iff_provable, Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.entails_and_iff_syntactic

theorem Logic.PropositionalLogic.Formula.entails_and_iff_syntactic✝ {α : Type}
  (e a b : Logic.PropositionalLogic.Formula α) :
  e.SyntacticEntails (a.and b) ↔ e.SyntacticEntails a ∧ e.SyntacticEntails b

Show details

fun {α} e a b =>
  {
    mp := fun h =>
      ⟨Logic.PropositionalLogic.Formula.SyntacticEntails.trans h
          Logic.PropositionalLogic.Formula.Provable.andElim1,
        Logic.PropositionalLogic.Formula.SyntacticEntails.trans h
          Logic.PropositionalLogic.Formula.Provable.andElim2⟩,
    mpr := fun a_1 =>
      And.casesOn a_1 fun ha hb =>
        have step1 :=
          Logic.PropositionalLogic.Formula.Derivable.ax
            Logic.PropositionalLogic.Formula.Provable.andIntro;
        have step2 :=
          Logic.PropositionalLogic.Formula.Derivable.mp
            (Logic.PropositionalLogic.Formula.Derivable.ax ha)
            (Logic.PropositionalLogic.Formula.Derivable.assumption (List.mem_singleton_self e));
        have step3 := Logic.PropositionalLogic.Formula.Derivable.mp step1 step2;
        have step4 :=
          Logic.PropositionalLogic.Formula.Derivable.mp
            (Logic.PropositionalLogic.Formula.Derivable.ax hb)
            (Logic.PropositionalLogic.Formula.Derivable.assumption (List.mem_singleton_self e));
        have step5 := Logic.PropositionalLogic.Formula.Derivable.mp step3 step4;
        Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
          (Logic.PropositionalLogic.Formula.Derivable.deduction step5) }

Complexity: 660 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.andElim1, Logic.PropositionalLogic.Formula.Provable.andElim2, Logic.PropositionalLogic.Formula.Provable.andIntro, Logic.PropositionalLogic.Formula.SyntacticEntails.trans

Lean core dependencies: And, Iff, List.mem_singleton_self

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.and_entails_left_syntactic

theorem Logic.PropositionalLogic.Formula.and_entails_left_syntactic✝ {α : Type}
  (e x : Logic.PropositionalLogic.Formula α) : (e.and x).SyntacticEntails e

Show details

fun {α} e x => Logic.PropositionalLogic.Formula.Provable.andElim1

Complexity: 17 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Provable.andElim1

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.and_entails_right_syntactic

theorem Logic.PropositionalLogic.Formula.and_entails_right_syntactic✝ {α : Type}
  (e x : Logic.PropositionalLogic.Formula α) : (e.and x).SyntacticEntails x

Show details

fun {α} e x => Logic.PropositionalLogic.Formula.Provable.andElim2

Complexity: 17 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Provable.andElim2

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.or_entails_left_syntactic

theorem Logic.PropositionalLogic.Formula.or_entails_left_syntactic✝ {α : Type}
  (a b : Logic.PropositionalLogic.Formula α) : a.SyntacticEntails (a.or b)

Show details

fun {α} a b => Logic.PropositionalLogic.Formula.Provable.orIntro1

Complexity: 17 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Provable.orIntro1

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.or_entails_right_syntactic

theorem Logic.PropositionalLogic.Formula.or_entails_right_syntactic✝ {α : Type}
  (a b : Logic.PropositionalLogic.Formula α) : b.SyntacticEntails (a.or b)

Show details

fun {α} a b => Logic.PropositionalLogic.Formula.Provable.orIntro2

Complexity: 17 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Provable.orIntro2

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic

theorem Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic✝ {α : Type}
  {e φ : Logic.PropositionalLogic.Formula α} (h1 : e.SyntacticEntails φ)
  (h2 : e.SyntacticEntails φ.neg) (a : Logic.PropositionalLogic.Formula α) : e.SyntacticEntails a

Show details

fun {α} {e φ} h1 h2 a =>
  have d1 :=
    Logic.PropositionalLogic.Formula.Derivable.mp (Logic.PropositionalLogic.Formula.Derivable.ax h1)
      (Logic.PropositionalLogic.Formula.Derivable.assumption (List.mem_singleton_self e));
  have d2 :=
    Logic.PropositionalLogic.Formula.Derivable.mp (Logic.PropositionalLogic.Formula.Derivable.ax h2)
      (Logic.PropositionalLogic.Formula.Derivable.assumption (List.mem_singleton_self e));
  have d3 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.ax
        (Logic.PropositionalLogic.Formula.provable_explosion φ a))
      d1;
  have d4 := Logic.PropositionalLogic.Formula.Derivable.mp d3 d2;
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction d4)

Complexity: 423 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.provable_explosion

Lean core dependencies: List.mem_singleton_self

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.entails_of_and_cases_syntactic

theorem Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic✝ {α : Type}
  {e φ c : Logic.PropositionalLogic.Formula α} (h1 : (e.and φ.neg).SyntacticEntails c)
  (h2 : (e.and φ).SyntacticEntails c) : e.SyntacticEntails c

Show details

fun {α} {e φ c} h1 h2 =>
  have hep :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.andIntro)
        (Logic.PropositionalLogic.Formula.Derivable.assumption
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans
                (congrArg (Or (e = φ))
                  (Eq.trans List.mem_cons._simp_1
                    (Eq.trans (congr (congrArg Or (eq_self e)) List.not_mem_nil._simp_1)
                      (or_false True))))
                (or_true (e = φ)))))))
      (Logic.PropositionalLogic.Formula.Derivable.assumption
        (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 (φ = e)) List.not_mem_nil._simp_1) (or_false (φ = e)))))
              (true_or (φ = e))))));
  have d1 :=
    Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax h2) hep);
  have hen :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.andIntro)
        (Logic.PropositionalLogic.Formula.Derivable.assumption
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans
                (congrArg (Or (e = φ.neg))
                  (Eq.trans List.mem_cons._simp_1
                    (Eq.trans (congr (congrArg Or (eq_self e)) List.not_mem_nil._simp_1)
                      (or_false True))))
                (or_true (e = φ.neg)))))))
      (Logic.PropositionalLogic.Formula.Derivable.assumption
        (of_eq_true
          (Eq.trans List.mem_cons._simp_1
            (Eq.trans
              (congr (congrArg Or (eq_self φ.neg))
                (Eq.trans List.mem_cons._simp_1
                  (Eq.trans (congrArg (Or (φ.neg = e)) List.not_mem_nil._simp_1)
                    (or_false (φ.neg = e)))))
              (true_or (φ.neg = e))))));
  have d2 :=
    Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax h1) hen);
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.case_split d1 d2))

Complexity: 3245 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.case_split, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.andIntro

Lean core dependencies: Eq, Eq.trans, False, List, Or, True, congr, congrArg, eq_self, of_eq_true, or_false, or_true, true_or

Used by: Logic.PropositionalLogic.syntacticConnectives

TipLogic.PropositionalLogic.Formula.entails_of_or_cases_syntactic

theorem Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic✝ {α : Type}
  {e φ ψ c : Logic.PropositionalLogic.Formula α} (hd : e.SyntacticEntails (φ.or ψ))
  (h1 : (e.and φ).SyntacticEntails c) (h2 : (e.and ψ).SyntacticEntails c) : e.SyntacticEntails c

Show details

fun {α} {e φ ψ c} hd h1 h2 =>
  have hep :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.andIntro)
        (Logic.PropositionalLogic.Formula.Derivable.assumption
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans
                (congrArg (Or (e = φ))
                  (Eq.trans List.mem_cons._simp_1
                    (Eq.trans (congr (congrArg Or (eq_self e)) List.not_mem_nil._simp_1)
                      (or_false True))))
                (or_true (e = φ)))))))
      (Logic.PropositionalLogic.Formula.Derivable.assumption
        (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 (φ = e)) List.not_mem_nil._simp_1) (or_false (φ = e)))))
              (true_or (φ = e))))));
  have d1 :=
    Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax h1) hep);
  have heq :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.andIntro)
        (Logic.PropositionalLogic.Formula.Derivable.assumption
          (of_eq_true
            (Eq.trans List.mem_cons._simp_1
              (Eq.trans
                (congrArg (Or (e = ψ))
                  (Eq.trans List.mem_cons._simp_1
                    (Eq.trans (congr (congrArg Or (eq_self e)) List.not_mem_nil._simp_1)
                      (or_false True))))
                (or_true (e = ψ)))))))
      (Logic.PropositionalLogic.Formula.Derivable.assumption
        (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 (ψ = e)) List.not_mem_nil._simp_1) (or_false (ψ = e)))))
              (true_or (ψ = e))))));
  have d2 :=
    Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax h2) heq);
  have d3 :=
    Logic.PropositionalLogic.Formula.Derivable.mp
      (Logic.PropositionalLogic.Formula.Derivable.mp
        (Logic.PropositionalLogic.Formula.Derivable.ax
          Logic.PropositionalLogic.Formula.Provable.orElim)
        d1)
      d2;
  have d4 :=
    Logic.PropositionalLogic.Formula.Derivable.mp (Logic.PropositionalLogic.Formula.Derivable.ax hd)
      (Logic.PropositionalLogic.Formula.Derivable.assumption (List.mem_singleton_self e));
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.Derivable.deduction
      (Logic.PropositionalLogic.Formula.Derivable.mp d3 d4))

Complexity: 3321 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SyntacticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.Provable.andIntro, Logic.PropositionalLogic.Formula.Provable.orElim

Lean core dependencies: Eq, Eq.trans, False, List, List.mem_singleton_self, Or, True, congr, congrArg, eq_self, of_eq_true, or_false, or_true, true_or

Used by: Logic.PropositionalLogic.syntacticConnectives

ImportantLogic.PropositionalLogic.syntacticConnectives

Propositional formulas over \(\alpha\), with syntactic entailment as the deducibility relation, form a Popper.Basis3.HasClassicalConnectives: conjunction, disjunction, and negation satisfy Popper’s characterizing properties for a conjunction, a disjunction, and a classical negation, all under syntactic entailment. Every downstream fact about folding premise or conclusion lists (PropositionalLogic.Formula.derive_bigAnd_cons and friends) applies to this instance without further proof, exactly because it is one.

instance Logic.PropositionalLogic.syntacticConnectives (α : Type) :
  Logic.Popper.Basis1.HasClassicalConnectives (Logic.PropositionalLogic.Formula α)
    (Logic.PropositionalLogic.syntacticBasis3 α).toBasis1

Show details

| Logic.PropositionalLogic.syntacticConnectives α =
  { and := Logic.PropositionalLogic.Formula.and, and_isConjunction := ⋯,
    or := Logic.PropositionalLogic.Formula.or, or_isDisjunction := ⋯,
    neg := Logic.PropositionalLogic.Formula.neg, neg_isClassicalNegation := ⋯ }

Complexity: 7806 (size of the value term)

Outer dependencies: Logic.Popper.Basis1.HasClassicalConnectives, Logic.Popper.Basis3.toBasis1, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.syntacticBasis3

Inner dependencies: Logic.Popper.Basis1.Demonstrate, Logic.PropositionalLogic.Formula.SyntacticEntails, Logic.PropositionalLogic.Formula.SyntacticEntails.trans, Logic.PropositionalLogic.Formula.and_entails_left_syntactic, Logic.PropositionalLogic.Formula.and_entails_right_syntactic, Logic.PropositionalLogic.Formula.entails_and_iff_syntactic, Logic.PropositionalLogic.Formula.entails_of_and_cases_syntactic, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra_syntactic, Logic.PropositionalLogic.Formula.entails_of_or_cases_syntactic, Logic.PropositionalLogic.Formula.or_entails_left_syntactic, Logic.PropositionalLogic.Formula.or_entails_right_syntactic, instToSeq, instToSeqList

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, Iff, List, List.append, List.mem_cons, List.mem_cons_self, List.mem_singleton, List.mem_singleton_self, Or, True, congr, congrArg, eq_self, id, of_eq_true, or_false, or_true, true_or

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

Semantics

NoteLogic.PropositionalLogic.Formula.SemanticEntails

Semantic entailment: every valuation making \(\varphi\) true also makes \(\psi\) true.

def Logic.PropositionalLogic.Formula.SemanticEntails {α : Type}
  (φ ψ : Logic.PropositionalLogic.Formula α) : Prop

Show details

| φ.SemanticEntails ψ =
  ∀ (v : Logic.PropositionalLogic.Valuation α),
    Logic.PropositionalLogic.Formula.val v φ = true →
      Logic.PropositionalLogic.Formula.val v ψ = true

Complexity: 41 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula

Inner dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Eq

Used by: Logic.PropositionalLogic.Formula.SemanticEntails.refl, Logic.PropositionalLogic.Formula.SemanticEntails.trans, Logic.PropositionalLogic.Formula.and_entails_left, Logic.PropositionalLogic.Formula.and_entails_right, Logic.PropositionalLogic.Formula.entails_and_iff, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra, Logic.PropositionalLogic.Formula.or_entails_left, Logic.PropositionalLogic.Formula.or_entails_right, Logic.PropositionalLogic.semanticBasis3, Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.SemanticEntails.refl

Reflexivity of semantic entailment: immediate from the definition.

theorem Logic.PropositionalLogic.Formula.SemanticEntails.refl {α : Type}
  (φ : Logic.PropositionalLogic.Formula α) : φ.SemanticEntails φ

Show details

fun {α} φ x h => h

Complexity: 25 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Eq

Used by: Logic.PropositionalLogic.semanticBasis3

TipLogic.PropositionalLogic.Formula.SemanticEntails.trans

Transitivity of semantic entailment: immediate from the definition.

theorem Logic.PropositionalLogic.Formula.SemanticEntails.trans {α : Type}
  {φ ψ χ : Logic.PropositionalLogic.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: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Eq

Used by: Logic.PropositionalLogic.semanticBasis3, Logic.PropositionalLogic.semanticConnectives

ImportantLogic.PropositionalLogic.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.

instance Logic.PropositionalLogic.semanticBasis3 (α : Type) :
  Logic.Popper.Basis3 (Logic.PropositionalLogic.Formula α)

Show details

| Logic.PropositionalLogic.semanticBasis3 α =
  { Follows := Logic.PropositionalLogic.Formula.SemanticEntails, refl := ⋯, trans := ⋯ }

Complexity: 37 (size of the value term)

Outer dependencies: Logic.Popper.Basis3, Logic.PropositionalLogic.Formula

Inner dependencies: Logic.PropositionalLogic.Formula.SemanticEntails, Logic.PropositionalLogic.Formula.SemanticEntails.refl, Logic.PropositionalLogic.Formula.SemanticEntails.trans

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.entails_and_iff

theorem Logic.PropositionalLogic.Formula.entails_and_iff✝ {α : Type}
  (e a b : Logic.PropositionalLogic.Formula α) :
  e.SemanticEntails (a.and b) ↔ e.SemanticEntails a ∧ e.SemanticEntails b

Show details

fun {α} e a b =>
  id
    {
      mp := fun h =>
        ⟨fun v hv =>
          (Bool.and_eq_true_iff.mp
              (Eq.mpr
                (id
                  (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v a)
                    (Logic.PropositionalLogic.Formula.val v b)))
                (Eq.mp
                  (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v a)
                    (Logic.PropositionalLogic.Formula.val v b))
                  (h v hv)))).left,
          fun v hv =>
          (Bool.and_eq_true_iff.mp
              (Eq.mpr
                (id
                  (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v a)
                    (Logic.PropositionalLogic.Formula.val v b)))
                (Eq.mp
                  (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v a)
                    (Logic.PropositionalLogic.Formula.val v b))
                  (h v hv)))).right⟩,
      mpr := fun a_1 =>
        And.casesOn (motive := fun x =>
          ∀ (v : Logic.PropositionalLogic.Valuation α),
            Logic.PropositionalLogic.Formula.val v e = true →
              Logic.PropositionalLogic.Formula.val v (a.and b) = true)
          a_1 fun ha hb v hv =>
          Eq.mpr
            (id
              (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v a)
                (Logic.PropositionalLogic.Formula.val v b)))
            (Eq.mp
              (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v a)
                (Logic.PropositionalLogic.Formula.val v b))
              (Bool.and_eq_true_iff.mpr ⟨ha v hv, hb v hv⟩)) }

Complexity: 1559 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: And, Bool, Bool.and, Bool.and_eq_true, Bool.and_eq_true_iff, Eq, Eq.mp, Eq.mpr, Iff, id

Used by: Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.and_entails_left

theorem Logic.PropositionalLogic.Formula.and_entails_left✝ {α : Type}
  (e x : Logic.PropositionalLogic.Formula α) : (e.and x).SemanticEntails e

Show details

fun {α} e x v hv =>
  (Bool.and_eq_true_iff.mp
      (Eq.mpr
        (id
          (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v e)
            (Logic.PropositionalLogic.Formula.val v x)))
        (Eq.mp
          (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v e)
            (Logic.PropositionalLogic.Formula.val v x))
          hv))).left

Complexity: 343 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: And, Bool, Bool.and, Bool.and_eq_true, Bool.and_eq_true_iff, Eq, Eq.mp, Eq.mpr, id

Used by: Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.and_entails_right

theorem Logic.PropositionalLogic.Formula.and_entails_right✝ {α : Type}
  (e x : Logic.PropositionalLogic.Formula α) : (e.and x).SemanticEntails x

Show details

fun {α} e x v hv =>
  (Bool.and_eq_true_iff.mp
      (Eq.mpr
        (id
          (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v e)
            (Logic.PropositionalLogic.Formula.val v x)))
        (Eq.mp
          (Bool.and_eq_true (Logic.PropositionalLogic.Formula.val v e)
            (Logic.PropositionalLogic.Formula.val v x))
          hv))).right

Complexity: 343 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: And, Bool, Bool.and, Bool.and_eq_true, Bool.and_eq_true_iff, Eq, Eq.mp, Eq.mpr, id

Used by: Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.or_entails_left

theorem Logic.PropositionalLogic.Formula.or_entails_left✝ {α : Type}
  (a b : Logic.PropositionalLogic.Formula α) : a.SemanticEntails (a.or b)

Show details

fun {α} a b v hv =>
  of_eq_true
    (Eq.trans
      (congrFun'
        (congrArg Eq
          (Eq.trans (congrFun' (congrArg or hv) (Logic.PropositionalLogic.Formula.val v b))
            (Bool.true_or (Logic.PropositionalLogic.Formula.val v b))))
        true)
      (eq_self true))

Complexity: 245 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.or, Bool.true_or, Eq, Eq.trans, True, congrArg, congrFun', eq_self, of_eq_true

Used by: Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.or_entails_right

theorem Logic.PropositionalLogic.Formula.or_entails_right✝ {α : Type}
  (a b : Logic.PropositionalLogic.Formula α) : b.SemanticEntails (a.or b)

Show details

fun {α} a b v hv =>
  of_eq_true
    (Eq.trans
      (congrFun'
        (congrArg Eq
          (Eq.trans (congrArg (Logic.PropositionalLogic.Formula.val v a).or hv)
            (Bool.or_true (Logic.PropositionalLogic.Formula.val v a))))
        true)
      (eq_self true))

Complexity: 223 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.or, Bool.or_true, Eq, Eq.trans, True, congrArg, congrFun', eq_self, of_eq_true

Used by: Logic.PropositionalLogic.semanticConnectives

TipLogic.PropositionalLogic.Formula.entails_of_entails_neg_contra

theorem Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra✝ {α : Type}
  {e φ : Logic.PropositionalLogic.Formula α} (h1 : e.SemanticEntails φ)
  (h2 : e.SemanticEntails φ.neg) (a : Logic.PropositionalLogic.Formula α) : e.SemanticEntails a

Show details

fun {α} {e φ} h1 h2 a v hv =>
  have hφv := h1 v hv;
  have hnφv := h2 v hv;
  absurd (Eq.mp (congrFun' (congrArg Eq (Eq.trans (congrArg not hφv) Bool.not_true)) true) hnφv)
    (of_decide_eq_true (id (Eq.refl true)))

Complexity: 315 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.SemanticEntails

Proof dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.not, Bool.not_true, Decidable.decide, Eq, Eq.mp, Eq.trans, Not, absurd, congrArg, congrFun', id, of_decide_eq_true

Used by: Logic.PropositionalLogic.semanticConnectives

ImportantLogic.PropositionalLogic.semanticConnectives

Propositional formulas over \(\alpha\), with semantic entailment as the deducibility relation, form a Popper.Basis3.HasClassicalConnectives: conjunction, disjunction, and negation satisfy Popper’s characterizing properties for a conjunction, a disjunction, and a classical negation, all under semantic entailment. Every downstream fact about folding premise or conclusion lists (PropositionalLogic.Formula.derive_bigAnd_cons and friends) applies to this instance without further proof, exactly because it is one.

instance Logic.PropositionalLogic.semanticConnectives (α : Type) :
  Logic.Popper.Basis1.HasClassicalConnectives (Logic.PropositionalLogic.Formula α)
    (Logic.PropositionalLogic.semanticBasis3 α).toBasis1

Show details

| Logic.PropositionalLogic.semanticConnectives α =
  { and := Logic.PropositionalLogic.Formula.and, and_isConjunction := ⋯,
    or := Logic.PropositionalLogic.Formula.or, or_isDisjunction := ⋯,
    neg := Logic.PropositionalLogic.Formula.neg, neg_isClassicalNegation := ⋯ }

Complexity: 3117 (size of the value term)

Outer dependencies: Logic.Popper.Basis1.HasClassicalConnectives, Logic.Popper.Basis3.toBasis1, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.semanticBasis3

Inner dependencies: Logic.Popper.Basis1.Demonstrate, Logic.PropositionalLogic.Formula.SemanticEntails, Logic.PropositionalLogic.Formula.SemanticEntails.trans, Logic.PropositionalLogic.Formula.and_entails_left, Logic.PropositionalLogic.Formula.and_entails_right, Logic.PropositionalLogic.Formula.entails_and_iff, Logic.PropositionalLogic.Formula.entails_of_entails_neg_contra, Logic.PropositionalLogic.Formula.or_entails_left, Logic.PropositionalLogic.Formula.or_entails_right, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation, instToSeq, instToSeqList

Lean core dependencies: And, Bool, Bool.and, Bool.and_self, Bool.not, Bool.not_false, Bool.or, Bool.or_eq_true, Bool.or_eq_true_iff, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, False, Iff, 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: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

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.

definitionlemmatheoremdeclared elsewheredependencyproof dependency

legend