4 ms·
> 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 form
by chriswarbo 6y ago
> 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 https://en.wikipedia.org/wiki/Modal_logic ).
- ProfHewitt 6y agoThanks Chris! It would be perfectly reasonable to be more explicit and use a subscript name for the theory after the ⊢. In fact, when more than one theory is being used, it is necessary to the use the subscript to avoid ambiguity. Unfortunately, many modal logics do not allow the subscript.