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