Completeness

Difficulty: hard — 1 definitions, 0 abbreviations, 7 lemmas, 1 theorems, 0 examples.

definition lemma theorem
legend

Completeness. Every tautology is provable in our Hilbert system, the converse of soundness (PropositionalLogic.Formula.soundness). The classical argument, due to Kalmár: first show that for any formula and any valuation, the literals matching that valuation prove the formula outright if it is true there, and prove its negation if it is false there (PropositionalLogic.Formula.kalmar below); then, given that this holds for every valuation of a tautology, eliminate the literals one at a time by case-splitting on each variable (PropositionalLogic.Formula.eliminate below), leaving the tautology itself provable from no hypotheses at all.

The formula \(\varphi\) itself if \(v\) makes it true, its negation otherwise.

def Logic.PropositionalLogic.Formula.starred {n : ℕ}
  (v : Logic.PropositionalLogic.Valuation (Fin (n + 1)))
  (φ : Logic.PropositionalLogic.Formula (Fin (n + 1))) :
  Logic.PropositionalLogic.Formula (Fin (n + 1))
Show details 
| Logic.PropositionalLogic.Formula.starred v φ =
  if Logic.PropositionalLogic.Formula.val v φ = true then φ else φ.neg

Complexity: 205 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Valuation

Inner dependencies: Logic.PropositionalLogic.Formula.val

Lean core dependencies: Bool, Eq, Fin, Nat, ite

Used by: Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.kalmar

Kalmár’s Lemma. Under a valuation, the literals for every atom together derive a formula if that valuation makes it true, and derive its negation otherwise.

theorem Logic.PropositionalLogic.Formula.kalmar {n : ℕ}
  (v : Logic.PropositionalLogic.Valuation (Fin (n + 1)))
  (φ : Logic.PropositionalLogic.Formula (Fin (n + 1))) :
  Logic.PropositionalLogic.Formula.Derivable
    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1)))
    (Logic.PropositionalLogic.Formula.starred v φ)
