tag:blogger.com,1999:blog-9871512.post115919038533924419..comments2022-09-03T20:56:46.577-04:00Comments on Tumbolia: Metamath isn't hygienicjtohttp://www.blogger.com/profile/03968844388108605008noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-9871512.post-33109524947333755692007-01-12T14:05:00.000-05:002007-01-12T14:05:00.000-05:00Yep. Metamath uses something called "disjoint var...Yep. Metamath uses something called "disjoint variables" to make sure that "x not in s".<br /><br />See the <a href="http://jorendorff.blogspot.com/2006/09/metamath-responds.html">follow-up post</a> for more details.jtohttps://www.blogger.com/profile/03968844388108605008noreply@blogger.comtag:blogger.com,1999:blog-9871512.post-66667620801147790232007-01-12T11:47:00.000-05:002007-01-12T11:47:00.000-05:00It the variable does not occure in a bound context...It the variable does not occure in a bound context, and if the context is not bound by the variable either or the substituent does not contain the context variable either, than no harm can happen.<br /><br />Or symbolically<br /><br /> (lambda x.t)[y/s] = <br /> lambda x.(t[y/s]) <br /><br /> for x<>y and x not in s<br /><br />ByeAnonymousnoreply@blogger.com