MercurialBlack,
@MercurialBlack@pleroma.mercurial.blog avatar

Describing the number 2 like there exists a z there exists a y there exists an x x in y and forall k k notin x and forall j j = x or j not in y and forall i i = x or i = y or i not in z

Ukko,
@Ukko@akko.disqordia.space avatar

@MercurialBlack just define it instead idiot. type Nat = O | S Nat. val 2 = S (S O).

MercurialBlack,
@MercurialBlack@pleroma.mercurial.blog avatar

@Ukko we don't have peano arithmetic yet

Ukko,
@Ukko@akko.disqordia.space avatar

@MercurialBlack what basis is there for the number 2? Is it just the classic "let's assume 2 exists and just describe it with 5000 theorems making sure no other number fits"?

MercurialBlack,
@MercurialBlack@pleroma.mercurial.blog avatar

@Ukko it's the smallest set with the property that 0 < 1 < 2, which is done with \in. 0 is defined as {}, and all other numbers are defined recursively as x U {x}.

It's the second smallest element of the smallest inductive set.

Ukko,
@Ukko@akko.disqordia.space avatar

@MercurialBlack isn't that literally peano arithmetic

MercurialBlack,
@MercurialBlack@pleroma.mercurial.blog avatar

@Ukko I wish. I can't figure out how to use recursive definitions.

nyoom,
@nyoom@akko.disqordia.space avatar

@MercurialBlack @Ukko why cant you just write it out as {{}, {{}}, {{}, {{}}}}?

Ukko,
@Ukko@akko.disqordia.space avatar

@nyoom @MercurialBlack the forall notin mess looked better

  • All
  • Subscribed
  • Moderated
  • Favorites
  • random
  • Hentai
  • doujinshi
  • announcements
  • general
  • All magazines