Show details 
fun {n} v φ =>
  Logic.PropositionalLogic.Formula.rec
    (fun a =>
      id
        (id
          (Bool.casesOn (motive := fun x =>
            v a = x →
              Logic.PropositionalLogic.Formula.Derivable
                (List.map
                  (fun i =>
                    if v i = true then Logic.PropositionalLogic.Formula.atom i
                    else (Logic.PropositionalLogic.Formula.atom i).neg)
                  (List.finRange (n + 1)))
                (if
                    Logic.PropositionalLogic.Formula.val v
                        (Logic.PropositionalLogic.Formula.atom a) =
                      true then
                  Logic.PropositionalLogic.Formula.atom a
                else (Logic.PropositionalLogic.Formula.atom a).neg))
            (v a)
            (fun hv =>
              Logic.PropositionalLogic.Formula.Derivable.assumption
                (List.mem_map.mpr
                  (Exists.intro a
                    ⟨List.mem_finRange a,
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (ite_cond_eq_false (Logic.PropositionalLogic.Formula.atom a)
                                (Logic.PropositionalLogic.Formula.atom a).neg
                                (Eq.trans (congrFun' (congrArg Eq hv) true) Bool.false_eq_true)))
                            (ite_cond_eq_false (Logic.PropositionalLogic.Formula.atom a)
                              (Logic.PropositionalLogic.Formula.atom a).neg
                              (Eq.trans (congrFun' (congrArg Eq hv) true) Bool.false_eq_true)))
                          (eq_self (Logic.PropositionalLogic.Formula.atom a).neg))⟩)))
            (fun hv =>
              Logic.PropositionalLogic.Formula.Derivable.assumption
                (List.mem_map.mpr
                  (Exists.intro a
                    ⟨List.mem_finRange a,
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (ite_cond_eq_true (Logic.PropositionalLogic.Formula.atom a)
                                (Logic.PropositionalLogic.Formula.atom a).neg
                                (Eq.trans (congrFun' (congrArg Eq hv) true) (eq_self true))))
                            (ite_cond_eq_true (Logic.PropositionalLogic.Formula.atom a)
                              (Logic.PropositionalLogic.Formula.atom a).neg
                              (Eq.trans (congrFun' (congrArg Eq hv) true) (eq_self true))))
                          (eq_self (Logic.PropositionalLogic.Formula.atom a)))⟩)))
            (Eq.refl (v a)))))
    (fun φ ihφ =>
      id
        (if hφ : Logic.PropositionalLogic.Formula.val v φ = true then
          Eq.mpr
            (id
              (congrArg
                (Logic.PropositionalLogic.Formula.Derivable
                  (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                (ite_congr (congrFun' (congrArg Eq (Eq.trans (congrArg not hφ) Bool.not_true)) true)
                  (fun a => Eq.refl φ.neg) fun a => Eq.refl φ.neg.neg)))
            (Logic.PropositionalLogic.Formula.Derivable.mp
              (Logic.PropositionalLogic.Formula.Derivable.ax
                (Logic.PropositionalLogic.Formula.provable_dni φ))
              (Eq.mp
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true))
                      (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)
                    (if_true φ φ.neg)))
                ihφ))
        else
          Eq.mpr
            (id
              (congrArg
                (Logic.PropositionalLogic.Formula.Derivable
                  (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                (Eq.trans
                  (ite_congr
                    (Eq.trans
                      (congrFun'
                        (congrArg Eq
                          (Eq.trans (congrArg not (Bool.of_not_eq_true hφ)) Bool.not_false))
                        true)
                      (eq_self true))
                    (fun a => Eq.refl φ.neg) fun a => Eq.refl φ.neg.neg)
                  (if_true φ.neg φ.neg.neg))))
            (Eq.mp
              (congrArg
                (Logic.PropositionalLogic.Formula.Derivable
                  (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true)
                  (fun a => Eq.refl φ) fun a => Eq.refl φ.neg))
              ihφ)))
    (fun φ ψ ihφ ihψ =>
      id
        (if hφ : Logic.PropositionalLogic.Formula.val v φ = true then
          if hψ : Logic.PropositionalLogic.Formula.val v ψ = true then
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq (Eq.trans (congr (congrArg and hφ) hψ) (Bool.true_and true)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg)
                    (if_true (φ.and ψ) (φ.and ψ).neg))))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.ax
                    Logic.PropositionalLogic.Formula.Provable.andIntro)
                  (Eq.mp
                    (congrArg
                      (Logic.PropositionalLogic.Formula.Derivable
                        (List.map (Logic.PropositionalLogic.Formula.literal v)
                          (List.finRange (n + 1))))
                      (Eq.trans
                        (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true))
                          (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)
                        (if_true φ φ.neg)))
                    ihφ))
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.trans
                      (ite_congr (Eq.trans (congrFun' (congrArg Eq hψ) true) (eq_self true))
                        (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg)
                      (if_true ψ ψ.neg)))
                  ihψ))
          else
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (ite_congr
                    (congrFun'
                      (congrArg Eq
                        (Eq.trans (congr (congrArg and hφ) (Bool.of_not_eq_true hψ))
                          (Bool.and_false true)))
                      true)
                    (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg)))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  (Logic.PropositionalLogic.Formula.provable_contrapose
                    Logic.PropositionalLogic.Formula.Provable.andElim2))
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hψ)) true)
                      (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg))
                  ihψ))
        else
          if hψ : Logic.PropositionalLogic.Formula.val v ψ = true then
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (ite_congr
                    (congrFun'
                      (congrArg Eq
                        (Eq.trans (congr (congrArg and (Bool.of_not_eq_true hφ)) hψ)
                          (Bool.false_and true)))
                      true)
                    (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg)))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  (Logic.PropositionalLogic.Formula.provable_contrapose
                    Logic.PropositionalLogic.Formula.Provable.andElim1))
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true)
                      (fun a => Eq.refl φ) fun a => Eq.refl φ.neg))
                  ihφ))
          else
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (ite_congr
                    (congrFun'
                      (congrArg Eq
                        (Eq.trans
                          (congr (congrArg and (Bool.of_not_eq_true hφ)) (Bool.of_not_eq_true hψ))
                          (Bool.false_and false)))
                      true)
                    (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg)))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  (Logic.PropositionalLogic.Formula.provable_contrapose
                    Logic.PropositionalLogic.Formula.Provable.andElim1))
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true)
                      (fun a => Eq.refl φ) fun a => Eq.refl φ.neg))
                  ihφ))))
    (fun φ ψ ihφ ihψ =>
      id
        (if hφ : Logic.PropositionalLogic.Formula.val v φ = true then
          if hψ : Logic.PropositionalLogic.Formula.val v ψ = true then
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq (Eq.trans (congr (congrArg or hφ) hψ) (Bool.true_or true)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg)
                    (if_true (φ.or ψ) (φ.or ψ).neg))))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  Logic.PropositionalLogic.Formula.Provable.orIntro1)
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.trans
                      (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true))
                        (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)
                      (if_true φ φ.neg)))
                  ihφ))
          else
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq
                            (Eq.trans (congr (congrArg or hφ) (Bool.of_not_eq_true hψ))
                              (Bool.true_or false)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg)
                    (if_true (φ.or ψ) (φ.or ψ).neg))))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  Logic.PropositionalLogic.Formula.Provable.orIntro1)
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.trans
                      (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true))
                        (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)
                      (if_true φ φ.neg)))
                  ihφ))
        else
          if hψ : Logic.PropositionalLogic.Formula.val v ψ = true then
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq
                            (Eq.trans (congr (congrArg or (Bool.of_not_eq_true hφ)) hψ)
                              (Bool.or_true false)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg)
                    (if_true (φ.or ψ) (φ.or ψ).neg))))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  Logic.PropositionalLogic.Formula.Provable.orIntro2)
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.trans
                      (ite_congr (Eq.trans (congrFun' (congrArg Eq hψ) true) (eq_self true))
                        (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg)
                      (if_true ψ ψ.neg)))
                  ihψ))
          else
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (ite_congr
                    (congrFun'
                      (congrArg Eq
                        (Eq.trans
                          (congr (congrArg or (Bool.of_not_eq_true hφ)) (Bool.of_not_eq_true hψ))
                          (Bool.or_false false)))
                      true)
                    (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg)))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.ax
                    (Logic.PropositionalLogic.Formula.provable_deMorgan_or φ ψ))
                  (Eq.mp
                    (congrArg
                      (Logic.PropositionalLogic.Formula.Derivable
                        (List.map (Logic.PropositionalLogic.Formula.literal v)
                          (List.finRange (n + 1))))
                      (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true)
                        (fun a => Eq.refl φ) fun a => Eq.refl φ.neg))
                    ihφ))
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hψ)) true)
                      (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg))
                  ihψ))))
    (fun φ ψ ihφ ihψ =>
      id
        (if hφ : Logic.PropositionalLogic.Formula.val v φ = true then
          if hψ : Logic.PropositionalLogic.Formula.val v ψ = true then
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq
                            (Eq.trans
                              (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_true)) hψ)
                              (Bool.false_or true)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg)
                    (if_true (φ.imp ψ) (φ.imp ψ).neg))))
              (Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.ax
                  Logic.PropositionalLogic.Formula.Provable.k)
                (Eq.mp
                  (congrArg
                    (Logic.PropositionalLogic.Formula.Derivable
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.trans
                      (ite_congr (Eq.trans (congrFun' (congrArg Eq hψ) true) (eq_self true))
                        (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg)
                      (if_true ψ ψ.neg)))
                  ihψ))
          else
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (ite_congr
                    (congrFun'
                      (congrArg Eq
                        (Eq.trans
                          (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_true))
                            (Bool.of_not_eq_true hψ))
                          (Bool.false_or false)))
                      true)
                    (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg)))
              (have h1 :=
                Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.assumption
                    (of_eq_true
                      (Eq.trans List.mem_cons._simp_1
                        (Eq.trans
                          (congr (congrArg Or (eq_self (φ.imp ψ)))
                            (Eq.trans List.mem_map._simp_1
                              (congrArg Exists
                                (funext fun a =>
                                  Eq.trans
                                    (congrFun' (congrArg And (List.mem_finRange._simp_1 a))
                                      (Logic.PropositionalLogic.Formula.literal v a = φ.imp ψ))
                                    (true_and
                                      (Logic.PropositionalLogic.Formula.literal v a = φ.imp ψ))))))
                          (true_or
                            (∃ a, Logic.PropositionalLogic.Formula.literal v a = φ.imp ψ))))))
                  (Logic.PropositionalLogic.Formula.Derivable.weaken
                    (List.subset_cons_self (φ.imp ψ)
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.mp
                      (congrArg
                        (Logic.PropositionalLogic.Formula.Derivable
                          (List.map (Logic.PropositionalLogic.Formula.literal v)
                            (List.finRange (n + 1))))
                        (Eq.trans
                          (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true))
                            (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)
                          (if_true φ φ.neg)))
                      ihφ));
              have h1d := Logic.PropositionalLogic.Formula.Derivable.deduction h1;
              have h2d :=
                Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.ax
                    Logic.PropositionalLogic.Formula.Provable.k)
                  (Eq.mp
                    (congrArg
                      (Logic.PropositionalLogic.Formula.Derivable
                        (List.map (Logic.PropositionalLogic.Formula.literal v)
                          (List.finRange (n + 1))))
                      (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hψ)) true)
                        (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg))
                    ihψ);
              Logic.PropositionalLogic.Formula.Derivable.mp
                (Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.ax
                    Logic.PropositionalLogic.Formula.Provable.negIntro)
                  h1d)
                h2d)
        else
          if hψ : Logic.PropositionalLogic.Formula.val v ψ = true then
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq
                            (Eq.trans
                              (congr
                                (congrArg or
                                  (Eq.trans (congrArg not (Bool.of_not_eq_true hφ)) Bool.not_false))
                                hψ)
                              (Bool.true_or true)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg)
                    (if_true (φ.imp ψ) (φ.imp ψ).neg))))
              (have h :=
                Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.mp
                    (Logic.PropositionalLogic.Formula.Derivable.ax
                      (Logic.PropositionalLogic.Formula.provable_explosion φ ψ))
                    (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_map._simp_1
                                (congrArg Exists
                                  (funext fun a =>
                                    Eq.trans
                                      (congrFun' (congrArg And (List.mem_finRange._simp_1 a))
                                        (Logic.PropositionalLogic.Formula.literal v a = φ))
                                      (true_and
                                        (Logic.PropositionalLogic.Formula.literal v a = φ))))))
                            (true_or (∃ a, Logic.PropositionalLogic.Formula.literal v a = φ)))))))
                  (Logic.PropositionalLogic.Formula.Derivable.weaken
                    (List.subset_cons_self φ
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.mp
                      (congrArg
                        (Logic.PropositionalLogic.Formula.Derivable
                          (List.map (Logic.PropositionalLogic.Formula.literal v)
                            (List.finRange (n + 1))))
                        (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true)
                          (fun a => Eq.refl φ) fun a => Eq.refl φ.neg))
                      ihφ));
              Logic.PropositionalLogic.Formula.Derivable.deduction h)
          else
            Eq.mpr
              (id
                (congrArg
                  (Logic.PropositionalLogic.Formula.Derivable
                    (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))))
                  (Eq.trans
                    (ite_congr
                      (Eq.trans
                        (congrFun'
                          (congrArg Eq
                            (Eq.trans
                              (congr
                                (congrArg or
                                  (Eq.trans (congrArg not (Bool.of_not_eq_true hφ)) Bool.not_false))
                                (Bool.of_not_eq_true hψ))
                              (Bool.true_or false)))
                          true)
                        (eq_self true))
                      (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg)
                    (if_true (φ.imp ψ) (φ.imp ψ).neg))))
              (have h :=
                Logic.PropositionalLogic.Formula.Derivable.mp
                  (Logic.PropositionalLogic.Formula.Derivable.mp
                    (Logic.PropositionalLogic.Formula.Derivable.ax
                      (Logic.PropositionalLogic.Formula.provable_explosion φ ψ))
                    (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_map._simp_1
                                (congrArg Exists
                                  (funext fun a =>
                                    Eq.trans
                                      (congrFun' (congrArg And (List.mem_finRange._simp_1 a))
                                        (Logic.PropositionalLogic.Formula.literal v a = φ))
                                      (true_and
                                        (Logic.PropositionalLogic.Formula.literal v a = φ))))))
                            (true_or (∃ a, Logic.PropositionalLogic.Formula.literal v a = φ)))))))
                  (Logic.PropositionalLogic.Formula.Derivable.weaken
                    (List.subset_cons_self φ
                      (List.map (Logic.PropositionalLogic.Formula.literal v)
                        (List.finRange (n + 1))))
                    (Eq.mp
                      (congrArg
                        (Logic.PropositionalLogic.Formula.Derivable
                          (List.map (Logic.PropositionalLogic.Formula.literal v)
                            (List.finRange (n + 1))))
                        (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true)
                          (fun a => Eq.refl φ) fun a => Eq.refl φ.neg))
                      ihφ));
              Logic.PropositionalLogic.Formula.Derivable.deduction h)))
    φ

