That Logic Blog

Invariants (preprint)

2008-02-26T15:46:00.003+11:00

I seem to have been on a bit of a blogging hiatus for a bit, while trying to get some research done. In this slightly self-indulgent post, I want to talk about some work I've done linking up a few things from universal algebra, category theory and combinatorial group theory.

I've been thinking a bit about invariants for logics and related things. That is, given two logics L and L', we wish to construct gadgets I(L) and I(L') that are isomorphic whenever L and L' are equivalent.

The above paragraph is rather fuzzy, mainly because I have not specified what I mean by a "logic". In the present context, I'm going to take this to be an equationally defined algebraic theory. Examples are things like boolean algebras, distributive lattices and monoids. This is in keeping with classical algebraic logic, which reinterprets logical operators such as conjunction by algebraic operations such as meet.

Within the above context, Patrick Dehornoy has managed to construct algebraic invariants. To every equational theory (satisfying some mild conditions), Dehornoy attaches an inverse monoid, which he has variously called the structure/structural/geometry monoid of the theory. The original construction is detailed in:

P. Dehornoy, Structural monoids associated to equational varieties; Proc. Amer. Math. Soc. 117-2 (1993) 293-304.

In some cases, the structure monoid of an equational theory turns out to be a group. This is, in particular, the case for the theories for semigroups and for commutative semigroups. Dehornoy later went on to show that the structure groups for these theories are Thompson's groups F and V, respectively - rather famous algebraic objects! For instance, they were the first known examples of finitely presentable infinite simple groups. The details are in:

P. Dehornoy, Geometric presentations for Thompson's groups.

In the above paper, Dehornoy constructs presentations for F and V by making essential use of Mac Lane's pentagon and hexagon coherence axioms (arising originally in monoidal and symmetric monoidal categories). This appearence of coherence axioms piqued my interest and I started trying to formalise the connection between structure monoids and coherence theorems. As a warm up to the general case, I toyed around with notions of associativity and commutativity for higher-order functions. This turned out to be a fruitful exercise, as the structure groups in these cases are the higher Thompson groups and the Higman-Thompson groups, respectively. These are infinite families of groups into which F and V slot, which share many of the properties of F and V. After this promising start, I thought about what the coherence axioms for higher-order associativity and commutativity might look like and ended up with a generalisation of the pentagon and hexagon axioms to the higher-order case. Interestingly enough though, several more axioms are required in the higher order case - these do not appear in the usual binary case since everything is a bit too "squished".

Then it was a matter of using the coherence theorems to build presentations of the groups. Being a lazy slob, I did not want to construct both presentations, so I cooked up a procedure that takes a coherent categorification of an equational theory and constructs a presentation for the associated structure monoid, thus saving me the effort.

Anyway, all of this is detailed in the following preprint:

Jonathan A. Cohen, Coherent presentations of structure monoids and the Higman-Thompson groups

Now its back to the thesis-writing salt mines for me (if you look at the conclusions section of the preprint, you'll get a vague idea of what my thesis is on. Stay tuned for more...)

Galavanting

2007-05-31T13:10:00.000+10:00

I fly off to the land up over on Saturday to attend various things as well as for a bit of a holiday. For the insatiably curious, there is a preprint floating around now covering the things I will be talking about: Coherence without unique normal forms.

Workshop Program

2007-01-24T16:23:00.000+11:00

The program for the workshop in Canberra on 5 - 7 February is now available here

It's not too late to register if you want to come along for the fun!

USMC'07

2006-12-07T15:37:00.000+11:00

We're having a workshop!

CALL FOR TALKS AND PARTICIPATION

Universal Structures in Mathematics and Computing

http://usmc07.rsise.anu.edu.au

The Australian National University
Canberra, Australia
5 - 7 February 2007

Aim:

Starting from very different motivations, various groups of mathematicians and computer scientists have sought to describe abstract structures in great generality. This parallel evolutionary process has led to various groups of researchers working on highly interrelated areas, though unable to effectively communicate with each other due to vastly differing languages.

This workshop aims to bring together researchers working in category theory, universal algebra, logic and their applications to computer science in order to highlight recent advances in these fields and to facilitate dialogue between the different camps. Of particular interest is work which spans two or more of these areas.

Structure and Scope:

The workshop will consist of several invited keynote talks as well as shorter contributed talks. Topics of interest include (but are not limited to):

* Operads and related structures
* Higher dimensional categories
* Coalgebras
* Clones in universal algebra
* Residuated lattices
* Algebraic logic
* Linear and other substructural logics
* Higher dimensional automata
* Concurrency theory
* Domain theory
* Type theory

Keynote Speakers:

* Brian Davey (La Trobe, Australia)
* Rob Goldblatt (VUW, New Zealand)
* Ross Street (Macquarie, Australia)
* Glynn Winskel (Cambridge, UK)

Talk submissions:

We solicit talks on topics related to the themes and spirit of the workshop. We aim to facilitate all those who wish to speak at the workshop. Submission of talks can be made by email to Alwen Tiu (Alwen.Tiu@rsise.anu.edu.au) or Jon Cohen (Jonathan.Cohen@rsise.anu.edu.au).

Registration:

Registration for the workshop can be done online through the workshop website. The online registration will be opened on Friday, 15th December 2006 until 2nd February 2007.

* Full registration: AU$ 55 (incl. GST)
* Student registration: AU$ 35 (incl. GST)

Important Dates and Information:

* Deadline for registration: 2nd February 2007
* Deadline for talk titles and abstracts submission: 19th January 2007
* Workshop: 5 - 7 February 2007

Accommodation:

A limited number of rooms have been reserved at University House (http://www.anu.edu.au/unihouse/) and Ursula College (http://ursula.anu.edu.au/Ursula/12.html). Please quote the workshop name "USMC workshop" when reserving the rooms.

In addition, there are many hotels and hostels for those wishing to arrange their own accommodation. Locations in the city centre as well as the suburbs of Turner and Braddon are within walking distance of the university.
Details can be found at http://www.canberratourism.com.au/.

Sponsors:

The workshop is sponsored by the Australian Mathematical Sciences Institute (AMSI) and National ICT Australia.

Travel support:

There are limited travel funds available to support students and early-career researchers from AMSI members. Applications of funds have to be made directly to AMSI. See http://www.amsi.org.au for details.

Organising Committee:

* Jonathan Cohen (ANU and NICTA)
* Brian Davey (La Trobe)
* Greg Restall (Melbourne)
* Alwen Tiu (ANU and NICTA)

Contact:
* Jon Cohen (Jonathan.Cohen@rsise.anu.edu.au)
* Alwen Tiu (Alwen.Tiu@rsise.anu.edu.au)

Workshop: Canberra Nov 28 - 30

2006-11-10T18:23:00.000+11:00

Well, I have really been neglecting my blog these days as I get stuck into my thesis research, move apartments and visit family... Melbourne was lots of fun and I am back in Sydney now at CoACT, where I will be for the next year or so at least. For those of you who will be around Canberra at the end of the month and are into higher categories, homotopy theory and all that good stuff, you may like to come along to The Morgan-Phoa Mathematics Workshop the aim of which is...:

It has been clear for several years that CoACT (Macquarie University) and Amnon Neeman's group at the CMA (Australian National University) have many common research interests. The plan for this Workshop is to investigate these connections, and to advance those research areas, in an informal and flexible setting. Some of these common interests include categorical homotopy theory, topos theory, triangulated categories, K-theory, higher categories, homological algebra, cohomology, and differential graded categories.

I'll see you there!

Ahoy Melbourne!

2006-08-02T09:24:00.000+10:00

Continuing my trend of hiding from my home university, I am now at the Department of Philosophy at Melbourne Uni, visiting fellow blogician Greg Restall. Who knows, this lot may be able to transform me from a philosophical australopithecine into a philosophical neanderthal? At some point in the near future, I shall preach the gospel of higher dimensional ~~algebra~~ logic and try to convert a few nonbelievers. Fingers crossed, eh?

Meaning via Proofs

2006-07-07T01:26:00.000+10:00

Verificationism is the idea, popular amongst the logical positivists, that the meaning of a sentence is to be equated with the method used to establish it. That is, a statement is true if and only if we can, in principle, verify its truth or if it is analytic, which is to say that it is true by definition.

Now, suppose that we are working in classical logic and wish to assert some statement φ and pretend for the moment that we are all happy little verificationists. This means that in order to assert φ, we first need to give a method for determining whether or not it is true. That is, we need to determine whether or not it is present in our model. Being logicians first and foremost, we proceed via structural induction. If φ is an analytic statement, otherwise known as an atomic proposition, then we are done. If φ is of the form "ψ and δ" then we are done if both ψ and δ are in our model. Proceeding in this manner, we can verify whether or not φ is in our model by verifying that a certain collection of atomic propositions and negated atomic propositions are present in our model.

This sort of explanation seems to give the impression that semantics precedes syntax. That is, the meaning of a syntactic expression is determined by its semantic interpretation. Or is it? Let's have a closer look at what is going on here. Returning to our assertion "ψ and δ", we reduced the verification of its presence in the model to the verification that ψ is in the model and the verification that δ is in the model. We can be somewhat facetious and invert this procedure. That is, suppose we already know that both ψ and δ are present in the model. Then we may assert "ψ and δ". Carrying on this inversion process, we can say that a statement is in the model if it is either analytic or can be constructed from the analytic statements via certain inference rules. In other words, what we have discovered is that our model of classical logic is nothing but the free boolean algebra generated by the analytic statements. But we can summarise the situation in a far more snappy manner:

Verification is dual to construction
An even more catchy war cry is:

Models are dual to proofs.
So, the inversion process that we followed allows us to say that syntax precedes semantics. This latter view is encompassed in what is known as proof theoretic semantics whereas the former view is, naturally, known as model theoretic semantics. Since, to a large extent, these theories are dual to one another both warrant serious attention. The latter has, however, had the lion's share of attention historically. Nevertheless, an intrepid group of researchers has been flying the flag of proof theoretic semantics. Its modern culmination is evident in both computational and mathematical logic in such places as interactive theorem proving and categorical semantics of linear logic. On the philosophical front, there has been a resurgence of interest lately, including a special issue of Synthese devoted to the subject. A good discussion of the sorts of things mentioned in this post is provided by the following paper from the volume (unfortunately, I cannot find a free version of the paper):

Meaning approached via proofs; Dag Prawitz

In the next post, I'll write a little about what categorical algebra has to do with this stuff.

Goedelian Memoirs

2006-07-04T17:58:00.000+10:00

I have just finished a charming little book by Gaisi Takeuti:

Memoirs of a Proof Theorist; Mariko Yasugi and Nicholas Passell

The book is a translation of "Goedel'', written in Japanese by Takeuti and translated bu Mariko Yasugi and Nicholas Passell. The book consists, predominantly, of a series of articles about Goedel's life and work. Takeuti offers several personal insights into Goedel, having worked with him at IAS in Princeton.

In proof theoretic circles, Takeuti's name is inextricably linked to his fundamental conjecture' of a cut elimiantion theorem for second order logic, about which I have written previously. Since this conjecture was such a dominating aspect of Takeuti's work at the time of his friendship with Goedel, it is a thread which repeats throughout the book. In this english translation, an appendix has been added in which Takeuti very quickly takes the reader from the definition of a sequent, via Gentzen's consistency proof of arithmetic, to the statement of the fundamental conjecture in a mere 14 pages. It is a testament to Takeuti's deep understanding of this subject that he is able to illuminate all of these results in so brief an exposition.

Takeuti writes of how he managed to arouse Goedel's interest in the conjecture, saying:

His view of my fundamental conjecture was that counter-examples would be discovered by the method of his Incompleteness Theorem or by nonstandard methods'

This comment came back to haunt Takeuti, who relays an exerpt from a referee's report of a paper on the conjecture:

The author claims that the consistency of number theory can be derived from the fundamental conjecture, but this is obvioously inconsistent with Goedel's incompleteness theorem.'

The belief that one cannot establish cut elimination for second order logic was, perhaps, forgiveable given the close temporal proximity with the proof of the incompleteness theorem. The controversy arises since second order logic is the proof theoretic incarnation of set theory. The reason is that, just as first order predicates are equivalent to sets, so second order predicates allow one to state properties of sets. Second order quantification then means, of course, that one can quantify over sets.

Since one can express set theory in second order logic, it is certainly possible to formalise Peano Arithmetic, hence the controversy. However, Gentzen's consistency proof of arithmetic shows that it is equivalent to the accessibility of the first epsilon number, which is the ordinal corresponding to an exponential stack of omega's, of height omega. Here, accessibility means that any strictly decreasing chain of ordinals below this ordinal is finite. This claim, which is justifiable on semantic grounds is, nevertheless, not provable in peano arithmetic. So, there is no clash with the Incompleteness Theorem - we are using an extension of arithmetic in order to prove the consistency of arithmetic.

The book is filled with descriptions both of Goedel's work and his professional relationships. Takeuti is remarkably candid at times when discussing Goedel's work, particularly his early result of the completeness of first order logic and offers many fascinating insights. The choice of title for the english translation is somewhat unfortunate. It is the memoirs of neither Goedel nor Takeuti. But perhaps this complaint is a tad glib - one could, perhaps, see it as the memoirs of Goedel's proof theoretic life.

On an administrative note, I have regular internet access over the next two weeks and have several posts lined up for this period.

Centres

2006-05-02T22:40:00.000+10:00

Craig Pastro and I have a preprint out!

Restricted exchange, braidings and the monoidal centre; Jonathan A. Cohen and Craig A. Pastro

Abstract:Braided monoidal categories arise naturally as centres of monoidal categories and have been the focus of much recent attention in both mathematics and physics. By suitably restricting the use of the exchange rule, we obtain a sequent calculus whose categorical semantics may be seen as freely constructing the centre of a monoidal category. This calculus is shown to admit a strongly normalising and confluent cut elimination procedure. The resulting logic fits neatly into the landscape of noncommutative logics and is distinguished by possessing a particularly perspicuous semantics.

Commutativity

2006-04-21T15:05:00.000+10:00

T-Rex teaches us that classical logic is commutative...

Topologic

2006-04-13T14:25:00.000+10:00

One recent goal of proof theory is to construct invariants of proofs. What do we mean by this? Well, say we have some formal system, F, which encodes a piece of mathematics. Suppose that we have some informal proof P in this piece of maths. Now, given that F encodes the relevant piece of maths, it can encode P. However, there is very likely to be a lot of different ways of encoding P in F. For instance, we could permute non-interacting sub-proofs, change the names of variables, include sub-proofs which don't essentially do anything etc. So, we have something like a fibration going on here. That is, we can imagine a set of all informal proofs, Inf, a set of all formal proofs, For and a projection p:For → Inf. What we would like to do is to slap a system of invariants on For in such a way that two formal proofs have the same invariant if and only if they are in the same fiber. Now, one might argue that we should be using categories instead of sets, since different proofs may be related (for instance, one may be a subproof of the other). This is the basic idea behind coherence theory and we won't be getting into that today.

Anyway, what is a good way of attaching invariants to proofs? Our choices are actually severely limited and most of them use some form of proof net or another. Proof nets were introduced in Girard's 1987 paper on linear logic, though a similar idea was present in earlier work of Chomsky, under the name of "phrase markers" (these appear in "The logical structure of linguistic theory"). The basic idea behind a proof net is to take a formal proof and turn it into a directed graph. I don't have any decent drawing software on this computer, so you're going to have to use your imagination here. Intuitively, we can see why this may work. For instance, a proof in the sequent calculus is almost-always a tree (although you can use "dag-style" proofs if you prefer, where "dag" stands for directed acyclic graph. Australian readers will no doubt be amused by the oxymoronic name "dag-style"). Now, suppose that we were to look at the tree defined by some proof, S, in the sequent calculus. Suppose that we label the nodes by the inference rule used at the relevant step in the proof. Now, if we have another proof that does all the same stuff but in a different order, it is going to generate an isomorphic tree. This is, in fact, not quite how proof nets work, but it is a useful way of conceptualising things (the complications arise, for instance, from axioms, which break the tree property).

Now, those of you with a penchant for topology may well be thinking that there should be a way to obtain an invariant from a topological structure. As it turns out, several people have thought about this and come up with some neat ideas.

As a first pass, notice that proof nets are abstract graphs. But we know that we can embed graphs in topological spaces. What sorts of spaces? Well, that depends on how commutative things are. If the logic is noncommutative (nonsymmetric monoidal category), then the corresponding proof nets are planar, so we can embed them in a sphere (oh, joy!).

The problems come in when we have some amount of symmetry, or commutativity. This breaks the planarity of the graph. One might think that every time you commute two elements, you need to attach a handle to your space. This intuition is roughly correct.

Anyway, now that I have whet your appetite, let me point you to some neat papers that deal with these ideas. First up, we have:

Planar and braided proof-nets for multiplicative linear logic with Mix; G. Bellin and A. Fleury

The above paper obtains a representation of proof nets in terms of CW-complexes in a two dimensional disk. The next paper looks at proofs as two-dimensional surfaces with boundary and contains an analysis of how commuting elements affects the topology of the corrsponding surface.

Implicit exchange in multiplicative proof nets; François Métayer

This next paper goes on to show that the surface associated to the proof structure is the surface of minimal complexity on which the proof can be drawn without crossings, while respecting the local orientation:

Two-dimensional proof structures and the exchange rule; Christophe Gaubert

Finally, building on this work, this next paper transforms the topological ideas into a logical framework:

Permutative logic; Jean-Marc Andreoli, Gabriele Pulciniand Paul Ruet

There's lots of fun ideas in the above papers, so happy reading!

Crunchy Logic

2006-04-04T11:26:00.000+10:00

Long time no post! I have been rather busy with various bits of administravia. I was also occupied for a week or so by scampering down to Canberra to give a progress report. At any rate, I have a backlog of topics I want to post about, so regular posting will resume very shortly!

Until then, why not hop along to Yarden Katz's new blog Crunchy Logic, which covers "Logic, philosophy, computer science and their non-empty intersection".

2-Theories

2006-03-07T13:31:00.000+11:00

Let's return to the question of what a logic is. This time, we'll leave philosophical concerns at the door and approach the question like a mathematician. Ahem.

Any logic you come across in the wild is going to have the same basic structure. It will have a set of "atomic" variables, A, and some operations that can be applied to this set. These include things like conjunction and negation, as well as scarier things like quantifiers. For today, let's pretend that quantifiers don't exist. Then, a logic is the "free structure generated by the given operations over A". For instance, say we have an n-ary connective, f. Then, whenever we have n things in our logic, say p₁,...,p_n, then we also have f(p₁,...,p_n).

Well, this still feels a bit wishy-washy. Can we be more mathematically precise? Yes we can. One classical way is to construct the Lindenbaum-Tarski algebra of the logic. The idea behind this construction is to pretend that the logical operations are algebraic operations and squint until you get a universal algebra (more technically, quotient out by the evident equivalence relation generated by implication).

Very well. So, we have a first pass at defining a logic: it is a "free universal algebra". All this means is that we grab some set A and some equational theory E and study the properties that any object satisfying E must satisfy (with the variables drawn from A, but this doesn't really matter). A theorem due to Birkhoff says that this is the same as a variety. Now, "variety" in this sense means a class of algebraic structures closed under homomorphic images, subalgebras and products. This is a different notion from what algebraic geometers mean by "variety". Examples of varieties are groups, rings, lattices,... So, studying a particular logic is "the same" as studying the variety of algebras that satisfy the equational theory of the logic (well, sometimes you have to consider universal Horn clauses, in which case you study "quasivarieties"). This is the classical point of view of algebraic logic. A cool introduction to this sort of thing is:

A Survey of Abstract Algebraic Logic; J. M. Font , R. Jansana and D. Pigozzi

If you don't have a subscription to Studia Logica, you can check out Chapter II of:

Algebraic logic; Hajnal Andréka, István Németi and Ildikó Sain

Abstract algebraic logic is a good start to understanding what logic is from a mathematical point of view. However, it suffers from one serious objection: it does not model proofs in a logic. That is, it equates any two proofs of a given statement. This is A Bad Thing.

Happily, there is a well-defined way of modelling proofs in some "universal algebra", dating back to Lambek. It can be viewed as pushing the Lindenbaum-Tarski construction up by one dimension: instead of taking the free term algebra of the logic, take the free category of the deductive system. This is a bit of a floppy definition, but you can see more of what I mean by this in:

Category theory for linear logicians; R. Blute, P. Scott

So, we can now do one better and say that logic is the study of "free categories with structure". Examples are, of course, cartesian closed categories, which are "the same" as intuitionistic logic and star-autonomous categories, which are "the same" as multiplicative linear logic (without exponentials). Now, above I was a bit sloppy with throwing around the term "algebra". What I meant before was algebra in the sense of "variety generated by an equational theory". This is not the same thing as the more familiar meaning of alebra as "algebra over a commutative ring k", which is a ring A equipped with a ring homomorphism from k into the centre of A. The viewpoint of category theory allows us to study logic in terms of "algebra" in this sense, via so-called full completeness theorems. For instance, various flavours of Hopf algebras form models of various flavours of (multiplicative) linear logic. This is cool!

We now know that in order to find a uniform description of logics, we need a uniform description of "categories with structure". There are various ways of accomplishing this, but none that are completely satisfactory! I'll talk about other approaches in later posts, but for now let's focus on things called 2-Theories.

Algebraic theories were introduced by Lawvere, in order to study the notion of "set with structure", such as groups, rings,... Formally, an algebraic theory is a category, C with products in which each object is a finite product of some object x. We then slap some extra arrows onto this category, expressing algebraic relations. A "model" of a theory is a functor F:C → Set. John Baez has a better description of these gizmos over at:

This weeks finds in mathematical physics: week 136; John Baez

Ok, so via these whacky gadgets, we can talk about a set with added structure. Heck, we can talk about other mathematical objects with structure. For instance, there is some theory of groups, say G:C → Set. We get the theory of toppological groups by changing Set to the category of topological spaces. That is, the theory of topological groups is something like G:C → Top. So, an algebraic theory is a product-preserving functor from C to some category.

Hmmm. Can we categorify this in order to describe categories with extra structure? Well, let's see. Our category C is basically the collection of objects of the form Xⁿ, for some object X where, as usual, Xⁿ is defined to be X x X^n-1. Let's start from changing from products to coproducts. Now, any such category is basically the same as "the skeletal category of finite sets". This is just the category whose objects are the finite ordinals 1,2,... The coproduct structure is given by disjoint union. In this way, we see that every object is generated by 1 and the coproduct. Let's call this category Fin.

Now, in order to describe a "categorical theory", what we want to do is take a functor from Fin to some 2-category equipped with coproducts, which preserves coproducts. This is the same thing as a category, except we now have 2-arrows, which go between arrows. The canonical example of a 2-category is Cat, the category of all small categories. The objects are categories, the arrows are functors and the 2-arrows are natural transformations.

We're not quite done, since Fin is a 1-category and we are trying to send it to a 2-category! No problem, we can turn Fin into a 2-category by adding in all the identity 2-arrows. Let's call this 2-category 2-Fin. We can now define a 2-theory! It is a a 2-category, T, with a specified coproduct structure, together with a 2-functor G_T:2-Fin → T, such that G_T is bijective on objects and preserves the coproduct structure.

2-Theories were defined and studied in the following nifty paper:

The syntax of coherence; Noson Yanofsky.

I said before that every approach to describing categories with structure has some catch. What's the catch here? Well, you cannot use these things to model contravariant structure on a category! This is a serious concern for logicians, since, for instance, this means that it fails to capture logics with some sort of implication (which corresponds to the Hom bifunctor). Bummer.

That's enough for today. In a later post, I'll describe another approach that uses a generalisation of operads in order to get around this problem.

Linear Logic - Naturally!

2006-02-13T12:00:00.000+11:00

Linear logic has enjoyed enormous popularity over the last couple of decades or so. For those without some training in structural proof theory, understanding the system can be quite intimidating, especially because of the funny notation and weird jargon. In this post, I am going to show you that, in fact, you could have invented linear logic!

To start with, we need to understand classical logic. Our basic ingredients are conjunction, disjunction and negation. I'll denote these by ⊗, ⊕ and ¬ respectively. Since we are doing proof theory, we build our logic by saying how to "introduce" these connectives and describing how they play with each other. This is easy for negation. We want it to act as a unit, so we just say that we have I → A ⊗ ¬A and A ⊕ ¬A → I. Here, I have overloaded the symbol "I" to mean "the strongest false proposition" when it appears on the left of an arrow and "the strongest true proposition" when it appears on the right of an arrow. Such overloading of symbols is quite common in proof theory, so it is best to get used to it. Now, at least for classical logic, I can be taken to mean, respectively, the bottom and top element of the associated boolean algebra, viewed as a lattice. Alternatively, it can be viewed as either the initial or terminal object of your categorical semantics. Anyway, we complete our describption of negation by throwing in the De Morgan laws (but these are derivable from the rest of the things we'll throw in later).

Anyway, let's move on. We need to say how to introduce conjunction and disjunction. As it turns out, there are two ways in which to do this - this is important later. Essentially, the distinction is to whether we treat conjunction as a cartesian product or a tensor product and dually for disjunction. We'll see in just a bit that this distinction does not matter at the moment - classical logic cannot tell the difference! With a view to the future, I'll reserve ⊗ and ⊕ for the tensor intepretation and use x and + for the cartesian/cocartesian interpretation of conjunction and disjunction, respectively.

If we choose the tensor option, then we throw in implications A ⊗ B → A ⊗ B and A ⊕ B → A ⊕ B. For the cartesian interpretation, we would throw in implications A x B → A, A x B → B, A → A + B and B → A + B. We also say that if A → B and A → C, then A → B x C. Dually if A → C and B → C, then A+B → C. The cartesian/cocartesian structure should be clear from these implications.

Now, classical logic also includes certain "structural rules", which describe the structure of sequents. If you don't know what sequents are don't worry - we won't need them today. There are three basic flavours of structural rules, each of which has a version for conjunction and for disjunction, respectively. The first is "exchange", which says that things commute. That is, we throw in implications A ⊗ B → B ⊗ A and A ⊕B → B ⊕ A. We're going to keep exchange in all of our systems today. The second type of structural rule is called "weakening". For this, we throw in implications A ⊗ B &rarr A, A &otimes B → A and, dually, A → A ⊕ B as well as B → A ⊕ B. Notice the similarity with the cartesian introduction rules! We'll exploit this in just a sec. Before that, let's take a peek at the last type of structural rule. It is called "contraction" and says that we have to throw in all implications of the form A → A ⊗ A and A ⊕ A → A.

With all of these structural rules, the cartesian and tensor interpretations collapse! Let's show that A ⊗ B → A x B. First, we certainly have A → A and B → B. We can then use weakening to obtain A ⊗ B &rarr A and A ⊗ B → B. Then, we can use the cartesian introduction rule to obtain A ⊗ B → A x B. I'll leave the derivation of A x B → A ⊗ B to you (hint: use a contraction). The derivations for disjunction are completely dual.

Now, what you may argue that you would like your logic to be able to tell the difference between a tensor product and a cartesian product. In order to achieve this, all you need to do is remove weakening and contraction. If you do this, then the tensor and caresian introduction laws fail to lead to the same thing, so they create different connectives. The ⊗, ⊕ are the main part of the multiplicative fragment of linear logic, whereas the x and + connectives come from the additive fragment of linear logic. To complete the scenario, all you need to do is add in some units for the additive fragment.

Well, we have have almost finished creating linear logic and it is not even dinner time yet! We have one more thing left to do, however. Recall that Glivenko's Theorem says that you can embed classical logic in intuitionistic logic, via the double-negation translation. That is, A is classically provable if and only if ¬¬A is intuitionistically provable. Can we get a similar embedding of classical logic into this logic we have just cooked up?

As it stands, there is no obvious way in which to embed classical logic. What we need to do is create a mechanism whereby we can access weakening and contraction without actually adding full weakening and contraction to our logic. Let's worry about contraction and weakening for ⊕ only, for now. Remember, what we want to do is to take a classical formula A and translate it into something provable in our logic. But to do so, we need to somehow give it access to weakening and contraction. So, let's have the translation mark A in a way that gives it access to these rules. Let's be crazy and denote this mark by ?. We'll also throw in some rules that say that any formula can be given access to weakening/contraction: A → ?A. Also, There's no point in marking a formula twice, so let's also say that ??A → ?A. Finally, postulate the ⊕ version of weakening and contraction only for formulae that have a ? out front. That is, contraction looks something like ?A ⊕ ?A → ?A. Everything for ⊕ pushes through in a completely dual manner. We could, say, mark formulae with a ! to give them access to the ⊗ weakening/contraction rules. These marks are the "exponentials" of linear logic and actually comprise an S4 modality - more on these critters here.

Apart from some added formalism and some theorems to say that everything works out as it should, you have now created linear logic!

News

2006-01-30T21:09:00.000+11:00

I realise that I have been a bit slack with posting recently. Apart from busily writing some papers and doing a little logic, I have been partaking in some holidaying. It's a hard life, I know.

I have also been organising the practicalities of my impending move to Sydney. From next week Monday, I shall be at The Centre of Australian Category Theory for a few months. Officially I am visiting Mike Johnson, but with the number of cool seminars within ambling distance, I will probably end up spreading myself around.

I would like to start up some NotYASS sessions in Sydney if there is sufficient interest. If you are in the area and are interested in having some drinks and partaking in a wilful disregard of academic subject boundaries, give me a holler.

Also for those in the Sydney area, I shall be participating in a weekly advanced modal logic reading group, with a bunch of people in Canberra. Naturally, I would like to have some people around to chat about this stuff in person, so if you are in the area, have some background in logic and would like to get together weekly to discuss some of the finer technical points of modal logic, let me know. We are most likely going to be using pieces of these three books, as well as selected research papers.

Some recent(ish) news from Canberra is that our logic group has continued to grow with Peter Baumgartner and Alwen Tiu both arriving over the last couple of months. Fellow student Rowan Martin-Hughes has also started up a blog, containing his musings on game theory, multi-agent systems and other such goodies. If you are interested in such things, then head on over Towards an Agent Society.

Anyway, regular posting will resume in a week or so, once I am settled in.

Invariants

2006-01-10T17:14:00.000+11:00

A little while ago, I was chatting with an algebraist and he asked whether I knew of any invariants for logics. Now, when a mathematician asks for an invariant, he is asking for something rather particular. This is best explained through some examples.

The simplest example of an invariant is this. Let F be the collection of all finite sets. Then, we can define an invariant function, c, which maps F to the natural numbers and takes a finite set to its cardinality. What is this an invariant of? Well, it is an invariant of the "equivalence" class of a finite set. That is, if two finite sets have different cardinality, then they cannot be isomorphic. Actually, in the case of finite sets, this invariant is complete, in the sense that two finite sets are isomorphic if and only if they have the same cardinality.

A more substantial example is given by the fundamental group of a topological space or, more generally, the sequence of homotopy groups. These do not always characterise the space as tightly as cardinalities do for finite sets, but Whitehead's Theorem says that it characterises homotopy equivalence if the space is sufficiently nice.
Edit: This is not quite correct, see the comments.

So, let's get back to logic. What sorts of invariants could we hope for here? One option is to just say that the algebraic models are invariants of the logic. For instance, propositional logic is essentially the theory of boolean algebras, intuitionistic logic of Heyting algebras and so on. Alternatively, we could grab some categorical models as invariants. So, for linear logic we get star-autonomous categories, for intuitionistic logic we get cartesian closed categories and so on.

Using algebraic or categorical models as invariants for logics is highly undesirable. This is because an invariant should be a simpler than the gadget it is an invariant of. Algebraic and/or categorical models are more like mirror images of the logic under consideration.

It turns out, that if we use some trickery, we can actually make some progress. Suppose that we have a set with an associative binary operator. Now, in virtue of having a binary operator, we can view the terms of this algebra as binary trees. The associativity criterion then becomes a criterion for identifying trees. Now, let's think about automorphisms of this space. Any automorphism, mapping trees to trees, must map trees of the same length to trees of the same length. Moreover, any two trees of the same length are "isomorphic", so permuting them is an automorphism. Now, if we think of the permutations as being composed of our basic associativity map a(bc) -> (ab)c, then we can ask to ensure that any two sequences of applications of this rule which result in this permutation should be identified. If you know anything about categorical coherence theory, you should be jumping up and down and waving Mac Lane's pentagon under my nose right about now. Indeed, the classical coherence theorem for monoidal categories can be used here. Used for what? Well, for helping to write down a collection of generators and relations for the automorphism group, of course!

When the dust has settled and we look at what the automorphism group is, it turns out to be very famous indeed. It is a group known as "Thompson's Group F", which has been the object of much study over the past forty years or so.

So, we can say that an invariant of the logic consisting of only an associative conjunction (not necessarily commutative) is Thomson's F. Using simlar trickery, we can discover that making the conjunction commutative also, results in Thomson's Group V. A very nice paper discussing all of this (with no mention of logic, mind you) is:

Geometric presentations for Thompson's groups; Patrick Dehornoy

Being able to calculate what Dehornoy calls "geometric groups" for algebraic identities paves the way for calculating invariants of logics. Certainly, we are still rather far from invariants of a reasonable complex logic, but this could well be the starting point for a fascinating link between substructural logic and algebra. If you are interested in this and wish to pursue it further, then please get in touch with me!

Basic Logic

2006-01-04T14:30:00.000+11:00

One of the common features of many philosophies of mathematics such as platonism, formalism, fictionalism and so on, is that they view mathematics as a constant, static entity. From this perspective, it makes sense claim something along the lines of "X is the correct foundation for mathematics", where X may be ZF set theory, category theory, constructive type theory or what have you.

However, a subject such as mathematics is constantly changing. So, why not allow this natural evolutionary process into your foundational doctrine? This is the view argued in a very entertaining fashion in:

Steps toward a dynamic constructivism; Giovanni Sambin.

Now, if one accepts that the body of mathematics is constantly changing and, a fortiori, that a foundational theory ought to be malleable, then the concept of mathematical truth is no longer static. This pluralist attitude towards mathematical truth may be refined to a pluralist attitude towards logic. Indeed, Sambin argues:

It is difficult to accept a plurality of logics and still believes that logic deals with a static, a priori, and hence univocal notion of truth.

Given that one accepts a pluralist position, one may seek a way in which to systematically organise various logical theories. To this end, Sambin seeks a common core for a multitude of logics, arriving at a system he calls Basic Logic, which is "the minimal core, with no structural rules". Thus, Sambin adopts a view common amongst substructural logicians of various pursuasions, though he argues via a different route. In order to understand a bit more about what Basic Logic is all about, one must turn to:

Basic logic: reflection, symmetry, visibility; Giovanni Sambin, Giulia Battilotti, Claudia Faggian.

Skipping out the ideological motivations, which are explained in the paper and implemented via a notion of "reflection", one may describe Basic Logic as being almost the logic that results from dropping weakening and contraction from intuitionistic logic. There is one additional ingredient and one technical modification. The extra ingredient is a coimplication, which is the residual or adjoint of multiplicative disjunction in exactly the same way as standard implication is the residual or adjoint of multiplicative conjunction. The technical modification is the one suppresses contexts.

While several logical systems can be seen as extensions of Basic Logic, one ought not see Basic Logic as being the ultimate core of logic and, indeed, Sambin does not claim it to be. For instance, it is an overarching assumption throughout the development that both conjunction and disjunction are commutative (so the statement that it is free of structural rules is not quite true). This is a rather strong requirement and immediately discards many interesting and useful noncommutative logics arising in linguistics and computer science.

Kreisel vs Lawvere

2005-12-12T17:14:00.000+11:00

(via Robert Seely on the categories mailing list). The slides should be interesting for anyone into foundations, category theory or both:

On 29 Nov 2005, the Montreal Category seminar hosted a talk by Jean-Pierre Marquis on the interaction between Kreisel's and Lawvere's views on category theory as a foundations for mathematics. It has been suggested that many on this list who were not able to attend the talk might find its contents of interest, and so would be interested to know that the slides for the talk are available on the triples seminar webpage, at
http://www.math.mcgill.ca/rags/seminar/

(scroll down to the talk itself - the direct link is here if you prefer). The slides are fairly complete, and give a good idea of the content of the talk itself.

Here is an abstract of the talk:

Jean-Pierre Marquis
Organization vs foundations: Kreisel, Lawvere and category theory

Abstract: it is well-known that in the nineteen-sixties, Bill Lawvere proposed that category theory could serve as a foundations for mathematics and logic. Only one logician reacted officially: Georg Kreisel. In a series of notes, appendices and reviews, Kreisel developed arguments against categorical foundations. In this talk, I will take a close look at his arguments, examine whether they are still convincing and propose that Kreisel's position is still underlying most of the arguments against categorical foundations heard to this day.

Polycategories

2005-12-06T16:01:00.000+11:00

Say I have a sequent A,B,C,D |- E,F. I can picture this graphically as the diagram on the left. Squinting at it a bit, one may see it as a sort of a circuit, which maps the input wires A,B,C and D to the output wires E and F. Of course, as it stands, this is not a morphism, but we'll make it into one in just a sec.

Before doing that, let's think about composition. How can we compose two sequents? The answer, of course, is that we use cut. For instance, we could cut our sequent A,B,C,D |- E,F with the sequent F,G,H |- L,K,M to obtain A,B,C,D,G,H |- E,L,K,M. It's easier to think of this geometrically, as in the diagram on the right.

Let's try and make these diagrams mathematically respectable. To do so, we'll generalise the notion of a category. Normally, a category consists of a bunch of objects, together with maps that go between objects. For our generalisation, we'll take lists of objects and maps between these lists. After doing the obvious things in order to ensure that everything is kosher, what we end up with is something called a polycategory. For instance, we generalise morphisms between objects, to polymorphisms between lists of objects. Just as we have functors between categories, we have polyfunctors between polycategories. These do what you expect. Say A and B are polycategories and F:A -> B is a polyfunctor. Then, each object a of A gets sent to F(a) and every polymorphism f: a1, a2, ..., an -> aa1, aa2, ..., aam gets sent to F(f):F(a1), F(a2), ..., F(an) -> F(aa1), F(aa2), ..., F(aam). Well, to be honest, defining composition of polymorphisms is slightly tricky. But not too tricky - we just use cut!

It is clear that we can view sequents as polymorphisms in the evident polycategory generated by the ambient deductive system. And composition becomes easy to understand if we draw polymorphisms as boxes with wires!

But wait, I promised that we would turn these diagrams into morphisms, not polymorphisms! How to do this? What we need to do is to recall that the comma in a sequent is really just a proxy for conjunction on the left and disjunction on the right. So, a sequent A,B,C |- D,E is really the same as A ⊗ B ⊗ C |- E ⊕ F. I'm using ⊗ for conjunction, because it is easier to talk about this stuff with a multiplicative conjunction, which is really just a tensor product. Similarly, disjunction is represented as ⊕ - direct sum! Both of these are examples of monoidal structures on a category. In fact, we can add it to a category too. It turns out that, in a well defined sense, adding ⊗ and ⊕ to a polycategory is a conservative extension. Let's name these things ⊗⊕-polycategories.

We're not quite all the way to viewing the boxes as morphisms in some category. What is missing is something that tells us how ⊗ and ⊕ interact. So, we need to make sure that they play nicely with each other, by saying that there is a natural transformation from A ⊗ (B ⊕ C) to (A ⊗ B) ⊕ C and, dually, there is one from (A ⊕ B) ⊗ C to A ⊕ (B &otimes C). After throwing in these natural transformations and writing down some sensible commutative diagrams, we get what is known as a weakly distributive category.

Here's the cool part. The 2-category consisting of all ⊗⊕-polycategories is equivalent to the 2-category consisting of all weakly distributive categories. With less jargon, polycategories and weakly distributive categories are essentially the same thing! Neato! So, I have kept my promise. The first box is a morphism from A ⊗ B ⊗ C ⊗ D to E ⊕ F in some weakly distributive category. If you want to see how to prove this, plus a bunch of other cool results, look no further than:

Weakly distributive categories; J.R.B. Cockett and R.A.G. Seely

I can't resist pointing to the world's coolest application of polycategories. This is sort of a continuation of something I wrote about a while ago. Namely, it is an application to causal quantum evolution in physics. The basic idea is that we can view a system of interacting quantum systems as a directed acyclic graph, where the nodes are subsystems and the edges represent the causality relation. From this, we can go ahead and derive a polycategory in a straightforward way. Then we can do all sorts of cool things like whacking on some hilbert space representations, density matrices and the like in order to describe the system. I could go on about this, but instead I'll just point to the relevant paper, since everything is explained beautifully in it!

Discrete quantum causal dynamics; Richard F. Blute, Ivan T. Ivanov and Prakash Panangaden.

Update: Weakly distributive categories tell us all about how to use polycategories to model the multiplicative fragment of linear logic. If you want to see how to deal with the additive fragment, including a neat application to concurrent processes, you should check out:

SigmaPi-Polycategories, additive linear logic and process semantics; Craig Pastro

Rock On

2005-11-19T09:19:00.000+11:00

I don't know about you, but when I think proof theory, I think high impact seminars. I think seminar announcements that say "Proof Theory is a highly explosive force waiting to erupt at every show". What am I talking about? Why, the Proof Theory Band of course! Cutting right to the truth, they say "The ability to create such a diverse style is why Proof Theory captures and holds the interest of fans...". Yes indeed! Be sure to check out the nifty wallpaper while you are there.

Modal Space and Computation

2005-11-16T13:35:00.000+11:00

It is an old result of Goedel that we can embed propositional intuitionistic logic (Int) in the classical propositional modal logic S4. This latter logic extends classical propositional logic (Prop) via a modality, [], satisfying the following conditions:

(1) [](p -> q) -> []p -> []q
(2) []p -> p
(3) []p -> [][]p

But in what sense is this result obvious? One route to the reason is provided by knowing that Int has as algebraic models complete Heyting algebras. These are complete lattices in which meet distributes over arbitrary join. Now, a complete boolean algebra is also a complete Heyting algebra. Since complete Boolean algebras form models of Prop, we may expect classical logic to embed into Int. This is indeed the case - it does so via the double negation translation (Glivenko's Theorem): p is provable in Prop if and only if ~~p is provable in Int. But we want to go the other way! That is, we want to embed Int inside of some classically based logic. How to do this?

Let's look at a specific Heyting algebra. Pick your favourite topological space X and let O(X) be the collection of all open sets of X. Then, O(X) is a complete Heyting algebra, with join defined by union and meet almost defined by set intersection. Since O(X) is closed under arbitrary union, we are happy on the join front, but for the meet of arbitrarly many members of O(X), we have to take the interior of the intersection.

Now, O(X) directly forms a model of Int by interpreting conjunction as the interior of intersection, disjunction as union, implication as the subset relation and negation as the interior of the relative complement. It is a theorem that every Boolean algabra is isomorphic to a Boolean algebra of sets. That is, a collection of sets closed under intersection, union and relative complement. So, what we need to do is to add a way of talking about topology to Prop. Have another look at the axioms for S4. What they seem to be saying is that [] forms a (topological) interior operator! This is precisely what we need, since an interior operator uniquely determines a topology of open sets (this is usually stated in terms of the dual notion of a closure operator and holds for a large variety of lattices, not just topological spaces).

So, with our S4 modality, we can build a topology on a Boolean algebra. The Goedel translation then becomes obvious. The only thing we really need to worry about is how to translate a negation. If t is our translation function, then we do this by simply taking t(~p) to be []~t(p). That is, we take it to be the interior of the relative complement!

This topological interpretations of things is very neat and leads to lots of nice things. But we can be a bit brash and crazy and ask what happens if we add an S4 modality to Int directly? Things start getting very interesting indeed! It turns out to be best to switch to category theory at this stage. Instead of working with interior operators, lets work with their dual - closure operators (the diamond of S4). Now, the categorical generalisation of a closure operator is what is called a monad. Since Int has as categorical models Cartesian Closed Categories (CCC), what we are effectively trying to do is to add a monad to a CCC. Moreover, since CCC's are equivalent to simply typed lambda calculi, we seem to be doing something sinister to type theory! What we have, in effect, done is to create what is known as the computational lambda calculus. This is a formal framework for reasoning about the equality of programs and was introduced in the following paper:

Computational Lambda Calculus and Monads; Eugenio Moggi

While the computational lambda calculus is, indeed, a rather nifty thing, we seem to have strayed from geometry. Can we get back? We can! One way is to go back to thinking about the box, or interior operator. Categorically, we can see this as a comonad, which preserves some monoidal structure (that of conjunction). We can then interpret this topologically as an "augmented simplicial set". Since simplical sets are a mainstay of topology, we can start thinking geometrically again. This is rather heady, abstract stuff, but you can read all about it here:

On the Geometry of Intuitionistic S4 Proofs; Jean Goubault-Larrecq, Éric Goubault

So, once again, we have derived a huge benefit by asking the question "Why is this result obvious?". Always a good thing to ask!

Formal Philosophy

2005-11-11T23:53:00.000+11:00

I have become increasingly interested in philosophical work that incorporates various bits and pieces of logic. Thus, it came as a very pleasant surprise when Vincent Hendricks passed on details of the following fascinating looking collection of interviews with a group of eminent philosophical logicians, semanticists etc. I'll reproduce the announcement here for those of you who like to think about formal approaches to philosophy, or philosophical methodology in general.

http://www.formalphilosophy.com/ :
Formal Philosophy
by

Vincent F. Hendricks

John Symons

Interviews with:
Johan van Benthem, Brian F. Chellas, Anne Fagot-Largeault, Melvin Fitting, Dagfinn Føllesdal, Haim Gaifman, Clark Nøren Glymour, Adolf Grünbaum, Susan Haack, Sven Ove Hansson, Jaakko Hintikka, H. Jerome Keisler, Isaac Levi, Ruth Barcan Marcus, Rohit Parikh, Jeff Paris, Gabriel Sandu, Krister Segerberg, Wolfgang Spohn, Patrick Suppes, Timothy Williamson.

Formal Philosophy is a collection of short interviews based on 5 questions presented to some of the most influential and prominent scholars in formal philosophy. We hear their views on formal philosophy, its aim, scope and how their work fits in these respects.

"This is a fabulous collection. Hendricks and Symons have performed an important service to the entire philosophical community. The interviews are not only rewarding in and of themselves but they will help the reader understand what has been going on and has been achieved in the past fifty years. "
--Ernie Lepore, Rutgers, NJ, USA

"Why do you do philosophy that way? Do you believe all philosophy could be done that way? Do you think it should be done that way? These are questions one seldom asks, except perhaps at dinner. Yet there is a lot one could learn from the answers, especially when they come from philosophers who do have a distinguished way of doing their job. Formal Philosophy identifies one such way and collects the answers of its eminent practitioners—not the quick answers one might give over an entrecôte, but the answers one gives when seriously prompted to reflect upon their daily profession. An enticing, provocative, completely novel way of surveying the landscape of contemporary philosophy."
--Achille Varzi, Columbia University, NY, USA

Read extracts of the interviews at www.formalphilosophy.com
Buy the book from Amazon
Formal Philosophy
by Vincent F. Hendricks & John Symons
Automatic Press / VIP
ISBN 8799101300 (paperback)
ISBN 8799101300 (hardback)
264 pages

Doing it Deeply

2005-11-01T10:21:00.000+11:00

One of the salient features of logical formalisms such as sequent calculi, tableaux and natural deduction is that the logical inference rules attack the main connective of a formula, either introducing it or eliminating it. This is to be contrasted with the situation in, say, elementary algebra where one may apply properties such as associativity and commutativity anywhere within a formula.

One may wish to add the ability for rules to act arbitrarily deeply within a formula to a logical formalism. But how can one do this in a sensible way? For many, the most obvious reply would be to utilise term rewriting. This consists of a bunch of "rewrite rules" which allow one to rewrite one term to another anywhere deep within a structure. For example, in a transformational grammar, one may have a rule such as VP --> V + NP, which rewrites a verb phrase into a verb followed by a noun phrase (that is, into a transitive verb).

The problem with just using term rewriting is that there does not, initially, seem to be a good notion of analytic proof, which is provided in the sequent calculus by cut elimination and in natural deduction by normalisation. This is a big concern, since it is analyticity that leads to important metalogical results such as consistency, interpolation and so on. One solution that has been pioneered recently goes under the name of Calculus of Structures. A good introduction to this formalism is provided by the following two papers:

A System of Interaction and Structure, Alessio Guglielmi

Deep Inference and Symmetry in Classical Proofs, Kai Brünnler

By massaging a one sided sequent calculus via the addition of the ability for rules to act arbitrarily deeply (effectively turning them into rewrite rules), one gains the ability to act arbitrarily deeply, while clinging to some notion of analyticity. This is evidenced by the fact that one can still prove all of the same metalogical results.

While this seems promising, to date the Calculus of Structures has only been convincingly adapted to logics which have an involutive negation. In other words, anything with an intuitionistic flavour has been more or less left out in the cold (though there are current efforts to rectify this situation). Moreover, many of the broad concepts are subsumed by categorical logic, while missing out on the important categorical notion of coherence, as is pointed out in the following paper:

Deep inference proof theory equals categorical proof theory minus coherence, Dominic Hughes

Does the above paper sound the death knell for the Calculus of Structures? Probably not, though it does suggest that one needs to understand categorical proof theory when attempting to build a system with deep inference. If not, then one faces the problem of not knowing whether something is just reinventing the wheel. If so, then fitting one's formalism within the context of existing work on things such as categorical logic leads to a clearer understanding of the contribution of the work and also makes the job of selling it to people in adjoining research areas that much easier.

NCB: What is logic?

2005-10-13T15:46:00.000+10:00

Hi, welcome back to NCB. This post is not about any specific talk. Rather, it is about a question I have been wondering about recently, after seeing philosophers going on about it at various conferences.

So, I am pretty happy to tell people that I work in logic (despite the odd looks I get). But when they ask for more details of what logic actually is, I flounder. There does not seem to be an all-encompassing answer. So, what is logic anyway?

If you're an old timer, you may say that logic is the study of truth. This is usually modelled algebraically by looking at something like (A,F), where A is some sort of (universal) algebra and F is a filter on A. For instance, for propositional logic we can take A to be a boolean algebra. For first order logic, we may like to use a polyadic algebra. The algebra A is essentially the term algebra of well formed formulae of our logic. The filter F is the set of "true" statements of our logic. Dually, we may like to look at the collection of all "false" well formed formulae, which forms an ideal I. We can rephrase logical statements in a nice way using algebra. For instance, sticking with boolean algebras, the associated logic is consistent iff I is a proper ideal. If (A,I) is consistent, then it is complete iff I is maximal in A. From this, it follows that (A,I) is consistent and complete if and only if the quotient A/I is the unique boolean algebra on two elements. For more on this view of logic, have a look at the following beautiful paper:

The basic concepts of algebraic logic. Paul Halmos. American Mathematical Monthly vol. 63 (1956) pp 363--387.

Ok, very well, so there is some nice algebra associated with the view that a logic ought to be equated with the concept of truth. But this does not seem to capture what is usually meant by logic. For instance, generations of students have had it hammered into their heads that logic is the study of reasoning. So how do we know that a given statement is true? Is it handed to us by some higher power?

The spiffy modern logician views logic as the study of consequence or deduction. That is, logic is more about "correct" forms of reasoning than about truth. Immediately we run into a problem.

Given that there is some collection of true statements, is there more than one correct way of deriving those statements? That is, is there only one logic or a multitude of logics?

If you answered yes to the first question, then you are a logical pluralist. If you answered no, then you are a logical monist. Now, for a mathematician, pluralism is perfectly reasonable. For instance, say I look at a category whose objects are smooth manifolds. Then what are the "correct" maps? Continuous? Differentiable? Smooth? Truth is, the choice of which class of maps you work with depends on what you are trying to capture. So why should it not be that way in logic?

The pluralism position has been parodied by saying something to the effect of "If you give me a piece of an argument, I'll give you a logic wherein it is valid". I highly doubt that any pluralist seriously thinks of things this way.

So, what is the answer to the subject of this post? Well, it seems reasonable to take logic to be the study of methods of deduction. If you're a philosopher, you'd probably want to change that to "...correct methods of deduction". But such a statement seems presumptious. Taking logic to be the study of deduction, it incorporates aspects of mathematics, computer science, philosophy and linguistics and should not be seen as lying completely in any one of these.

NCB: Probably True?

2005-10-12T14:06:00.000+10:00

How many tautologies are there in propositional logic? Yeah yeah, countably many of the critters. Fine. But what happens if I pick a propositional formula at random? What are my chances of lucking out and picking a tautology? This is the question that Alan Woods set out to answer. Alan is the one in the middle.

It turns out that it matters what you mean by random. Let's think about how we would do this asymptotically. Well, for a start, we'll just represent formulae using and, or, not and parentheses. So, we may think of a propositional formula as being a binary tree. Let's focus our attention on such trees with m literals over n variables. Actually, let's fix n throughout. Let T(m) denote the total number of such trees and let True(m) denote the number of such trees that represent tautologies. Then, unsurprisingly, we can say that the probability of a tautology is the limit as m goes to infinity of True(m)/T(m). Let's call this number P(True).

Another way to consider random formulae is to take a random walk to construct a tree and see what formula we end up with. To do this, start by flipping a fair coin. If it is heads, then roll a 2n-sided die to pick a literal. Stop at this stage. If it is tails, then we are goingto make the node a boolean connective. Flip the coin again to decide if it is a conjunction or disjunction. Then, rinse wash and repeat for the two conjuncts/disjuncts. Notice that there is no guarantee that this process even terminates, but it can be shown that it does so with probability 1. Now, what we have is a well defined probability of any particular formula appearing as a result of this process. Define p(True) to be the sum of the probabilities for each tautology.

Now, it turns out that P(True) and p(True) compute different numbers, though they are related. What can be shown is that p(True) < P(True) for every n (remember that n is the number of variables we are working with). Moreover, as n tends to infinity, p(True) is asymptotically 1/(4n) and P(True) is asymptotically 3/(4n). Want precise numbers? Ok, with n=3, we get p(True) = 0.0642 and P(True) = 0.165.

Of course, there is nothing really special about counting tautologies. Why not consider the probability of hitting some other propositional formula? All this and more has been done! For the details, look no further than:

And/or tree probabilities of boolean functions. Daniele Gardy and Alan Woods.

Stay tuned for more NCB fun tomorrow!