Connectives

Difficulty: optional — 11 definitions, 0 abbreviations, 1 lemmas, 15 theorems, 0 examples.

definition lemma theorem

legend

Popper’s relational characterizations of conjunction, disjunction, classical negation, intuitionistic negation, and implication: not connectives built into the syntax of a basis, but properties an object can have, stated purely in terms of relative demonstrability. A basis need not have anything satisfying these properties, and if something does, that is what makes it a conjunction, a disjunction, a classical negation, an intuitionistic negation, or an implication.

Source: Binder, Piecha & Schroeder-Heister (eds.), The Logical Writings of Karl Popper, Trends in Logic 58 (2022). Editors’ introduction: section 5.5 (conjunction and disjunction, rules (C∧) and (C∨)), section 5.6 (the conditional, rule (C>)), section 6.1 (classical negation, rules (C¬k1) and (C¬k2)), section 6.2 (intuitionistic negation, rule (C¬i)).

NoteLogic.Popper.Basis1.IsConjunction

\(m\) is a conjunction of \(a\) and \(b\): for every object \(d\), \(m\) alone derives \(d\) exactly when \(a\) and \(b\) together derive \(d\).

conjunction

def Logic.Popper.Basis1.IsConjunction {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a b m : Obj) : Prop

Show details

| S.IsConjunction a b m = ∀ (d : Obj), S.Demonstrate ⟪m⟫ ⟪d⟫ ↔ S.Demonstrate ⟪a, b⟫ ⟪d⟫

Complexity: 111 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq

Lean core dependencies: Iff, List

Used by: Logic.Popper.Basis1.HasConjunction, Logic.Popper.Basis1.demonstrate_cons_of_isConjunction, Logic.Popper.Basis1.isConjunction_congr, Logic.Popper.Basis1.isConjunction_unique

NoteLogic.Popper.Basis1.IsDisjunction

\(j\) is a disjunction of \(a\) and \(b\): for every object \(d\), \(d\) alone derives \(j\) exactly when \(d\) derives \(a\) or \(b\).

disjunction

def Logic.Popper.Basis1.IsDisjunction {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a b j : Obj) : Prop

Show details

| S.IsDisjunction a b j = ∀ (d : Obj), S.Demonstrate ⟪d⟫ ⟪j⟫ ↔ S.Demonstrate ⟪d⟫ ⟪a, b⟫

Complexity: 111 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq

Lean core dependencies: Iff, List

Used by: Logic.Popper.Basis1.HasDisjunction, Logic.Popper.Basis1.demonstrate_cons_of_isDisjunction, Logic.Popper.Basis1.isDisjunction_congr, Logic.Popper.Basis1.isDisjunction_unique

NoteLogic.Popper.Basis1.IsClassicalNegation

\(n\) is a classical negation of \(a\): for every context \(d\) and every object \(c\), \(d\) together with \(n\) derives \(c\) exactly when \(d\) alone derives \(a\) or \(c\).

classical-negation

def Logic.Popper.Basis1.IsClassicalNegation {Obj : Type} (S : Logic.Popper.Basis1 Obj) (a n : Obj) :
  Prop

Show details

| S.IsClassicalNegation a n = ∀ (d c : Obj), S.Demonstrate ⟪d, n⟫ ⟪c⟫ ↔ S.Demonstrate ⟪d⟫ ⟪a, c⟫

Complexity: 147 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq

Lean core dependencies: Iff, List

Used by: Logic.Popper.Basis1.HasClassicalNegation, Logic.Popper.Basis1.contradictory_of_isClassicalNegation, Logic.Popper.Basis1.isClassicalNegation_congr, Logic.Popper.Basis1.isClassicalNegation_unique

ImportantLogic.Popper.Basis1.demonstrate_cons_of_isConjunction

A conjunction can stand in for its two conjuncts anywhere at the front of a premise list: the rest of the premises, and what is being derived, make no difference. This is what lets a whole list of premises be folded down to a single formula, one conjunction at a time.