Complexity: 112678 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.literal, Logic.PropositionalLogic.Formula.starred, Logic.PropositionalLogic.Valuation

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.ax, Logic.PropositionalLogic.Formula.Derivable.deduction, Logic.PropositionalLogic.Formula.Derivable.weaken, Logic.PropositionalLogic.Formula.Provable.andElim1, Logic.PropositionalLogic.Formula.Provable.andElim2, Logic.PropositionalLogic.Formula.Provable.andIntro, Logic.PropositionalLogic.Formula.Provable.k, Logic.PropositionalLogic.Formula.Provable.negIntro, Logic.PropositionalLogic.Formula.Provable.orIntro1, Logic.PropositionalLogic.Formula.Provable.orIntro2, Logic.PropositionalLogic.Formula.provable_contrapose, Logic.PropositionalLogic.Formula.provable_deMorgan_or, Logic.PropositionalLogic.Formula.provable_dni, Logic.PropositionalLogic.Formula.provable_explosion, Logic.PropositionalLogic.Formula.val

Lean core dependencies: And, Bool, Bool.and, Bool.and_false, Bool.false_and, Bool.false_eq_true, Bool.false_or, Bool.not, Bool.not_false, Bool.not_true, Bool.of_not_eq_true, Bool.or, Bool.or_false, Bool.or_true, Bool.true_and, Bool.true_or, Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, False, Fin, List, List.finRange, List.map, List.mem_finRange, List.mem_map, List.subset_cons_self, Nat, Not, Or, True, congr, congrArg, congrFun', dite, eq_self, funext, id, if_true, ite, ite_cond_eq_false, ite_cond_eq_true, ite_congr, of_eq_true, true_and, true_or

