Zulip Chat Archive

Stream: general

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


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Nov 09 2019 at 23:48):

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

view this post on Zulip François G. Dorais (Nov 10 2019 at 00:51):

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

view this post on Zulip Marc Huisinga (Nov 10 2019 at 01:05):

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

view this post on Zulip 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. :-(

view this post on Zulip Mario Carneiro (Nov 10 2019 at 07:29):

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

view this post on Zulip Mario Carneiro (Nov 10 2019 at 07:31):

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

view this post on Zulip Mario Carneiro (Nov 10 2019 at 07:32):

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

view this post on Zulip Mario Carneiro (Nov 10 2019 at 07:32):

"the S combinator" isn't much better though

view this post on Zulip 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