Re: [isabelle] Setting up a logic: need instructions.



On 24 Feb 2010, at 18:53, Bart Kastermans wrote:

> I am trying to better understand how logics that come with Isabelle are set up, and how to set up my own.  Is there any good documentation on this?  Explaining the use of TrueProp, and say all the commands in the first 150 lines of a file like IFOL.thy .

Isabelle was of course designed for this purpose, but as nearly everybody wants to use higher-order logic, most of the development and documentation has gone in that direction.

The early papers on Isabelle might give you some useful background information; see http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html

Unfortunately, the early documentation (which did devote some space to this question) is hopelessly out of date.

The file IFOL.thy begins with a lot of references to automated tools which have been made available to first-order logic. You will not need these immediately and they may not even be relevant to your logic.

IFOL.thy then introduces a type o of truth values for the formalism being defined. We do not of course identify this with the "real" type of truth values. The judgement Trueprop mediates between the two levels, and Trueprop(P) is most easily interpreted as "P == True".

Then, the logical constants are introduced. The inference rules governing them are then introduced as axioms. And that is it! You only need to do more if you want special syntax (which you can see in this file) or automation.

The discussion above presupposes that you are working in the natural deduction framework. To formalise a sequent calculus require some technical tricks, which you can see in the file Sequents.thy.

Larry Paulson






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.