• @funkless_eck
    link
    English
    42 months ago

    seems a little sus to use + to define +

    • @[email protected]
      link
      fedilink
      English
      92 months ago

      No, it’s correct. You define the operation by it’s properties. It’s not saying that “a plus 0 = a” but “the result of applying the binary operation ‘+’ to any number with 0 should give the original number.”

      • is just a symbol. You could instead write it as +(a,0)=a and +(a,S(b))=S(+(a,b)).

      You have to have previously defined 1=S(0), 2=S(1), 3=S(2), and so on.