My question motivated by a part of this page from Saul Kripke's book Naming and Necessity, which is also viewable on google books. In the middle of the page he say something, which seems unnatural to me: Namely he implies that one mathematical theorem can be proved in two different formal systems. Later, in a slightly different context he starts talking about possible worlds and how there are difficulties to identify one referent (e.g. president Nixon) in another world.

Why doesn't it seem to be a problem for him to identify a to be proven statment, when changing from one formal system to another?

Independend of the reference to Kripke: If I show a mathematical identity in one formal system, then the whole deduction is based on a particular axiomatic framework. Any theorem should be unique and not to be found under another axiom system. So by this reasoning, if one considers one statement in one theory, it can not be proven in another. Clearly, there are many models of set and in this sense there are different abstractions of the same intuitively true relation 2+3=5, but proving it in one arithmetic doesn't imply anything about it in another, right? It (that is, the analog) should in priciple be re-proved there. Therefore, i.e. because there are different foundations (similar to there being different religions), it shouldn't be possible to distiguish one framework as better than another and to we wouldn't know how to infer any truth of the real world relation from the maths.

Is there a reason or possibility to identify a statement (which can be derived from a logical framework) to another statement in another framework?

  • "proving it in one arithmetic doesn't imply anything about it in another, right?" - what if one is a superset of the other?
    – Xodarap
    Commented May 18, 2012 at 20:23
  • @Xodarap: What you're saying is proving something by only using certain axioms, so the other axioms never touch it? I don't know, but I think then the prove is really the same and so it's the same statement. I guess this also always applies if one axiom set can exaclty be reconstructed by the others, i.e. you can use the same symbols again and write down the same string as prove. Then if one can say the axioms are distinguishable at all, this would be a way to justify an identity in that case, yes.
    – Nikolaj-K
    Commented May 18, 2012 at 20:30

3 Answers 3


I think the answer you are looking for might be this: There is no syntactic way to identify theorems across different formal systems. If, that is, you look only at the symbols that comprise the theorem then the only "content" is their relation to the axioms of your formal system via the deductive system that allows you to prove it (the theorem) from them (the axioms). And this "content", being dependent upon the formal system you are considering, must differ across formal systems.

On the other hand there certainly are semantic ways to identify theorems across different systems. Of course here you are not merely identifying a proposition P (NB: it now has a truth value so it is a proposition) in formal system m with one in formal system n. What you are doing is identifying P in the model M of m with P' in the model N of n. And here, as Begoner's answer suggests, given the right models, you can of course identify P and P' because you can see that you are talking about the same 'stuff', e.g. natural numbers and natural numbers within ZFC. In short, semantic identification is dependent not simply on your formal system but also on the models you choose - and you can therefore choose models in which your propositions can be identified.

(I have used "identification" informally throughout this answer.)

  • Kripke's book is a rejection of "descriptive" theories of naming, which I think would also reject what you call "semantic identification."
    – Xodarap
    Commented May 20, 2012 at 15:54
  • 1
    I took the question to be motivated by Kripke's comment, not to be asking for an exegesis of Kripke.
    – Chuck
    Commented May 20, 2012 at 20:05

Yes. This has to do with the reason we construct formal systems in the first place: generally, we have a particular intuitive notion in mind and want to construct rules that give structure to that notion. For example, we have an intuitive notion of natural number, and we devise the axiom a+S(b) = S(a+b) in Peano Arithmetic to reflect (part of) what we know about natural numbers. We can assert the very same statement about natural numbers in ZFC, although doing so would be more complicated and require several definitions (since + and S(.) are not primitive notions of ZFC). The difference between ZFC and PA arises not because they say different things about natural numbers; rather, it arises because they can describe a variety of objects other than natural numbers. The reason a statement in ZFC may not be equivalent to one in PA is because one may apply to a certain object and the other may not; nonetheless, insofar as specific objects such as natural numbers are concerned, they say exactly the same thing.

  • Okay, I see, but then there is no formal restriction on how to identify these with each other, just the fact that I want the intuitive natural numbers to be this and that symbol in PA and this and that symbbol in ZFC and that they fulfill certain basic facts. If I take some symbols A,B,C,D,E in a random formal framework and say these are 1,3,4 abd + and = and these seem to have some natural number properties, but then I can not show ADCEC (i.e. 1+3=4), then this is the only reason I say "well, these are obviously not formal representations of the natura numbers".
    – Nikolaj-K
    Commented May 19, 2012 at 18:33
  • addon: Something like the Goldbach conjecture and also the idea that it might be true only comes up because I play around with the numbers in one formal system and there it turns out that the conjecture is true are least for every number I try it on. Proving some theorem in another, maybe stronger, theory (with added axioms, say axiom of choice to name a popular one) is then really only that: a prove in some theory. This is somewhat weak (since there seems to be no justification that the statement is then necessarily true for quantitative relations of real object) but I guess it works for me.
    – Nikolaj-K
    Commented May 19, 2012 at 18:39

Here's an example to argue against the doubt that the "same" theorem cannot be proven in multiple mathematical systems: take p -> p for p a propositional variable. It can be proven in intuitionistic propositional logic, classical proposition logic, classical first order logic, Robinson's arithmetic, Peano's arithmetic, ZFC, in fact just about any formal mathematical system yet devised.

In fact in the history of formal mathematical theories there is in practice little difficulty in identifying the same statement in different theories. Overwhelmingly the theories are either in the same language or there is a natural interpretation of one theory in the other. (For example the interpretation of propositional logic in first-order logic by treating propositional variables as zero-placed predicates, or the interpretation of much of modern mathematics in the language of set theory.) Once we work in the same language, two statements are the "same" if and only if they are the same string of symbols.

As far as I remember Kripke, his developed theory is that we can identify the same things across different possible words. Rigid designators such as "water" or "Nixon" identify the same thing across worlds (see http://en.wikipedia.org/wiki/Rigid_designator for more info).

In the same way I would argue that the name "p -> p" rigidly designates the same theorem in each of these different formal systems.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .