Payor's Lemma holds in provability logic, distributivity is invoked when moving from step 1) to step 2) and this can be accomplished by considering all instances of distributivity to be true by axiom & using modus ponens. This section should probably be rewritten with the standard presentation of K to avoid confusion.

W.r.t. to this presentation of probabilistic logic, let's see what the analogous generator would be:

Axioms:

• all tautologies of Christiano's logic
• all instances of $(x\to y)\to ({\square }_{p}x\to {\square }_{p}y)$ (weak distributivity) --- which hold for the reasons in the post

Rules of inference:

• Necessitation $⟨x,{\square }_{p}x⟩$
• Modus Ponens $⟨x\to y,x,y⟩$

Then, again, step 1 to 2 of the proof of the probabilistic payor's lemma is shown by considering the axiom of weak distributivity and using modus ponens.

(actually, these are pretty rough thoughts. Unsure what the mapping is to the probabilistic version, and if the axiom schema holds in the same way)

No particular reason (this is the setup used by Demski in his original probabilistic Payor post).

I agree this is nonstandard though! To consider necessitation as a rule of inference & not mentioning modus ponens. Part of the justification is that probabilistic weak distributivity ($⊢x\to y⟹⊢{\square }_{p}x\to {\square }_{p}y$) seems to be much closer to a 'rule of inference' than an axiom for me (or, at least, given the probabilistic logic setup we're using it's already a tautology?).

On reflection, this presentation makes more sense to me (or at least gives me a better sense of what's going on / what's different between ${\square }_p$ logic and $\square$ logic). I am pretty sure they're interchangeable however.

Yep! Thanks!

Yep! Fixed.

We know that the self-referential probabilistic logic proposed in Christiano 2012 is consistent. So, if we can get probabilistic Payor in this logic, then as we are already operating within a consistent system this should be a legitimate result.

Will respond more in depth later!

Language mix-up. Meant improper integrals.

Now that I'm thinking about it, my memory's fuzzy on how you'd actually calculate them rigorously w/infinitesimals. Will get back to you with an example.

Have updated the definition of the derivative to specify the differences between $f$ over the hyperreals and $f$ over the reals.

I think the natural way to extend your $f$ to the hyperreals is for it to take values in an infinitesimal neighborhood surrounding rationals to 0 and all other values to 1. Using this, the derivative is in fact undefined, as $\text{st}\left(0/\Delta x\right)=0/\text{st}\left(\Delta x\right)=0/0.$

I agree. This is what I was going for in that paragraph. If you define derivatives & integrals with infinitesimals, then you can actually do things like treating dy/dx as a fraction without partaking in the half-in half-out dance that calc 1 teachers currently have to do.

I don't think the pedagogical benefit of nonstandard analysis is to replace Analysis I courses, but rather to give a rigorous backing to doing algebra with infinitesimals ("an infinitely small thing plus a real number is the same real number, an infinitely small thing times a real number is zero"). *Improper integrals would make a lot more sense this way, IMO.

Here the magic lies in depending on the axiom of choice to get a non-principal ultrafilter. And I believe I see a crack in the above definition of the derivative. f is a function on the non-standard reals, but its derivative is defined to only take standard values, so it will be constant in the infinitesimal range around any standard real. If $f\left(x\right)=x^2$, then its derivative should surely be $2x$ everywhere. The above definition only gives you that for standard values of $x$.

Yep, the definition is wrong. If $f:R\to R$ then let ${}^{\ast }f$ denote the natural extension of this function to the hyperreals (considering ${}^{\ast }R$ behaves like $R$ this should work in most cases). Then, I think the derivative should be

$$f^{\prime }\left(x\right)=\text{st}\left(\frac{{}^{\ast }f(x+\Delta x){-}^{\ast }f\left(x\right)}{\Delta x}\right)$$

W.r.t. what the derivative of ${}^{\ast }f$ should be, I imagine you can describe it similarly in terms of  ${}^{\ast \ast }R$, which by the transfer principle should exist (which applies because of Łoś's theorem, which I don't claim to fully understand).

For $f\left(x\right)=x^2,$ the derivative then is:

$$\begin{array}{cc}{f}^{\prime }\left(x\right)& =\text{st}\left(\frac{(x+\Delta x{)}^2-x^2}{\Delta x}\right),\\ & =\text{st}(2x+\Delta x),\\ & =2x.\end{array}$$

I'm familiar with \setminus being used to denote set complements, so \not\in seemed more appropriate to me ($I$ is not an element of $U$). I interpret $I\setminus U$ as "the elements of $I$ not in $U$," which is the empty set in this case? (also the elements of $U$ are sets of naturals while the elements of $I$ are naturals, so it's unclear to me how much this makes sense)