Skip to content

Derive löb induction from later introduction and guarded fixpoints

Ralf Jung requested to merge ralf/löb into gen_proofmode

This follows the proof at https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem, which I found after stumbling upon https://semantic-domain.blogspot.de/2016/05/lobs-theorem-is-almost-y-combinator.html. I don't actually understand the proof but Coq believes it...

Open question: Should we require every SBI to be a Cofe, to avoid this extra side-condition for Löb?

Edited by Ralf Jung

Merge request reports