I'd like to plug the NIWA wiki network for Nintendo games. I think more independent wikis should federate in similar ways, to strategize beyond just search engine hits.
I love philosophy Calvinball, so I would counter by asserting that undetectable implies no possession, an immediate contradiction. Or go further and assert that undetectable implies nonexistence. We all possess an immense undetectable nonexistent sphere. No bounds on assumptions means I can make up anything to annoy the interlocutor.
So, you're right. This shows why we should use formal math, so we can agree on the result yet bicker about the interpretation. Some folks point to Cantor's diagonalization theorem to show that some unnameable things exist, when the theorem doesn't say that at all.
No surjective function exists from names to real numbers (diagonalization). With any naming scheme, some unnamed real numbers always remain.
On the other hand, given any real number, I can name it. I'll run out of unique names, since no injective function exists from real numbers to names.
So, some unnamed real numbers will always remain (non-constructively), I can make real numbers that escape a naming scheme (constructively), and no unnameable real numbers exist.
My hidden assumption: I said the set of names must be countable! I assumed you would know that naming means assigning a finite string (in the Ithkuil writing system of course). and don't nitpick further or else I'll have to write a proof in Agda or Rocq lol
You proved that definable implies nameable, and also unnameable implies undefinable. Obviously true. However, the idea of undefinable real numbers closely resembles a modern version of the paradox. No surjective function exists from definitions to real numbers.
Really, the blurb about "seems impossible to verify this by giving positive instances" contains the tension between constructive math and non-constructive math. Does an unnameable (and undefinable) thing actually exist? If a tree falls in a forest, but no one can hear it, does it make a sound?
> No surjective function exists from definitions to real numbers.
I'm not really up on maths so this is possibly a stupid question, but can't any real number be written as an ASCII string, which is basically an integer number, so there is a direct mapping there?
Or is it because the ASCII number wouldn't be in order that makes the difference?
Or is it that you can't write that mapping as a mathematical function perhaps?
It's because most real numbers are uncomputable. That means, most of the time, the only way to check that two numbers (i.e. names) are the same is to spend infinite time looking at all their infinite digits.
I love approval voting the most by pure simplicity and effectiveness. How does score voting work better than STAR? I thought STAR degenerates into score voting when clone candidates run?
I haven't heard much of an argument against proportional voting before. Your article just casts doubt, but doesn't really make a decisive argument against. I actually don't like proportional voting because it reifies parties into the system, but I only support it because I think it can break the party duopoly and step towards better systems. I should rethink that.
Not really. Math uses no physical observation, only axioms. Nothing can "prove" or "disprove" axioms. However, if observation supports the axiomatic theory, then we use the theory for physical prediction. If observation doesn't, then we don't use the theory. Does that count as "disproof"?
In practice, infinite sets never exist as enumerations of every element, but as ways to generate more elements along with descriptions for which elements to include. Infinite set theories allow for equivocating a finite description with the infinite enumeration. In contrast, programming languages usually make a distinction between data (always finite) and data generation (possibly infinite). I would think that counts as a "disproof" in a way.
This was the answer I was looking for. You're reminding me that existence of infinity is an axiom, like parallel lines dont intersect. We can remove that axiom and get a new mathematical framework, but by their nature, axioms are not something to prove or disprove.
Exactly. For example, John Mayberry wrote "The Foundations of Mathematics in the Theory of Sets" (2000). Half of the book consists of philosophical arguments for his "Euclidean set theory" contrasted against the big bad "Cantorian set theory". He takes inspiration from Euclid's common notion 5 "the whole is greater than the part". On page 277, formula 8.3.1, his Axiom of Euclidean Finiteness goes like this: any injective endofunction is also surjective, ∀f∀Y((f:Y→Y ∧ 1to1(f)) ⇒ onto(f)).
I've come to believe that many related incompatible theories have interpretations between each other. For example, hyperbolic geometry has a Euclidean-like Poincare disk model, and Euclidean space exists locally in a hyperbolic space. Boolean logic contains intuitionistic logic (just add the law of excluded middle), but intuitionistic logic contains Boolean logic through the double negation translation. Similar might happen for finite set theories, infinite set theories, and neutral set theories. The fun includes finding the right translation so that we can all enjoy our different tastes in axioms.
1. Fix a formal system S. In the LLM example, it uses first-order arithmetic, but I don't see why we wouldn't be able to use ZFC.
2. Let D be the set of subsets of the natural numbers N which are definable by a finite formula in S.
3. There are countably many finite formulas, so |D| <= |N|.
4. Cantor's theorem says that the size of the power set of N is greater than |N|.
5. Therefore there must be subsets of N which are not definable by a finite formula in S.
If you disagree with this, I would be interested to know.
Not happy to respond to LLM talk, but you seem interested anyway. Some sleight of hand happens between "fixing a formal system" and using Cantor's theorem for the metamathematical analysis, as if we use classical set theory anyway. Note that you cannot construct any particular example of a non-definable set, which should cast doubt of existence. I'll disagree by pointing to anti-classical set theories. The axiom of infinity proves independence from ZFC, so I can freely replace the axiom of infinity with its negation, then the natural numbers no longer form a set. Some constructive analysis systems include an axiom that every real-valued function is continuous (as discontinuous functions are undecidable).
I recently played around with what I call "manual tail-call optimization": transform a tail call to a goto to the beginning of the function. Check it out: https://godbolt.org/z/3fY1v1oeW
int factorial_loop_iterative(int n, int a){
while(n > 0){
a = a * n;
n = n - 1;
}
return a;
}
int factorial_loop_recursive(int n, int a){
if(n > 0){
return factorial_loop_recursive(n - 1, a * n);
}else{
return a;
}
}
int factorial_loop_manual(int n, int a){
tailcall:
if(n > 0){
a = a * n;
n = n - 1;
goto tailcall;
}else{
return a;
}
}
int (*factorial_loop)(int n, int a) = factorial_loop_manual;
int factorial(int n){
return factorial_loop(n, 0);
}
I recommend against, of course! Incorrectly sequencing the manual version results in bugs (swap the assignment for n and a), which the recursive version doesn't need to care about.
I see replies that keep repeating the same "it's got no smoke and tar so it must cause far less harm", as if common sense always matches reality. Coating the lungs with cooked propylene glycol and glycerine could cause similar harm to smoke and tar, or even entirely new harms, but I don't really know that. Use empiricism and share reviews, please.
"Conclusion: Smokers or former smokers who switch to e-cigarettes may reduce their exposure to carcinogens and lower their risk of developing severe health issues associated with conventional smoking. However, in healthy individuals who have never smoked traditional cigarettes, the use of e-cigarettes introduces several cardiovascular and respiratory adverse effects. These findings suggest that while e-cigarettes can be a strategic harm reduction tool for smokers, they are not a safe option for non-smokers."
"CONCLUSIONS: After thorough evaluation for other potential etiologies, vaping was considered to be the most likely common causal etiology for all patients due to the temporal association of symptomatic chronic lung disease with e-cigarette use and partial improvement in symptoms after e-cigarette cessation. In this series, we associate the histopathologic pattern of small airway–centered fibrosis, including constrictive bronchiolitis, with vaping, potentially defining a clinical and pathologic entity associated with e-cigarette use. (Funded in part by the National Institutes of Health.)"
"Abstract: [cut] With well-known health risks from traditional smoking, e-cigarettes are viewed as a safe way of smoking, appealing more to youth. Additionally, extensive e-cigarette marketing boosted by the internet and fame has resulted in worries that e-cigarettes can lead to a renormalization of cigarette smoking and can be used as a new method to consume vaporized drugs. Although the concern that e-cigarettes are as harmful as traditional smoking has been raised, youth and most healthcare providers remain relatively unaware. [cut]"
The reality is that cigarette smoking was on the way out with young people before vapes came along. Whether it's less harmful isn't the only relevant point, if it's still harmful and has dramatically expanded the market then it's a bad thing.
We do have many decades of inhaled medications that used pg and vg carrier vapors so its not like we have zero idea on their relative safety. It may cause some harm, but it is assuredly less harmful than smoking or else people using asthma inhalers would have shown significant problems from it.
>> My thing is, how healthy are ecigs compared to real cigarettes really?
> Use empiricism
> Smokers or former smokers who switch to e-cigarettes may reduce their exposure to carcinogens and lower their risk of developing severe health issues associated with conventional smoking.
Why yes, I want to read research confirming common sense. And more valuable, I can read the nuance of it too (quantifying how much safer compared to cigarettes).
I got stuck in a loop on 8 "Adding zero to the right", blindly following the tip below the box keeps looping induction introduction. Looping 9 times following the help tip, it eventually complains about an invalid proof state (kernel isn't general enough?). Where's the inductive hypothesis... doh the green box labeled IH on the left side. User error lol. But I feel that folks unfamiliar with proofs would struggle with it.
Also, please remove the rise-in animation so that switching proofs feels faster and less flashy. The rest of the website design has enough flash.
Enough complaints, pretty cool! I did all 20 exercises. Thanks for sharing.
Thank you for the feedback! Will address. Yeah, I intentionally tried to not make the UI too easy to prove things and it shows all possible actions that can be taken from the current point, so that in the future another mode could be added for writing proofs from scratch.
Just thought of how to fix the problem I had. Since the program already highlights the inductive hypothesis blue (but doesn't underline), consider adding a clickable underline to it (Rewrite with IH) instead of requiring the green IH box on the left (banner blindness). See if you can get rid of any drag&drop features and focus more on underline and click (TouchProof, not DragProof). Then the tip box would only need to explain clicking underlined terms.
And another thing, when 2 underlined terms nest (say, Sn+0=0 with underlines on Sn+0 and n), hovering should highlight only the more specific term (hovering on n highlights both Sn+0 and n the same color).
You sound like you believe in philosophical skepticism. Tell me: can a map ever properly describe the territory? When would a map properly describe the territory? (Can a theory ever properly describe reality? What does a theory need to properly describe reality?)
We know that universal Turing machines can emulate other Turing machines. Weirdos like Wolfram believe that a universal Turing machine can emulate reality. In a quick skim of this lecture series, the presenter doesn't talk about that, rather he just calls computation a scientific principal (universal and fundamental in the sense of physical laws, not fundamental in the sense of emulating reality on a computer).
https://www.niwanetwork.org/members/
reply