equivalent formulation of substitutability
We do induction on the complexity of .
If is atomic, then any is free for in , and clearly is just , which has no bound variables.
If is of the form , then is free for in iff is free for in both and iff no variables in are bound in either or iff no variables in are bound in .
Finally, suppose is of the form . Since is free in , is not , and is free for in iff is not in and is free for in iff, by induction, is not in and no variables of are bound in iff no variables of are bound in , which is just (since ).
If does not occur free in (either occurs bound in or not at all in ), then is obviously free for in , but is just , and there is no guarantee that variables in are bound in or not.
In the special case where is a variable , we see that is free for in iff is not bound in , provided that occurs free in . In other words, is free for in iff no free occurrences of in are in the scope of , where is either or . So if is not bound in , is free for in , regardless of whether is free or bound in . Also, is always free for in .
|Title||equivalent formulation of substitutability|
|Date of creation||2013-03-22 19:35:57|
|Last modified on||2013-03-22 19:35:57|
|Last modified by||CWoo (3771)|