theorem Logic.Popper.Basis1.demonstrate_cons_of_isConjunction {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {a b m : Obj} (h : S.IsConjunction a b m) (Rest Q : List Obj) :
  S.Demonstrate ⟪m, Rest⟫ Q ↔ S.Demonstrate ⟪a, b, Rest⟫ Q

Show details

fun {Obj} S {a b m} h Rest Q =>
  have da :=
    (h a).mpr
      (Logic.Popper.Basis1.demonstrate_of_mem S List.mem_cons_self (List.mem_singleton_self a));
  have db :=
    (h b).mpr
      (Logic.Popper.Basis1.demonstrate_of_mem S
        (List.mem_cons.mpr (Or.inr (List.mem_singleton_self b))) (List.mem_singleton_self b));
  have habm :=
    (h m).mp
      (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self m)
        (List.mem_singleton_self m));
  {
    mp := fun hyp c D hD =>
      have key := hyp c D hD;
      have hm :=
        habm m (Rest ++ D) fun q hq =>
          Eq.mpr
            (id
              (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, Rest ++ D⟫ m)
                (List.mem_singleton.mp hq)))
            (Logic.Popper.Basis1.rg ⟪m, Rest ++ D⟫ m List.mem_cons_self);
      Logic.Popper.Basis1.tg (a :: b :: (Rest ++ D)) (m :: (Rest ++ D)) c
        (fun x hx =>
          Or.casesOn (List.mem_cons.mp hx)
            (fun heq =>
              Eq.mpr
                (id
                  (congrArg (fun _a => Logic.Popper.Basis1.Deduce (a :: b :: (Rest ++ D)) _a) heq))
                hm)
            fun hx =>
            Logic.Popper.Basis1.rg (a :: b :: (Rest ++ D)) x
              (List.mem_cons.mpr (Or.inr (List.mem_cons.mpr (Or.inr hx)))))
        key,
    mpr := fun hyp c D hD =>
      have key := hyp c D hD;
      have ha :=
        da a (Rest ++ D) fun q hq =>
          Eq.mpr
            (id
              (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, Rest ++ D⟫ a)
                (List.mem_singleton.mp hq)))
            (Logic.Popper.Basis1.rg ⟪a, Rest ++ D⟫ a List.mem_cons_self);
      have hb :=
        db b (Rest ++ D) fun q hq =>
          Eq.mpr
            (id
              (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, Rest ++ D⟫ b)
                (List.mem_singleton.mp hq)))
            (Logic.Popper.Basis1.rg ⟪b, Rest ++ D⟫ b List.mem_cons_self);
      Logic.Popper.Basis1.tg (m :: (Rest ++ D)) (a :: b :: (Rest ++ D)) c
        (fun x hx =>
          Or.casesOn (List.mem_cons.mp hx)
            (fun heq =>
              Eq.mpr
                (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce (m :: (Rest ++ D)) _a) heq)) ha)
            fun hx =>
            Or.casesOn (List.mem_cons.mp hx)
              (fun heq =>
                Eq.mpr
                  (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce (m :: (Rest ++ D)) _a) heq))
                  hb)
              fun hx => Logic.Popper.Basis1.rg (m :: (Rest ++ D)) x (List.mem_cons.mpr (Or.inr hx)))
        key }

Complexity: 6287 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.IsConjunction, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.demonstrate_of_mem

Lean core dependencies: Eq, Eq.mpr, Iff, List, List.append, List.mem_cons, List.mem_cons_self, List.mem_singleton, List.mem_singleton_self, Or, congrArg, id

Used by: Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons

ImportantLogic.Popper.Basis1.demonstrate_cons_of_isDisjunction

A disjunction can stand in for its two disjuncts anywhere at the front of a conclusion list: the rest of the conclusions, and what is doing the deriving, make no difference. This is what lets a whole list of conclusions be folded down to a single formula, one disjunction at a time.

theorem Logic.Popper.Basis1.demonstrate_cons_of_isDisjunction {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {a b j : Obj} (h : S.IsDisjunction a b j) (P Rest : List Obj) :
  S.Demonstrate P ⟪j, Rest⟫ ↔ S.Demonstrate P ⟪a, b, Rest⟫

Show details

fun {Obj} S {a b j} h P Rest =>
  have dja :=
    (h a).mpr
      (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self a) List.mem_cons_self);
  have djb :=
    (h b).mpr
      (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self b)
        (List.mem_cons.mpr (Or.inr (List.mem_singleton_self b))));
  have djab :=
    (h j).mp
      (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self j)
        (List.mem_singleton_self j));
  {
    mp := fun hyp c D hD =>
      have hac := hD a List.mem_cons_self;
      have hbc := hD b (List.mem_cons.mpr (Or.inr List.mem_cons_self));
      have hjc :=
        djab c D fun q hq =>
          Or.casesOn (List.mem_cons.mp hq)
            (fun heq =>
              Eq.mpr (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c) heq)) hac)
            fun hq =>
            Eq.mpr
              (id
                (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c)
                  (List.mem_singleton.mp hq)))
              hbc;
      hyp c D fun q hq =>
        Or.casesOn (List.mem_cons.mp hq)
          (fun heq =>
            Eq.mpr (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c) heq)) hjc)
          fun hq => hD q (List.mem_cons.mpr (Or.inr (List.mem_cons.mpr (Or.inr hq)))),
    mpr := fun hyp c D hD =>
      have hjc := hD j List.mem_cons_self;
      have hac :=
        dja c D fun q hq =>
          Eq.mpr
            (id
              (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c)
                (List.mem_singleton.mp hq)))
            hjc;
      have hbc :=
        djb c D fun q hq =>
          Eq.mpr
            (id
              (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c)
                (List.mem_singleton.mp hq)))
            hjc;
      hyp c D fun q hq =>
        Or.casesOn (List.mem_cons.mp hq)
          (fun heq =>
            Eq.mpr (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c) heq)) hac)
          fun hq =>
          Or.casesOn (List.mem_cons.mp hq)
            (fun heq =>
              Eq.mpr (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, D⟫ c) heq)) hbc)
            fun hq => hD q (List.mem_cons.mpr (Or.inr hq)) }

Complexity: 6602 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.IsDisjunction, instToSeq, instToSeqList

Proof dependencies: Logic.Popper.Basis1.demonstrate_of_mem

Lean core dependencies: Eq, Eq.mpr, Iff, List, List.append, List.mem_cons, List.mem_cons_self, List.mem_singleton, List.mem_singleton_self, Or, congrArg, id

Used by: Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons

NoteLogic.Popper.Basis1.IsImplication

\(m\) is an implication from \(b\) to \(c\): for every context \(D\), \(D\) alone derives \(m\) exactly when \(D\) together with \(b\) derives \(c\). Unlike Popper.Basis1.IsConjunction, Popper.Basis1.IsDisjunction, and Popper.Basis1.IsClassicalNegation, the context here ranges over full premise lists rather than a single object, matching Popper’s own turnstile — this is what makes the rule the deduction theorem itself, rather than something the deduction theorem needs to be derived from separately.

implicationdeduction-theorem

def Logic.Popper.Basis1.IsImplication {Obj : Type} (S : Logic.Popper.Basis1 Obj) (b c m : Obj) : Prop

Show details

| S.IsImplication b c m = ∀ (D : List Obj), S.Demonstrate D ⟪m⟫ ↔ S.Demonstrate ⟪D, b⟫ ⟪c⟫

Complexity: 105 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq, instToSeqList

Lean core dependencies: Iff, List

Used by: Logic.Popper.Basis1.HasImplication, Logic.Popper.Basis1.demonstrate_mp, Logic.Popper.Basis1.isImplication_congr, Logic.Popper.Basis1.isImplication_unique

ImportantLogic.Popper.Basis1.demonstrate_mp

Modus ponens: an implication together with what it starts from derives what it ends at.

modus-ponens

theorem Logic.Popper.Basis1.demonstrate_mp {Obj : Type} (S : Logic.Popper.Basis1 Obj) {b c m : Obj}
  (h : S.IsImplication b c m) : S.Demonstrate ⟪m, b⟫ ⟪c⟫

Show details

fun {Obj} S {b c m} h =>
  have this :=
    (h [m]).mp
      (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self m)
        (List.mem_singleton_self m));
  id this

Complexity: 328 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.IsImplication, instToSeq

Proof dependencies: Logic.Popper.Basis1.demonstrate_of_mem, instToSeqList

Lean core dependencies: List, List.mem_singleton_self, id

Used by: (none)

ImportantLogic.Popper.Basis1.contradictory_of_isClassicalNegation

