I would really want to see there Go with their goroutines, Kotlin with their coroutines, and good old Java with their CompletableFuture vs. virtual threads (and compare that with non-continuation ThreadPoolExecutor).
IMO the discussion without Go is really lacking, as it's the whole point of Go.
Yet at the same time federal government allowed home insurance to be non-actuarial (aka insolvent) for natural disasters like hurricanes. So essentially the rest of the country subsidise residents in disaster-prone areas. So Californians pay to make home insurance lower for Floridians.
It's true that the National Flood Insurance Program does this, but that's only for flooding (which, admittedly, is a big part of hurricane damage...). Flood coverage is however not a standard rider on homeowner's insurance policy products, and I'm also unsure whether it can ever be. I've only ever seen it offered as an additional policy product.
The concern over pricing below the actuarially fair value is well-placed[0], but I'd urge being precise.
Taxpayers. Imo if we didn't have such high national debt in the US, those interest payments to the debt could have instead been used for something like national health insurance. The politicians of the past really screwed us all with the debt.
There was a bit of a mitigating circumstance of COVID (for Trump and Biden), which caused the debt to jump for many countries as well (and not just the US), but it's not like Trump et co are helping the math along with all the tax cuts and asking for a US$ >1T military budget.
If she's anything like my mom, i.e. someone who has been using computers for a while now but never had the confidence to experiment with it, any small change will freak her out and there really is a long tail of those. It's not a matter of Linux not being good enough, being different is already a real problem.
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.
I always wanted to, say, look at any theorem and see what axiomatic it requires. Or in other way, see the theorem tree like in the article under a different set of axioms.
Of course, for some results there are proofs discovered only under one axiomatic, but it's true under some others as well, just the proof wasn't discovered yet.
If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.
It simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element.
I mean this quite seriously: have you considered reading any first course in set theory?
As I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)
Godel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims
you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.
That increases the likelihood that they are right.
> support your point with explanation or be ignored :-)
Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.
A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong
coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.
I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory.
Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.
ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it.
Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.
Eh? Any first course in set theory will present ZFC as a one-sorted theory with ten axioms (/schemas) in first order logic (inheriting an equality symbol, forall, implies etc) with one binary predicate (namely set membership), or will present a theory that is equiconsistent with a usual ZFC presentation. Honestly I’m not sure how you simultaneously claim to be a PhD in formalisation and also not be aware of the existence of Isabelle/ZF, for example.
I referred to specific definition in wikipedia.
Your "first course notes" are irrelevant here, they can't be reviewed, they not proofread and unlikely can be considered as any reasonable quality if we are talking about real formalization of math.
its hard to me to tell what this means formally(as I said I am not expert).
There is no "interpret" operator in zfc.
I believe what it says if you add some robinson axioms + some logical rules on top of zfc, you can carry your results.
It's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given.
You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.
You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
No, once you start formalize this, it becomes complicated. There is a reason why looks like there is no "peano can be derived from zfc" theorem which would close dispute, and my opponents need to throw links on bro math from stackexchange in this discussion.
Would be good to see witnesses description text after the case reveal. E.g. I kinda remember text says "black eyebrows" but the image clearly shows white eyebrows, would be cool to review.
reply