I added some information to Tractatus Logico-Philosophicus. As this topic (interpretation of the Tractatus) is really complex (and I certainly do not have complete knowledge) and I am new to nLab, I am not quite sure about what and how much to put in. Any advice?
]]>Just some idle thoughts:
To quote from David C’s previous blog, an entry about a Wittgenstein conference:
What then of universal arithmetic statements? Well, their meaning is constitued by their proof, typically a proof by mathematical induction.
…
But this idea of a statement taking its meaning from its proof meets with problems. It suggests that a proposition has no meaning before it has been proved, and that we can’t say we have two different proofs of the same proposition.
Clearly one can get carried away and attribute to W. ahistorical ideas, but here I go anyway.
Compare the above idea, that the meaning of a proposition is carried by its proof, with that of homotopical type theory, that a proposition consists of its proofs. If a proposition is not inhabited, then it is not provable. In the world of HoTT, one sees a proposition as a type, and the fact it has different proofs really tells us something about the ’space’ (=’homotopy type’) that that proposition ’is’. When assuming, or imposing, proof irrelevance in one’s type theory, then we really only care about the binary situation exists/doesn’t exist a proof. But in practice, mathematics is not like this (cf Atiyah-Singer index theorem, 4-colour theorem etc). Rarely do people find a proof and then move on to the next proposition, using only the truth value they just discovered; they want to explore the ’space’ that is that proposition/type.
]]>