A classical negation and the statement it negates cannot both hold: taken together they are contradictory. This needs no extra postulate beyond Popper.Basis1.IsClassicalNegation itself, unlike excluded middle, which demonstrates \(a\) or \(n\) from nothing.

classical-negation

theorem Logic.Popper.Basis1.contradictory_of_isClassicalNegation {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {a n : Obj} (h : S.IsClassicalNegation a n) : S.Contradictory ⟪a, n⟫

Show details

fun {Obj} S {a n} h e E x =>
  (h a e).mpr
    (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self a)
      (List.mem_cons.mpr (Or.inl rfl)))
    e E fun b hb =>
    Eq.mpr
      (id (congrArg (fun _a => Logic.Popper.Basis1.Deduce ⟪_a, E⟫ e) (List.mem_singleton.mp hb)))
      (Logic.Popper.Basis1.rg (e :: E) e List.mem_cons_self)

Complexity: 891 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Contradictory, Logic.Popper.Basis1.IsClassicalNegation, instToSeq

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_of_mem, instToSeqList

Lean core dependencies: Eq, Eq.mpr, List, List.append, List.mem_cons, List.mem_cons_self, List.mem_singleton, List.mem_singleton_self, Or, congrArg, id, rfl

Used by: (none)

NoteLogic.Popper.Basis1.IsIntuitionisticNegation

\(n\) is an intuitionistic negation of \(b\): for every object \(c\), \(c\) alone derives \(n\) exactly when \(c\) together with \(b\) derives nothing at all. Unlike classical negation, this only ever gives an empty conclusion directly — reaching an arbitrary conclusion from \(b\) and \(n\) together (as a classical negation does, by Popper.Basis1.demonstrate_of_contradictory) is not part of the characterization.

intuitionistic-negation

def Logic.Popper.Basis1.IsIntuitionisticNegation {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  (b n : Obj) : Prop

Show details

| S.IsIntuitionisticNegation b n = ∀ (c : Obj), S.Demonstrate ⟪c⟫ ⟪n⟫ ↔ S.Demonstrate ⟪c, b⟫ []

Complexity: 101 (size of the value term)

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.Demonstrate, instToSeq

Lean core dependencies: Iff, List

Used by: Logic.Popper.Basis1.HasIntuitionisticNegation, Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation, Logic.Popper.Basis1.isIntuitionisticNegation_congr, Logic.Popper.Basis1.isIntuitionisticNegation_unique

ImportantLogic.Popper.Basis1.contradictory_of_isIntuitionisticNegation

An intuitionistic negation and the statement it negates cannot both hold either. What is missing compared with the classical case is not this, but the step from here to an arbitrary conclusion.

intuitionistic-negation

theorem Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation {Obj : Type}
  (S : Logic.Popper.Basis1 Obj) {b n : Obj} (h : S.IsIntuitionisticNegation b n) :
  S.Contradictory ⟪b, n⟫

Show details

fun {Obj} S {b n} h =>
  have hnb :=
    (h n).mp
      (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self n)
        (List.mem_singleton_self n));
  Logic.Popper.Basis1.demonstrate_mono S
    (fun x hx =>
      Or.casesOn (List.mem_cons.mp hx)
        (fun h_1 =>
          Eq.ndrec (motive := fun {n} =>
            S.IsIntuitionisticNegation b n → S.Demonstrate [n, b] [] → x ∈ [n, b] → x ∈ ⟪b, n⟫)
            (fun h hnb hx => List.mem_cons.mpr (Or.inr (List.mem_singleton_self x))) h_1 h hnb hx)
        fun hx => List.mem_cons.mpr (Or.inl (List.mem_singleton.mp hx)))
    (fun x hx => hx) hnb

Complexity: 1142 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Contradictory, Logic.Popper.Basis1.IsIntuitionisticNegation, instToSeq

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_mono, Logic.Popper.Basis1.demonstrate_of_mem

Lean core dependencies: Eq, List, List.append, List.mem_cons, List.mem_singleton, List.mem_singleton_self, Or

Used by: (none)

ImportantLogic.Popper.Basis1.isConjunction_congr

Anything mutually deducible with a conjunction of \(a\) and \(b\) is itself one. Together with Popper.Basis1.isConjunction_unique, this says the characterizing property picks out exactly one statement up to mutual deducibility, which is what entitles it to be called a definition.

