> Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. You don't need to choose a concrete implementation. If you don't want to choose a…
((x / y) * y) = x is not a true statement about real numbers, regardless of if division by zero is defined as an error or as being equal to 0. The true statement is ( y != 0 -> ((x / y) * y) = x ), and this holds no…
Yudkowsky was not fooled. He made three tweets on this subject in that time frame, which can all be seen using this link: https://nitter.net/ESYudkowsky/search?f=tweets&since=2023-05... First tweet: > ...can we get…
"Carrier" isn't a mathematical term, they're just using that word in place of the word "set" to distinguish it from ZF sets. "Group" refers to a specific kind of mathematical structure[0], but it's just given as an…
You're right, that was imprecise of me. But if F = (\x. \y. (|n| args...)) is equivalent to True or False, then it is also equivalent to (F True False), which brings us back to a toplevel (|n| args...). Another slight…
I'm pretty sure it's impossible to write a function that tests for zero for these numerals. Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) with some number of args.…
I explicitly said that I don't mind calling it "art". I meant that things like "AI songwriting" should be given a different name than "songwriting" like "photography" has a different name than "painting", even though…
You'll note that "photography" as an art has its own name and is considered a different art than painting or drawing. And if you took a photo and then said "I drew this", people would say you were lying. So personally I…
I mostly agree, but one really nice use case for recursion is when dealing with trees. For example, writing a function parse_object() that recursively calls itself to parse child objects is way more pleasant than…
None of the comment is apt. You're seeing people you disagree with and assuming that if they disagree with you it must be because they're crazy, and then you use words like "cult" and "LARP" to try to dismiss them…
Oh my god will you people stop with the bullshit psychoanalysis. People disagree about things all the time, it's normal, you don't need to invoke this pseudo-Freudian nonsense to explain why people disagree with you…
I wish people wouldn't spread rumors like this. ActivityPub does have shared inboxes[0] and Mastodon does use them[1], so no duplicate messages will be sent in your example. [0]…
I think if we take "description of a number" to mean "ZF formula that uniquely picks out that number", then that cannot be defined, because a formula picks out a number when it is true for that number and false for all…
You might want to check out the Gödel–Gentzen negative translation[0], which is an interpretation of classical logic in intuitionistic logic, which can be (somewhat inaccurately) summarized as "if P is provable in…
Sorry, you seem to be confusing HTTPS with E2EE. Mastodon already uses HTTPS for all its traffic, including the traffic between servers.
In addition to this, I'd like to add that intuitionistic logic is consistent if and only if classical logic is. This follows from the Godel-Gentzen negative translation[0], which implies that for any contradiction in…
Cantor's work on infinity and the diagonal argument was hugely important in mathematics, paving the way for important results like Godel's incompleteness theorems, the halting problem, the creation of modern set theory…
Maybe it would have been a good idea to have two names for unwrap, one which would mean "I'm certain that this value will always be okay", and another which would mean "I'm taking a shortcut because I'm writing a script…
Mathematicians can skip a lot of steps because they have a good intuition of what's possible and what's not, so it's enough when they know that in principle something could be proven. But this can make it hard for a…
I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove…
Quoting from Wikipedia about Rice's theorem: > for any non-trivial property of partial functions, no general and effective method can decide whether an algorithm computes a partial function with that property This…
Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs…
There's a big difference between publishing the source code of malware while clearly stating that it's malware, vs publishing trojan malware on NPM while knowing that it will be automatically installed by a bunch of…
Hmm, good try, but it's not quite right. Here's a simpler way to get all the numbers divisible by 2, 3, 5, or 7, in a 100-number range, and which I think is easier to verify that it's correct:…
I did propose a solution to all these reputational damages you mentioned: requiring clearly labeling derivative works as derivative works. Someone selling something that looks like your work won't affect your reputation…
> Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. You don't need to choose a concrete implementation. If you don't want to choose a…
((x / y) * y) = x is not a true statement about real numbers, regardless of if division by zero is defined as an error or as being equal to 0. The true statement is ( y != 0 -> ((x / y) * y) = x ), and this holds no…
Yudkowsky was not fooled. He made three tweets on this subject in that time frame, which can all be seen using this link: https://nitter.net/ESYudkowsky/search?f=tweets&since=2023-05... First tweet: > ...can we get…
"Carrier" isn't a mathematical term, they're just using that word in place of the word "set" to distinguish it from ZF sets. "Group" refers to a specific kind of mathematical structure[0], but it's just given as an…
You're right, that was imprecise of me. But if F = (\x. \y. (|n| args...)) is equivalent to True or False, then it is also equivalent to (F True False), which brings us back to a toplevel (|n| args...). Another slight…
I'm pretty sure it's impossible to write a function that tests for zero for these numerals. Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) with some number of args.…
I explicitly said that I don't mind calling it "art". I meant that things like "AI songwriting" should be given a different name than "songwriting" like "photography" has a different name than "painting", even though…
You'll note that "photography" as an art has its own name and is considered a different art than painting or drawing. And if you took a photo and then said "I drew this", people would say you were lying. So personally I…
I mostly agree, but one really nice use case for recursion is when dealing with trees. For example, writing a function parse_object() that recursively calls itself to parse child objects is way more pleasant than…
None of the comment is apt. You're seeing people you disagree with and assuming that if they disagree with you it must be because they're crazy, and then you use words like "cult" and "LARP" to try to dismiss them…
Oh my god will you people stop with the bullshit psychoanalysis. People disagree about things all the time, it's normal, you don't need to invoke this pseudo-Freudian nonsense to explain why people disagree with you…
I wish people wouldn't spread rumors like this. ActivityPub does have shared inboxes[0] and Mastodon does use them[1], so no duplicate messages will be sent in your example. [0]…
I think if we take "description of a number" to mean "ZF formula that uniquely picks out that number", then that cannot be defined, because a formula picks out a number when it is true for that number and false for all…
You might want to check out the Gödel–Gentzen negative translation[0], which is an interpretation of classical logic in intuitionistic logic, which can be (somewhat inaccurately) summarized as "if P is provable in…
Sorry, you seem to be confusing HTTPS with E2EE. Mastodon already uses HTTPS for all its traffic, including the traffic between servers.
In addition to this, I'd like to add that intuitionistic logic is consistent if and only if classical logic is. This follows from the Godel-Gentzen negative translation[0], which implies that for any contradiction in…
Cantor's work on infinity and the diagonal argument was hugely important in mathematics, paving the way for important results like Godel's incompleteness theorems, the halting problem, the creation of modern set theory…
Maybe it would have been a good idea to have two names for unwrap, one which would mean "I'm certain that this value will always be okay", and another which would mean "I'm taking a shortcut because I'm writing a script…
Mathematicians can skip a lot of steps because they have a good intuition of what's possible and what's not, so it's enough when they know that in principle something could be proven. But this can make it hard for a…
I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove…
Quoting from Wikipedia about Rice's theorem: > for any non-trivial property of partial functions, no general and effective method can decide whether an algorithm computes a partial function with that property This…
Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs…
There's a big difference between publishing the source code of malware while clearly stating that it's malware, vs publishing trojan malware on NPM while knowing that it will be automatically installed by a bunch of…
Hmm, good try, but it's not quite right. Here's a simpler way to get all the numbers divisible by 2, 3, 5, or 7, in a 100-number range, and which I think is easier to verify that it's correct:…
I did propose a solution to all these reputational damages you mentioned: requiring clearly labeling derivative works as derivative works. Someone selling something that looks like your work won't affect your reputation…