(P → (Q → R)) → (P → Q) → (P → R)

Stream: general

[Kevin Buzzard]

import logic.basic tactic.library_search
example (P Q R : Prop) : (P → (Q → R)) → (P → Q) → (P → R) := by library_search -- fails

I thought that this was a thing. It doesn't have a name? I was taught as an undergraduate that it was one of the three axioms of classical logic, the other two being LEM and P -> Q -> P.

[Kenny Lau]

but with context we are essentially using Fitch system where the only axiom is LEM

[François G. Dorais]

I believe some people call this bind. (re: monad)

[Marc Huisinga]

in my formal systems lecture it was called the german equivalent of "distribute"

[Scott Morrison]

I'm not sure I expected library_search to work here, but { intros, library_search } certainly should, simply because { intros, solve_by_elim } should work, because

import logic.basic tactic.library_search
example (P Q R : Prop) : (P → (Q → R)) → (P → Q) → (P → R) :=
begin
  intros,
  apply a,
  exact a_2,
  apply a_1,
  exact a_2,
end

works. However solve_by_elim fails, which is surely a bug. :-(

[Mario Carneiro]

I think it is in init.core, although it might be for Type only

[Mario Carneiro]

example (P Q R : Type) : (P → (Q → R)) → (P → Q) → (P → R) := combinator.S

[Mario Carneiro]

I know this theorem as "axiom 2". Thanks mathematicians

[Mario Carneiro]

"the S combinator" isn't much better though

[Chris B]

If the Sort/Prop version ends up getting included in something permanent, Frege seems like a pretty good choice.

Description: Axiom Frege. Axiom A2 of [Margaris] p. 49
...
This axiom was part of Frege's original system and is known as Frege in the literature