From: Jim Pryor Date: Mon, 20 Sep 2010 02:27:59 +0000 (-0400) Subject: week2: tweak, undecidability of pred logic X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6e55a9652a8a082eceb8efaa0eedbce91a79716f week2: tweak, undecidability of pred logic Signed-off-by: Jim Pryor --- 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 `M ≡ N` 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 `L1, ..., Ln` 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 `L1, ..., Ln` such that:
``````M L1 ... Ln x y ~~> x
N L1 ... Ln x y ~~> y
``````
-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]]##