Timeline for In what sense does the sentence $\operatorname{con}(\mathsf{PA})$ "say" that $\mathsf{PA}$ is consistent?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 24, 2023 at 20:45 | comment | added | Timothy Chow | Let us continue this discussion in chat. | |
| Nov 24, 2023 at 16:04 | comment | added | abo | @TimothyChow. "one could still argue that it doesn't say that 114 is the sum of three cubes." There's more to be said, obviously. FWIW, without justification, i would say those extra clauses aren't necessary - but it would take me too long to argue the point. Still the clause I was asking for is clearly necessary. BTW I do agree with you that what S' status in PA is, is irrelevant to what S expresses. | |
| Nov 24, 2023 at 15:53 | comment | added | abo | @TimothyChow. "But it's standard practice to tacitly assume some "base theory" and to regard sentences that are provably equivalent using the base theory as expressing the same thing." I'm not sure what you include as a "base theory," but according to this rule, all the things which are provable in the base theory express the same thing, since they are provably equivalent. Unless the base theory is exceptionally weak, that just can't be right. | |
| Nov 24, 2023 at 14:31 | comment | added | Timothy Chow | (continued) Returning to the example of the sum of three cubes, even if I were to put in the extra clause that you mention, one could still argue that it doesn't say that 114 is the sum of three cubes; it says that either 114 is a nonnegative cube plus a nonnegative cube minus a nonnegative cube, or 114 is a nonnegative cube minus a nonnegative cube minus a nonnegative cube, or 114 is the sum of three nonnegative cubes. And that's not exactly synonymous with "114 is the sum of three cubes"; the equivalence has to be proved! | |
| Nov 24, 2023 at 14:18 | comment | added | Timothy Chow | (continued) This is why I find your answer slightly overly pedantic for the purposes of answer the OP's question. Yes, if you weaken the base theory enough, then some of these equivalences are no longer valid. But some base theory is always assumed, and the OP's concern is not with the precise logical strength of this base theory; it's a much more basic confusion about what it even means for a formal string to express a statement of arithmetic. | |
| Nov 24, 2023 at 14:15 | comment | added | Timothy Chow | @abo You raise a good point. Does $SS0 + S0 = SSS0$ say that 1+2=3? One could argue no, it says that 2+1=3, which is not the same thing. But it's standard practice to tacitly assume some "base theory" and to regard sentences that are provably equivalent using the base theory as expressing the same thing. Certainly, with something as complex as Con(PA), such freedom is standardly permitted. E.g., in Lawrence Paulson's formalization, you see this sort of thing all the time. | |
| Nov 24, 2023 at 13:56 | comment | added | Timothy Chow | @SamHopkins Strictly speaking, a formal string doesn't "say" anything. With that caveat, yes, Con(PA) does correctly express "PA is consistent" in the sense that if someone were to exhibit a formal proof of Con(PA), using axioms that we accept as true, then we would recognize that formal proof as yielding a correct mathematical proof that PA is consistent. | |
| Nov 24, 2023 at 7:38 | comment | added | abo | I'd disagree S says 114 is the sum of 3 cubes, because S does not contain the case +xxx + yyy + zzz. So S does not say 114 is the sum of 3 cubes, but something stronger. Sure, you can trivially check that this other case can be excluded, but you do need to check it. That is, replacing 114 with 90 in your S, does S(90) say that 90 is the sum of 3 cubes? | |
| Nov 24, 2023 at 5:31 | comment | added | Sam Hopkins | So to be clear, you are (in disagreement with a previous answer) asserting that con(PA) does say that PA is consistent? | |
| Nov 24, 2023 at 4:33 | history | answered | Timothy Chow | CC BY-SA 4.0 |