@SuricrasiaOnline Clearly it shifts stdout to the left 943 bits. Hope you've got those newfangled AVX modes.

actually after he's dug out of the graves in the ground, he's not called "Frankenstein's Monster", he's called "lava"

thinking back to the guy travelling to mexico to avoid the dutch covid "hysteria". to mexico, where at each entrance there is someone to measure your temperature and force you to wash your hands and put on a mask. btw, this guy was wearing a mask incorrectly in the train while explaining this plan.

endogenous and exogenous hormones

bleaugh hormones. can't live with em. can't live without em. amirite folxks

@nonphatic thats what i thought

@iitalics keysboard

anyway, the point of this story is that I want to arrange things in my Lisp so the equality-check operator, when applied to functions f g, returns the prop `∀ x, f x = g x'.

and then there can be a bit of automatic proof search that allows you to cast such props back to booleans.

i guess the formula should look more like `∀ x, is-natural x → _' to make it true. and then we'd have to define `(is-natural x)' in a clever way so that it doesn't start by inspecting the type of `x' and see if it's an int, since `τ whatever' isn't (guaranteed to be) an int.

unless we do some evil type-level hackery? might be possible to arrange that in my Lisp.

(τ is the dual to Hilbert's ε operator, i.e. τ P is the strongest counterexample to ∀ x, P x, so P(τ P) → ∀ x, P x. similarly, ε P is the weakest example of ∃ x, P x, so ∃ x, P x → P (ε x). and forall-elim / exists-intro turn this into a bi-implication.)

so you can just say like `∀ x, x = 0 ∨ ∃ y, x = y + 1' in this "logic" as (forall (λ (x) (or (= x 0) (exists (λ (y) (= x (+ y 1))))))), where `forall', `or' and `exists' are constructors and the rest just regular old Lisp values.

in unrelated news, thinking about what would happen if I wrote a hol-style verifier in Lisp. and we'd use HOAS to represent propositions.

so you have a function `(verify prop proof) -> bool' that checks `proof' is a valid proof of `prop'. and `∀ x, P x' is encoded as `(forall P)', where `P' is an arbitrary one-parameter function.

and we'd just let P have side effects, since we're in Lisp.

and forall-intro would look like `(P (τ P)) → ∀ x, P x', where `τ' is just a one-field struct constructor

- Accept-language
- nl, en;q=0.9, de;q=0.8, es;q=0.5, fr;q=0.4, Python, Haskell, Befunge, C, C++, assembly;q=0.6, Lisp;q=0.6, FORTH;q=0.2, *;q=0.1

- Content-Type
- programming; languages; maths; daily life; weird

- X-Powered-By
- English Breakfast tea with a splash of milk

Admin

/'ɑ.nə/ & legally certified as they who must become Master & (intuitionistic) maths / programming / languages & pronouns: they/them (or best offer) & tra(i)ns, crows and sheep & as seen in children's magazine & UTC+00:00 unless mentioned otherwise

"acceptably deranged" — @aeonofdiscord

Joined Jul 2019