Just a typo error correction I hope you have spotted it
> On 24 Oct 2018, at 18:45, Bruno Marchal <[email protected]> wrote: > > 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) Kxy = x. (Of course) > 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 [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/d/optout. -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
