Neither G nor -G are theorems, but (G or -G) is a theorem.
As an analogy (whose deepness I don’t quite know), this is like if the logical system was a person (who I will name Peano) who I determine will never figure out whether G is true or false. Peano, however, knows that G must be either true or false. He can know (G or -G) even if he can never know G nor know -G.
The tricky thing, I think, is to not accidentally mix the meta lels.
Neither G nor -G are theorems, but (G or -G) is a theorem.
As an analogy (whose deepness I don’t quite know), this is like if the logical system was a person (who I will name Peano) who I determine will never figure out whether G is true or false. Peano, however, knows that G must be either true or false. He can know (G or -G) even if he can never know G nor know -G.
The tricky thing, I think, is to not accidentally mix the meta lels.