## Stream: general

### Topic: satisfaction:quantifiers with conditional

#### 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?

#### Mario Carneiro (May 25 2020 at 19:21):

where do the parentheses go in that statement?

#### Mario Carneiro (May 25 2020 at 19:23):

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 (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


#### 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.

#### Kevin Buzzard (May 25 2020 at 19:59):

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

#### Kevin Buzzard (May 25 2020 at 19:59):

I think it's a great way of learning.

#### Kevin Buzzard (May 25 2020 at 20:01):

Why don't you prove Mario's example?

#### 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


#### Chris Hughes (May 25 2020 at 20:11):

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.

Last updated: May 10 2021 at 00:31 UTC