# Logic

### A Quick Bit of Temporal Logic: Introducing CTL

This post is something that I'm thinking of including in my book. I haven't decided whether I want to spend this much time on logics; they're really interesting and fun - but there's lots of other interesting and fun stuff, and there's only so much space. The topic of the moment is temporal logic - that is, a logic which is built for reasoning about things that change over time. To begin with, why do we want temporal logic? Most of the time, when we want to use logical reasoning, we use predicate logic. So why do we need another logic? Why Temporal Logic? One of the basic properties of…

### Red, Orange, Yellow 3: Submarine Proof

Both philosophy people and Beatles people should enjoy this one... I was studying for my final exam in predicate logic, while simultaneously browsing through the Flickr "Song Chart" Pool (thanks to Of Two Minds.) The next thing I know, I’m trying to work out this proof: Click the image for the a larger version, with the solution spelled out. If you still don’t get it, just enjoy this instead: When part one ends, links to the other parts should appear at the bottom of the player.

### What makes linear logic linear?

Sorry for the lack of posts this week. I'm traveling for work, and I'm seriously jet-lagged, so I haven't been able to find enough time or energy to do the studying that I need to do to put together a solid post. Fortunately, someone sent me a question that I can answer relatively easily, even in my jet-lagged state. (Feel free to ping me with more questions that can turn into easy but interesting posts. I appreciate it!) The question was about linear logic: specifically, what makes linear logic linear? For those who haven't ever seen it before, linear logic is based on the idea of…

### Mathematical Constructions and the Abstraction Barrier

There was an interesting discussion about mathematical constructions in the comment thread on my post about the professor who doesn't like infinity, and I thought it was worth turning it into a post of its own. In the history of this blog, I've often talked about the idea of "building mathematics". I've shown several constructions - most often using something based on Peano arithmetic - but I've never really gone into great detail about what it means, and how it works. I've also often said that the underlying theory of most modern math is built using set theory. But what does that really…

### The Kripke Model for Intuitionistic Logic

As promised, today, I'm going to show the Kripke semantics model for intuitionistic logic. Remember from yesterday that a Kripke model has three parts: (W, R, :-), where W is a set of worlds; R is a transition relation between worlds; and ":-" is a forces relation that defines what's true in a particular world. To model intuitionistic logic, we need to add some required properties to the transition and forcing relations. With these additional properties, we call the transition relation (R) "≤"; if A and B are worlds in W, then "A≤B" means that B is accessible from A. For an intuitionistic…

### Kripke Semantics and Models for Intuitionistic Logic

To be able to really talk about what a logic (or a calculus) means, you need to define a model of that logic. A model is a way of associating entities in the logic/calculus with some kind of real entity in a way where all statements in the logic about the logical entity will also be true about the real-world entity. Models are incredibly important, because it's relatively easy to design a logic which looks as if it's perfectly valid, but which contains some subtle error which leads to it being essentially meaningless - showing a model for a logic guarantees that that can't happen. The model…

### Intuitionistic Logic (partial rerun)

I'm incredibly busy right now adjusting to my new job and my new commute, which is leaving me less time than usual for blogging. So I'm going to raid the archives, and bring back some interesting things that appeared on the old Blogger blog, but were never posted here. As usual, that will involve some cleanups and rewrites, so this won't be identical to the original posts. I've written about logic before, and mentioned intuitionistic logic at least in passing. Intuitionistic logic is an interesting subject. Intuitionistic logic is a variation of predicate logic which is built on the idea…

### An Experiment with π-calculus and Programming Language Design

I feel like a bit of a change of pace, and trying a bit of an experiment. Re-reading Backus's old FP work reminds me of what I was doing the last time I read it, which was back in grad school. At the time, I was working on some stuff involving parallel computation, and I discovered Robin Milner's π-calculus as a tool for describing parallel computation. You can think of π-calculus as being a sort of parallel (pun intended) for the λ-calculus: in sequential, single-threaded computation, λ-calculus can be a great tool for describing what things mean. But λ-calculus has absolutely no way of…

