librexpr

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 construction, you can just say something like "let (N, 0, +, *) be a structure satisfying the peano axioms" and work from there.

For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly.

Why is that problematic? The constructions are isomorphic under the sentences that actually matter. This kind of statement is usually called a "junk theorem", and they are a thing in type theory too, see for example this quote from a faq by Kevin Buzzard about why Lean defines division by zero to be zero:

The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.

https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized.

Is that actually true? At the very least writing out the axioms and derivation rules is easier for set theory, since it's simpler than type theory. And there has been plenty of computer-verified mathematics done in Metamath/set.mm and Isabelle/ZF, even though less has been done than in type theory. Currently the automated tools are better for type theory, but it seems likely to me that that has more to do with how much effort has been put into type theory than any major inherent advantages of it.

---

More generally, types in type theory are also constructed! The real numbers in Lean don't come from the platonic realm of forms, they are constructed as equivalence classes of cauchy sequences. And the construction involves a lot of type-theoretic machinery which I'd usually rather ignore when working with reals, much like I'd usually rather ignore the set-theoretic construction of the real numbers. And the great thing is that I can ignore them, in either foundation!

So I just don't really buy these common criticisms of set theory, which to me seem like double standards.

((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 matter how you define division by zero.

More generally, in normal math, every theorem that involves division by some value Y which could be zero must have as hypothesis that Y is not equal to zero. All these theorems still work in systems like Lean where division by zero is defined to be zero, so nothing is lost.

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 confirmation on this being real?

https://nitter.net/ESYudkowsky/status/1664313290317795330#m

Second tweet, which is a reply:

Good they tested in sim, bad they didn't see it coming given how much the entire alignment field plus the previous fifty years of SF were warning in advance about this exact case

https://nitter.net/ESYudkowsky/status/1664357633762140160#m

Third tweet:

Disconfirmed.

https://nitter.net/ESYudkowsky/status/1664639807002214401#m

The second tweet does not explicitly say "conditional on this turning out to be real", but given that the immediately preceding tweet was expressing doubt, it is implicit from the context that that is what he meant.

"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 example. The important part is that any object can be part of a group, so if the collection of all groups existed as an object, then it would also be part of a group, indirectly containing itself and leading to paradox.

[0] https://en.wikipedia.org/wiki/Group_(mathematics)

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 correction/expansion is that (|n| args...) = n - numargs when n >= numargs. This happens to coincide with False when n = numargs + 1, so it would have been better if I had said "when n > numargs + 1".

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. This call must be toplevel, not as an argument to another function, because otherwise it is lazy and not executed. The number of args also cannot be infinite, since that would require an infinitely large program.

The expansion into |n|(args...) must happen before we know what n is, because in the lambda calculus we can't know anything about a function without calling it. Since it happens before we know what n is, then the number of args will necessarily be the same for all n. When n > numargs, |n|(args...) ignores all its arguments and halts, and therefore f cannot be a useful test for zero.

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 all of these things are considered "art". The name could be just "AI songwriting", or it could be some fancier name (like "photography" has a fancy name).

Giving it a different name would also imply that you shouldn't submit AI songs to a songwriting competition, much like you wouldn't submit a photograph to a painting competition, but you could have separate competitions for AI songs, and separate competitions that accept anything, and so on.

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 have no problem with considering GPT stuff "art", but I think it should be considered a separate art form and given a different name.

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 manually managing your own stack, especially if the tree has many kinds of objects and many branches.

Unfortunately in most languages this pattern will lead to stack overflow on medium-sized inputs, so you can't often use it unless you're using a language like Racket or Erlang which can't really stack overflow.

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 without engaging with their arguments. This does not lead to good discussion.

I think that unaligned and sufficiently smart AI could kill everyone because I looked at the arguments for and against and came to a conclusion. Presumably this is the same thing you did. I know my own mind better than you, and I'm telling you that your attempts to explain why I disagree with you are completely off the mark.

We don’t enact public policy based on predictions of a biblical apocalypse, nor do we ban televisions or computers because groups like the Amish disapprove of them.

The reason we don't do that is because we evaluate their arguments and disagree with them. It has nothing to do with who they are or why they believe what they believe.

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 about the risks of AI. You can do better than this.

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] https://www.w3.org/TR/activitypub/#x7-1-3-shared-inbox-deliv...

[1] https://github.com/mastodon/mastodon/blob/a5a00d7f7adff5e0af...

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 others, but by Tarski[0], the truth predicate cannot be defined inside the logic itself. So "the set of all numbers which cannot be described" cannot be talked about using ZF.

However, there is a way around it, by taking as axiom that ZF is consistent, choosing some model M of ZF, and then talking about the set S of numbers inside M that cannot be described.

[0] https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo...

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 classical logic, then not not P is provable in intuitionistic logic".

[0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...

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 classical logic, you can get the same contradiction in intuitionistic logic more or less by adding "not not" before both sides of the contradiction. The same applies to the axiom of choice: set theory with choice is consistent if and only if set theory without choice is consistent[1].

This means that you don't get any safety by rejecting the law of excluded middle, nor by rejecting the axiom of choice. For this reason, I think intuitionistic logic is trading away a lot of power for basically no gain.

[0] https://en.wikipedia.org/wiki/G%C3%B6del%E2%80%93Gentzen_neg...

[1] https://en.wikipedia.org/wiki/Axiom_of_choice#Independence

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 which allowed unifying effectively all of known mathematics into one theory, etc.

It's a pure naval-gazing exercise

The response to the idea [...] should be "who cares".

If anything sets back mathematics, it's when people have this kind of attitude towards the parts of math they find unintuitive.

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 or just want it to compile for now". Maybe a longer name like "assert_valid()" for the one where you're sure it's okay. That might make it easier to find the places where shortcuts were taken and forgotten.

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 beginner to understand what reasoning is allowed and what isn't allowed. However, when going back to foundations, I've found that how proofs work is surprisingly simple.

For example, in Metamath[0] (which was mentioned in another comment), there are just two inference rules. First is modus ponens[1], which says "if A is true, and if A being true implies that B is true, then B is true". Second is the rule of generalization[2], which says "if A is unconditionally true, then for all x A is true". If you start with the axiomatic statements of classical logic + set theory, pretty much all of mathematics can be inferred just by repeatedly applying these two rules to derive more true statements.

The hard part is developing a good feel for what's possible within this system and what's not, so that you can start skipping large numbers of steps too. As someone who's self-learning this stuff I've personally found exploring Metamath very helpful for this, because I find it helpful to break things down to the foundations when I'm not sure about a bit of reasoning, and Metamath is good at breaking things down to the foundations. But to each their own. Regardless, if you haven't already done so, I'd recommend learning classical logic if you want to understand proofs.

[0] http://us.metamath.org/mpeuni/mmset.html

[1] http://us.metamath.org/mpeuni/ax-mp.html

[2] http://us.metamath.org/mpeuni/ax-gen.html

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 non-trivial properties about your program and which have had practical applications, for example F* and its use in Project Everest.

https://project-everest.github.io/

https://www.fstar-lang.org/

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 basically translates to "for each non-trivial property P, there exists a program x for which it is undecidable if x has the property P", or "∀P ∃x such that it's undecidable if x has property P".

Notice that in this statement, programs are quantified using an "exists", not a "forall". Something similar holds for what you said here:

its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties

Translated to logic, this becomes "for every program y which takes as input a property and outputs a Turing Machine, there exists a property P such that the y(P) does not have property P", or "∀y ∃P y(P) does not have property P".

Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties.

As a simple example where it's possible to prove a non-trivial property, take the property "x is the identity function". This is a non-trivial property, because it is not true about all programs, nor is it false about all programs. And it is trivial to prove that the function "(n) => n" satisfies this property.

Now, I additionally think that most practical programs can have their correctness / incorrectness proven. My reason for this belief is that generally, I expect coders to understand why the code they're writing should work. If nobody understands why the code works, I'd generally consider that a bug, or at least a major code smell. But if the programmer actually understands why the code works, and hasn't made any mistakes, then in principle their understanding could be converted into a proof, because proofs are more or less just correct reasoning, but written out formally. Of course, it would still be very hard, but it's not "provably impossible".

Edit: minor text change

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 where we can prove their correctness / incorrectness. What's more, I'd argue that if you're writing code whose behaviour is literally undecidable, you're doing something wrong, unless you're doing it for research purposes or something like that.

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 package managers and cause damage. The former is fine; the latter is clearly malicious and is or should be a crime.

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:

    numbers_not_divisible_by_2_3_5_7 = []
    for i in range(520, 620):
        is_divisible = False
        for p in [2, 3, 5, 7]:
            if i % p == 0:
                is_divisible = True
                break
        if not is_divisible:
            numbers_not_divisible_by_2_3_5_7.append(i)

    print(numbers_not_divisible_by_2_3_5_7)
    print(len(numbers_not_divisible_by_2_3_5_7))

[521, 523, 527, 529, 533, 541, 547, 551, 557, 559, 563, 569, 571, 577, 583, 587, 589, 593, 599, 601, 607, 611, 613, 617, 619]

You really need to use all the primes from 2 to 13 inclusive to get a limit of 23. And even then I was only able to prove it by brute-forcing up to the primorial of 13, but maybe there's a simpler way.

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 if they have to explicitly and clearly disclaim that the derivative work has nothing to do with you. We can make this requirement last significantly longer than copyright.

And someone selling copies cheaper might give you a reputation for being too expensive, but a) that's the money issue again, and b) this can only happen after 20-50 years, at which point you've had plenty of time to build your business, and c) even after 20-50 years, you only have a problem if you were completely stagnant, because any new changes you made to the work will last 20-50 years after the most recent change.

