Löb's Theorem

Löb's Theoremis theorem proved by Martin Hugo Löb which states: 

□(□C→C)→□C If PA proves "If Peano arithmetic proves 'X', where  □then X", then Peano arithmetic proves X means "X is provable"

Which has consequences for reflective reasoning.

□(□C→C)→□C , where  □X means "X is provable".