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?

@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.

@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.

(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.

(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!

@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.

@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.

To be more precise, I would say that sentences that have been shown to be equivalent using the base theory are regarded as expressing the same thing. That is, I don't mean to include provable equivalences that haven't been discovered yet. Now, I agree that if the proof of equivalence is sufficiently nontrivial, then people might hesitate to declare that the two sentences "say exactly the same thing." But even then, for the purposes of the OP's question, I think it's fine.

It would of course be silly to use such a weird formalization in practice; we typically want to appeal only to "easy" equivalences. But it would still work.

The trouble with appealing to our intuitions about synonymy is that we then have no objective way to adjudicate disagreements. For mathematical purposes, this type of objectivity is more important than being scrupulously faithful to our intuitions about whether two assertions "mean exactly the same thing."

To put it another way, you and I may never agree on exactly which formal sentences "say" that 114 is a sum of three cubes, because we simply have different intuitions on the matter. But for mathematical investigations, such a disagreement doesn't matter, because we can agree on a base theory and then we can agree on which sentences adequately formalize "114 is the sum of three cubes" for the purposes of investigating if the statement is provable in various extensions of the base theory.

Hi. If I understand you correctly, you are claiming that "114 is the sum of three cubes and Fermat's Last Theorem holds" says the same thing as "114 is the sum of three cubes." If that's the case, you have an obviously different idea of what "say" means from me, and our argument is completely semantic.

I'm not sure what you may be using as a base theory, but suppose it's Q. Then you are committed to the idea that x * 0 = 0 and x + 0 = 0 say the same thing, since they are both theorems, indeed axioms, of Q. That spins my head, but if you are happy with it, peace be with you.

I agree that my notion of synonymy does not allow for an objective way to adjudicate disagreements. Tough, but that's life! There has to be a certain amount of good faith. I would expect someone, if they are in good faith, to agree that x * 0 = 0 does not mean the same thing as x + 0 = 0. Would you, for instance, hold (if you understand my sense of synonymy, which I think you do) claim they say the same thing?

I guess you can't edit lines. Obviously, change x + 0 = 0 to x + 0 = x in the two preceding comments.