Timeline for "local variables" in first-order formulas
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 17, 2021 at 16:20 | comment | added | Pineapple Fish | It seems to be that the way in Enderton's book is much more practical when supplemented with extension by definition; en.wikipedia.org/wiki/Extension_by_definitions . Because Enderton's solution still doesn't allow you to arbitrarily substitute (and it shouldn't), but what you can do is make a new predicate variable, then use this theorem in Enderton's book, and voila, using metatheory you can prove you now have a WFF/expression with the same meaning into which you can substitute anything! | |
| Dec 17, 2021 at 16:11 | comment | added | Pineapple Fish | So would this be a good illustration of how to use this in practice: you have defined $x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y)$ so generalizing $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$ but then you can't substitute $x$ or $y$ in for $z$ (even if you're trying to prove something as simple as $z=z$) so instead you first prove that $\forall x\forall y(x=y\leftrightarrow\forall t(t\in x\leftrightarrow t\in y))$ (which is logically equivalent to the first WFF) and you are now free to substitute in for $z$ and prove things like $z=z$ | |
| Oct 12, 2011 at 1:16 | comment | added | Chad Musick | You can find an explicit construction of this in Muchnick's "Advanced Compiler Design & Implementation" in the section on static single-assignment form (SSA). | |
| Oct 11, 2011 at 19:18 | history | answered | Carl Mummert | CC BY-SA 3.0 |