Thomas Pavel wanted that something is identical to itself. In most formal combinator theory x = x is given as an axiom, yet I did not take it. Likewise, the rule: if x = y then y = x is also given, usually, but you can prove it too!
That is very simple, but admittedly subtle, probably more difficult than all the exercises given so far, so don’t worry and feel free to look at the solution. Note that the meta-logic is the usual informal classical logic. Here is the formal theory of combinators: Three rules and two reduction axioms: 1) If x = y and x = z, then y = z 2) If x = y then xz = yz 3) If x = y then zx = zy 4) Kxy = x 5) Sxyz = xz(yz) Exercise(*): a) prove that x = x, Hint use 1) and 4). 2) prove that the rule which follows is correct: If x = y then y = x. Bruno (*) Solution (coming from a book by Rosser) below: ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; 1) x = x Proof: Kxy = y (by 4) Thus we have Kxy = x and Kxy = x, so by “1)” we have that x = x. 2) if x = y then y = x Proof Let us suppose x = y. But by the exercise just above, x = x, so now we have x = y and x = x, so by “1)” again, we have y = x. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
