X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=a8e3ca4e6968aa393b6de9e0a7a8c1d74724d7be;hp=bd86cbbf3a0cadaadc2f259b3602b5c04ff878c9;hb=1123b395aebb6b5392b3582bd0e310a8a4e32ff5;hpb=9d8dfd07484c34af18d22e3a948f76f0c9feb2b3

diff --git a/week2.mdwn b/week2.mdwn
index bd86cbbf..a8e3ca4e 100644
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -324,13 +324,13 @@ The logical system you get when eta-reduction is added to the proof system has t
 
 >	if `M`, `N` are normal forms with no free variables, then <code>M &equiv; N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.
 
-That is, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments <code>L<sub>1</sub>, ..., L<sub>n</sub></code> such that:
+This implies that, when `M` and `N` are (closed normal forms that are) syntactically distinct, there will always be some sequences of arguments <code>L<sub>1</sub>, ..., L<sub>n</sub></code> such that:
 
 <pre><code>M L<sub>1</sub> ... L<sub>n</sub> x y ~~> x
 N L<sub>1</sub> ... L<sub>n</sub> x y ~~> y
 </code></pre>
 
-That is, closed beta-plus-eta-normal forms will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
+So closed beta-plus-eta-normal forms will be syntactically different iff they yield different values for some arguments. That is, iff their extensions differ.
 
 So the proof theory with eta-reduction added is called "extensional," because its notion of normal form makes syntactic identity of closed normal forms coincide with extensional equivalence.
 
@@ -432,6 +432,7 @@ But is there any method for doing this in general---for telling, of any given co
 
 *	[Scooping the Loop Snooper](http://www.cl.cam.ac.uk/teaching/0910/CompTheory/scooping.pdf), a proof of the undecidability of the halting problem in the style of Dr Seuss by Geoffrey K. Pullum
 
+Interestingly, Church also set up an association between the lambda calculus and first-order predicate logic, such that, for arbitrary lambda formulas `M` and `N`, some formula would be provable in predicate logic iff `M` and `N` were convertible. So since the right-hand side is not decidable, questions of provability in first-order predicate logic must not be decidable either. This was the first proof of the undecidability of first-order predicate logic.
 
 
 ##[[Lists and Numbers]]##