Logic
goodmath | April 28, 2009This 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…
chaoticutopia | May 10, 2008Both 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.
goodmath | January 30, 2008 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…
goodmath | November 4, 2007 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…
goodmath | March 28, 2007 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…
goodmath | March 27, 2007 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…
goodmath | March 26, 2007 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…
goodmath | March 21, 2007 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…
goodmath | March 12, 2007 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…
goodmath | March 7, 2007 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…
goodmath | January 29, 2007Another 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…
goodmath | January 27, 2007 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…
goodmath | August 10, 2006In 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…
goodmath | July 25, 2006So, 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…
goodmath | July 19, 2006Time 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…
goodmath | July 18, 2006[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…