### Basics: Modal Logic

I've received a request from a long-time reader to write a basics post on modal logics. In particular, what is a modal logic, and why did Gödel believe that a proof for the existence of God was more compelling in modal logic than in standard predicate logic. The first part is the easy one. Modal logics are logics that assign values to statements that go beyond "This statement is true" or "This statement is false". Modal logics add the concepts of possibility and necessity. Modal logic allows statements like "It is necessary for X to be true", "It is possible for X to be true", etc. The…

### Basics: Axioms

Today's basics topic was suggested to me by reading a crackpot rant sent to me by a reader. I'll deal with said crackpot in a different post when I have time. But in the meantime, let's take a look at axioms. What is an axiom? If you want to do any kind of formal or logical reasoning, or any kind of inference, you need to start with some set of known facts. There is simply no way of performing inference starting from absolutely no knowledge. Axioms are the set of known facts that are accepted as basic primitive unproven facts: all proofs are ultimately built upon the inference rules of…

### Basics: Syntax and Semantics

Another great basics topic, which came up in the comments from last fridays "logic" post, is the difference between syntax and semantics. This is an important distinction, made in logic, math, and computer science. The short version of it is: syntax is what a language looks like; semantics is what a language means. It's basically the distinction between numerals (syntax) and numbers (semantics). In terms of logic, the syntax is a description of what a valid statement looks like: what the pieces of a statement are, and all of the different ways that the pieces can get put together to form…

### Basics: Logic, aka "It's illogical to call Mr. Spock logical"

This is another great basics topic, and it's also one of my pet peeves. In general, I'm a big science fiction fan, and I grew up in a house where every saturday at 6pm, we all gathered in front of the TV to watch Star Trek. But one thing which Star Trek contributed to our vocabulary, for which I will never forgive Gene Rodenberry, is "Logic". As in, Mr. Spock saying "But that would not be logical.". The reason that this bugs me so much is because it's taught a huge number of people that "logical" means the same thing as "reasonable". Almost every time I hear anyone say that something is…

### Metamath and the Peano Induction Axiom

In email, someone pointed me at an automated proof system called [Metamath][metamath]. Metamath generates proofs of mathematical statements using ZF set theory. The proofs are actually relatively easy to follow, which is quite unusual for an automated theorem prover. I'll definitely write more about Metamath some other time, but I thought it would be interesting today to point to [metamaths proof of the fifth axiom of Peano arithmetic][meta-peano], the principle of induction. Here's a screenshot of the first 15 steps; following the link to see the whole thing. [metamath]: http://us.metamath…

### The Category Structure for Linear Logic

So, we're still working towards showing the relationship between linear logic and category theory. As I've already hinted, linear logic has something to do with certain monoidal categories. So today, we'll get one step closer, by talking about just what kind of monoidal category. As I keep complaining, the problem with category theory is that anytime you want to do something interesting, you have to wade through a bunch of definitions to set up your structures. I'll do my best to keep it short and sweet; as short as it is, it'll probably take a bit of time to sink in. First, we need a…

### Towards a Model for Linear Logic: Monoidal Categories

Time to come back to category theory from out side-trip. Category theory provides a good framework for defining linear logic - and for building a Curry-Howard style type system for describing computations with *state* that evolves over time. Linear logic provides a way of defining a valid *model* for part of linear logic (the multiplicative operators) that aren't tractable using other modeling techniques. I'm going to show you the relationship between models for linear logic and category theory. It's going to take a couple of days to go through the whole shebang, but even the parts that we…

### Linear Logic

[Monday][yesterday], I said that I needed to introduce the sequent calculus, because it would be useful for describing things like linear logic. Today we're going to take a quick look at linear logic - in particular, at *propositional* linear logic; you can expand to predicate linear logic in a way very similar to the way we went from propositional logic to first order predicate logic. So first: what the heck *is* linear logic? The answer is, basically, logic where statements are treated as *resources*. So using a statement in an inference step in linear logic *consumes* the resource. This is…