If you don't think that this solution is sufficient, then it would seem that we've found the main point of disagreement.

You also asked:

What makes you qualified to opine on how long it takes for a creator to make “enough money”? What makes you qualified to decide that a certain amount of monetary harm is “less important”?

The way I answer these questions is by viewing money as a means to an end. I think money only matters insofar as it positively or negatively affects someone's life, so to me the question is, "to what extent is this person negatively impacted by less money 20-50 years later, compared to everyone who is negatively impacted by the restrictions on their actions?"

---

As for the rest of my comment, I was elaborating on my opinions, yes. And yes, these opinions are largely based on what seems reasonable to me. I don't have the desire nor time to do a thorough study to find the actually correct number of years, and even if I did, the question is sufficiently complicated that I expect that there would still be a lot of uncertainty left even after thorough research. In addition, since it's partially a moral issue, gut feeling will always be a necessary component of this.

Finally, your original question wasn't about concrete numbers, merely persuasiveness:

But, devil’s advocate, I haven’t heard a super convincing argument as to why something I make should ever revert to public domain, especially while I’m alive. Why shouldn’t I have the right to take my work to my grave and never have someone else profit from it?

So I don't feel bad about explaining my own point of view, which is persuasive to me even if not to you, as an attempt to answer that question.

I've been nerdsniped haha.

