amavect

I've thought about this before. It gets harder when dealing with >2 inputs and names longer than 1 letter, so I organized it with lines to make it look more tree-like.

  │u│v│x│y
  ├─┴─├─┴─
  │f  │g
  ├───┴─
  │h
  └─

With >2 inputs and longer names.

  │uh│v  │xizzy│yeez
  ├──┴─  ├─────┴────
  │fooey │gar
  ├──────┴───
  │hello
  └─────

The associative property.

  (a+b)+c=a+(b+c)=a+b+c

  │a│b    │b│c
  ├─┴─    ├─┴─
  │+  │c│a│+  │a│b│c
  ├───┴─├─┴─  ├─┴─┴─
  │+    │+    │+
  ├─────┴─────┴─
  │=
  └─

The quadratic formula.

  (-b±sqrt(b^2-4*a*c))/(2*a)
  
    │b│2│4│a│c
    ├─┴─├─┴─┴─
    │^  │*
    ├───┴─
  │b│-    
  ├─├─    
  │-│sqrt│2│a
  ├─┴────├─┴─
  │±     │*
  ├──────┴─
  │/
  └─

Obviously, it takes way more space and time to draw. Tell me if you like it!

>it very quickly learns to work on "it's on adjacent lines therefore it's a third apart" when you read sheet music

Maybe you read sheet music different than how I do, but when I play euphonium or trombone, I translate from note position+features to finger+mouth position without needing to think about the note letter. More like, "I see the note located here with an accidental feature in the context of the clef and key signature therefore I use this finger position and mouth position". I would love to simplify it down to "it's located here therefore I use this finger position and mouth position".

Keep the accidentals to notate alternate finger positions for enharmonics (and microtones), but eliminate the global variables, the clefs and key signature. Heck, keep the key signature to reduce the noise of alternate fingering symbols, but PLEASE eliminate the clefs. I would also love to play treble clefs at the same sight-reading speed as bass clefs. Also, staff notation should visually repeat every octave, but it doesn't.

Wow, I wish I had this when I learned to play. Keys, clefs, and accidentals felt like a hazing ritual, completely accidental (hah!) complexity. I always hated that I couldn't read the treble instrument parts at sight-reading speed simply because the sheet music used a different clef.

Rotational symmetry or L^2 norm only matter in vector formulations. I assumed a scalar formulation.

Conservation of E-field flux certainly implies additive-homomorphism (addition of charges equals addition of forces). But that seems a bit ahistorical because Maxwell would develop field theory 70 years after Coloumb. Either way, the axiom you choose requires empirical justification, and I think a home hobbyist could more easily demonstrate by experiment that adding charges will add the forces.

Or, if you meant F(r,1,1) = K/r^2, then yeah, conservation of E-field flux could give you an inverse square law. But again, that requires an experiment to justify the axiom.

Actually, yes! We can use homogenous-degree-1 (provable from the homomorphism) to prove it.

  F(r,q0,q1)
  = F(r,q0*1,q1*1)
  = q0*q1*F(r,1,1)

Very simple! It remains to show that F(r,1,1) = K/r^2, as intended.

Show by experiment that the force of charge0 against charge1+charge2 equals the force of charge0 against charge1 plus charge0 against charge2. Induce an additive-homomorphic property F(r,q0,q1+q2) = F(r,q0,q1)+F(r,q0,q2). Then, exponent 1 follows.

I figured this out by listing a bunch of mathematical properties. I couldn't see how the author jumps from zero-preserving to multiply-charges, and I still don't know how, but we can call it out of scope lol

  r : distance between p and q
  q0 : charge 0
  q1 : charge 1
  F : coulomb force function
  charge-commutative: F(r,q0,q1) = F(r,q1,q0)
  zero-preserving: 0 = F(r,q0,0)
  additive-homomorphic: F(r,q0,q1+q2) = F(r,q0,q1)+F(r,q0,q2)
  
  homogenous-degree-1: F(r,q0,n*q1) = n*F(r,q0,q1)
  multiplicative-separability: F(r,q0,q1) = K*R(r)*Q(q0,q1)
  multiply-charges: F(r,q0,q1) = K*R(r)*(q0*q1)^a

  Given F(r,q0,q1) = K*R(r)*(q0*q1)^a, charge-commutative, zero-preserving, additive-homomorphic.
  Induction using additive-homomorphic proves homogenous-degree-1. (For example, F(r,q0,2*q1) = F(r,q0,q1+q1) = 2*F(r,q0,q1))
  Equational proof follows from homogenous-degree-1:
  K*R(r)*(q0*n*q1)^a = n*K*R(r)*(q0*q1)^a
  (q0*n*q1)^a = n*(q0*q1)^a
  n^a*(q0*q1)^a = n*(q0*q1)^a
  n^a = n
  n = 0 or a = 1
  n≠0, therefore a=1.

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.

https://www.niwanetwork.org/members/

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

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.

guess I won't respond now :( "what is a real number, anyways" is one of my favorite questions, not foolish 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.

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?

Thanks for sharing!

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.

Ranked choice is not better. It has the center squeeze effect.

A reminder to support approval voting, star voting, and proportional voting so we can end the 2 party system. https://www.youtube.com/watch?v=yhO6jfHPFQU https://www.equal.vote/

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

https://en.wikipedia.org/wiki/Axiom_of_infinity#Independence

https://en.wikipedia.org/wiki/Constructive_analysis#Anti-cla...

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.

For example? And does "first-order arithmetic" mean ZFC?

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.

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.

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

