Zulip Chat Archive

Stream: general

Topic: satisfaction:quantifiers with conditional


view this post on Zulip Ami (May 25 2020 at 19:19):

Assume that we have this formula: Q=∀x(∀yAy→Bx). if ∀yAy is false, can I conclude that Q is satisfied?

view this post on Zulip Mario Carneiro (May 25 2020 at 19:21):

where do the parentheses go in that statement?

view this post on Zulip Mario Carneiro (May 25 2020 at 19:23):

if you mean Q=x,((y,A(y))B(x))Q=\forall x, ((\forall y, A(y))→B(x)), then yes - if y,A(y)\forall y, A(y) is false then (y,A(y))B(x)(\forall y, A(y))→B(x) is true (for all xx), which is the statement of QQ

view this post on Zulip Mario Carneiro (May 25 2020 at 19:26):

Can you prove it?

import tactic

variables {α : Type*} (A B : α  Prop)
def Q :=  x, ( y, A y)  B x

example (h : ¬  y, A y) : Q A B := sorry

view this post on Zulip Ami (May 25 2020 at 19:51):

Thank you. I got this. What confuses me is that If I start to replace variables with constants, for instance A(2)=True and B(2)=False, Then I have a false conditional A(2)→B(2). I can not see this when I evaluate this formally and I do not understand why this example does not show that Q is not satisfied.

view this post on Zulip Kevin Buzzard (May 25 2020 at 19:59):

Why don't you formalise what confuses you in Lean?

view this post on Zulip Kevin Buzzard (May 25 2020 at 19:59):

I think it's a great way of learning.

view this post on Zulip Kevin Buzzard (May 25 2020 at 20:01):

Why don't you prove Mario's example?

view this post on Zulip Kevin Buzzard (May 25 2020 at 20:02):

import tactic

variables {α : Type*} (A B : α  Prop)
def Q :=  x, ( y, A y)  B x

example (h : ¬  y, A y) : Q A B :=
begin
  show  (x : α), ( (y : α), A y)  B x,
  sorry
end

view this post on Zulip Chris Hughes (May 25 2020 at 20:11):

If you put the brackets in a different place, then it won't necessarily be true. x,(y,(A(y)B(x)))\forall x, (\forall y, (A(y) \to B(x))) won't necessarily be true. That's probably the source of the confusion.


Last updated: May 10 2021 at 00:31 UTC