`→`

for one-step contraction,
@@ -7,10 +7,7 @@ zero-or-more step reduction. Hindley and Seldin use
`⊳`_{1}

and
`⊳`

.
-As we said in the main notes, when M and N are such that there's some P that M
-reduces to by zero or more steps, and that N also reduces to by zero or more
-steps, then we say that M and N are **beta-convertible**. We write that like
-this:
+As we said in the main notes, when `M` and `N` are such that there's some `P` that `M` reduces to by zero or more steps, and that `N` also reduces to by zero or more steps, then we say that `M` and `N` are **beta-convertible**. We write that like this:
M <~~> N
@@ -31,11 +28,11 @@ when discussing the metatheory. Instead we'll use `<~~>` as we said
above. When we want to introduce a stipulative definition, we'll write
it out longhand, as in:
-> T is defined to be `(M N)`.
+> `T` is defined to be `(M N)`.
or:
-> Let T be `(M N)`.
+> Let `T` be `(M N)`.
We'll regard the following two expressions:
@@ -92,7 +89,7 @@ what (c) reduces to. So if we took (b) to reduce to `\y. y y`, we'd wrongly be
counting (b) to be equivalent to (c), instead of (a).
To reduce (b), then, we need to be careful to that no free variables in what
-we're substituting in get captured by binding λs that they shouldn't be
+we're substituting in get "captured" by binding λs that they shouldn't be
captured by.
In practical terms, you'd just replace (b) with (a) and do the unproblematic substitution into (a).
@@ -147,7 +144,7 @@ furthermore lack any notion of a bound position.
## Review: syntactic equality, reduction, convertibility ##
-Define N to be `(\x. x y) z`. Then N and `(\x. x y) z` are syntactically equal,
+Define `N` to be `(\x. x y) z`. Then `N` and `(\x. x y) z` are syntactically equal,
and we're counting them as syntactically equal to `(\z. z y) z` as well. We'll express
all these claims in our metalanguage as:
@@ -158,16 +155,16 @@ This:
N ~~> z y
-means that N beta-reduces to `z y`. This:
+means that `N` beta-reduces to `z y`. This:
M <~~> N
-means that M and N are beta-convertible, that is, that there's something they both reduce to in zero or more steps.
+means that `M` and `N` are beta-convertible, that is, that there's something they both reduce to in zero or more steps.
The symbols `~~>` and `<~~>` aren't part of what we're calling "the Lambda
Calculus". In our mouths, they're just part of our metatheory for talking about it. In the uses of
the Lambda Calculus as a formal proof theory, one or the other of these
-symbols (or some notational variant of them) is added to the object language.
+symbols (or some notational variant of them) is added to the object language. But only in outermost contexts. It's like the "sequent" symbol (written `=>` or `⊢`

) in [Gentzen-style proof systems](https://en.wikipedia.org/wiki/Sequent_calculus) for logic. You can't embed the `~~>` or `<~~>` symbol inside lambda terms.
See Hankin Sections 2.2 and 2.4 for the proof theory using `<~~>` (which he
writes as `=`). He discusses the proof theory using `~~>` in his Chapter 3.