From ???@??? Mon Aug 30 14:01:22 1999 X-Sieve: cmu-sieve 1.3 Return-Path: Received: from po4.andrew.cmu.edu (PO4.ANDREW.CMU.EDU [128.2.10.104]) by mail1.andrew.cmu.edu (8.9.3/8.8.2) with ESMTP id IAA21506 for ; Mon, 30 Aug 1999 08:47:26 -0400 (EDT) Received: (from daemon@localhost) by po4.andrew.cmu.edu (8.9.3/8.9.3) id IAA07770 for awodey+@MAIL1.ANDREW.CMU.EDU; Mon, 30 Aug 1999 08:47:26 -0400 (EDT) Received: via switchmail for awodey+@andrew.cmu.edu; Mon, 30 Aug 1999 08:47:26 -0400 (EDT) Received: from cmu2.cs.cmu.edu (CMU2.CS.CMU.EDU [128.2.206.46]) by po4.andrew.cmu.edu (8.9.3/8.9.3) with ESMTP id IAA07758 for ; Mon, 30 Aug 1999 08:47:24 -0400 (EDT) Received: (from daemon@localhost) by cmu2.cs.cmu.edu (8.9.3/8.9.3) id IAA26392 for awodey+@andrew.cmu.edu; Mon, 30 Aug 1999 08:47:24 -0400 (EDT) Received: via localmail; Mon, 30 Aug 1999 08:47:23 -0400 (EDT) Received: from smtp2.andrew.cmu.edu (SMTP2.ANDREW.CMU.EDU [128.2.10.82]) by cmu2.cs.cmu.edu (8.9.3/8.9.3) with ESMTP id IAA26388 for ; Mon, 30 Aug 1999 08:47:23 -0400 (EDT) Received: from avigad.hss.cmu.edu (PC39902.PC.CC.CMU.EDU [128.2.229.48]) by smtp2.andrew.cmu.edu (8.9.3/8.9.3) with SMTP id IAA06352 for ; Mon, 30 Aug 1999 08:47:22 -0400 (EDT) Date: Mon, 30 Aug 1999 08:48:27 -0400 (Eastern Daylight Time) From: Jeremy Avigad To: Steve Awodey Subject: Re: advice on modal logic In-Reply-To: Message-ID: X-X-Sender: avigad@MAIL1.ANDREW.CMU.EDU MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Dear Steve, Modal logic is outside my realm of expertise. I once decided to learn more about modal logic and its applications to CS, and I picked up a book in the CSLI series that looks pretty good. I never got past the first chapter -- but I will leave it in your mailbox. When the box is interpreted as provability, you get something known as "provability logic." I've always wanted to know more about this; there's a famous result that says the provability logic of arithmetic is exactly S4. Jeremy