Many Logics

• Notation helps us express ourselves clearly and concisely. Gatekeeping isn't the point.

• We're going to talk a little bit about formal proof systems. Specifically, we're going to talk about the kind of proof system that laypeople tend to be most familiar with, and why it's not very good. And then we'll introduce a better kind of system.
• But first, a bit of notation.
• The first item here is a sort of meta-notation. The idea is that, above the line, I have a list of premises, and below the line I have a conclusion that follows from the premises.
• The second item is a notation specifically for formal proof systems. When I put a little tack in front of a formula, I'm saying that that formula is provable.

• Here we have one possible set of axioms for a Hilbert system.

• In the Hilbert-style system, we had a small number of axioms and a single rule of inference.

• One of the oldest known mathematical proofs is the classical proof that there are infinitely many primes, usually attributed to Euclid.
• This proof can be read as an algorithm that takes as input a set of prime numbers and yields a prime not in that set.
• Similarly, each proof in Euclid's Elements is a procedure that shows how to construct an object with some property.
• Until the late 19th century, all mathematics had this essentially “constructive” character.
• This changed with Cantor's theory of infinite sets and the first formalizations of real numbers and related concepts.

• “Mode” and “modality” are just fancy words that mean “sense in which a proposition might be true”.
• A “modal logic”, then, is a logic that admits multiple senses of truth.
• Modes are often denoted typographically by shapes; e.g., means “ is true in the sense.”

• People only passingly familiar with modal logic mostly know the modes of possibility and necessity.
• We'll talk about those in a bit, but I wanted to start with something slightly less well known, to get people thinking about modes in general.
• So suppose that we like intuitionistic logic, but we still want to be able to talk about things that are true “in the classical sense.” We could do this with a “classical mode”.
• What theorems involving this mode should we be able to prove? (Wait for answers, then advance.)
• It's not obvious how we should do this. Just asserting as axioms all the things we want to be true is usually not the right approach.
• But it turns out we don't need any creativity here.

• The best-known modalities are the modalities of necessity and possibility.
• I'm not sure why these modalities are so significant.
• I know that formal modal logic was originally devised to study them, but I don't know why they were considered so important as to motivate that.
• I also know that Aristotle provided an account of these modalities, but I don't know much about it other than that it has long been considered unsatisfactory.

Roughly: affine logic omits the rule of contraction; linear logic goes further and omits the rule of weakening.