Just found this quora question which is the same as what you asked: <https://www.quora.com/Assume-n-1-How-can-I-prove-one-can-onl...>

But the answers seem wrong? The first one uses only the primes 2 to 7 instead of 2 to 13, but there's a reason I used 2 to 13, and it's that there's a counterexample if you use less than that. Even using 2 to 11, which is more than they use, a counterexample exists between 520 and 620, where there are 25 numbers which are not divisible by any of 2, 3, 5, 7, or 11:

[521, 523, 527, 529, 533, 541, 547, 551, 557, 559, 563, 569, 571, 577, 583, 587, 589, 593, 599, 601, 607, 611, 613, 617, 619]

For the proof by induction at the bottom of the page, I'll admit I just don't understand it, but at first glance it seems impossible to me that it would work given how short it is and it doing things that just don't seem to make sense. But maybe I'm missing something.

Regardless, having triple-checked it, I will take pride that my proof is probably correct :P

Edit: Now by double-checking this particular comment I've found that there are actually only 24 numbers between 520 and 620 which are not divisible by any prime from 2 to 11. 25 is if you use 2 to 7. This has no effect on the proof though, only this comment about the quora proofs, and even then my point stands.

(I meant 20 + 30, not 20 + 50, sorry for the confusion.)

I don't think I understand in what ways it can be damaging to reputation. Maybe you mean if I pretended to be the original author? Because in that case I think it's a different issue than copyright. You can have no copyright but still have laws about proper disclaimers and proper attribution, and I'd be in favor of that. I don't care if I have to clearly and explicitly label all my derivative works as a "fanwork", so long as I'm allowed to legally make and distribute them at all.

Other than that, you mentioned "multiple kinds of social harm". But I'm looking through your other comments on this submission, and the only other place where I've found where you explicitly state a harm is here:

That claim doesn’t hold water when the pirate is enjoying the value of the work, and is ignoring the costs of it’s creation including time.

Which as far as I can tell is just the money issue again. Sorry if I missed another harm that you mentioned, but for now as far as I can tell every harm is either money, or a harm which can be addressed by much less restrictive laws than copyright.

Now, assuming that money is the only harm of copying, which is what I believe, then it's the only issue that copyright needs to deal with. And given that copyright has harms of its own, both socially and with respect to freedom*, then once money is dealt with I think the copyright should be removed.

So then it becomes a debate on what would be a "reasonable" copyright, which would mostly avoid the "money" harm, while also mostly avoiding the harms of copyright itself. I don't think it makes sense to reward children for their parents' creation (except insofar as they might inherit money that the parent has already earned), so I think anything longer than life is already much too long.

