Logic:
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...
Read on »
Posted on January 30, 2008 1:26 PM • 8 Comments •
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...
Read on »
Posted on November 4, 2007 3:30 PM • 77 Comments •
As promised, today, I'm going to show the Kripke semantics model for intuitionistic logic....
Read on »
Posted on March 28, 2007 10:20 PM • 5 Comments •
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...
Read on »
Posted on March 27, 2007 8:53 PM • 6 Comments •
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...
Read on »
Posted on March 26, 2007 9:07 PM • 13 Comments •
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...
Read on »
Posted on March 21, 2007 8:53 PM • 26 Comments •
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...
Read on »
Posted on March 12, 2007 4:51 PM • 26 Comments •
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...
Read on »
Posted on March 7, 2007 3:15 PM • 12 Comments •
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:...
Read on »
Posted on January 29, 2007 8:08 PM • 12 Comments •
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...
Read on »
Posted on January 27, 2007 2:14 PM • 45 Comments •
In email, someone pointed me at an automated proof system called 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...
Posted on August 10, 2006 10:53 AM • 3 Comments •
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...
Posted on July 25, 2006 3:42 PM • 3 Comments •
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...
Posted on July 19, 2006 4:13 PM • 3 Comments •
Monday, 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;...
Posted on July 18, 2006 4:16 PM • 11 Comments •