Well, I have no clue about their relative safety and would like to read more.

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.

Direct health implications of e-cigarette use: a systematic scoping review with evidence assessment https://pmc.ncbi.nlm.nih.gov/articles/PMC11317248/

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

E-Cigarette Use, Small Airway Fibrosis, and Constrictive Bronchiolitis https://pmc.ncbi.nlm.nih.gov/articles/PMC10137322/

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

E-cigarettes and Vaping: A Smoking Cessation Method or Another Smoking Innovation? https://pmc.ncbi.nlm.nih.gov/articles/PMC9833272/

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

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

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.

Cool!! I really like how the overflow condition reads. "When the source and destination have the same sign, but the result a different sign, then signed addition overflows."

x86 has SETC/SETNC and SETO/SETNO to pull the carry/overflow bits out of the status register.

  u+: ADD then SETNC
  u-: CMP then SETNC
  s+: ADD then SETNO
  s-: CMP then SETNO

C23 adds checked arithmetic, and gcc implements them as built-in, generating SETO/SETNO. I can't find a way to generate SETNO otherwise. https://godbolt.org/z/4EjecdW1d

  #include <stdint.h>
  #include <stdckdint.h>

  int add_u(unsigned x, unsigned y){
    return x <= ~y;
  }
  int sub_u(unsigned x, unsigned y) {
    return x <= y;
  }
  int add_u2(unsigned x, unsigned y){
    return !ckd_add(&x, x, y);
  }
  int sub_u2(unsigned x, unsigned y) {
    return !ckd_sub(&x, x, y);
  }
  int add_s(int x, int y){
    return !ckd_add(&x, x, y);
  }
  int sub_s(int x, int y) {
    return !ckd_sub(&x, x, y);
  }

Now, I the difficulty you talk about goes deeper than high level language semantics. Math and predicate logic can't easily talk about a carry flag or an overflow flag. Math equivocates unsigned comparisons with signed comparisons: unsigned < means carry flag, signed < means sign flag != overflow flag. Thus, by coincidence, unsigned < can talk about carry, but < cannot talk about only overflow (without the sign flag). Furthermore, a theorem-proving language wants to prove that overflow cannot happen before attempting to calculate it.

So, despite you clearly showing that carry and overflow have the same calculation cost, I don't know how to represent those predicates in a usual math language with equal symbol length or complexity.

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

I included that to try to explain the symbol soup that correctly encodes the preconditions (the ∀ lines). I intended that to mean "I need to make sure that y+x doesn't overflow", even that unsigned arithmetic cannot express that precondition in that way, as you point out. From there, derive y ≤ INT_MAX-x as the actual precondition for unsigned addition. I forgot that "ensure" actually means something in some programming languages, sorry for the confusion.

More simply put, unsigned addition needs to check that y+x doesn't overflow, while signed addition needs to check that y+x doesn't overflow and doesn't underflow. So, unsigned arithmetic has a simpler precondition that would win a technical debate on whether to use signed or unsigned arithmetic, but since most programming languages lack theorem proving, signed arithmetic wins on the small integer assumption.

Pedantically, that doesn't properly invert post-increment in the loop step. It decrements one extra time. If I need to use the loop index after the loop, then decrementing in the condition would cause problems.

  size_t i = size;
  while(i-- > 0){
    // loop body, possibly break
  }
  use(i); // i wraps below 0

  size_t i = size;
  while(i > 0){
    i--;
    // loop body, possibly break
  }
  use(i); // i doesn't wrap

Practically, i leaves the for-loop scope, so most never encounter this problem.

I believe the main issue lies in most programming languages lacking theorem proving capabilities to prove the safety of integer operations.

The safety conditions for unsigned arithmetic:

  Ensure y+x ≤ INT_MAX.
  If x ≤ UINT_MAX-y, then x+y evaluates correctly:
  ∀x∀y(x ≤ UINT_MAX-y → ∃z(z = y+x))

  Ensure y-x ≤ INT_MAX.
  If x≤y, then y-x evaluates correctly:
  ∀x∀y(x≤y → ∃z(z = y-x))

The safety conditions for signed arithmetic:

  Ensure INT_MIN ≤ y+x and y+x ≤ INT_MAX.
  To avoid overflow or underflow, first compare x to 0.
  In the case x≤0, INT_MIN-x cannot underflow, and y+x cannot overflow. If y compares greater than INT_MIN-x, then y+x evaluates correctly.
  In the case 0≤x, then INT_MAX-x cannot overflow, and y+x cannot underflow. And if y compares less than INT_MAX-x, then y+x evaluates correctly.
  ∀x∀y((x≤0 ∧ INT_MIN-x≤y)∨(0≤x ∧ y≤INT_MAX-x) → ∃z(z = y-x))

  Ensure INT_MIN ≤ y-x and y-x ≤ INT_MAX.
  To avoid overflow or underflow, first compare x to 0.
  In the case 0≤x, INT_MIN+x cannot underflow, and y-x cannot overflow. If y compares greater than INT_MIN+x, then y-x evaluates correctly.
  In the case x≤0, INT_MAX+x cannot overflow, and y-x cannot underflow. If y compares less than INT_MAX+x, then y-x evaluates correctly.
  ∀x∀y((0≤x ∧ INT_MIN-x≤y)∨(x≤0 ∧ y≤INT_MAX+x) → ∃z(z = y-x))

The programmers that prefer unsigned arithmetic intuitively feel the greater simplicity compared to signed integers, but without any theorem proving, I agree that your assumption of small integers strongly supports signed integers.