logic

Stream: new members

[BANGJI HU]

the statment below are true or false？
(∃ x : A, true) → (∃ x: A, PP x → ∀ x : A,PP x)

[Edward van de Meent]

It is true

[Edward van de Meent]

The bracketing might be a bit subtle though

[Edward van de Meent]

the statement you want is
(∃ x : A, true) → (∃ x: A, (PP x → ∀ y : A,PP y))

[Edward van de Meent]

Or at least, that version is true (for all A).

[BANGJI HU]

variable (A : Type)
variable (PP : A → Prop)

theorem existence_implication :
  (∃ x : A, true) → (∃ x : A, (PP x → ∀ y : A, PP y)) :=
begin
  assume h : ∃ x : A, true,

  have h1 : ∃ x : A, (PP x → ∀ y : A, PP y),
  {
    cases h with w hw,
    apply exists.intro w,
    assume HPPw : PP w,
    assume y : A,
    sorry
  },

  exact h1
end

[BANGJI HU]

here is my lean3 code but seem to be some problem

[BANGJI HU]

@Edward van de Meent

[Edward van de Meent]

I'm sorry, I don't know lean3 syntax

[BANGJI HU]

A : Type,
PP : A → Prop,
w : A,
hw : true,
HPPw : PP w,
y : A
⊢ PP y

[BANGJI HU]

exact HPPw?

[BANGJI HU]

@Edward van de Meent

[Edward van de Meent]

Do you understand why the statement is true? Can you explain it in words?

[BANGJI HU]

Using symbols alone rather than words always causes confusion.

[BANGJI HU]

If set A is not empty (i.e., there exists at least one element), then there exists an element x such that if x has the property PP, then all elements in set A also have the property PP.

[BANGJI HU]

so i think trivial will work

[Edward van de Meent]

the fact that this is true is not exactly trivial. the key lies in the fact that the proof uses case distinction on if PP holds for all elements or not

[Edward van de Meent]

translating that to lean should do the trick

[BANGJI HU]

(x : A, true) → ( x: A, (PP x → y : A,PP y))equivalent?

[Alex Mobius]

I suggest doing excluded-middle to the inner arrow.

[Philippe Duchon]

In words: either there exists some (y:A) such that PP y does not hold, or PP holds for all A's.

In the latter case, then the x whose existence is guaranteed by the premise can be used to prove the goal. In the former case, this y can be used (and the implication is proved differently in the two cases).

And IIRC, you do need the law of excluded middle (i.e., classical logic) for this.

[edklencl]

axiom em : ∀ (P : Prop), P ∨ ¬P
theorem excluded_middle_example {A : Type} (P : A → Prop) :
  (∃ x : A, P x) →
  (∀ x : A, P x → ∃ y : A, P y) →
  ∃ z : A, P z :=
begin

  intros h1 h2,

  cases (em (∃ y : A, ¬P y)) with case1 case2,
  {
    exact h1 },
  {
   exact h1 },
end

[edklencl]

here is my lean 3 code

[Philippe Duchon]

This is not a good example of using the excluded middle: since your first premise is just the same as your final goal, you could just use fun h1 _ => h1 (which is, in fact, what you are doing, only shorter: in both cases, your solution is h1)

(Not sure if this would be compatible with Lean 3)

[edklencl]

variable (A : Type)
variable (PP : A → Prop)

theorem existence_implication :
  (∃ x : A, true) → (∃ x : A, (PP x → ∀ y : A, PP y)) :=
begin
  assume h : ∃ x : A, true,

  have h1 : ∃ x : A, (PP x → ∀ y : A, PP y),
  {
    cases h with w hw,
    apply exists.intro w,
    assume HPPw : PP w,
    assume y : A,
    sorry
  },

  exact h1
end

[Alex Mobius]

What are you having trouble with?

[Alex Mobius]

The first "assume" in your code can probably be replaced with intro h, since it is your given.

Here's how I'd go about applying law of excluded middle here (by_cases is a tactic that applies law of excluded middle and immediately splits into cases of true and false):

import Init.Classical

variable (A : Type)
variable (PP : A → Prop)

theorem existence_implication :
  (∃ x : A, true) → (∃ x : A, (PP x → ∀ y : A, PP y)) := by
  intro h
  have ⟨ some_x, True ⟩ := h

  by_cases forall x, PP x
  case pos PP_U_true =>
    -- PP is universal
    sorry
  case neg PP_U_false =>
    -- PP is not universal
    sorry