## 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