# Belief is indexed by proof system

The fact that some people "believe" in constructive logic to the exclusion of classical (and vice versa) always confused me. I think I now have a concrete example why: because it muddles the content of a proposition with the symbols used to express it.

Both classicists and constructivists answer "do you believe that A and B imply A?" with "yes". If I then point out that, interpreting "and" as tensor product and "imply" as linear implication, this is not a theorem of linear logic, this will not change anyone's mind. This is because A ⊗ B ⊸ A in linear logic represents a different proposition than A ∧ B ⊃ A in constructive or classical logic.

The law of the excluded middle is exactly analogous: the symbols A ∨ ¬A signify different propositions in classical and constructive logic, so it makes perfect sense that one is a theorem and the other not. That they use the same symbols and are pronounced the same is nothing more than a historical accident.

So I "believe", classically, that A ∨ ¬A—by which I mean nothing more than that it is provable; and I "do not believe", constructively, that A ∨ ¬A—by which I mean nothing more than that it is not provable. I don't see how one can consistently take "A or not A is an unacceptable theorem" as a strike against classical logic in favor of constructive logic, yet not take "A and B imply A is not an acceptable theorem" as a strike against constructive logic in favor of linear logic.

More generally, I find appeals to intuitive notions of "truth" in foundational mathematics misguided. To pick but one example, is the axiom of choice true or false? No, it is not! Rather, systems with AC describe a different notion of "set" than systems without it, just as classical, constructive, and linear logics describe different notions of truth.

## (2012-7-26) Addendum: Meaning, not belief

Perhaps this post would be better titled "Meaning is indexed by proof system". It is not that I believe certain symbol-strings relative to a chosen proof system; it is that which proposition the symbol-string "A ∨ ¬A" denotes depends on what proof system we interpret it in.

I say "perhaps" because this begs the question of what, exactly, it is that is being denoted, or what it is for a logical proposition to have meaning—a classic conundrum of analytic philosophy that I do not wish to commit to answering here.