> On 24 Oct 2018, at 18:45, Bruno Marchal <marc...@ulb.ac.be> wrote: > > Thomas Pavel
Oops. Thomas Pales. Sorry! > 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. -- 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.
