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

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

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.

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.

  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);
  }

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

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

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.

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

  #include 
  #include 

  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);
  }

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.

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

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.

  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

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

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

  for(size_t i = 0; i < size; i++){
    // loop body
  }
  for(size_t i = size; i > 0;){ i--;
    // loop body
  }

  dB_P = log(10)/10
  dB_F = log(10)/20
  log(10*V) = log(V) + 20*dB_F  // the level of 10 V equals 20 dB more than the power level of 1 V.

  SPL = 20*10^-6 * Pa
  hearing_damage = log(SPL) + 90*dB_F  // hearing damage occurs over 90 dB_F above SPL (neglecting A-weighting)
  pow(hearing_damage) = pow(log(SPL) + 90*dB_F))
  pow(hearing_damage) = pow(log(SPL) + 90*log(10)/20))
  pow(hearing_damage) = SPL*pow(90*log(10)/20))
  pow(hearing_damage) = SPL*31622.7766  // the pressure of hearing damage occurs above 31622 times SPL
  pow(hearing_damage) = 0.632455532 Pa  // the pressure of hearing damage occurs above 0.632 Pa

  log(reference_unit) + value*dB_F (or dB_P)
  log(reference_unit) - value*dB_F (or dB_P)

Sure we can, with some naive algebra. If we can take log(x,base) and drop the base, then we can also take pow(base,x) and drop the base. Since bits=log(2), then pow(bits)=2. You can probably connect it to the reverse of things, like integrals.

Also, for fun, I'll play with some notation tricks.

  log(freq) = pitch
  freq = pow(pitch)
  octave = log(2)

  400*Hz = 100*Hz*4  // the frequency 400 Hz equals 4 times 100 Hz
  log(400*Hz) = log(100*Hz) + log(4)
  log(400*Hz) = log(100*Hz) + 2*log(2)
  log(400*Hz) = log(100*Hz) + 2*octave
  log(400*Hz) = log(100*Hz) + 2*octave  // the pitch of 400 Hz equals 2 octaves above the pitch of 100 Hz

  cent = log(2)/1200
  A4 = log(440*Hz)
  B4 = A4 + 200*cent  // the pitch B4 equals 200 cents above A4
  B4 = log(440*Hz) + 200*log(2)/1200
  B4 = log(440*Hz) + log(2^(2/12))
  B4 = log(440*Hz * 2^(2/12))
  pow(B4) = 493.883 Hz  // the frequency of B4 equals 493.883 Hz

  pow(log(440*Hz) + 200*log(2)/1200)
  exp(ln(440) + 200*ln(2)/1200)

https://en.wikipedia.org/wiki/File:Total_population_living_i...

https://en.wikipedia.org/wiki/Extreme_poverty