Used by: Logic.PropositionalLogic.Formula.completeness

Variable elimination. If some formula is derivable from the literals of every valuation restricted to a list of atoms, then it is provable outright, no hypotheses needed — by peeling one atom off the list at a time, case-splitting between the two valuations that agree except at that atom.

theorem Logic.PropositionalLogic.Formula.eliminate {n : ℕ}
  {χ : Logic.PropositionalLogic.Formula (Fin (n + 1))} (L : List (Fin (n + 1))) :
  L.Nodup →
    (∀ (v : Logic.PropositionalLogic.Valuation (Fin (n + 1))),
        Logic.PropositionalLogic.Formula.Derivable
          (List.map (Logic.PropositionalLogic.Formula.literal v) L) χ) →
      Logic.PropositionalLogic.Formula.Derivable [] χ
Show details 
fun {n} {χ} x x_1 x_2 =>
  List.brecOn (motive := fun x =>
    x.Nodup →
      (∀ (v : Logic.PropositionalLogic.Valuation (Fin (n + 1))),
          Logic.PropositionalLogic.Formula.Derivable
            (List.map (Logic.PropositionalLogic.Formula.literal v) x) χ) →
        Logic.PropositionalLogic.Formula.Derivable [] χ)
    x Logic.PropositionalLogic.Formula.eliminate._f x_1 x_2