I think 50 is more than enough, since someone making a work at 20 will be able to receive income from it until they're 70, which is almost their entire life. I think it's very rare that a work will make no money for the first 50 years but then suddenly start making money, but even in that case the author will probably have already moved on, made more works and/or made money in other ways by then, so at that point the monetary harm is less important.

I'm in favor of requiring manually registering to extend copyright past 20 because I think most works will never make money and are not intended to make money (most memes, for example), so those works should become public domain faster. I also think that most works that make money will have started doing so in the first 20 years, so it will be rare that a money-making work will unintentionally enter the public domain after 20 years.

I'll note that I'm less confident about registration than about shorter copyright. However, I view the "manual registration" as a compromise, so if we removed it and just went for a flat number of years, I would advocate for less than 50 years, maybe 30 or 40.

(*I think it's a restriction on my freedom that I have things in my head which I can't use. It wouldn't be realistic to argue that I should avoid looking at any copyrighted material my entire life, and as long as I can't feasibly do that and still take part in society, I will have ideas derived from copyrighted works and be unable to legally act on them)

Edit: I should also address startups and corporations making software. In that case, 50 years is already quite long, and the software almost never stays exactly as it is, it evolves. And every new change will last another 20-50 years. So you'll only be able to use version 20-50 years out of date, so in almost all cases the corporation will still have their competitive edge.

I'm just an amateur, but if you don't mind some brute-forcing, it's enough to prove that for every n between 1 and (2*3*5*7*11*13)/10+1=3004, exclusive of 1 but inclusive of 3004, there are at most 23 numbers between 10n and 100+10n which are not divisible by any of P={2, 3, 5, 7, 11, or 13}. Let's call numbers which are not divisible by P "potential primes". Every prime greater than 13 is a potential prime but not vice-versa.

This obviously works for the n we check manually because if there are at most 23 potential primes, there are at most 23 primes.

This also works for n greater than those we check manually, because potential primes in this set "loop" when you get past 30030. Because 30030 is divisible by every prime in P, for any x which is divisible by P, 30030 + x will also be divisible by P. Similarly, if x is a potential prime, 30030 + x will also be a potential prime. This means that there are all the same potential primes from 0 to 30030 as there are from 30030 to 30030*2, and from 30030*2 to 30030*3, and so on. Since by brute force, there was always at most 23 potential primes in the first loop (plus the beginning of the second loop, to make up for the fact that we start at n=2), then it must be true in every later loop.

Here is code that does the brute force in ruby 3, finishing the proof:

  require 'prime'
  
  def get_cycle_extended(n)
    # Get every "potential prime"
    primes = Prime.each(n).to_a
    cycle = []
    for i in 0...(primes.reduce(:*) + 200) # + 200 to be safe
      is_eliminated = false
      for prime in primes
        if i % prime == 0
          is_eliminated = true
          break
        end
      end
      cycle << i if not is_eliminated
    end
    cycle
  end
  
  p get_cycle_extended(5) # just checking that get_cycle makes sense
  
  size = 13
  cycle = get_cycle_extended(size)
  
  for n in 2..3004
    s = 10*n
    e = 100 + s
    restricted = cycle.filter { |x| (s..e).include?(x) }
    if restricted.length > 23
      raise "false at #{n}"
    else
      p restricted
    end
  end

The ability to preserve, study, and build on works is very important to me. Some of my favorite fiction is fanfiction, there are many ROM hacks and mods that improve games I've played, etc. Shorter copyright would enable these things by making them legally possible sooner. I think there would be more high-quality media and software if copyright was shorter, in the 20 to 50 years range.

I'm also not hurting anyone by making copies of things, the only negative side-effect is that the creator might make less money. On the other hand, the fact that it's illegal to make modified versions of copyrighted works, or to send them to my friends, has been a significant inconvenience in my life and to my creativity. Money for the author is important, and we make concessions for that by having copyright, but in the absence of anything else the default ought to be freedom, not copyright.

I'd go for 20 years of copyright by default, with the option of renewing up to 50 years, which ought to be long enough for the creator to make their money.

As an aside, I don't care if others sell copies of my work, that's why I prefer to release it under open-source licenses or into the public domain directly.

It didn't mess up the instruction "make every fifth line bold". The blank spaces between each "paragraph" are empty lines, so it counted them too. I think this is perfectly reasonable behavior, it's what I would have done absent further instructions too.

You can see it in the generated code on the bottom right during that part of the demo. It loops over the lines and bolds them when index % 5 == 0.

Edit: I guess with the 1-based indexing of natural languages, the code actually bolds lines number 1, 6, etc. So arguably it should have done index % 5 == 4 instead, to bold lines number 5, 10, etc. But funnily enough, if it had done that, it would have bolded all the empty lines, so it would have seemed like it didn't do anything.