Löb's Theoremis theorem proved by Martin Hugo Löb which states:
□(□C→C)→□CIf PA proves "If Peano arithmetic proves 'X',where□then X", then Peano arithmetic proves Xmeans "Xis provable"
Which has consequences for reflective reasoning.
□(□C→C)→□C , where □X means "X is provable".
@Multicore I accidentally deleted your contribution by submitting an edit I started writing before you published yours. I'm letting you add it back so it remains attributed to you. Also, if you can do some relevance voting that would be helpful.