Okay, so I’ve actually finished working through the proof that any inaccessible Jónsson cardinal must be Mahlo (-Mahlo even), but I haven’t had much time to write stuff up. The main issue is that I’ve also been working my way through Sh413, which contains the result that any which is an inaccessible Jónsson cardinal must be -Mahlo.
What I’ll try to do is write up the proof that any inaccessible Jónsson cardinal must be Mahlo. That’s a bit more work than the thread I was following earlier, but not by much. One thing I will do is take the existence of the desired club guessing sequences for granted. I feel moderately comfortable in doing this because the construction of these sequences is incredibly similar to the construction in the case that in EiSh819.
From there, I want to try and write up the result of working through the first section of Sh413. There’s a lot of material in that first section which ends up being tertiary to the main result, and I would like to write up a “straight shot” proof of the result. In particular, there is a really cool construction of a club guessing sequence provided that we have a stationary set which does not reflect outside of itself (Claim 0.14 from Sh413). Actually I might write that part up sooner rather than later.