Truth in turnstiles

We're often told that "logic" is at the heart of mathematics. We're told that you cannot do math without logic, that mathematics requires it. Personally, I subscribe to the view of formalism, which basically says that math is the manipulation of symbols according to rules. Do we need full-blown propositional logic to manipulate symbols? I hope not.

We need to decide what we mean by "logic." There are a lot of different kinds, believe it or not, and it's not just a matter of expressive power. Alternative logics often entirely disagree with "classical" or typical logic. For instance, paraconsistent logic will tolerate a contradiction without going nuts, and relevance logic takes perhaps a more intuitive approach to material implication, though it's also more complex. When we say "logic," we often mean classical logic, but I honestly cannot see why it should be privileged over other logics. Classical logic is more intuitive than paraconsistent logic, but at the cost of increased complexity (and fragility). On the other hand, it's less intuitive than relevance logic, for the sake of simplicity. Now, maybe this is a happy medium along a spectrum of intuition versus simplicity. But it seems to me that if you're building the foundation of mathematics, you'll favor simplicity over intuition; a happy medium isn't your goal.

The foundation of mathematics, in truth, is entailment, represented by the turnstile. Entailment basically means "given some statements (which look like) X, you can prove another statement (which looks like) Y." Note that this is very different from material implication, which isn't even meaningful at this level (because we haven't even picked a logic yet, let alone laid out its axioms). The actual axioms you're working with can then be defined using the turnstile. Those axioms are often logical in nature, to lay a strong foundation for other mathematical principles (such as ZFC), but there's no requirement that we use logic at this stage. You could, for instance, define the rules of untyped lambda calculus (which are themselves fairly simple) using only the turnstile, and then you would have a Turing-complete system that was defined without logic at all!

So where does this leave us? Different logics have different uses, and we can pick which one we want or need on a case-by-case basis. The turnstile is used to formalize this detachment, making it a framework for choosing a logical system. But we should remember that, technically, we don't need to use a logical system at all. It just happens to be quite convenient to do so.