Complexity: 521 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.literal, Logic.PropositionalLogic.Valuation

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable.case_split, Logic.PropositionalLogic.Formula.Derivable.deduction

Mathlib dependencies: Function.update, Function.update_congr, Function.update_of_ne, Function.update_self

Lean core dependencies: And, Bool, Bool.false_eq_true, Bool.not, Bool.not_false, Bool.not_true, Eq, Eq.mp, Eq.trans, False, Fin, List, List.Nodup, List.map, List.map_congr_left, List.nodup_cons, Nat, Ne, Not, True, congrArg, congrFun', eq_self, ite, ite_cond_eq_false, ite_cond_eq_true, ite_congr, of_eq_true

Used by: Logic.PropositionalLogic.Formula.completeness

Completeness. Every tautology is provable — the converse of PropositionalLogic.Formula.soundness.

theorem Logic.PropositionalLogic.Formula.completeness {n : ℕ}
  {φ : Logic.PropositionalLogic.Formula (Fin (n + 1))} (h : φ.Tautology) : φ.Provable
Show details 
fun {n} {φ} h =>
  Logic.PropositionalLogic.Formula.Derivable.provable_of_nil
    (Logic.PropositionalLogic.Formula.eliminate (List.finRange (n + 1))
      (List.nodup_finRange (n + 1)) fun v =>
      have this := Logic.PropositionalLogic.Formula.kalmar v φ;
      Eq.mp
        (congrArg
          (fun _a =>
            Logic.PropositionalLogic.Formula.Derivable
              (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1))) _a)
          (if_pos rfl))
        (Eq.mp
          (congrArg
            (fun _a =>
              Logic.PropositionalLogic.Formula.Derivable
                (List.map (Logic.PropositionalLogic.Formula.literal v) (List.finRange (n + 1)))
                (if _a = true then φ else φ.neg))
            (h v))
          this))

