Help with quantifiers

Stream: new members

[Jose Balado]

I got stuck trying to prove these two, please can anyone help me with the solutions:

theorem DG2 (α : Type*) (A : α → Prop) : (¬ ∃ x, ¬ A x) → ∀ x, A x := sorry
theorem NG1 (α : Type*) (A : α → Prop) : (¬ ∀ x, A x) → ∃ x, ¬ A x := sorry

Thanks,
Jose

[Scott Morrison]

What have you tried? (See also #backticks)

[Kevin Buzzard]

Is this homework? And what Scott said.

[Jose Balado]

Hi Scott, and Kevin, thanks a lot for your message.

It is not homework, I am just trying to learn Lean on my own, and I doing the exercises that I found in a Logic text book using Lean, but the book is not related at all with Lean.
In the book the relations between quantifiers are given for granted and used without demonstration. That is why I thought it to be a good idea to use theorem and then use it directly in other demonstrations.
All the exercises in the book have solutions, so for me it is more like translating them to Lean, to help me to learn how to translate natural deduction proofs into Lean. Hopefully that will help me to understand better natural deduction too.

I had to try to solve the problem again as I had deleted all that I tried. I usually just keep the solutions that work.

This what I tried but it is clearly wrong. Any hint?

theorem DG2 (α : Type*) (A : α → Prop) : (¬ ∃ x, ¬ A x) → ∀ x, A x :=
assume h : ¬ ∃ x, ¬ A x,
show ∀ x, A x, from
classical.by_contradiction
(assume h1 : ¬ ∀ x, A x,
 have h2 : ∀ x, A x, from
     classical.by_contradiction(
     assume x : α,
     assume h3 : ¬ A x,
     have h4 : (∃ x, ¬ A x), from ⟨x , h3⟩,
     show false, from h h4),
  show false, from h1 h2)

[Patrick Massot]

Do you insist on writing a proof term or would you be happy using tactics?

[Jose Balado]

Hi Patrick, thanks for your message.
I tried to learn tactics, but found it very confusing, also, proof theorem looks to me more similar to natural deduction. Maybe I am wrong?
But yes, I plan to learn tactics.

[Patrick Massot]

Ok, I'll give you a better term mode start then:

theorem DG2 (α : Type*) (A : α → Prop) : (¬ ∃ x, ¬ A x) → ∀ x, A x :=
assume h1 x,
classical.by_contradiction _

[Yaël Dillies]

You could first try showing (¬ ∃ x, A x) → ∀ x, ¬ A x. I'll let you appreciate how this is basically the definition of ∃.

[Patrick Massot]

I assume he is already past that stage

[Patrick Massot]

Anyway, I do recommend learning tactic mode. The tutorials project is hopeful good enough, and it features proving all this (in tactic mode).

[Jose Balado]

Yes, that one was easy, thanks Yael

theorem NP1 (α : Type*) (A : α → Prop) : (¬ ∃ x, A x) → ∀ x, ¬ A x :=
assume h1 : ¬ ∃ x, A x,
show ∀ x, ¬ A x, from
    (
      assume y,
      assume h2 : A y,
      have h3 : ∃ y, A y, from exists.intro y h2,
      show false, from h1 h3
    )

[Yaël Dillies]

Now, swapping the ¬ around is a matter of simplifying ¬ (¬ something) to something and hopefully you should have a clearer view by now :smile:

[Jose Balado]

oh, I said that was easy, but not, in fact I don't understand it completely. Any hit about logical principles that I can look at, to understand it better Yaël? :upside_down:
Thanks Patrick, will try that, I guess this is one of the things where Type Theory is different from Set theory. The need to assume that x to be able to do the demonstration. I think it is mentioned somewhere in Logic and Proof.

[Jose Balado]

Thanks Patrick and Yaël.

theorem DG2 (α : Type*) (A : α → Prop) : (¬ ∃ x, ¬ A x) → ∀ x, A x :=
assume h,
assume x,
classical.by_contradiction
(
  assume h1,
  have h2 : ∃ (x : α), ¬A x, from ⟨x, h1⟩,
  show false, from h h2
)

Anyway, this is weird, need to think about it. :grinning_face_with_smiling_eyes:

[Patrick Massot]

No, the keyword assume is a bit confusing but there is no difference with first order logic foundations here. In order to prove a statement starting with ∀ x, ..., the direct proof starts with "Let's fix an arbitrary x". This is what assume x is doing

[Patrick Massot]

I was answering your previous message, but we wrote at the same time

[Patrick Massot]

Great. Now you're ready to rewrite it as λ h1 x, classical.by_contradiction (λ h2, h1 ⟨x, h2⟩)

[Patrick Massot]

And this is the signal you should be learning tactic mode instead of obfuscated mode.

[Kevin Buzzard]

@Jose Balado I've just been writing lean files and YouTube tutorials for this sort of thing for my UGs -- maybe https://github.com/ImperialCollegeLondon/M40001_lean/blob/master/src/2021/logic/README.md and https://youtube.com/playlist?list=PLVZep5wTamMmeF968ovIjd-uc1I6kdirJ might help?

[Jose Balado]

yes Patrick, I see, I got it wrong, the case I was referring being different for Type theory was this:
In contrast, the statement (∀ x : U, P x) → ∃ x : U, P x is not provable in Lean.

Yes, using Lambda notation is not a problem.

Ok, I will give a try to tactics, but even this short code looks weird, I can not see how I can related this to natural deduction.

example : y = x → y = z → x = z :=
assume h1 : y = x,
assume h2 : y = z,
show x = z,
  begin
    rw ←h1,
    rw h2
  end

[Patrick Massot]

Jose Balado said:

yes Patrick, I see, I got it wrong, the case I was referring being different for Type theory was this:
In contrast, the statement (∀ x : U, P x) → ∃ x : U, P x is not provable in Lean.

I still don't see a difference. That statement wouldn't be provable in any (sound) foundation.

[Jose Balado]

@Kevin Buzzard
Everything helps, looks interesting, thanks for the link.

[Patrick Massot]

I don't understand what's wrong with your short code involving two rewrites. But I'm a mathematician so I don't know what is "natural deduction".

[Kevin Buzzard]

It's those crazy fractions I think

[Patrick Massot]

Kevin is also a mathematician :grinning:

[Kevin Buzzard]

On the Discord the other day I was telling someone that in the maths department we specialise in unnatural deduction

[Patrick Massot]

He tries to pretend but he knows there are all sorts of crazy fractions (including typing rules)

[Jose Balado]

Usually the way of presenting First Order demonstrations in first year Mathematical logic books. Like this, for example:
https://leanprover.github.io/logic_and_proof/natural_deduction_for_first_order_logic.html

:grinning_face_with_smiling_eyes:

[Jose Balado]

@Patrick Massot
To give more context about (∀ x : U, P x) → ∃ x : U, P x is not provable in Lean.

-- This is subtle: the proof does not go through if we do not declare a variable u of type U, even though u does not appear in the statement of the theorem.
-- This highlights a difference between first-order logic and the logic implemented in Lean.
-- In natural deduction, we can prove ∀x P(x) → ∃x P(x), which shows that our proof system implicitly assumes that the universe has at least one object.
-- In contrast, the statement (∀ x : U, P x) → ∃ x : U, P x is not provable in Lean.
-- In other words, in Lean, it is possible for a type to be empty, and so the proof above requires an explicit assumption that there is an element u in U.

And I think I saw that in several logic books, but, can be completely mistaken, of course. :smile:

https://leanprover.github.io/logic_and_proof/first_order_logic_in_lean.html

[Patrick Massot]

I understand this very well. But the analogue statement in set theory would not be ∀x P(x) → ∃x P(x), it would be (∀ x ∈ A, P(x)) → ∃ x ∈ A, P(x)
for some unspecified set A, and this isn't provable either.

[Kevin Buzzard]

I remember telling one of the Isabelle crowd that we'd defined a perfectoid space and they asked if we'd proved any theorems about it and I said no, and they said "oh so all you did was proved the type was inhabited?" and I said "oh no we didn't do that either"

[Kevin Buzzard]

I've never quite understood this. I have a memory from model theory lectures that they assume all models are nonempty

[Jose Balado]

Ok, I thought Set Theory and First Order Logic to be based in exactly the same foundations, aside from the Axiom of Choice. It seems they are not. Also, Type Theory feels different than Set Theory and probably better to represent other domains aside from Maths.
But my knowledge of Set Theory and Mathematical Logic is really basic, so it is just a gut feeling.

[Mario Carneiro]

Patrick Massot said:

Jose Balado said:

yes Patrick, I see, I got it wrong, the case I was referring being different for Type theory was this:
In contrast, the statement (∀ x : U, P x) → ∃ x : U, P x is not provable in Lean.

I still don't see a difference. That statement wouldn't be provable in any (sound) foundation.

Actually, this is an axiom or provable in FOL and HOL foundations

[Mario Carneiro]

the catch is that all types are nonempty in these foundations

[Eric Wieser]

false is not a type in those foundations?

[Mario Carneiro]

no

[Mario Carneiro]

in FOL, propositions are not types

[Mario Carneiro]

and this is one reason why they can't be

[Mario Carneiro]

in HOL whenever you construct a new type you have to prove it is nonempty before the construction is admitted

[Jose Balado]

@Mario Carneiro Thanks, that is really interesting.

[Patrick Massot]

Jose Balado said:

Also, Type Theory feels different than Set Theory and probably better to represent other domains aside from Maths.

I claim type theory is much closer to how mathematicians actually think than FOL+set theory.

[Patrick Massot]

It takes a bit of time to realize this because our polite lie that maths relies on set theory is an old habit. Of course the truth is math is completely foundation-agnostic.

[Mario Carneiro]

It's a soft type theory though, and defeq is definitely not a thing

[Patrick Massot]

Anyway, I should go to sleep now that my teaching is ready for tomorrow.

[Jose Balado]

Hi, is there a way to simplify this theorem? Don't like too much the idea of using two by_contradicition.
Thanks.

theorem NG1 (α : Type*) (A : α → Prop) : (¬ ∀ x, A x) → ∃ x, ¬ A x :=
assume h : ¬ ∀ x, A x,
show ∃ x, ¬ A x, from
classical.by_contradiction
(
  assume h1 : ¬ ∃ x, ¬ A x,
  have h2 : ∀ x, A x, from
  assume x,
  classical.by_contradiction(
    assume h3,
    have h4 : ∃ (x : α), ¬A x, from ⟨x, h3⟩,
    show false, from h1 h4
  ),
  show false, from h h2
)

[Eric Wieser]

I mean, you can golf it to one line as:

λ h, classical.by_contradiction $ λ h2, h $ λ x, classical.by_contradiction $ λ hA, h2 ⟨x, hA⟩

It turns out this is pretty much how mathlib proves docs#not_forall (the forward direction of which is your statement):

not.decidable_imp_symm $ λ nx x, nx.decidable_imp_symm $ λ h, ⟨x, h⟩

where decidable.not_imp_symm is basically just by_contradiction.

[Jose Balado]

@Eric Wieser Thanks Eric, will take a look at it.

[Jose Balado]

A little bit difficult for me to follow mathlib, but looks really interesting. Thanks for the link Eric