I'm taking an advanced symbolic logic class where we're using substitution a lot to handle for-all and existential statements. One thing that occurs to me is that, according to our textbook, The Incompleteness Phenomenon: A New Course in Mathematical Logic, I can make a sentence more complex, but I can't go back the other direction. For example, let's say I have the sentence:
( x + y > 2y + 2 )
I could allow the replacement:
t = (6z + 9i)
( x + y > 2y + 2 )(x/t)
= ( (6z + 9i) + y > 2y + 2 )
But as far as I am aware, there's no real way for me to go the other direction, i.e.,
( x + y > 2y + 2 )(t/x)
Am I wrong? If I'm right that I can't go "back" to a less complex sentence through substitution, are there other acceptable techniques for abstracting complex sentences "back" to more simple ones?
Note that I use t to signify an M-term, and x, y, and i to be variables (in this case free ones) in a sentence here.
You can come up with a meaningful definition of what it means to substitute terms for terms in a term, but the technical details are a bit tricky and it's rarely needed. (I have never seen it in the logic literature, but only in computer implementations of logical systems.)
If you want to talk about the relation between a (postulated) abstraction and a (given) instantiation, why not just use existential quantification in the meta-language: $\phi$ is a possible abstraction of $\psi$ iff there is a variable $x$ and a term $t$ such that $\phi[t/x] \equiv \psi$. You don't need to define the notion $\phi[x/t]$ to do this.