Category Archives: Logic

What makes linear logic linear?

Leave a reply

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?

Continue reading →

Mathematical Constructions and the Abstraction Barrier

79 Replies

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 mean? That’s the important question, and the subject of this post.

Continue reading →

Kripke Semantics and Models for Intuitionistic Logic

Leave a reply

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.

Continue reading →

Intuitionistic Logic (partial rerun)

Leave a reply

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 that there should be a stronger notion of “truth” in logic: that the strict categorization of all statements in classical logic as either true or false is too strong. In intuitionistic logic, a statement is only true if you can prove that it is true. It is not enough to prove that it’s opposite is false: In propositional logic, it is not the case that ¬¬P→P.

Continue reading →

An Experiment with π-calculus and Programming Language Design

Leave a reply

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 describing the concept of multiple
things happening at once. π-calculus is fundamentally built on the concept of multiple threads
which can only share information by passing messages.

There’s a reason that reading Backus made me think of this, beyond just the temporal coincendence of the fact that I was working with π-calculus the last time I read Backus’s
FP paper. One of the major points that Backus made was how poorly the vonNeumann model was
at describing many computations; that has become far more true in recent years. Even my laptop now has multiple processors; computation just isn’t single-threaded anymore. But most programming languages are basically deeply single-threaded. Even Haskell, for all of its functional
purity, isn’t particularly good at multi-threaded execution. But I’ve always thought it would be
a great idea to build a language around π-calculus the way that ML is built around λ-calculus.

So my experiment, such as it is, is to see if I can work through how to create an actual, useful, non-pathological programming language based on the π-calculus; and not just do that,
but do it publicly, here on the blog.

Continue reading →

Basics: Modal Logic

Leave a reply

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.

Continue reading →

Basics: Axioms

Leave a reply

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.

Continue reading →

Basics: Syntax and Semantics

Leave a reply

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

Continue reading →

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

47 Replies

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 logical, they don’t mean that it’s logical – in fact, they mean something almost exactly opposite – that it seems correct based on intuition and common sense.

If you’re being strict about the definition, then saying that something is logical by itself is an almost meaningless statement. Because what it means for some statement to be “logical” is really that that statement is inferable from a set of axioms in some formal reasoning system. If you don’t know what formal system, and you don’t know what axioms, then the statement that something is logical is absolutely meaningless. And even if you do know what system and what axioms you’re talking about, the things that people often call “logical” are not things that are actually inferable from the axioms.

Continue reading →