# Zulip Chat Archive

## Stream: general

### Topic: (P → (Q → R)) → (P → Q) → (P → R)

#### Kevin Buzzard (Nov 09 2019 at 23:47):

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 (Nov 09 2019 at 23:48):

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

#### François G. Dorais (Nov 10 2019 at 00:51):

I believe some people call this `bind`

. (re: monad)

#### Marc Huisinga (Nov 10 2019 at 01:05):

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

#### Scott Morrison (Nov 10 2019 at 06:18):

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 (Nov 10 2019 at 07:29):

I think it is in `init.core`

, although it might be for Type only

#### Mario Carneiro (Nov 10 2019 at 07:31):

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

#### Mario Carneiro (Nov 10 2019 at 07:32):

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

#### Mario Carneiro (Nov 10 2019 at 07:32):

"the S combinator" isn't much better though

#### Chris B (Nov 20 2019 at 03:19):

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

Last updated: May 11 2021 at 13:22 UTC