Induction on 2 variables

[pkim]

Is it possible to use induction on two variables at the same time?

as in (foo x) ^ (foo y) -> (foo x y)

sigma: {x <- (cdr x) , y <- (cdr y)

Thanks

[Ian W.]

This is not (necessarily) an example of induction on two variables at
once, a technique which we have not covered in this class. Induction
on a single variable v requires a car/cdr instantiation of v, and any
instantiation of other variables. In this case, both your
instantiations of x and y are car/cdr instantiations, so this could be
part of an induction hypothesis on either variable. In any case, your
choice of sigma is safe. Another example of a legal induction on x
would be sigma = {x -> (cdr x), y -> (foo (bar (baz z y w)))}.

Ian

[Behnam Robatmili]

Hi all,

In my extended office hours on Tuesday, we had a long debate about
part 6 of question 3. I'm now fully confident that my answer is correct:

6- If every relative of x is happy, then x is happy

(forall e in A: R(x, e)->(happy e)) -> (happy x)

Let me do this step by step:

If "every relative of x is happy", then "x is happy"
Assuming (P x) = "every relative of x is happy" and (Q x) = "x is
happy", then the answer will be in form (P x) -> (Q x)
Obviously (Q x) = (happy x)
Lets talk about (P x). It checks if every relative of x is happy. So
for every element e in A, if e is a relative of x then the formula
checks if e is happy. That gives us (forall e in A: R(x, e)->(happy e))
Notice that it is different from (forall e in A: R(x, e)^(happy e)),
which means every object is a relative of A and happy!

So the final answer is: (forall e in A: R(x, e)->(happy e)) -> (happy x)

There was a question in the class that caused some doubts: If e is a
relative of x and is not happy then the forall part in our answer
returns false and so the whole formula returns true! That is true, but
it doesn't violate our answer! The statement says "if every relative
of x is happy, then x is happy." It doesn't say "if a relative of x is
not happy, then x is not happy." In other words, x being happy doesn't
mean that all its relatives are necessarily happy!

Does that make sense? Please let me know if you have question.

Behnam

[Anar Seyf]

Makes sense. What would the answer be to this:

IFF every relative of x is happy, then x is happy
(that is, x is happy ONLY if every relative is happy)?

[Behnam Robatmili]

Yes, but also vice versa meaning that every relative is happy when x
is happy. In other words, I think it becomes: (P x) <-> (Q x) in which
P and Q are the same as in my previous email (other TAs can also
comment on this).

Does that make sense?

Behnam