Complexity: 1744 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable, Logic.PropositionalLogic.Formula.Tautology

Proof dependencies: Logic.PropositionalLogic.Formula.Derivable, Logic.PropositionalLogic.Formula.Derivable.provable_of_nil, Logic.PropositionalLogic.Formula.eliminate, Logic.PropositionalLogic.Formula.kalmar, Logic.PropositionalLogic.Formula.literal, Logic.PropositionalLogic.Formula.starred, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Eq, Eq.mp, Fin, List.finRange, List.map, Nat, congrArg, if_pos, ite, rfl

Used by: Logic.PropositionalLogic.Formula.semantic_iff_provable

Demonstrability for the semantic Basis III instance, between a single premise and a single conclusion, is provability of the implication: the interesting half, where soundness and completeness together turn the semantic fact PropositionalLogic.Formula.SemanticEntails into a purely proof-theoretic one. A private stepping stone towards PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic below, which generalises this from one premise and one conclusion to arbitrary finite lists of each.

theorem Logic.PropositionalLogic.Formula.semantic_iff_provable✝ {n : ℕ}
  {φ ψ : Logic.PropositionalLogic.Formula (Fin (n + 1))} :
  (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1.Demonstrate ⟪φ⟫ ⟪ψ⟫ ↔
    (φ.imp ψ).Provable
Show details 
fun {n} {φ ψ} =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a ↔ (φ.imp ψ).Provable)
        (propext
          (Logic.Popper.Basis1.demonstrate_singleton
            (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1))))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a ↔ (φ.imp ψ).Provable)
          (propext
            (Logic.Popper.Basis3.follows_toBasis1
              (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))) φ ψ))))
      {
        mp := fun h =>
          Logic.PropositionalLogic.Formula.completeness fun v =>
            if hv : Logic.PropositionalLogic.Formula.val v φ = true then
              of_eq_true
                (Eq.trans
                  (congrFun'
                    (congrArg Eq
                      (Eq.trans
                        (congr (congrArg or (Eq.trans (congrArg not hv) Bool.not_true)) (h v hv))
                        (Bool.or_true false)))
                    true)
                  (eq_self true))
            else
              of_eq_true
                (Eq.trans
                  (congrFun'
                    (congrArg Eq
                      (Eq.trans
                        (congrFun'
                          (congrArg or
                            (Eq.trans (congrArg not (Bool.of_not_eq_true hv)) Bool.not_false))
                          (Logic.PropositionalLogic.Formula.val v ψ))
                        (Bool.true_or (Logic.PropositionalLogic.Formula.val v ψ))))
                    true)
                  (eq_self true)),
        mpr := fun h v hv =>
          have this := Logic.PropositionalLogic.Formula.soundness h v;
          Eq.mp
            (congrFun'
              (congrArg Eq
                (Eq.trans
                  (congrFun' (congrArg or (Eq.trans (congrArg not hv) Bool.not_true))
                    (Logic.PropositionalLogic.Formula.val v ψ))
                  (Bool.false_or (Logic.PropositionalLogic.Formula.val v ψ))))
              true)
            this })

Complexity: 6034 (size of the value term)

Dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis3.toBasis1, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable, Logic.PropositionalLogic.semanticBasis3, instToSeq

Proof dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_singleton, Logic.Popper.Basis3.follows_toBasis1, Logic.PropositionalLogic.Formula.completeness, Logic.PropositionalLogic.Formula.soundness, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.false_or, Bool.not, Bool.not_false, Bool.not_true, Bool.of_not_eq_true, Bool.or, Bool.or_true, Bool.true_or, Eq, Eq.mp, Eq.mpr, Eq.trans, Fin, Iff, Nat, Not, True, congr, congrArg, congrFun', dite, eq_self, id, of_eq_true

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

Demonstrability for the syntactic Basis III instance, between a single premise and a single conclusion, is provability of the implication for free: PropositionalLogic.syntacticBasis3’s deducibility is provability of the implication, by definition. The syntactic counterpart to PropositionalLogic.Formula.semantic_iff_provable above.

