Formal proof of implication

Question

I am currently stuck on this particular task. I need to formally prove that

(∃a ∀b (b<a)) → (∀a ∃b (a<b))

Now, what I have so far is that I need to prove that the above implication is a tautology, and that my premises are (∃a ∀b (b<a)) A and (∀a ∃b (a<b)) B.

I am not sure where to go next...

I tried assuming that A is True. Next I assume that A→B is True. Using Modus Ponens if A and A→B are True I can prove B. Therefore, if A and B are True the implication of both must be True. But I am not convinced this works.

Alternatively I tried assuming A is true. If A is true it means ∃a ∃b (b<a) is also true. That means there must be a b that satisfies the same condition? If a and bare swapped? So ∃a ∃b (a<b)? and then somehow deduce ∀a ∃b (a<b)?

Any help would be appreciated, thanks!

Answer 1

I tried assuming that A is True. Next I assume that A→B is True.

That is clearly awry. Never assume the thing that you want to prove. You should assume $A$ then derive $B$ under that assumption, so that you may deduce that $A→B$ holds.

Alternatively I tried assuming A is true. If A is true it means $∃a ∃b (b<a)$ is also true. That means there must be a b that satisfies the same condition? If a and b are swapped? So $∃a ∃b (a<b)$? and then somehow deduce $∀a ∃b (a<b)$?

Not quite. You don't derive an existance from an universal.

But the technique you need is alpha-replacement.   We can safely substitute the bound term with any token that does not already occur within the scope of the quantifier.   So think of it as proving $\exists a~\forall b~(b<a)\to \forall b~\exists a~(b<a)$ then juggling the letters.

• Begin
  • Assume $\exists a~\forall b~(b<a)$
    • Let $y$ be an arbirary term.
      • Let $x$ be a witness for the assumption.
      • $\forall b~(b<x)$ via instantiation of existential bound $a$ to witness $x$.
      • $y<x$ via instantiation of universal bound $b$ to arbitrary $y$.
    • $\exists b~(y<b)$ via generalisation of witness $x$ to existential bound $b$.
  • $\forall a~\exists b~(a<b)$ via generalisation of arbitrary $y$ to universal bound $a$
• Done: $\exists a~\forall b~(b<a)\to \forall a~\exists b~(a<b)$

Answer 2

I will assume you are stating this for real numbers (that is to say, you omit to write "$\in \Bbb R$" in the quantifiers). Suppose that A is true, so that there exists a number $a$ such that for every number $b$ the relation $b<a$ holds; if $c$ is any number, then $c<a$ hence B holds. So, A implies B as desired.

Answer 3

When you have to prove that some sentence of the form "$(\forall x\in X)\,P(x)$, you should start by : "Let $x$ be some element of $X$, let's prove $P(x)$".

Here, suppose "$(\exists a_0)(\forall b)\, b<a_0$" is true. Let's prove "$(\forall b) (\exists a)\, b<a$" (I changed the letters, to simplify the proof).

So let $b$ be some element. The $a_0$ given by the hypothesis is now a good candidate for the conclusion : let $a=a_0$, we have $b<a$, so that the conclusion is true.

What you have to understand is that in "$(\exists a)(\forall b)\, P(a,b)$", the "$a$" is the same for every $b$. In "$(\forall b) (\exists a)\, P(a,b)$", $a$ is dependent on $b$ : you can chose it after $b$ has been given.

One final note : your "$<$" relation is quite odd : of all the $b$ that must verify $b<a$, there is in particular $a$, so $a$ should verify $a<a$. Maybe a bad notation ? At least a confusing one :-)

Answer 4

Assume $$\tag1\exists a\forall b(b<a).$$ Accordingly, let $a_0$ such that $$\tag2\forall b(b<a_0).$$ We want to show (based on the hypothesis $(1)$) that $\forall a\exists b(a<b)$. So let $a$ be arbitrary. By specialization from $(2)$, we have $a<a_0$. So by letting $b=a_0$, we have $a<b$, i.e., $\exists b(a<b)$. As $a$ was arbitrary, we showed $$ \forall a\exists b(a<b).$$ As all this happend under the hypothesis $(1)$, we have $$\exists a\forall b(b<a)\to\forall a\exists b(a<b). $$