>>12018430>The pop-sci phrasing that "in any reasonable deduction system, there are true statements that are not provable" is actually retarded.I think the best way to read that phrasing is via a common use notion of LEM in the metalogic.
As in
>There are statements so that neither nor are provable, and one of them "must be truth."The point of disagreement can maybe be highlighted with a more concrete example.
Let
denote the statement
>The pair of 15 × 15 matrices with integer entries, and , can be multiplied in some order (e.g. would be one such product) such that the result is the zero matrix.This is known to be computationally undecidable (mortal matrix problem).
I.e. there cannot be an algorithm that, given any two matrices, returns the correct answer to the claim.
So presented any pair of matrices, we're sadly not in the situation to promise to eventually be able to report that they can be multiplied to 0 or that they can't be multiplied to 0.
We can consider the claim that P is decidable for all matrices, i.e.
and this can also be written with just one universal quantifier over the naturals, since we just need to code 2*15^2 naturals with 1, i.e. this is effectively just a statement of the form
.
is trivially provable in Peano Arithmetic via Excluded middle but it's not anymore if you drop it (i.e. do Heyting arithmetic).
Now what about the common language sentence
>The pair of 15 × 15 matrices with integer entries can either be multiplied in some order so that the result is the zero matrix, or it can't.If we judge this to be true, you use an apparently sensible notion of "truth" that however escapes provability.