theorem Logic.PropositionalLogic.Formula.syntactic_iff_provable✝ {n : ℕ}
  {φ ψ : Logic.PropositionalLogic.Formula (Fin (n + 1))} :
  (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))).toBasis1.Demonstrate ⟪φ⟫ ⟪ψ⟫ ↔
    (φ.imp ψ).Provable
Show details 
fun {n} {φ ψ} =>
  Eq.mpr
    (id
      (congrArg (fun _a => _a ↔ (φ.imp ψ).Provable)
        (propext
          (Logic.Popper.Basis1.demonstrate_singleton
            (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))).toBasis1))))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a ↔ (φ.imp ψ).Provable)
          (propext
            (Logic.Popper.Basis3.follows_toBasis1
              (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))) φ ψ))))
      Iff.rfl)

Complexity: 3185 (size of the value term)

Dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis3.toBasis1, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.Provable, Logic.PropositionalLogic.syntacticBasis3, instToSeq

Proof dependencies: Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_singleton, Logic.Popper.Basis3.follows_toBasis1

Lean core dependencies: Eq, Eq.mpr, Fin, Iff, Iff.rfl, Nat, congrArg, id

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

Folding a premise list down to its conjunction, one adjacent pair at a time, never changes what can be derived — for any Popper.Basis1.HasConjunction instance, since its own conjunction witness is exactly the licence this needs. No separate hypothesis about the conjunction operation has to be threaded in: it is already part of what the instance provides. Used below for both the semantic and the syntactic instance.

theorem Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons✝ {n : ℕ}
  {B : Logic.Popper.Basis1 (Logic.PropositionalLogic.Formula (Fin (n + 1)))}
  [C : Logic.Popper.Basis1.HasConjunction (Logic.PropositionalLogic.Formula (Fin (n + 1))) B]
  (Γ' : List (Logic.PropositionalLogic.Formula (Fin (n + 1))))
  (γ : Logic.PropositionalLogic.Formula (Fin (n + 1)))
  (Q : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))) :
  B.Demonstrate [List.foldl (Logic.Popper.Basis1.HasConjunction.and B) γ Γ'] Q ↔
    B.Demonstrate (γ :: Γ') Q
Show details 
fun {n} {B} [Logic.Popper.Basis1.HasConjunction (Logic.PropositionalLogic.Formula (Fin (n + 1))) B]
    x x_1 x_2 =>
  List.brecOn (motive := fun x =>
    ∀ (x_3 : Logic.PropositionalLogic.Formula (Fin (n + 1)))
      (x_4 : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))),
      B.Demonstrate [List.foldl (Logic.Popper.Basis1.HasConjunction.and B) x_3 x] x_4 ↔
        B.Demonstrate (x_3 :: x) x_4)
    x Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons._f✝ x_1 x_2

Complexity: 577 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.HasConjunction, Logic.PropositionalLogic.Formula

Proof dependencies: Logic.Popper.Basis1.demonstrate_cons_of_isConjunction

Lean core dependencies: Fin, Iff, Iff.rfl, Iff.trans, List, List.foldl, Nat

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

Folding a conclusion list down to its disjunction, one adjacent pair at a time, never changes what can be derived — the dual of PropositionalLogic.Formula.demonstrate_bigAnd_cons above, using a Popper.Basis1.HasDisjunction instance’s disjunction witness the same way.

theorem Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons✝ {n : ℕ}
  {B : Logic.Popper.Basis1 (Logic.PropositionalLogic.Formula (Fin (n + 1)))}
  [C : Logic.Popper.Basis1.HasDisjunction (Logic.PropositionalLogic.Formula (Fin (n + 1))) B]
  (Δ' : List (Logic.PropositionalLogic.Formula (Fin (n + 1))))
  (δ : Logic.PropositionalLogic.Formula (Fin (n + 1)))
  (P : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))) :
  B.Demonstrate P [List.foldl (Logic.Popper.Basis1.HasDisjunction.or B) δ Δ'] ↔
    B.Demonstrate P (δ :: Δ')
Show details 
fun {n} {B} [Logic.Popper.Basis1.HasDisjunction (Logic.PropositionalLogic.Formula (Fin (n + 1))) B]
    x x_1 x_2 =>
  List.brecOn (motive := fun x =>
    ∀ (x_3 : Logic.PropositionalLogic.Formula (Fin (n + 1)))
      (x_4 : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))),
      B.Demonstrate x_4 [List.foldl (Logic.Popper.Basis1.HasDisjunction.or B) x_3 x] ↔
        B.Demonstrate x_4 (x_3 :: x))
    x Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons._f✝ x_1 x_2