inferential-definition

theorem Logic.Popper.Basis1.isConjunction_congr {Obj : Type} (S : Logic.Popper.Basis1 Obj) {a b m m' : Obj}
  (h : S.Mutual m m') (hc : S.IsConjunction a b m) : S.IsConjunction a b m'

Show details

fun {Obj} S {a b m m'} h hc d =>
  Iff.trans
    { mp := fun x => Logic.Popper.Basis1.demonstrate_congr_premise S ⟨h.right, h.left⟩ x,
      mpr := fun x => Logic.Popper.Basis1.demonstrate_congr_premise S h x }
    (hc d)

Complexity: 667 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsConjunction, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_congr_premise, instToSeq, instToSeqList

Lean core dependencies: Iff.trans, List

Used by: (none)

ImportantLogic.Popper.Basis1.isDisjunction_congr

Anything mutually deducible with a disjunction of \(a\) and \(b\) is itself one.

inferential-definition

theorem Logic.Popper.Basis1.isDisjunction_congr {Obj : Type} (S : Logic.Popper.Basis1 Obj) {a b j j' : Obj}
  (h : S.Mutual j j') (hj : S.IsDisjunction a b j) : S.IsDisjunction a b j'

Show details

fun {Obj} S {a b j j'} h hj d =>
  Iff.trans
    { mp := fun x => Logic.Popper.Basis1.demonstrate_congr_conclusion S ⟨h.right, h.left⟩ x,
      mpr := fun x => Logic.Popper.Basis1.demonstrate_congr_conclusion S h x }
    (hj d)

Complexity: 667 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsDisjunction, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_congr_conclusion, instToSeq, instToSeqList

Lean core dependencies: Iff.trans, List

Used by: (none)

ImportantLogic.Popper.Basis1.isClassicalNegation_congr

Anything mutually deducible with a classical negation of \(a\) is itself one.

inferential-definition

theorem Logic.Popper.Basis1.isClassicalNegation_congr {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {a n n' : Obj} (h : S.Mutual n n') (hn : S.IsClassicalNegation a n) : S.IsClassicalNegation a n'

Show details

fun {Obj} S {a n n'} h hn d c =>
  Iff.trans
    { mp := fun x => Logic.Popper.Basis1.demonstrate_congr_premise S ⟨h.right, h.left⟩ x,
      mpr := fun x => Logic.Popper.Basis1.demonstrate_congr_premise S h x }
    (hn d c)

Complexity: 805 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsClassicalNegation, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_congr_premise, instToSeq, instToSeqList

Lean core dependencies: Iff.trans, List

Used by: (none)

ImportantLogic.Popper.Basis1.isIntuitionisticNegation_congr

Anything mutually deducible with an intuitionistic negation of \(b\) is itself one.

inferential-definition

theorem Logic.Popper.Basis1.isIntuitionisticNegation_congr {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {b n n' : Obj} (h : S.Mutual n n') (hn : S.IsIntuitionisticNegation b n) :
  S.IsIntuitionisticNegation b n'

Show details

fun {Obj} S {b n n'} h hn c =>
  Iff.trans
    { mp := fun x => Logic.Popper.Basis1.demonstrate_congr_conclusion S ⟨h.right, h.left⟩ x,
      mpr := fun x => Logic.Popper.Basis1.demonstrate_congr_conclusion S h x }
    (hn c)

Complexity: 655 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsIntuitionisticNegation, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_congr_conclusion, instToSeq, instToSeqList

Lean core dependencies: Iff.trans, List

Used by: (none)

ImportantLogic.Popper.Basis1.isImplication_congr

Anything mutually deducible with an implication from \(b\) to \(c\) is itself one.

inferential-definition

theorem Logic.Popper.Basis1.isImplication_congr {Obj : Type} (S : Logic.Popper.Basis1 Obj) {b c m m' : Obj}
  (h : S.Mutual m m') (hm : S.IsImplication b c m) : S.IsImplication b c m'

Show details

fun {Obj} S {b c m m'} h hm D =>
  Iff.trans
    { mp := fun x => Logic.Popper.Basis1.demonstrate_congr_conclusion S ⟨h.right, h.left⟩ x,
      mpr := fun x => Logic.Popper.Basis1.demonstrate_congr_conclusion S h x }
    (hm D)

Complexity: 591 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsImplication, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Follows, Logic.Popper.Basis1.demonstrate_congr_conclusion, instToSeq, instToSeqList

Lean core dependencies: Iff.trans, List

Used by: (none)

TipLogic.Popper.Basis1.mutual_of_demonstrate

Mutual deducibility between two statements, read off from demonstrability each way.

theorem Logic.Popper.Basis1.mutual_of_demonstrate {Obj : Type} (S : Logic.Popper.Basis1 Obj) {m m' : Obj}
  (h1 : S.Demonstrate ⟪m⟫ ⟪m'⟫) (h2 : S.Demonstrate ⟪m'⟫ ⟪m⟫) : S.Mutual m m'

Show details

fun {Obj} S {m m'} h1 h2 =>
  ⟨(Logic.Popper.Basis1.demonstrate_singleton S).mp h1,
    (Logic.Popper.Basis1.demonstrate_singleton S).mp h2⟩

Complexity: 199 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.Mutual, instToSeq

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

Used by: Logic.Popper.Basis1.isClassicalNegation_unique, Logic.Popper.Basis1.isConjunction_unique, Logic.Popper.Basis1.isDisjunction_unique, Logic.Popper.Basis1.isImplication_unique, Logic.Popper.Basis1.isIntuitionisticNegation_unique

ImportantLogic.Popper.Basis1.isConjunction_unique

A conjunction of \(a\) and \(b\) is settled up to mutual deducibility: any two statements that both count as one are interdeducible. This is what makes the characterizing property a definition rather than merely a constraint.

uniqueness-of-definition

theorem Logic.Popper.Basis1.isConjunction_unique {Obj : Type} (S : Logic.Popper.Basis1 Obj) {a b m m' : Obj}
  (h : S.IsConjunction a b m) (h' : S.IsConjunction a b m') : S.Mutual m m'

Show details

fun {Obj} S {a b m m'} h h' =>
  Logic.Popper.Basis1.mutual_of_demonstrate S
    ((h m').mpr
      ((h' m').mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self m')
          (List.mem_singleton_self m'))))
    ((h' m).mpr
      ((h m).mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self m)
          (List.mem_singleton_self m))))

Complexity: 543 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsConjunction, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.mutual_of_demonstrate, instToSeq

Lean core dependencies: List, List.mem_singleton_self

Used by: (none)

ImportantLogic.Popper.Basis1.isDisjunction_unique

A disjunction of \(a\) and \(b\) is settled up to mutual deducibility.

uniqueness-of-definition

theorem Logic.Popper.Basis1.isDisjunction_unique {Obj : Type} (S : Logic.Popper.Basis1 Obj) {a b j j' : Obj}
  (h : S.IsDisjunction a b j) (h' : S.IsDisjunction a b j') : S.Mutual j j'

Show details

fun {Obj} S {a b j j'} h h' =>
  Logic.Popper.Basis1.mutual_of_demonstrate S
    ((h' j).mpr
      ((h j).mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self j)
          (List.mem_singleton_self j))))
    ((h j').mpr
      ((h' j').mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self j')
          (List.mem_singleton_self j'))))

Complexity: 543 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsDisjunction, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.mutual_of_demonstrate, instToSeq

Lean core dependencies: List, List.mem_singleton_self

Used by: (none)

ImportantLogic.Popper.Basis1.isClassicalNegation_unique

A classical negation of \(a\) is settled up to mutual deducibility. The characterization carries a context on the premise side, so the statement being negated appears twice as a premise and has to be contracted away.

uniqueness-of-definition

theorem Logic.Popper.Basis1.isClassicalNegation_unique {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {a n n' : Obj} (h : S.IsClassicalNegation a n) (h' : S.IsClassicalNegation a n') : S.Mutual n n'

Show details

fun {Obj} S {a n n'} h h' =>
  have step := fun {p q} hp hq =>
    have haq :=
      (hq p q).mp
        (Logic.Popper.Basis1.demonstrate_of_mem S
          (List.mem_cons.mpr (Or.inr (List.mem_singleton_self q))) (List.mem_singleton_self q));
    Logic.Popper.Basis1.demonstrate_mono S
      (fun x hx =>
        Or.casesOn (List.mem_cons.mp hx) (fun heq => List.mem_cons.mpr (Or.inl heq)) fun hx => hx)
      (fun x hx => hx) ((hp p q).mpr haq);
  Logic.Popper.Basis1.mutual_of_demonstrate S (step h h') (step h' h)

Complexity: 1229 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsClassicalNegation, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_mono, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.mutual_of_demonstrate, instToSeq

Lean core dependencies: Eq, List, List.append, List.mem_cons, List.mem_singleton_self, Or

Used by: (none)

ImportantLogic.Popper.Basis1.isIntuitionisticNegation_unique

An intuitionistic negation of \(b\) is settled up to mutual deducibility.

uniqueness-of-definition

theorem Logic.Popper.Basis1.isIntuitionisticNegation_unique {Obj : Type} (S : Logic.Popper.Basis1 Obj)
  {b n n' : Obj} (h : S.IsIntuitionisticNegation b n) (h' : S.IsIntuitionisticNegation b n') :
  S.Mutual n n'

Show details

fun {Obj} S {b n n'} h h' =>
  Logic.Popper.Basis1.mutual_of_demonstrate S
    ((h' n).mpr
      ((h n).mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self n)
          (List.mem_singleton_self n))))
    ((h n').mpr
      ((h' n').mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self n')
          (List.mem_singleton_self n'))))

Complexity: 505 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsIntuitionisticNegation, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.mutual_of_demonstrate, instToSeq

Lean core dependencies: List, List.mem_singleton_self

Used by: (none)

ImportantLogic.Popper.Basis1.isImplication_unique

An implication from \(b\) to \(c\) is settled up to mutual deducibility.

uniqueness-of-definition

theorem Logic.Popper.Basis1.isImplication_unique {Obj : Type} (S : Logic.Popper.Basis1 Obj) {b c m m' : Obj}
  (h : S.IsImplication b c m) (h' : S.IsImplication b c m') : S.Mutual m m'

Show details

fun {Obj} S {b c m m'} h h' =>
  Logic.Popper.Basis1.mutual_of_demonstrate S
    ((h' [m]).mpr
      ((h [m]).mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self m)
          (List.mem_singleton_self m))))
    ((h [m']).mpr
      ((h' [m']).mp
        (Logic.Popper.Basis1.demonstrate_of_mem S (List.mem_singleton_self m')
          (List.mem_singleton_self m'))))

Complexity: 603 (size of the value term)

Dependencies: Logic.Popper.Basis1, Logic.Popper.Basis1.IsImplication, Logic.Popper.Basis1.Mutual

Proof dependencies: Logic.Popper.Basis1.Demonstrate, Logic.Popper.Basis1.demonstrate_of_mem, Logic.Popper.Basis1.mutual_of_demonstrate, instToSeq, instToSeqList

Lean core dependencies: List, List.mem_singleton_self

Used by: (none)

NoteLogic.Popper.Basis1.HasConjunction

A basis \(B\) equipped with a distinguished conjunction operation, witnessed by actually satisfying Popper’s characterizing property for it. Takes \(B\) as an explicit parameter, rather than extending Popper.Basis3, so that several of these mixins can be required together (as the classical bundle further below does) without each independently — and possibly inconsistently — picking its own underlying basis for the same carrier.

structure Logic.Popper.Basis1.HasConjunction (Obj : Type) (B : Logic.Popper.Basis1 Obj) : Type

• and : Obj → Obj → Obj

• and_isConjunction : ∀ (a b : Obj), B.IsConjunction a b (Logic.Popper.Basis1.HasConjunction.and B a b)

Show details

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.IsConjunction

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: Logic.Popper.Basis1.HasClassicalConnectives, Logic.PropositionalLogic.Formula.demonstrate_bigAnd_cons

NoteLogic.Popper.Basis1.HasDisjunction

A basis \(B\) equipped with a distinguished disjunction operation, witnessed by actually satisfying Popper’s characterizing property for it.

structure Logic.Popper.Basis1.HasDisjunction (Obj : Type) (B : Logic.Popper.Basis1 Obj) : Type

• or : Obj → Obj → Obj

• or_isDisjunction : ∀ (a b : Obj), B.IsDisjunction a b (Logic.Popper.Basis1.HasDisjunction.or B a b)

Show details

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.IsDisjunction

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: Logic.Popper.Basis1.HasClassicalConnectives, Logic.PropositionalLogic.Formula.demonstrate_bigOr_cons

NoteLogic.Popper.Basis1.HasClassicalNegation

A basis \(B\) equipped with a distinguished classical negation operation, witnessed by actually satisfying Popper’s characterizing property for it.

structure Logic.Popper.Basis1.HasClassicalNegation (Obj : Type) (B : Logic.Popper.Basis1 Obj) : Type

• neg : Obj → Obj

• neg_isClassicalNegation : ∀ (a : Obj), B.IsClassicalNegation a (Logic.Popper.Basis1.HasClassicalNegation.neg B a)

Show details

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.IsClassicalNegation

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: Logic.Popper.Basis1.HasClassicalConnectives

NoteLogic.Popper.Basis1.HasIntuitionisticNegation

A basis \(B\) equipped with a distinguished intuitionistic negation operation, witnessed by actually satisfying Popper’s characterizing property for it. Independent of classical negation: a basis can have either, both (in which case they coincide, per Popper’s own observation that classical negation then “absorbs” the intuitionistic one), or neither.

structure Logic.Popper.Basis1.HasIntuitionisticNegation (Obj : Type) (B : Logic.Popper.Basis1 Obj) : Type

• neg : Obj → Obj

• neg_isIntuitionisticNegation : ∀ (a : Obj), B.IsIntuitionisticNegation a (Logic.Popper.Basis1.HasIntuitionisticNegation.neg B a)

Show details

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.IsIntuitionisticNegation

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: (none)

NoteLogic.Popper.Basis1.HasImplication

A basis \(B\) equipped with a distinguished implication operation, witnessed by actually satisfying Popper’s characterizing property for it. Implication is not built from conjunction, disjunction, and negation (doing so only recovers implication classically, needing excluded middle): it is its own primitive characterization, independent of the other four mixins here.

structure Logic.Popper.Basis1.HasImplication (Obj : Type) (B : Logic.Popper.Basis1 Obj) : Type

• imp : Obj → Obj → Obj

• imp_isImplication : ∀ (b c : Obj), B.IsImplication b c (Logic.Popper.Basis1.HasImplication.imp B b c)

Show details

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.IsImplication

Lean core dependencies: Eq, HEq, eq_of_heq

Used by: (none)

NoteLogic.Popper.Basis1.HasClassicalConnectives

The classical connectives — conjunction, disjunction, and classical negation — bundled together against one shared basis \(B\), for the common case of a genuinely classical logic that wants all three at once. Each piece remains independently usable (via the generated projections to each of the three parent classes) for code that only needs one of them.

structure Logic.Popper.Basis1.HasClassicalConnectives (Obj : Type) (B : Logic.Popper.Basis1 Obj) : Type

• (inherited from Logic.Popper.Basis1.HasConjunction)

  and : Obj → Obj → Obj

• (inherited from Logic.Popper.Basis1.HasConjunction)

  and_isConjunction : ∀ (a b : Obj), B.IsConjunction a b (Logic.Popper.Basis1.HasConjunction.and B a b)

• (inherited from Logic.Popper.Basis1.HasDisjunction)

  or : Obj → Obj → Obj

• (inherited from Logic.Popper.Basis1.HasDisjunction)

  or_isDisjunction : ∀ (a b : Obj), B.IsDisjunction a b (Logic.Popper.Basis1.HasDisjunction.or B a b)

• (inherited from Logic.Popper.Basis1.HasClassicalNegation)

  neg : Obj → Obj

• (inherited from Logic.Popper.Basis1.HasClassicalNegation)

  neg_isClassicalNegation : ∀ (a : Obj), B.IsClassicalNegation a (Logic.Popper.Basis1.HasClassicalNegation.neg B a)

Show details

Outer dependencies: Logic.Popper.Basis1

Inner dependencies: Logic.Popper.Basis1.HasClassicalNegation, Logic.Popper.Basis1.HasConjunction, Logic.Popper.Basis1.HasDisjunction

Lean core dependencies: Eq, HEq, eq_of_heq

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

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