I was trying to do exercise 1 on page 30 from some logic notes. The question was to show:
$$ {t^*}^{\mathcal A}(a_1,\dots,a_n) = t^{\mathcal A}(\tau_1^{\mathcal A}(a_1,\dots,a_n),\dots,\tau_m^{\mathcal A}(a_1,\dots,a_n))$$
I was trying to do it by induction on length of L-terms. I was having trouble with the base cases. When $|t^*|=1$ then its either a variable or a constant. Lets consider the constant which seems easier. In that case ${t^*}(y_1,\dots,y_n) = t(\tau_1(y_1,\dots,y_n),\dots,\tau_m(y_1,\dots,y_n)) = \underline c$ for some $\underline c \in L^f$. What confuses me is what happens to the above once we bring the interpretation in the given L-structure $A$. What is clear to me is:
$$t(\tau_1(_1,\dots,y_n),\dots,\tau_m(y_1,\dots,y_n)) = \underline c $$
if we interpret $t$ in $\mathcal A $we would get:
$$t^{\mathcal A}(\tau_1(a_1,\dots,a_n),\dots,\tau_m(a_1,\dots,a_n)) = \underline c^{\mathcal A} = c$$
whats not specifically clear to me is if I can just bring in the interpretation inside to the tau's also. If I did that it feels like cheating, nearly as if I just asserted what I wanted to prove instead of actually proving it. Or am I allowed to just pretend that I can evaluate $\tau^{\mathcal A}(a_1,\dots,a_m)$? Like it feels very weird to me to assert:
$$ t^{\mathcal A}(\tau_1^{\mathcal A}(a_1,\dots,a_n),\dots,\tau_m^{\mathcal A}(a_1,\dots,a_n)) $$
without proof or anything. I thought that exactly what we wanted to prove, that evaluating the top L-term trickled down to the remaining L-terms. What exactly makes:
$$ {t^*}^{\mathcal A}(a_1,\dots,a_n) = t^{\mathcal A}(\tau_1^{\mathcal A}(y_1,\dots,y_n),\dots,\tau_m^{\mathcal A}(y_1,\dots,y_n)) = \underline c^{\mathcal A}$$
correct?
Intuitively I know that evaluating $t$ gives just out the constant and that we can ignore whatever was fed into the L-term since we are just outputting the constant regardless. Is that why its valid? Because we would have ignored the input not matter what it was and if it was $\tau^{\mathcal A}(a_1,\dots,a_n)$ or any other element of A would have not mattered.
Regardless of the answer, it seems that assuming $\tau^{\mathcal A}(a_1,\dots,a_n)$ evaluates to something assuming the hypothesis (i.e. $\tau$ could be any arbitrary L-term, including of the ones in the form of the theorem we are trying to prove. Thus, it might be we need to assume the theorem to be true about composite L-term evaluation for us to assume $\tau^{\mathcal A}$ evaluates to something sensible). So as far as I can tell that should be part of the induction hypothesis (or its only valid to say we have access to tau evaluated on the L-structure by the induction hypothesis, since that could also be of the same for as our hypothesis). So the crux:
$$\tau^{\mathcal A}(a_1,\dots,a_n)$$
is actually something I can assume I can do without assuming what I am trying to prove?
Answer
Just to be clear about notation, $t(x_1,\dots,x_m)$ is a term, $\tau_i(y_1,\dots,y_n)$ are terms for all $1\leq i\leq m$, and $t^*(y_1,\dots,y_n)$ is the composite term $t(\tau_1(y_1,\dots,y_n),\dots,\tau_m(y_1,\dots,y_n))$.
I'm confused about why you write "assuming $\tau^\mathcal{A}(a_1,\dots,a_n)$ evaluates to something assumes the hypothesis" and "am I allowed to just pretend I can evaluate $\tau^\mathcal{A}(a_1,\dots,a_n)$?". Given any structure $\mathcal{A}$ and any term $\tau(y_1,\dots,y_n)$, there is a function $\tau^\mathcal{A}\colon A^n\to A$ (this is the first definition on p.29 of your notes). So yes, of course you can evaluate $\tau^\mathcal{A}(a_1,\dots,a_n)$. This is not what the problem is about.
Ok, so as for handling your concern about the base case. Suppose $t(x_1,\dots,x_m)$ is the constant symbol $c$. Then also $t^*(y_1,\dots,y_n)$ is the constant symbol $c$, and the evaluations $t^\mathcal{A}\colon A^m\to A$ and $t^{*\mathcal{A}}\colon A^n\to A$ are both constant functions with value $c^\mathcal{A}$.
So the left-hand side of the equation you're supposed to show is $t^{*\mathcal{A}}(a_1,\dots,a_n) = c^\mathcal{A}$. For the right-hand side, suppose $\tau_i^\mathcal{A}(a_1,\dots,a_n) = b_i$. Then we have $$t^\mathcal{A}(\tau_1^\mathcal{A}(a_1,\dots,a_n),\dots,\tau_m^\mathcal{A}(a_1,\dots,a_n)) = t^\mathcal{A}(b_1,\dots,b_m) = c^\mathcal{A}.$$
You write "Intuitively I know that evaluating $t$ gives just out the constant and that we can ignore whatever was fed into the $L$-term since we are just outputting the constant regardless. Is that why its valid?" Yes!
No comments:
Post a Comment