Complexity: 577 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.HasDisjunction, Logic.PropositionalLogic.Formula

Proof dependencies: Logic.Popper.Basis1.demonstrate_cons_of_isDisjunction

Lean core dependencies: Fin, Iff, Iff.rfl, Iff.trans, List, List.foldl, Nat

Used by: Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic

Completeness, generalised. The semantic and syntactic Basis III instances agree on demonstrability between any nonempty finite list of premises and any nonempty finite list of conclusions, not only a single formula on each side. PropositionalLogic.semanticConnectives and PropositionalLogic.syntacticConnectives do the actual work: providing conjunction/disjunction witnesses against the semantic and syntactic bases is what lets a whole premise list collapse to its conjunction and a whole conclusion list collapse to its disjunction, reducing the general claim to the single-premise, single-conclusion case already settled by soundness and completeness.

theorem Logic.PropositionalLogic.Formula.demonstrate_semantic_iff_syntactic {n : ℕ}
  {γ δ : Logic.PropositionalLogic.Formula (Fin (n + 1))}
  {Γ' Δ' : List (Logic.PropositionalLogic.Formula (Fin (n + 1)))} :
  (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1.Demonstrate (γ :: Γ') (δ :: Δ') ↔
    (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))).toBasis1.Demonstrate (γ :: Γ')
      (δ :: Δ')
Show details 
fun {n} {γ δ} {Γ' Δ'} =>
  Eq.mpr
    (id
      (congrArg
        (fun _a =>
          _a ↔
            (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))).toBasis1.Demonstrate (γ :: Γ')
              (δ :: Δ'))
        (Eq.symm
          (propext (Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons✝ Γ' γ (δ :: Δ'))))))
    (Eq.mpr
      (id
        (congrArg
          (fun _a =>
            _a ↔
              (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))).toBasis1.Demonstrate
                (γ :: Γ') (δ :: Δ'))
          (Eq.symm
            (propext
              (Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons✝ Δ' δ
                [List.foldl
                    (Logic.Popper.Basis1.HasConjunction.and
                      (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1)
                    γ Γ'])))))
      (Eq.mpr
        (id
          (congrArg
            (fun _a =>
              (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1.Demonstrate
                  [List.foldl
                      (Logic.Popper.Basis1.HasConjunction.and
                        (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1)
                      γ Γ']
                  [List.foldl
                      (Logic.Popper.Basis1.HasDisjunction.or
                        (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1)
                      δ Δ'] ↔
                _a)
            (Eq.symm
              (propext
                (Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons✝ Γ' γ (δ :: Δ'))))))
        (Eq.mpr
          (id
            (congrArg
              (fun _a =>
                (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1.Demonstrate
                    [List.foldl
                        (Logic.Popper.Basis1.HasConjunction.and
                          (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1)
                        γ Γ']
                    [List.foldl
                        (Logic.Popper.Basis1.HasDisjunction.or
                          (Logic.PropositionalLogic.semanticBasis3 (Fin (n + 1))).toBasis1)
                        δ Δ'] ↔
                  _a)
              (Eq.symm
                (propext
                  (Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons✝ Δ' δ
                    [List.foldl
                        (Logic.Popper.Basis1.HasConjunction.and
                          (Logic.PropositionalLogic.syntacticBasis3 (Fin (n + 1))).toBasis1)
                        γ Γ'])))))
          (Iff.trans Logic.PropositionalLogic.Formula.semantic_iff_provable✝
            (Iff.symm Logic.PropositionalLogic.Formula.syntactic_iff_provable✝)))))

Complexity: 45752 (size of the value term)

Dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis3.toBasis1, Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.semanticBasis3, Logic.PropositionalLogic.syntacticBasis3

Proof dependencies: Logic.PropositionalLogic.Formula.Provable, Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons, Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons, Logic.PropositionalLogic.Formula.semantic_iff_provable, Logic.PropositionalLogic.Formula.syntactic_iff_provable, Logic.PropositionalLogic.semanticConnectives, Logic.PropositionalLogic.syntacticConnectives, instToSeq

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Fin, Iff, Iff.symm, Iff.trans, List, List.foldl, Nat, congrArg, id

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.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend