2

I am (sort of) familiar with inductive proofs about wffs, but proofs by induction about terms took me by surprise.

Prove by Induction that:

if variable assignments q, q' agree on all variables in term t, then $$ \overline{q}(t) = \overline{q'}(t) $$

I believe I have my base case, at least:

1) If t is a (free?) variable x, then, trivially, if q(x) = q'(x), then $$ \overline{q}(t) = \overline{q'}(t) $$

Hopefully, this is somewhat correct. But it is the next step, the inductive step, that I have no idea how to procede with. We have defined a term to be either a variable, a contant, or a function (taking terms). So I am guessing I now have to prove the same principle holds for constants and functions. Am I right? If so, how would one start such a proof? (There is of course also the very likely possibility I have gotten all the above wrong ...)

tom tronbone
  • 423
  • 1
    For constant , you have to consider that they have no variables "inside"; so the assertion is vacuously true. – Mauro ALLEGRANZA Nov 14 '14 at 13:10
  • 1
    Having proved the base case (variables and constants) you have to proceed by induction to show that the property holds for $f^n(t_1, \ldots, t_n)$ assuming that it holds for $t_1,\ldots, t_n$. – Mauro ALLEGRANZA Nov 14 '14 at 13:12
  • @MauroALLEGRANZA Thank you very much. 1) So, two variable assignments will also have a constant denote the same? 2) Ok, so my base case includes both variables and constants (not just variables as I wrote)? 3) So there's only 1 inductive step, then? – tom tronbone Nov 14 '14 at 13:26
  • 1
    A constant $c$ denotes an object $c^*$; does the "denotation" of the symbol $c$ depends on some variable $x$ ? NO. So $q(c)=q'(c)$ for every $q,q'$. – Mauro ALLEGRANZA Nov 14 '14 at 13:36
  • 1
    Yes; we have two "base" cases : variables and constants, and one "inductive step" : $f^n(t_1,…,t_n)$. – Mauro ALLEGRANZA Nov 14 '14 at 13:37

0 Answers0