← Feed

Posts

• View post

  i am not a mathematician or a computer scientist, i'm a linguist. it just so happens that i study the languages with which people express precise arguments and computations.

• View post

  I had a pretty fucking cool dad.

• View post

  A self-referential self-referential statement about self-referential statements: I can make statements about myself, like this one.

• View post

  Is there a name in category theory for the following situation? Two categories A and U with functors i : A → U and r : U → A such that for all X : U, irX retracts onto X (maybe naturally in X?). Like a "retraction up to retraction" or something. I ask because the type theoretic version of that where A : U are nested universes is enough to set up Russell's paradox (well known).

• View post

  catfishing.net #677 - 8/10 🎉 🐈🐈🐈🐈🐈 🐟🐈🐈🐟🐈

• View post

  https://www.youtube.com/watch?v=ND5dk1JnMhE

• View post

  this list escalates so quickly https://en.wikipedia.org/wiki/Copenhagenization

• View post

  Nausicaä of the Valley of the Wind (1984), in addition to being the greatest work of art ever made, contains a remarkably current (if not very subtle) metaphor for AI (hint: it is not the Sea of Decay).

• View post

  Constructive order theory puzzle! Prove that every strong total order is decidable (and conversely every decidable total order is strong), with the following definitions: A partial order is a binary relation that is reflexive, transitive and antisymmetric.A total order is a partial order in which ∀ x y. ∥ (x ≤ y) + (y ≤ x) ∥.A strong total order is a partial order in which ∥ ∀ x y. (x ≤ y) + (y ≤ x) ∥ (hence a total order).An order is decidable if ∀ x y. (x ≤ y) + ¬(x ≤ y).

• View post

  IMAGINE, IF YOU WILL, A PERSON WHO HAS BUILT HIS IDENTITY AND CAREER ON HIS LOVE AND KNOWLEDGE OF LOGIC; WHO HAS SPENT YEARS AND CONSIDERABLE MONEY STUDYING LOGIC; WHO HAS GRADUATED WITH A DEGREE IN LOGIC; WHO PERHAPS TEACHES LOGIC TO CHILDREN OR EVEN LECTURES ON IT AT A UNIVERSITY. NOW IMAGINE DISCOVERING THAT THIS PERSON HAS ONLY EVER HEARD ABOUT ONE FOUNDATION IN THEIR ENTIRE LIFE: IT IS THE ZERMELO–FRAENKEL SET THEORY.

• View post

  I've just added to my formalisation of @jemlord 's "Easy Parametricity" a short proof that every function of type (A : U) → A → A is the identity. Such a neat idea!