Hence, I (standing outside of PA) assert that (since I think PA is probably consistent) agents who use PA don’t know whether PA is consistent, but, believe the world is consistent.
Theres two ways to express “PA is consistent”. The first is ∀A¬(A∧¬A). The other is a complicated construct about Gödel-encodings. Each has a corresponding version of “the world is consistent” (indeed, this “world” is inside PA, so they are basically equivalent). The agent using PA will believe only the former. The Troll expresses the consistency of PA using provability logic, which if I understand correctly has the gödelization in it.
Theres two ways to express “PA is consistent”. The first is ∀A¬(A∧¬A). The other is a complicated construct about Gödel-encodings. Each has a corresponding version of “the world is consistent” (indeed, this “world” is inside PA, so they are basically equivalent). The agent using PA will believe only the former. The Troll expresses the consistency of PA using provability logic, which if I understand correctly has the gödelization in it.