Zulip Chat Archive

Stream: new members

Topic: Contrapositive law without excluded middle?


view this post on Zulip Golol (May 10 2020 at 15:30):

Hi, I am trying to solve the following exercise:
example : (p → q) → (¬q → ¬p) := sorry
I have a working proof using em, but the exercise is listed as working without classical.
I don't see a way of getting to \not q without arguing that p being true would lead to absurd (needs em to make an or-elim).
Is ther a way to do this without em?

view this post on Zulip Kenny Lau (May 10 2020 at 15:32):

hint: (not p) is defined to be (p -> false)

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:33):

Yes, you have to intro or lam until the goal is false.

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:34):

and then put together what you have to make a proof of false from your contradictory assumptions.

view this post on Zulip Golol (May 10 2020 at 15:41):

aah thanks, perfect!
Not wanting to open a new thread, there was something else I wondered about.
The tutorial in section 3 (Propositional logic) does such a nice job of showing you how beautifully you can dobasically everything with "->", but then hits you with things like add.elim, or.intro etc. which seem clunky at first and a bit "artificial" (but they probably make more sense later).
I thinkthat basically:
variables p q r: Prop
#constant and.intro : p->q->p and q
#constant and.elim_left : p and q -> p
#constant or.intro_left: p->p or q
#constant or.elim (p or q) -> (p->r) -> (q -> r) -> r
etc.
should achieve exactly the same, at least in this specific section about Propositional logic?

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:42):

Section 3 of what?

view this post on Zulip Golol (May 10 2020 at 15:43):

https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html#exercises

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:43):

These things are essentially constants anyway, they are basically defined when you create the types

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:44):

For a tactic-based take on it, try Proposition World in the natural number game.

view this post on Zulip Golol (May 10 2020 at 15:46):

Im only at quantifiers, idk tactics yet :D. But I think this stuff is super cool.

view this post on Zulip Golol (May 10 2020 at 15:47):

I wanna learn this, get up to date with the state of the art of analysis/pde in the database and get going

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:48):

If you start with the natural number game then you go straight into tactics and you don't have to learn all this #constant and and.elim stuff. I agree that they're artificial, they're not the way a mathematician thinks about how to manipulate these things.

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:48):

Tactic mode is a much better model for a mathematician

view this post on Zulip Golol (May 10 2020 at 15:50):

Then Ill do that. After I read the inductive types chapter though. Thanks!

view this post on Zulip Golol (May 10 2020 at 15:52):

(Im still living in the undergrad fantasy world where you should linearily understand all preceding mathematics to be allowed to use something)

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:57):

The natural number game is basically an argument that Theorem Proving In Lean is written in the wrong order for mathematicians.

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:58):

Our forthcoming book Mathematics in Lean will be developing the theory in an order more appropriate for mathematicians, and there will certainly be tactics before and.intro.

view this post on Zulip Mario Carneiro (May 10 2020 at 17:03):

Golol said:

(Im still living in the undergrad fantasy world where you should linearily understand all preceding mathematics to be allowed to use something)

The nice thing about formalized mathematics is that this is actually a viable strategy


Last updated: May 14 2021 at 02:15 UTC