satisfaction:quantifiers with conditional

Stream: general

[Ami]

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

[Mario Carneiro]

where do the parentheses go in that statement?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Ami]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

I think it's a great way of learning.

[Kevin Buzzard]

Why don't you prove Mario's example?

[Kevin Buzzard]

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

[Chris Hughes]

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