I have an objection towards the Troll Proof you linked in the picture. Namely, line 2 does not follow from line 1. □C states that “C is provable within the base system”, but the Troll Proof has “base system + □C→C” as its assumptions, per line 3.
The strongest statement we can get at line 2 is □((□C→C)→C), by implication introduction.
I have an objection towards the Troll Proof you linked in the picture. Namely, line 2 does not follow from line 1. □C states that “C is provable within the base system”, but the Troll Proof has “base system + □C→C” as its assumptions, per line 3.
The strongest statement we can get at line 2 is □((□C→C)→C), by implication introduction.