> 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.
> 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.
> 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
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.
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.
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.
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".
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.
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.
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.
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.