PA + (◻C → C) |- I’m still struggling to completely understand this. Are you also changing the meaning of ◻ from ‘derivable from PA’ to ‘derivable from PA + (◻C → C)’? If so, are you additionally changing L to use provability in PA + (◻C → C) instead of provability in PA?
Doug S.:
That’s u+25FB (‘WHITE MEDIUM SQUARE’).Eliezer Yudkowsky:
PA + (◻C → C) |- I’m still struggling to completely understand this. Are you also changing the meaning of ◻ from ‘derivable from PA’ to ‘derivable from PA + (◻C → C)’? If so, are you additionally changing L to use provability in PA + (◻C → C) instead of provability in PA?