> If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them)
It doesn't mean that. The formal system is explicit: it's the system we're using to write statements like `◻P` (it's a form of modal logic https://en.wikipedia.org/wiki/Modal_logic ).
It doesn't mean that. The formal system is explicit: it's the system we're using to write statements like `◻P` (it's a form of modal logic https://en.wikipedia.org/wiki/Modal_logic ).