That Logic Blog

Thesis!

2009-04-02T16:31:00.002+11:00

I graduated from my PhD in December and have finally gotten around to placing my thesis on the arXiv. Because of the space limitations of arXiv metadata, the abstract on the webpage has been truncated somewhat, so I will put the real abstract below.

Coherence for rewriting 2-theories: General theorems with applications to presentations of Higman-Thompson groups and iterated monoidal categories; Jonathan Asher Cohen

Abstract:

The problems of the identity of proofs, equivalences of reductions in term rewriting systems and coherence in categories all share the common goal of describing the notion of equivalence generated by a two-dimensional congruence. This thesis provides a unifying setting for studying such structures, develops general tools for determining when a congruence identifies all reasonable parallel pairs of reductions and examines specific applications of these results within combinatorial algebra. The problems investigated fall under the umbrella of ``coherence'' problems, which deal with the commutativity of diagrams in free categorical structures --- essentially a two-dimensional word problem. It is categorical structures equipped with a congruence that collapses the free algebra into a preorder that are termed ``coherent''.

The first main result links coherence problems with algebraic invariants of equational theories. It is shown that a coherent categorification of an equational theory yields a presentation of the associated structure monoid. It is subsequently shown that the higher Thompson groups $F_{n,1}$ and the Higman-Thompson groups $G_{n,1}$ arise as structure groups of equational theories, setting up the problem of obtaining coherent categorifications for these theories.

Two general approaches to obtaining coherence theorems are presented. The first applies in the case where the underlying rewriting system is confluent and terminating. A general theorem is developed, which applies to many coherence problems arising in the literature. As a specific application of the result, coherent categorifications for the theories of higher order associativity and of higher order associativity and commutativity are constructed, yielding presentations for $F_{n,1}$ and $G_{n,1}$, respectively.

The second approach does not rely on the confluence of the underlying rewriting system and requires only a weak form of termination. General results are obtained in this setting for the decidability of the two-dimensional word problem and for determining when a structure satisfying the weakened properties is coherent. A specific application of the general theorem is made to obtain a conceptually straightforward proof of the coherence theorem for iterated monoidal categories, which form a categorical model of iterated loop spaces and fail to be confluent.

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!

NCB: Provability Thresholds

2005-10-11T14:46:00.000+10:00

Welcome to the first Neo Conference Blogging (NCB) post! Today's post covers some things discussed by Andreas Weiermann, hailing from The University of Utrecht (and not just because he knows where I blog). That's Andreas on the left, standing next to Alan Woods of The University of Western Australia and Andrew Brook-Taylor of The University of Vienna. We'll see Alan again in a later NCB post.

Now, we all know that Peano Arithmetic (PA) is incomplete, thanks to that crazy hipster Goedel. Problem is, not all of us are particularly enamoured of sentences that say naughty things about themselves. Do there exist natural number theoretic statements which are true for the natural numbers but unprovable in PA? Wouldn't it be deliciously scandalous if Goldbach or Riemann were in on such a conspiracy? Wouldn't it indeed!

As a matter of fact, there do exist number theoretic statements that are "naturally independant". One example is the Goodstein Sequence. This gizmo converges, but to prove that we need to use transfinite induction up to epsilon zero. Thanks to Gentzen, we also know that this is precisely what is needed to prove the consistency of PA. So, the Goodstein Sequence cannot be proven to converge from within PA. Pretty neat, huh?

One salient feature of the Goodstein Sequence is that it converges slower than Eric Moussambani approaching the finish line in a 10,000 meter race. Perhaps it is this sort of slow convergence that is behind its unprovability? Andreas showed us that it is, as well as a whole lot more, such as how to pinpoint precisely how fast a certain function has to grow for the associated statement (say about goodstein sequences) to be provable in PA.

I won't go through the actual results, since they rely on some technical definitions and, anyway, are explained in the paper below. Here's a neat logical limit law that Andreas mentioned, though. let &phi be a sentence in the language of linear orders. For some ordinal &alpha, let us say that &alpha |= &phi if &phi holds on the set of predecessors of &alpha. Suppose that we pick some ordinal &beta at random. What is the probability that &beta |= &phi? One way is to some asymptotic trickery and define a norm functions on ordinals (I won't get into the details). Then, fix some ordinal &alpha that lies between &omega^&omega and epsilon zero. Consider the number of ordinals &beta of norm n less than &alpha such that &beta |= &phi divided by the total number of ordinals of norm n less than &alpha. Then, it turns out that the limit as n goes to infinity of this ratio is either zero or one! So, depending on your choice of &alpha, a random ordinal less than &alpha almost surely satisfies &phi or almost surely does not. I told you it was neat!

Andreas has a survey paper discussing some trickery with phase transitions and such:

Analytic combinatorics, proof theoretic ordinals and phase transitions for independence results. Andreas Weiermann.

For the phase transition characterisation of Goodstein Sequences, see:

Classifying the phase transition for Hydra games and Goodstein sequences. Andreas Weiermann

More NCB tomorrow!

Neo Conference Blogging

2005-10-10T18:02:00.000+10:00

I have arrived back in Canberra after attending the AAL and AustMS conferences, both of which were lots of fun. While I had planned on partaking in some live conference blogging, this proved too much when coupled with going to talks, giving talks, chatting with fellow conference attendees, eating with fellow conference attendees, drinking with fellow conference attendees....oh and sleeping.

One thing that I could do is to give a summary of the conferences based on the notes that I scrawled and the handouts that were...uh...handed out. I'm not sure how valuable this would be and I would be sure to give short thrift to talks that were too far from my core interests. Not to mention the other worries brought up a while ago over at logicandlanguage.net.

So, I have decided on an alternative style of conference blogging. I will make a series of posts describing various things that I learned about at the conferences, either in official talks or unofficial chats. If I can hunt down relevant articles (preferably online), I'll point to those too. I will try to make an effort to convey the intentions of the official talks, but will not have qualms about going off on a tangent. I will also make no attempt to give a complete overview of the conferences, focusing instead on those aspects that I understood the best. In all, I think this approach is more suited to my blogging style, in as much as I have one.

Subject to other constraints, I will try and make one post a day until I run out of conference topics to talk about and return to my usual posting rate of every week or so. This time I will keep to my blogging promise. Pinky swear!

Aargh Spam

2005-10-04T20:40:00.000+10:00

I have been on holiday for a few days and returned to find my blog covered in filthy comment spam. I have reverted the comment system back to the standard blogger system and have turned on word verification. Hopefully this will be enough to filter out the spambots.

I am on holiday for a few more days, regular posting will resume soon.

Eep!

2005-09-28T09:42:00.000+10:00

The conference schedule has turned out to be rather full, so I haven't had time to blog details (as you may have noticed). I've decided to make some posts at the end of the conference covering mainly the stuff that I understood the best. This will probably be some time next week. There have been some nice talks on algebra, proof theory and nonclassical logic so far, with more to come. One rather curious question was raised: Does anybody in Australia do classical logic? I couldn't think of anybody...

Substructurally Yours

2005-09-24T02:50:00.000+10:00

There has been a lot of interesting work on substructural logics coming out of Japan for a while now. The class of logics which has received the most attention are the so-called FL logics. FL stands for Full Lambek Calculus and is what you get if you drop the structural rules of weakening, exchange and contraction from intuitionistic logic. If you prefer other terminology, this is the same as noncommutative multiplicative additive linear logic.

What makes FL particularly nice is that it has a perspicuous algebraic semantics given by residuated lattices. Briefly, a residuated lattice is a set that carries both a monoid and a lattice structure such that the monoid has both right and left residuals. These may be seen as left and right division operators and satisfy the properties that x.y &le z iff x &le z/y iff y &le x\z. Categorically, this corresponds to saying that we have a biclosed monoidal category with both finite sums and finite products. A residuated lattice is the special case where the category is a poset.

Given FL as a base, we can build up other substructural logics by adding structural rules. These may be the standard weakening, contraction and exchange rules or more exotic rules with cute names like mingle and expansion.

So, what counts as a structural rule? And in what way does the property of an extension of FL rely on the structure of the additional structural rules? These questions and much more are answered in the following paper:

Which Structural Rules Admit Cut Elimination? - An Algebraic Criterion. Kazushige Terui

This paper is chock full of interesting stuff, so I will only sketch bits of it. In order to keep you reading, I'll state one of the main results in grandiose wording. Every substructural logic over FL has cut elimination! Wowzer!

Let's try make this a bit more precise. First, an example. Say we take FL and add contraction but not exchange. Then, the resulting calculus is quite easily seen to not have cut elimination. So the grandiose statement needs some refinement. Specifically, if we identify a logic with its set of provable formulae/sequents, then the result says that any such logic over FL can be given a cut free sequent calculus. Still cool.

How does this all work? It pushes through in a way that is very familiar from exotic structural proof theory, such as the calculus of structures. First, say that a structural rule satisfies the syntactic propagation property if it propagates from atomic formulae to all formulae. In other words, all instances of the rule can be reduced to atomic instances.

Returning to our example of FL with contraction but no exchange, let's extend contraction to act on arbitrary sequences of formulae. Then, this modified version satisfies the syntactic propagation property, while the version with standard exchange does not. We may be onto something here!

As it so happens, Terui shows that every extension of FL having cut elimination satisfies the syntactic propagation property on all of its structural rules. What about the converse? It turns out that this is true also, but in order to prove it, Terui introduces a semantic propagation property. This property is stated in terms of, you guessed it, fancy sorts of residuated lattices.

So, a structural extension of FL has cut elimination iff it satisfies the syntactic propagation property iff it satisfies the semantic propagation property. Our tweaked version of FL with contraction satisfies syntactic propagation, so has cut elimination. This is a special case of a more general phenomenon. Given any collection of structural rules, we can complete them (in the Knuth-Bendix sense) to another set of structural rules that results in cut elimination. Moreover, this completion preserves provability. Now that is super cool!

Anyway, I'll stop there and point you to the paper for lots more juicy details!

On a side note, I am in Perth now for the Australasian Association of Logic annual conference, as well as the Australian Mathematical Society annual conference (since the movie was boring, I read the above paper and wrote this post on the plane flight over). The latter has streams in logic and algebra, which I will generally be hanging around. I'll even be giving talks in each conference (the things they let me get away with!). I'll be blogging details as the conferences progress. Whether this will be liveblogging depends on whether I can leech some wireless. Otherwise, I'll try to do daily posts.

Axis Roundup

2005-09-13T14:23:00.000+10:00

I'm back in Canberra now and, as promised, here is a roundup of the weekend Logic Axis meeting. The amount of detail varies for different talks, mainly based on how tired I was (I had just spent 12 hours on a bus, arriving only an hour or so before the workshop began) and the level of my ignorance of the area... First, Saturday!

Koji Tanaka: Logical Pluralism, Non-Euclidean Geometry and Kant's a Priori. The basic goal was to understand precisely what claim Beall and Restall are making about logical pluralism. The thrust of the talk is that B+R do not have a proper notion of what a "logic" is and so, while there is no objection to there being different a priori accounts of validity, it is not clear how this leads to different logics. One strange feature that came up is that B+R seem to be monist when it comes to metaphysical necessity. If that is the case, argue Goddu and Wyatt, then one must wonder what makes classical logic so different that we ought to be pluralists in this case. Question time for this talk cleared up some things for me. It was pointed out that a pluralist attitude with respect to pure logics is perfectly reasonable, with little to object over. So, the case of applied logics is where the meat is. That is, when we want our logic to capture a certain notion such as, say, metaphysical necessity. If this is the case, then it is not clear that B+R have clearly delineated pure and applied logic, given their stance on metaphysical necessity.

Allen Hazen: Theories of Sets, Theories of Numbers. The thrust here was to seek out the correct restrictions of axiomatic set theory that capture various weak theories of arithmetic. That is, such that each theory can interpret the other. The focus was on Robisnson Arithmetic (Q) and accounts of weak set theories due to Tarski and Lewis, repsecitvely, were analysed with respect to Q.

Thomas Forster: Delinearising Ehrenfeucht-Mostowski. The kick off point is a theorem of Ehrenfeucht-Mostowski, which says that if T is a theory with infinite models, then for any total order I, there is some model of T in which I embeds as a set of indescernables (SOI). A SOI is basically a collection of variables such that the logic cannot descide between them. That is, if one has a property, then they all have that property. Notice the amount that my arms are waving here! Anyway, Thomas made the point that there does not seem to be a good reason why this result should rely on embedding a total order. What about other orders? After sketching how to do this for circular orders, we went on to see how to generalise to arbitrary structures. The thorny part of stating the definition seems to be the bit I waved my arms over above - defining what it means to be a set of indiscernables. This is easy enough in the total order case, but a lot more care needs to be taken in the general setting.

Ed Coleman: Argumentum ad Nauseum. This was an extended discussion of logical fallacies of the "ad whatnot" kind. It was pointed out that there is no good collection of possible logical fallacies out there and, those that are in existence, are inconsistent even in what the various fallacies mean. It was proposed that one ought to create the "Book of Objections", which contains a good theory of fallacies and outlines all possible fallacies. Of course, it is not clear that such a book would be finite in length...

Graham Priest: The Language of Dialetheism 1: Dialetheism, Language and the World. I found this talk vary useful, since it went quite some way to making clear to me what dialetheism is actually all about. Dialetheism is the belief that there can be true contradications. It was pointed out that there are two possible flavours of contradiction: contradictions in language and contradictions in the world. Contradictions in language tend to play on word level ambiguity. As such, it is not overly clear to me that there can be something of a proper linguistic dialethea, which does not rely on the underlying ambiguity. The world level dialetheism is slightly more reasonable. As far as I understand it, an example would be that of moving bodies, since they are in motion and yet, at any given instant of time, they are at rest. Personally, I feel that this is just another case of ambiguity, since motion is usually taken to mean changes/movement through time.

After all that, it was time for wine, dinner and a merry old time before gathering back on Sunday. What happened on Sunday? Read on to find out...

Kieren Nanasi: Mathematical Objects and the Makes-No-Difference Argument. The makes-no-difference argument goes something like this. Pretend that you are at least a little bit of a platonist, for the moment. Suppose now that all mathematical objects suddenly blinked out of existence. Since mathematical objects are a-causal, their disappearing would make no difference to the physical world. As a resultm an ontology in which they feature would be untenable. Therefore, even if mathematical objects did exist, an ontology in which they feature would be untenable. Now thinking about objects suddenly blinking out of existence is incoherent. So, it seems reasonable to weaken the argument to saying that if there were no mathematical objects, then this would make no difference to the physical world. We were taken through several more refinements of the argument, ending with a version which only applies to abstract mathematical objects. Whatever those are...

Demetrios Bastiras: Politis on Aristotle and the Law of Non Contradiction. My ignorence is at its highest here, since I am not very familiar with Aristotle's writings. We were introduced to some writings of Politis, wherein he analyses Aristotle's stance on the law of non contradiction. Aristotle believed that if we accept that some contradictions are true, then we must accept that all contradictions are true. Politis disagreed with this entailment which, I guess, would make him an Australian philosopher! Politis further argued that metaphysics is prior to logic and must be analysed in this light. I guess that this is reasonble for philosophical logic, where it seems that logic is used mainly as a tool for trying to analyse metaphysical arguments. Well, that's my impression anyway.

Peter Quigley: Structure and inconsistency. Quite hard for me to give a summary of this talk, since it mainly consisted of analysing various animations of rotating objects, wherein an inconsistency was added. The thrust of the talk was seeing how these inconsistencies affect our perceptions. It certainly worked, most of the audience was quite disturbed as their perceptions of what was going on flipped between alternative views as the objects rotated!
Edit:Peter's animations can be found here.

Chris Mortensen: Analysis of inconsistent and incomplete Necker Cubes. More geometric inconsistencies here, though this talk covered a classification of possible inconsistencies. At the first level are inconsistencies taht arise in the two dimensional case. That is, ambiguities that arise by virtue of the projection of an object onto the plane. At the second level are inconstencies that arise in three dimensions where we only look at the vertices and edges of the object in question (that is, at the edges). Finally, the third level of inconsistency is again at the three dimensional level but this time we look at the faces of the object in question.

Jon Cohen: Notions of Proof Equivalence. Hey, that's me! I spoke about the problem of analysing ambiguity in natural language. There are two levels of ambiguity here. In the first instance is word level ambiguity, which is not terribly interesting. The second case is structural ambiguity, where the meanings of the words are fixed, but the ambiguity arises due to vagueness as to the scope of words. This type of ambiguity is a lot more interesting. Working under the assumption that language is compositional, structural ambiguity must arise due to different possible ways of composing the meaning of a sentence together. I used this as a jumping off point to give an introduction to the category theory approach to logic, framed in terms of gadgets arising in quantum gravity. One thing that comes out of this is that it is actually possible to account for some phenomena that are usually taken to be semantic using syntactic constructs. I need to think about this aspect a bit more, since it seems to say that the syntax/semantics distinction is even more blurry than commonly assumed. If you're a sucker for technical details, I squibbed up a broad overview over here.

Ross Brady: Classical Deduction and Relevant Deduction. The basic plot was to analyse Fitch-style natural deduction from the point of view that each step of the deduction should be "relevant" in some sense. I was quite tired by this stage, so did not follow along very well. From where I was sitting, it looked like Ross was talking about the sorts of concerns that those people doing "deep inference" proof theory care about. I'll have to chat with him at the AAL!

That's it for the workshop. It's a bit of a shame that Ross and I are the only attendees of the workshop that will also be going to the AAL. It just shows up how fragmented the australian logic community is, which is a pity.

Travel Time

2005-09-06T15:05:00.000+10:00

I'm off to Sydney tomorrow to visit the Centre of Australian Category Theory. I'll be speaking in The Australian Category Seminar about categorical and algebraic logic as well as giving a department seminar. I'm looking forward to finding out a bit more about their research activities, since they have a very impressive number of experts!

After that, I'll be going to Melbourne for the weekend, home of logic blogger Greg Restall. I suspect that he may not be there. Over the weekend is a rather intense philosophical logic workshop, with very many interesting looking talks. My little talk will be on proof equivalence (what else?). While there, I'll also see a bit about dialetheism, relations between Kant's a priori and logical pluralism, relations between relevant and classical deduction and much much more. Should be fun.

Oh yes, thanks to Kenny for telling me about the Melbourne workshop and putting me in contact with Graham Priest.

I'm not sure if I'll have any internet access while I am away. I'll take lots of notes though and post details of the workshop when I get back.

Coherence

2005-08-26T11:27:00.000+10:00

Take a category. Now add a tensor product. Slap in a unit for the tensor product. Add a dose of associativity for the tensor product. While you're at it, stir in some commutativity also. Fold in some diagrams saying that the associativity, commutativity and unit behave properly. What you have now is a symmetric monoidal category. This is the basic building block for making categorical semantics of substructural logics such as, say, linear logic.

If you're smart as a whip, you'll be able to prove a coherence theorem. In grandiose wording, this says that "every diagram commutes". More down to earth, any diagram built only out of the associativity, commutativity and unit maps commutes. This was first formulated and proven by Kelley and Mac Lane in response to a question of Steenrod (when is there a canonical map between modules of certain "shapes" over a fixed ring). First, those Cat maniacs formulated the problem in terms of monoidal categories (heck, they cooked up the categories on the spot!). Then they ran into a bit of a problem. Sure, there are some shapes that have a canonical map between them. The problem, however, is constructing the map. Generally you need to compose together a few maps to get it. Only, sometimes an intermediate shape appears in the composition which is in neither the domain nor codomain. And this object's size is unbounded. Oh, woe is canonicity!

Notice something there? This is precisely the same as the situation with the cut rule. The problem with it is that it leads to intermediate formulae of unbounded size in the proof. Kelley and Mac Lane noticed this analogy, but were not able to make it into anything more than just an analogy. Instead, they proved coherence by defining a notion of a constructible map and proving that every canonical map is constructible. Sounds familiar, eh? This is precisely the point of cut elimination.

Now, via Kreisel, Mac Lane started up a correspondence with Grigori Mints, who was still in the Soviet Union at the time. Mints was able to turn the analogy with cut elimination into more than just an analogy. He showed Mac Lane how the terms arising in a monoidal category are, for all intents and purposes, the same as the terms arising in a certain relevant logic. By proving cut elimination for this logic, Mints was able to conclude coherence immediately! For a short summary of the correspondence between Mac Lane and Mints, see:

"Why Commutative diagrams coincide with equivalent proofs", Saunders Mac Lane, Contemporary Mathematics vol 13, 1982; 387--401

In short, if you have any interest in proof theory and have not read this article yet, then what are you doing still sitting at your computer? Go get it!

What blew me away with this article is that it pretty much covers most of the category theory wizardry used in (exponential free) linear logic, but predates Girard's paper by 5 years. Moreover, the stuff that it speaks about happened way before the article itself was published! Crazy!

Computer Mathematics

2005-08-23T18:03:00.000+10:00

I am rather swamped with things to do at the moment, so my computability logic escapades have been put on halt. This recent upswing in the number of things to do has led me to wish that my computer could do some of them for me. Perhaps the hard bits such as, oh I don't know, proving my theorems. Yeah. That would be grand.

There are two possible routes to follow when getting computers to attack theorems. On the one hand, we can ask that the computer does everything on its own. We just give it the statement of the theorem and away it churns creating a proof. Most succesful theorem provers of this kind more or less use souped up versions of resolution. The most prominent example is OTTER, which handles first order logic with equality.

What's resolution? Say you have a clause C that contains some literal x and another clause D which contains the negation ~x. Then, the resolution rule says to pass to the union of C\{x} and D\{~x}. A resolution refutation is one which consists of a sequence of applications of the resolution rule and ends in the empty clause. As such, it is a negative procedure: feed in the negation of your statement. If your statement is a theorem then the negation is not satisfiable and resolution will be able to pick up on this.

As you might suspect, just using resolution is not a particularly good way of deriving theorems that mathematicians are actually interested in. Moreover, doing things only in first order logic vastly limits what you can even express to begin with. So, not much analysis can be done, for example.

The other approach is to have some amount of user interaction. The most prominent approach to this style of theorem proving is dubbed the "LCF philosophy". LCF stands for the Logic of Computable Functions, which was introduced by Dana Scott around 1970. LCF is also the name of a theorem prover, originally developed in Lisp at Edinburgh. Its philosophy is to have a trusted kernel of procedures that are "trusted" to be correct. Typically, these would be some set of rules characterising higher order logic or some sort of typed lambda calculus. Everything else in the system is built on top of this kernel and compiled down to functions that only use the kernel rules. Much like how a modern operating system is built. While LCF itself is no longer around, many famous modern interactive theorem provers are directly descendent from it, for example Isabelle and HOL4. Incidentelly, the language ML was designed and built specifically for the task of interactive theorem proving which led inter alia to the first incarnation of Isabelle. LCF-style theorem proving has shown up recently on mathematical radars with Georges Gonthier's recent verification of the proof of the Four Colour Theorem:

A Computer Checked Proof of the Four Colour Theorem; Georges Gonthier

Alas, interactive theorem provers do not free me from doing any work. Quite the opposite in fact. This is because, in order to give a fully verified proof of a theorem in an intereactive prover, one must grapple with the "gap problem". What's that? In almost any nontrivial proof, there are statements to the effect of "it is trivial to see that...", "The reader may verify that,...", "the other 1,987,456 cases go through without essential changes" etc. Now, you can't just say that to a computer. You have to fill in all of the gaps! It would be nice if these systems were able to automatically fill in the gaps but, alas, they can't. Oh dear. At any rate, for a light overview of the sorts of problems involved and stuff that has been done, look no further than:

The Challenge of Computer Mathematics; Henk Barendregt and Freek Wiedijk

Computability Logic 1

2005-08-09T16:58:00.000+10:00

In between much excitement, I have started teaching myself computability logic. As I mentioned before, this logic is semantically motivated and, as yet, does not have a completely satisfactory proof theory.

The idea behind computability logic is to model interactive computation. In order to do this, we set up the situation as a game between the user and the computer. In this scenario, we want the computer to win, since this means that the problem is computable and there is an algorithm for solving it. Play proceeds via a sequence of labelled moves, or labmoves. These are strings representing the move, labelled with which player made the move. A run is a finite or infinite sequence of labmoves and a position is a finite run.

It is quite easy to define one of the simplest notions of game involved, that of a constant game. This consists of a set of runs not containing a special symbol, say ♠. This set satisfies the condition that a run is contained within it iff all of its nonempty finite initial segments are there too. These runs code up the legal runs for the game. We force each player to play according to the rules by stipulating that the first player to make an illegal move immediately loses. That is, say the game is in position Γ and I make the move α. If Γ is a legal run but (Γ, α) is not then I lose. Boo!

Together with this collection of legal runs, a constant game also contains a function which sends each run to one of the players, indicating who has won. There are various finiteness conditions that one can stipulate on the set of runs, but I will introduce these as and when they are needed.

One important point to note is that we have not stipulated that, at any given stage of the game, only one player can move. If this happens to be the case, we say that the game is strict. In general, we will not restrict ourselves to strict games as these do not model all the sorts of interactive computation we may find ourselves performing.

One way to think of what is going on is to imagine interacting with a server. We keep sending it queries and it keeps replying. Of course, nothing is stopping, say, Bob from being annoying and sending lots of requests before receiving any replies from the server. Moreover, at any given stage the server may reply to any of Bob's previous queries or Bob could send yet another request. No sweat, we can model that, since we do not require the game to be strict.

Let's look at how to recover classical logic and Church-Turing style computablity. If every legal run in a constant game has length at most k, then we say that the game has depth k. Classical propositional logic corresponds to depth 0 games. There are precisely two of these. One of them returns the computer as the winner immediately and the other returns me as the winner immediately. If we model one of these as truth and the other as falsity, then we have classical logic. That is, all that matters is the input - we immediately get an answer. This is not particularly interesting but will eventually lead to classical logic being an elementary fragment of computability logic.

Modelling traditional computation is slightly trickier, though not too hard. What we do is model it as a depth 2 game. If we do nothing, then the computer has won (since it has nothing to answer for!). The next level consists of us handing the computer an input. At this stage, we are at depth 1 and we have won the game! The next level consists of all of the computer's possible responses. Now, what does it mean for the computer to have a winning strategy for this game? Precisely that no matter what our input, one of the computer's possible replies is the correct one. So, traditional computation is a depth 2 game, in this setup. This is not to be confused with how we traditionally model nondeterministic computation by building a tree or somesuch. In this situation, the tree represents the actual computation steps that the computer is performing. In Computability Logic, we are only interested in the interaction going on, not in the actual computation steps.

Next time: Non-constant games and operations on games.

Proofs as Games

2005-08-02T18:23:00.000+10:00

Proof theory has undergone many transformations over the hundred or so years of its existence. It seems reasonable to roughly segregate its development, though note that my partition of history is rather arbitrary! In particular, important open problems from each period are still being actively researched today and I haven't mentioned stuff like proof complexity. Nevertheless, here it is:

1900-1930: The birth of proof theory, in the guise of Hilbert's program for formalising mathematics. The end of this period is marked, of course, by the incompleteness theorems. However, this is not to say that the program was completely without use. On the contrary, much current work in computer science can be seen as an extension of work arising from this period. For instance, Russell and Whitehead's Principia did not give us a foundations for mathematics, but it did so for programming language theory by giving us type theory. Moreover, Hilbert's epsilon calculus is still going strong and is in active use in the proof assistant community.
1931-1986: This period predominantly consisted of analysing the ordinal strength of increasingly complex systems. A representative problem of this period was Takeuti's Conjecture, which is roughly the assertion that second order logic has cut elimination. Or, if you want to be fancy, you can say analysis instead of second order logic. This conjecture implies, for instance, the consistency of full second order arithmetic (PA2). Of course, Takeuti's conjecture cannot be proven from within PA2. As such, it was widely believed to be false for quite a while. This belief turned out to be wrong. The first proof was given by Tait in 1965, building on previous work of Schutte. This proof was semantic, a style of proving cut elimination that is often unsatisfactory since it does not provide enough information. In 1972, Jean-Yves Girard provided a syntactic proof of the theorem and subsequently gave birth to System F, which has continued to hold importance for programming language theory.
1987-2000: I choose to mark the beginning of this period with Girard's paper on linear logic. This view may be somewhat contentious. The reason is that, if one focuses on the exponential-free fragment of linear logic, then these logics had been around for many years under various names (relevant, paraconsistent, substructural,...). However, the main feature of Girard's approach is more philosophical: we should study proofs as the objects of interest, not the set of provable assertions. Subsequently, our semantics should be a semantics of proofs. That is, formulae should correspond to objects in a space and proofs to maps between them. In this way, we can begin to ask what distinguishes proofs of the same assertion. Developing a good semantics of proofs is an ongoing problem and much exciting work remains to be done. Already at this stage of history, there were indications that classical proof systems such as sequent calculi would buckle under the pressure of applications. They managed to hold up, but only just...
2001-Present: Welcome to the new millenium! With the majority of logicians finding themselves in computer science departments, proof theory has become a powerful weapon for attacking computational problems. It turns out that the world of computation presents many more challenges for proof theory than the world of truth. For instance, in a concurrent or distributed system, it matters in what order processes are executed. This leads to a whole host of concerns, since nice things like conjunction no longer commute. Moreover, computers are now networked, with computations regularly being distributed around many machines. What does interactive computation mean? What, pray tell, is a computational problem anyway and how can we capture this in logic?

Typically, for a computational logic, nobody knows how to give a cut-free sequent calculus or similar system. This has led to a host of different formalisms being invented or brought in from the cold, with the inter-relationships amongst them not completely understood: Display logic, hypersequents, calculus of structures, proof nets, cirquent calculus,...

The problem is fundamental. If we are going to take seriously the claim that proofs correspond to programs, then we need a system that facilitates the study of the dynamics of proofs. Arm-wavy claims such as "linear logic is resource sensitive" are not sufficient. Increasingly, logicians and computer scientists are starting to desire a reasonable model of interactive computation. Two related systems present themselves at the moment: Computability Logic, introduced by Giorgi Japaridze and Ludics, introduced by Girard. The striking feature of each is that they are based on the idea of modelling computations/proofs by certain games. Computability Logic presents a major problem to proof theory, since it is semantically motivated and developed, with no clear way of capturing it in a syntactic system. As for Ludics, it is not clear precisely how it relates to computation.

As I am currently teaching myself both computability logic and ludics (I spent most of the morning printing and binding imposingly heavy papers!), I have decided to make a series of posts keeping a log of my progress. If anyone else is interested in learning about these systems, let me know and we can maybe do an internet-based reading group thingy!

Summer Fun

2005-07-26T14:32:00.000+10:00

Every year, ANU offers summer scholarships in order to allow undergraduates in Australia or New Zealand to get a taste of research. These scholarships cover transport costs, accomodation and three meals a day at one of the residential colleges as well as spending money. There are also regular social events, both amongst the summer scholars (who come from a wide range of disciplines and locations) and within the particular research schools and departments.

So if you like logic, come on over! There are a number of logic projects available, with more to come. During the summer, there is also the Logic Summer School, as well as a stream of international visitors. I have hacked up a little page with some more info, as well as details of the projects that I am offering.

If this sounds like fun to you, then drop me a note at jonathan(dot)cohen(at)anu(dot)edu(dot)au. Apply the uniform substitution (dot) --> . and (at) --> @ to get my email address. Similarly, if you know anyone who may be interested then go ahead and pass on the details.

Workshops Day 2

2005-07-20T13:35:00.000+10:00

It's lunchtime at StreetFest, so I'll take the opportunity to post a bit about what's been going on!

John Baez kicked off the day with a talk on higher dimensional gauge theory. The basic idea here seems to be that you figure out what happens when particles move around on a manifold with odd curvature. The interesting thing is that it is no longer possible to compare, say, two vectors but it is only possible to compare them relative to some path which brings them together. The other cool thing I found out about is something called a "thin homotopy". This is just like Ye Olde Homotopy, except that it sweeps out no area. For instance a homotopy which only does stuff like backtracking along a path is a thin homotopy. Working modulo thin homotopies seems to be the thing to do in this area. Anyway, the slides from the talk are up here.

After that there was a really fun talk by Timothy Porter, who has a wonderful sense of mathematical humour! He was speaking about topological quantum field theories and I managed to follow along a bit and see what manifolds and cobordisms have to do with braided monoidal categories. Neat stuff!

Next up was Andrey Lazarev who spoke about graph cohomology. I don't really understand this stuff so I won't say any more.

In between the talks I had some nice discussions with category theorists about higher dimensional rewriting, noncommutative logic and that sort of jazz. I'll probably hang around at Streetfest for the rest of today and tomorrow - this post will be updated later with the afternoon's talks. Mayhaps someone else will blog details of the philosophy workshop...

Update (26/7): Not many more of the talks were logic related so I decided to stop posting details.

Workshops Day 1

2005-07-19T23:55:00.000+10:00

This morning I hung out at StreetFest and learned a bunch of stuff about category theory. First up was Ross Street who spoke about centres in monoidal categories. A monoidal category is essentially a category that carries a "monoid" structure, which may be thought of as a tensor product. An example from logic is the tensor product (conjunction) of linear logic. Or, if you prefer other language, the "fusion" of relevant logic. Or of Lambek Calculus or...

Here's a nice way to think about this. Suppose we only have the tensor-like conjunction. Then, a formula looks something like A ⊗ B ⊗ C. Represent each of A, B and C as a string connected between two bars. So, we have something that looks like:

The centre of this widget is all those formulae A such that A ⊗ X ≡ X ⊗ A for all other X. It turns out that the centre of a moinoidal category is always "braided". That means, if A and B are both in the centre and we go from A ⊗ B to B ⊗ A, then it matters whether we passed A "under" B or A "over" B. This corresponds to the following two situations for our strings:

Remember that the strings are tied at the top and the bottom, so there is no way to pass from one "braiding" to the other (without cutting the strings of course!). Thus, the centre of a monoidal category forms a "braided" monoidal category. These crazy cats crop up all over the place. Quite famously, they are related to topological quantum field theories! The idea is that we imagine some particles (two say. Perhaps named A and B...) floating around in space (on a plane, say). Then, they can pass around each other in all sorts of fanciful ways. If we trace the history of where each particle has been, lo and behold we have a braiding!

As it happens, there are two ways to define a centre in a monoidal category. On the one hand, we can postulate a bunch of commutative diagrams which say that we can shift elements in the centre around however we please. This is called the "lax" centre. The other way is more refined and related to some constructions in algebra (which I have not fully grokked yet!). Essentially, each object, A, in the centre comes equipped with a bunch of "natural transformations", one for each object X in the category, which take A ⊗ X to X ⊗ A. Interestingly enough, these two notions of centre are not always the same (something I hadn't realised before today).

The other highlight of the categorical morning was Robin Cockett, who gave a beautiful talk about turning differential calculus into category theory! That is, we search for categorical analogues of "differentiable" and "smooth" functions. The idea is that we extend lambda calculus with the ability to do differentiation. Except, we do this in a category theoretic setting. This was quite a fun talk with lots of neat diagrams (no one can draw diagrams like a linear logician can!). Rather than waddle may way through discussing this stuff, I'll just point you to the paper (hot off the presses!) wherein all of this is done:

Differential Categories; R Blute, JRB Cockett, RAG Seely

I skipped out on the afternoon's categorical proceedings in order to hop along to the philosophical methodology workshop. Today's events were mainly devised for a group of visiting undergrads and had philosophers explaining their own take on general methodologies for doing philosophy. This was quite a nice insight into the philosophy world for me (since I am, after all, a philosophical neanderthal...). One of my motivations is that I would like to understand how people come up with conjectures and build arguments, so that I cant teach a computer to do the same! I managed to catch two of the talks. First up was Alan Hájek, who spoke about "Philosophical Heuristics". This was quite a neat talk explaining some general procedures for examining philosphical arguments in order to find bogus features. The general techniques are very familiar from maths, though there I think the situation is often a lot clearer since, for instance, definitions are clearly delineated! Quite amusingly, and rather contentiously by Canberra standards, his handout labelled nonclassical logics as weird... After that, Dave Chalmers spoke about "Terminological Disputes" - general ways of deciding whether an argument/disagreement is "terminological". That is, whether there is only a disagreement because the different parties parse a certain term differently.

Tomorrow I will once more hang out at StreetFest for part of the morning and then head over to see what else the philosphers have to say about methodology!

Workshops Galore

2005-07-17T15:11:00.000+10:00

The next two weeks are fairly busy this end of the world. Starting tomorrow is the ANU wing of StreetFest, so a bunch of category theorists will descend on Canberra to mark Ross Street's 60th birthday. I'll be going along to a few of the talks (those whose abtracts don't fly too far over my head!). Coinciding with Streetfest, the philosophers are putting on a workshop on philosophical methodology, which I will try to get to (well, at least to a bit of it!). Following hot on the heels of that is an instructional program and workshop on noncommutative geometry and index theory, which I will also be attending. I'll post details of any talks that are directly related to logic.

Blogicians

2005-07-14T00:40:00.000+10:00

Both Kenny Easwaran (Antimeta) and Gillian Russell (logicandlanguage.net) were at ANU this week. Gillian was game enough to lead a NotYASS session, despite only arriving in Canberra the same day (if you'll pardon my colloquialism, on ya Gil!). At any rate, here is a pic of the three of us. Unfortunately, we couldn't seem to agree what camera to look at (maybe their pictures fared better)...

What do you mean?

2005-07-12T14:49:00.000+10:00

How do I understand what people say? It seems like an impossible thing to do. Every day people utter sentences I have never heard before. And I take it all in and understand them. Bizarre! The most natural explanation of this phenomenon is that I understand what each of the words mean individually and I have some rudimentary understanding of how to put them together to form sentences. But, come now, that can't be all there is to it! Let's see what the linguists have had to say about this.

Compositionality is the principle which states that the meaning of a compound expression is a function of the meaning of its parts and of the syntactic rule by which they are combined. It is this second part which carries most of the import.

Even in purely logical endeavors, the situation is not cut and dry. For instance, in the substitutional interpretation of classical predicate logic, one can derive (∀ x)φ(x) from φ(a), where a is arbitrary. This breaks compositionality. That is, how is one to find the correct interpretation of (∀ x)φ(x) given only one φ(a)? One possibility is to add an infinitary rule, which essentially identifies the universal quantifier with an infinite conjunction. This proposal suggests to me that something like descriptive set theory may be useful, wherein hierarchies of sets correspond to suitable classes of first order sentences.

Not every linguist is too chuffed with compositionality and many counterexamples have been proposed. However, for the most part, these can be dealt with by modifying and/or enriching the syntactic aspect. One of the objections is sentences such as the following:

(1) Joseph said that a child had been born who would become ruler of the world.

Sentence (1) is ambiguous. That is, will the child become ruler of the world in the future of Joseph or in his past? Both are possible. One of the most interesting approaches to dealing with this is similar to how one deals with de dicto/de re ambiguities. That is, one invokes the following:

(*) Different possible interpretations of a sentence correspond to different derivations.

"Derivations" here is taken to mean something along the lines of a derivation in a categorial grammar. Or, say, in parsing. This is quite appealing and is a good motivation for studying isomorphisms of derivations. That is, one would like a natural notion of isomorphism, wherein isomorphic derivations correspond to the same interpretation of a sentence. Is it possible that breaking derivations up into isomorphism classes deals with ambiguity? This does seem like a plausible notion, though one would have to assess the actual notion of isomorphism before being fully convinced.

So, are there sentences which are not compositional? Well, if so, then they would be very odd sentences indeed. That is because every recursively enumerable language can be generated by a compositional grammar. Unfortunately, the way this works is to pick and choose your particular grammar. Not so nice. As a result, one will always eventually run into trouble when using a particular compositional grammar.

So, one possible explanation of how I understand what you say is that I am very good at picking the correct compositional grammar to use in the correct situation. Or, more likely, I have evolved a particular grammar that works quite well in most situations. This is evidenced by the fact that I, like all other children, probably uttered a sentence such as:

(2) I seed two mans

The problem with (2) is, of course, that whatever grammar I was using at the time was a bit too weak and had rules for changing the tense and for pluralising that are not always correct. I'm a bit better at doing these things now...

(The technical parts of this post are mainly based on T.M.V. Janssen's article in The Handbook of Logic and Language)

NICTA L&C

2005-07-04T16:10:00.000+10:00

NICTA's Logic and Computation Program has finally decided to admit that I exist. They may, of course, come to rue this decision... And, no, I am not either of the two people in the photo at the top of that page. Heck, I don't even know who they are! Although, that picture isn't on any other group member's biography page. Hmmm....

Dichotomy 2

2005-06-29T22:24:00.000+10:00

This post is a sort of continuation of my previous ramblings about dichotomy theorems.

Recall that Schaefer's Theorem essentially says that every boolean constraint satisfaction problem (CSP) is either in P or NP-Complete. Is there any real content to this? That is, if P is not equal to NP, then is there anything in between? The answer to this question is given by a famous result due to Richard Ladner - if P is not NP, then there is an incomplete set in NP - P. That is, there is a problem which is in NP, but in neither P nor NP-Complete. This result is contained in:

On the Structure of Polynomial Time Reducibility; Richard E. Ladner

A nice follow-up paper, which includes a succint account of two proofs of Ladner's Theorem in an appendix is:

Uniformly Hard Languages; Rod Downey and Lance Fortnow

Actually, Ladner's Theorem says that there would be a dense hierarchy of sets between P and NP. So, somehow Schaefer managed to home in on a large piece of NP that skips out anything in between P and NP, whether there is anything there or not. I previously pointed to some articles that look to extend Schaefer's theroem to broader classes of CSP's by translating everything into universal algebra.

Another approach is given in the following remarkable paper (with an unfortunately long title!):

The Computational Structure of Monotone Monadic SNP and Constraint Satisfiaction: A Study Through Datalog and Group Theory; Tomas Feder and Moshe Vardi

Their approach is to start from Fagin's Theorem, which says that NP is precisely the class of languages expressible in existensial second order logic. By placing increasingly many syntactic restrictions on the language they use, they eventually end up with a logic which does not seem to fall prey to Ladner's Theorem. This logic then turns out to be equivalent to the class of CSP problems, though one direction of the equivalence uses a randomised reduction (it is an enticing open problem to derandomise this).

The article does not really succeed in identifying a large subclass of NP that has a dichotomy theorem. What it does do, however, is to explain the various cases of Schaefer's theorem and why each of them are polynomial, in a manner which facilitates generalisation. What they discovered is that "linear equations mod 2" is polynomial for a very different reason to the other cases. Rather than summarise their results (of which there are many!), I'll just point you to slides for a talk that I gave recently on the topic:

Deeper into Dichotomy: Splitting the Computational Universe; Jon Cohen

I tend to say a lot more in a talk than is on my slides and this talk was no exception. One thing I mentioned that is not on the slides is a neat dichotomy result from combinatorics. Consider the problem of deciding whether it is possible to colour the vertices of a graph with three or fewer colours in such a way that no two adjacent vertices have the same colour (that is, the 3-colourability problem). If you squint a bit, then you'l see that this is the same as asking if there is a homomorphism from the graph you are interested in, to the complete graph on three vertices, K3. To see this, just paint each vertex of K3 with a different colour and remember that there are no self-loops.

So, we have turned the colourability problem into a homomorphism problem. Now, there is nothing wrong with varying the target graph. What you get is the H-colouring problem. If the target graph is a complete graph, then you just get the standard k-colourability problem. It turns out that, depending upon the type of the target graph, we get a dichotomy! That is, if the target graph is bipartite, then the H-Colourability problem is in P, otherwise it is NP-Complete. This result is contained in:

On the Complexity of H-Coloring; P. Hell and J. Nesetril, J. Combin. Theory Ser. B, 48 (1990) pp. 92--110.

Anyway, there is loads of interesting stuff in Feder and Vardi's paper and it is well worth checking out if you are interested in the interaction between logic, complexity theory and group theory!

Typesetting

2005-06-20T17:48:00.000+10:00

I am busy writing a longish paper on some proof theoretic mumbo jumbo. As such, I probably won't post much until the blasted thing is finished (writing about logic is not a very efficacious way to have a break from writing about logic :). But, that is not the point of this post.

Typesetting a logic paper, especially a structural proof theory one, can be quite tedious. I am aware of the Latex for Logicians page and am using the bussproofs package for typesetting formal proofs and calculi and such. Later on, I will probably need to typeset some proof nets also. For this, I am thinking of using the XY-Pic package, which I have used in the past for drawing simple diagrams.

Does anyone with experience typesetting this sort of thing have any helpful suggestions? In particular, if you have hacked up some macros or parsers or such that make the job a little easier, I'd be most grateful if you would pass it on! Even some code snippets of good ways to typeset stuff like proof nets would be handy, so that I don't need to reinvent the wheel. Thanks!

Labelled Tableux

2005-06-13T22:34:00.000+10:00

Yes, I know that Greg scooped me on this one, but Thomas Sutton has started a blog charting his development of a modal logic theorem prover written in Haskell and based around labelled tableaux. I point you to: Labelled Tableaux.

Labelled what you ask? A tableau is a proof theoretic gadget that looks and feels much like a collection of "uspide down sequent rules". The idea of tableaux is that instead of proving a formula, we show that its negation is inconsistent with the logic. This works especially well in the case of modal logic, since the tableau rules tend to match the frame semantics quite closely. Moreover, if the statement is not a theorem, then we can extract a countermodel from the failed proof search. This is quite dandy! For an introduction to tableau calculi for modal logic, including as much modal logic as is required, see:

Tableau Methods for Modal and Temporal Logic, Rajeev Gore'

(Full disclosure: Raj is one of my PhD supervisors. Of course, I give the article three thumbs up :)

So, what is all this labelling about then? Well, modal proof theory is a tricky thing to get right. In order to avoid nasty things such as infinite looping during proof search, many people have incorporated "labels" into their tableau calculi. This is not so nice from a theoretical point of view, since it obfuscates the essence of the logic and has a very "hacky" feel to it. Of course, if you are actually building a theorem prover, then labels are very handy!

A question that occurs to me is whether anyone has beaten semantic tableaux into providing systems for paraconsistent logics. This is a family of logics where an inconsitency does not necessarily trivialise the theory. Or, alternatively, where both a statement and its negation can be theorems! The basic strategy of attacking the negation of a formula seems, at first glance, to be at odds with this property. I'd be interested in any work that proves me otherwise.

Anyway, I'll be interested to see how the project turns out for Thomas. Maybe he'll let me play around with it when he is done... :)

To Categories!

2005-06-07T17:27:00.000+10:00

One hot area of proof theory research is categorical semantics of proofs. For some, this abstraction may seem like needless faffing about. I'll admit that I used to think that myself. I'll try to convey the intuitions that led me to change my mind.

Traditionally, the way in which one obtains an algebraic model of a logic is to pass to the so-called Lindenbaum algebra of the logic. Let's look at that process for classical logic. The first step is to define an equivalence relation on the set of well formed formulas (wff's). If x and y are wff's then define the equivalence relation ~ by saying that x ~ y iff |- x <-> y. Letting [x] denote the equivalence class of x under this relation, we define a partial order on the set of equivalence relations by saying that [x] <= [y] iff x |- y. So we have a poset, which we can turn into a lattice in the obvious way by defining [x]&[y] = [x&y] and [x]v[y] = [x v y]. Why might this not be a good enough semantics for us? Well, the point is that the partial order only records the fact that there is some proof of x |- y -- that is, some deduction from x to y. Thinking topologically for a moment, suppose we have two points in a topological space. Then, the equivalent notion would be to say that there is a path from x to y. But, whether or not all paths are "equivalent" depends on the space!

Recall that given two paths f,g from x to y in some space, f and g are homotopic if they can be continuously deformed into each other. This is not possible if, for example, there is a hole between them. Merely recording the fact that there is a path does not capture this information.

So, one might try to do the same thing for logic. If you try to do it concretely, by defining actual topologies on the logic, then you'll find yourself getting into a bit of a tangle. In fact, I tried to do this for a while, before caving in and doing it via categories. Categories work much smoother!

The idea is that we build a category C whose objects are formulae and whose arrows are "equivalence classes of proofs" between formulae. Defining the equivalence relation in a reasonable manner is a tricky business. Looking a bit closer, take two formulae x and y and consider the set of all proofs from x to y (for the finicky category people out there, there is no real loss in making the category locally small). This is denoted Hom(x,y). If this is nonempty, then we can "look inside" and consider how the equivalence relation works out. One usually does this by proving cut elimination and then looking at cut-free proofs. I'll discuss a logic where this procedure works out in a really cool way from a mathematical standpoint in a later post.

But, why stop there? We may delve deeper into Hom(x,y) and look at procedures for sending one proof to another, just like a homotopy! In the current set up, this means that we would have a bunch of what are called 2-morphisms. These are fella's that send morphisms to morphisms. Sound heady? It's not. What we have done is to form a category whose objects are the sets Hom(x,y) and whose arrows are transformations of proofs. Thinking about this more would take us deep into the waters of n-categories, so I will leave that for another post.

Taking a step back and having a look at what we have done, we see that categorical semantics focus on proofs whereas traditional algebraic semantics focus on "mere" provability. There are some nice theorems that go via category theory to derive models for a logic which are complete in a very strong sense. That is, if two proofs are equivalent, then they are equivalent in every model and if they are not equivalent, then there is some model in which they are not equivalent. These "models" are usually built from some heavy duty mathematical gadgets.

Anyway, for those looking for a good survey of category theory as it applies to logic, check out:

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

Logic Down Under

2005-06-02T15:15:00.000+10:00

The deadline is fast approaching for submissions to this year's Australasian Association for Logic Conference. Paper abstracts need to be in by July 24, with the conference being held September 24 -- 25 in Perth (my home town!). The early deadline is partly because the conference is sponsored by the ASL, with abstracts appearling in the Bulletin of Symbolic Logic. This also means that I need to decide what I want to speak on pretty soon!

This conference immediately precedes the Australian Mathematical Society Annual Conference. Among the special sessions this year are three of interest to the logically minded: Logic, Algebra and Mathematics of Computation. Abstract deadlines for the AustMS meeting are not available yet, but will most likely be late August.

It is a pity that this year's Victorian Algebra Conference has been scheduled to coincide with the AAL conference, so I won't be able to attend both. Monday of this conference does not clash with the AAL though and has the theme of groups and combinatorics, which was lots of fun last year.

However, with the coupling of the AAL and AustMS meetings, it means that the organisers have been able to pursuade some international speakers to come along, including Heinrich Wansing, Michael Zakharyaschev, Andreas Weiermann and Angus MacIntyre.

Dichotomy

2005-05-24T16:39:00.000+10:00

Way back at the dawn of complexity theory, it was proven that the problem of deciding whether an arbitrary 3-CNF formula is satisfiable is NP-Complete. Here, 3-CNF means that in conjunctive normal form, each clause has three literals. Say that your 3-CNF formula is built from k variables. One way to model the satisfiability problem is to attach to each clause the set of all k-tuples that satisfy that clause. The satisfiability problem then boils down to deciding whether these sets have a nontrivial intersection.

We can abstract things a little here. The tuples we considered above are, of course, k-ary relations on the alphabet {0,1}. Start by taking a collection of relations on {0,1} of arbitrary, but finite, rank. Now, build a formula by using existential quantification of variables as well as conjunctions of relations on those symbols. In other words, conjunction of things that say stuff like "(x1,x2,x3) is in relation R". What we have now is something called a boolean constraint satisfaction problem. We may very well be interested in the complexity of such problems.

Let X be a set of these sorts of relations. Then, the "Schaefer Dichotomy Theorem" says that deciding whether the constraint problem for X is satisfiable is in P if and only if one of the folloing conditions holds:
(1) Every relation in X contains a tuple in which all entries are 0
(2) Every relation in X contains a tuple in which all entries are 1
(3) Every relation in X is definable by a conjunction of horn clauses
(4) Every relation in X is definable by a formula by a formula in CNF in which each clause contains at most one unnegated variable.
(5) Every relation in X is definable by a 2-CNF formula
(6) Every relation in X is the set of solutions of a set of linear equations over {0,1}, considered as a field.
Otherwise, the problem is NP-Complete.

This result is contained in:

The complexity of satisfiability problems, Thomas J. Schaefer

We might be interested in extending this "dichotomy" to arbitrary constraint satisfaction problems (CSPs). This is considered in the following paper, where it is also shown that there is a strong connection to the algebraic notion of "clones":

Classifying the Complexity of Constraints using Finite Algebras; Bulatov, Jeavons and Krokhin.

They state Schaeffer's dichotomy theorem in the special case of boolean CSPs where each operation is actually a function. It turns out that a set of such operations is tractable (i.e., the corresponding problem is in P) if it contains an essentially non-unary operation. Otherwise it is NP-Complete. What is an essentially non-unary operation? Well, it is an n-ary function whose value does not depend on only one coordinate as, say, the projection functions do.

This is all quite neat. However, times have changed and P is no longer considered all that tractable. Can we get a more refined analysis of the cases in the Dichotomy Theorem? The answer is yes, and is considered in the following paper, which also uses clones:

The Complexity of Satisfiability Problems: Refining Schaefer's Theorem

For those who prefer categorical language, a clone is what is also known as an "algebraic theory". That is, take a category, C, which has finite products. An algebraic theory is more or less the image of a functor from C to the category of sets that preserves finite products.

Logicomp

2005-05-19T00:55:00.000+10:00

Anthony Widjaja To has started Logicomp, a blog devoted to the links between logic and computation and, in particular, finite model theory and descriptive complexity. In his first couple of posts, Anthony looks at different subsystems of first order logic that are decidable and yet surprisingly strong.

It's nice to see the blogging community growing and incorporating a nice cross section of modern logic. I am also quite pleased to grab my first blog scoop :)

Quantifying Symmetry

2005-05-14T13:22:00.000+10:00

This week, my first published paper came out online. In it, I consider the problem of making precise the vague notion that one object may have more qualitatively different symmetries than another. It's expository in nature and (I hope) easy to read. There's nothing new in it, but I am still quite pleased that my first publication was an invited paper!

Quantifying Symmetry, Jonathan A. Cohen

Its contents are more or less a different spin on a piece of my undergraduate dissertation. For the adventurous:

Small Base Groups, Large Base Groups and the Case of Giants, Jonathan Cohen

Linguistic Tricks

2005-05-11T16:30:00.000+10:00

So, I have been doing a little linguistics. A shocking revelation, I know, but I may as well jabber on about it a bit.

Way back in the days before colour television, Jim Lambek turned the linguistic notion of categorial grammar into logic. We've all seen something of the sort in school - nouns, adjectives, subjects and silly old intransitive verbs - to name but a few of the categories you may very well have been subjected to. The question then is how members of these categories can be glued together to form a valid sentence. Or, to turn the problem on its head, how we can get a computer to decide whether or not a sentence is grammatical. Lambek addresses these in his paper:

The Mathematics of Sentence Structure, J. Lambek

Forever more, the system presented in that paper has been known as Lambek Calculus. If you are familiar with Sequent calculus, Lambek Calculus fits in like this. Start with Ye Olde Calculus for the negation free fragment of intuitionistic logic. First off, get rid of contraction and weakening. What happens is that conjunction shatters into an "additive" version and a "multiplicative" version. Keep only the multiplicative version. Then, do something dastardly and devious - drop exchange also. If you do this, then implication breaks up into two versions of implication, both of which are residuated with respect to your conjunction. What this means is that x and y entails z if and only if x entails that y implies z. And the same thing with "implies" replaced with your other implication, let's be silly and call that "coimplication". Lambek denotes these little beauties by / and \ respectively. If you like category theory, this just means that Hom (x and y, z) is isomorphic to Hom(x, y / z) and also to Hom(x, y \ z). So, we have some adjunctions floating around.

Linguistically, however, getting rid of all of the structural rules is a bit on the dodgy side. For instance, it has been shown that the Lambek Calculus only really generates context free grammars. Most unsatisfactory! What we can do, however, is to let the structural rules back in a controlled and regimented way (much like linear logic...). So, for instance, we may have a unary operator that says that everything in its scope has access to weakening. Here is an example where this all makes sense:

(1) Take the book to John

Let us now postulate that the noun phrase "John" has access to weakening. In which case, we derive that the following is grammatically valid:

(1') Take the book to John, Mary, Jane and Susan

This makes a lot of sense linguistically. Logically, however, these structural "modalities" open up a can of worms. For instance, if we make the conjunction commutative, by adding back exchange, then the two sorts of implication collapse back to classical implication. If we now add modalities for contraction and weakening, then we get linear logic! Although...exchange is not really warranted on linguistic grounds, because we do really want the two sorts of implication to be different.

I suppose the area where this sort of stuff is best understood is the proof theoretic side of things, where Belnap's "Display Logic" provides a nice formalism for systematically adding in these sort of modalities and obtaining cut elimination for free. More or less what is known is contained in this thesis:

Reasoning with polarity in categorial type logic, Raffaella Bernardi

I'll speak about the semantic side of things another time, when I have grokked a bit more...

Logician?

2005-05-06T10:26:00.000+10:00

(Definition via Uncyclopedia)

A logician is an entertainer who tries to make people laugh by playing tricks and acting, not unlike clowns do, but clowns take their jobs much more seriously than most logicians. Most traditional logicians try to reduce as much as they can to absurdity, using reductio ad absurdum , thus making falsum the sound basis of all knowledge.

In most cases, logicians have a very high EQ, and their social skills are more developed than those of average people. At parties, they are often in the center of the attention, dancing and telling wild stories and a lot of rubbish to entertain people. Their favorite trick is to ask people to state something, which they then reduce to absurdity within seconds.

Doing Proofs

2005-05-02T10:41:00.000+10:00

Casually reading through Greg Restall's book on substructural logics, I came across a curious line:

"However, proofs are not so easy to construct in tree form - often it is easier to construct proofs writing the consecutions in a list."

Personally, I have always found the "list" way of constructung proofs to be rather arbitrary and nonintuitive. If I have access to a sequent(esque) system, then I invariably construct the proof by doing a backwards "proof search". But maybe that is because I cut my (logical) teeth by working on theorem proving software.

I'm interested in seeing what method other people prefer, so leave a comment if you have a preference!

Symmetry of Phase Transitions

2005-04-29T08:50:00.000+10:00

(sorry, I couldn't find free versions of most of the papers linked to in this post. If you find free versions, please let me know).

One hot research areas of recent times is phase transition phenomena in discrete structures. One of the first examples is that of a random graph. Fix a certain number n of vertices, initially with no edges. Now, add an edge uniformly at random (so you add one of the n(n-1)/2 possible edges , selected at random). Pay attention to a graph property that you like. Let's say the size of the maximally connected subset (that is, the largest subset of the graph such that there is a path between any two vertices). I'll call this the MCS for brevity. Something pretty cool happens when you repeat the process. That is, keep throwing random edges in, keeping track of the size of the MCS. What you will find is that a "phase transition" happens where the MCS suddenly jumps from being very small, to being almost all of the graph. That is, the number of connected components of the graph suddenly decreases. This is very similar to what happens when, say, a liquid transitions to a gas in a physical system, hence the name.

It turns out that these sort of transitions happen in the boolean satisfiability problem also. One example is by tracking the hardness of a problem relative to the clause/variable ratio. A representative publication on this topic is:

Phase Transitions and Backbones of 3-SAT and Maximum 3-SAT. Weixiong Zhang

It turns out that understanding phase transitions may very well be linked to one of my pet topics - symmetries of boolean functions. We look at a slightly different phase transition though.

Say you have a boolean function, f, of n variables. Well, not just any such fundtion. Specifically, f is monotone (so contains no negated atoms) and its automorphism group is transitive. As usual, the automorphism group acts by permuting variables. Now, pick some probability p and assign each variable of f the value 1 independantly with probability p. Let u(p,f) denote the probability that f is satisfied under this assignment. Since u is monotone in p, intervals of values of p pick out a corresponding interval of values of u.

With this in mind, fix some small real e > 0. Define the threshold interval to be the interval [p1,p2] such that u(p1,f) = e and u(p2,f) = 1 - e. In words, this is the interval of probabilities such that f goes from being almost surely unsatisfied to being almost surely satisfied. If this interval is "small", then we have ourselves a phase transition.

Remember that we have some knowledge of how the automorphism group, G, of f acts though. What we do now is to look at the action that G induces on the powerset of variables in f. It turns out that if the orbits of "large" subsets is "large", then the transition interval is small, hence we have ourselves a phase transition. This result crops up in the following paper:

Influences of Variables and Thresholds under Group Symmetries" J. Borgain and G. Kalai.

Now, let us look at what happens in graphs. It turns out that we can be quite general here. A monotone graph property P is one such that if some graph G satisfies P, then every graph on the same set of vertices containing G as a subgraph satisfies P as well. The trick now is to move to something called the Hamming Space and pick out a subset, A, of n points that is "monotone" and is left invariant under some transitive permutation group on that variable set. The threshold interval for A turns out to be very very small indeed. In fact, around O(1/log(n)). From this, one can deduce the same result for montone graph properties. That is, every monotone graph property undergoes a phase transition. That's Cool! This result is contained in:

Every Monotone Graph Property has a Sharp Threshold Ehud Friedgut, Gil Kalai

The natural question then to ask is what the transitive group looks like? In the special case of monotone boolean functions with transitive automorphism group, this amounts asking what the group must be for the function to undergo a phase transition, in the probability sense. Using the usual permutation group trickery, we can answer it for the special case of primitive groups. It turns out that in this case, the group must either be the full alternating or symmetric group on the variable set:

Asymptotic Behaviour of Finite Permutation Groups Acting on Subsets Carmit Benebnisty and Aner Shalev.

Certainly both of these groups satisfy the property that the orbits of "large" subsets are "large", since they both act transitively on the set of k-subsets for any valid k.

Unspeakable Sin

2005-04-28T11:06:00.000+10:00

Back when I was an undergraduate and only just starting out on the mathematical path, I learned a fair amount of vector calculus, topology and manifold theory from a rather entertaining (some say peculiar) man named Mike Alder. Now, anyone who believes that reading pure maths notes cannot make you laugh is invited to peruse Mike's manifolds notes (and, yes, that is an aweful lot of stuff for a one semester undergraduate level course). Sadly, he has not made his algebraic topology notes available online.

But this is all besides the point. Mike sometimes moonlights as a writer for Philosophy Now. In one such article, he considers the case of someone he once knew who refused to accept modus ponens as a valid rule of inference. In Mike's words:

"I was pretty clear therefore that Miss B had done something heinous. Whether it merited a prison term I was not quite clear. Maybe it was something where pointing out the error of her ways and deporting her to Australia would be enough. But it was very bad. Immoral if not illegal"

At any rate, it is a rather entertaining article. Those who do not like reading opinionated stuff when the opinion is not their own are hereby warned. If you have the moxy, then go on to read:

The Compleate Logician or Miss Blakemore's Unspeakeable Sin, Mike Alder

Also, picking up on a thread from logicandlanguage.net, Mike has an article available wherein he considers the distinction between science and philosophy and why many scientists try as hard as possible to distance themselves from philosophy. Again, this article comes with a warning for those sensitive to a bit of criticism:

Newton's Flaming Laser Sword or Why Mathematicians and Scientists don't like Philosophy but do it anyway, Mike Alder

At least he 'fesses up and says "You might, just possibly, have been able to detect a touch of intellectual snobbery in this view of philosophy".

Discretely Causal

2005-04-18T13:50:00.000+10:00

Physicists have long considered spacetime to consist of a smooth real manifold equipped with a fancy sort of metric. One condition on a spacetime that physicists such as Roger Penrose favour as being "physically reasonable" is global hyperbolicity. What this condition essentially means is that some sort of "global" time coordinate exists. In particular, it makes sense to speak about causality.

Rafael Sorkin initiated the study of causal sets. A causal set is a partially ordered set that is locally finite. That is each set of the form {x : a <= x <= b} is finite:
Spacetime and Causal Sets, Rafael Sorkin.

What is intriguing is that we now have a discrete object, namely a causal set, which in some way encodes information about spacetime. Researchers have extended this in a few different ways. In one direction, one may wonder what a causal set looks like to an observer based at one point of the set:

The internal description of a causal set: What the universe looks like from the inside. Fontini Markapoulou.

The basic thrust of the above paper is that whenever you are at some point in a causal set, you know what events have happened in the past. Then, as you shift around the causal set, the set of events that are in your past changes. Markapoulou characterises this with some simple category theory that is explained very nicely in her paper.

For those familiar with branching temporal logics, such as CTL*, there isn't much new here. Most developments of branching temporal logics assume that the past is linear and that the future is branching. That is, when you stand at a moment in time, there is only one possible history, but many possible futures. An exception is one of the logics in the following paper, which augments CTL(*) with a branching past operator:

Once and for all, Kupferman, O.; Pnueli, A (you or your institution needs an IEEE Explore account to view this paper).

Now, a natural concern is whether the notion of a causal set is intrinsically artificial. That is, given a causal set, is it possible to reconstruct a continuous spacetime? The following paper answers this in the affirmative:

A domain of spacetime intervals in general relativity. Keye Martin and Prakash Panangaden

Martin and Panangaden do something very cool in this paper. Given a spacetime M, and a point x in M, let F(x) be all the points that are in the future of x and reachable by a timelike curve starting at x. Define a partial order on m by x <= y iff y is in F(x). Then, given a countable dense subset of points of some spacetime, together with the "causality relation" (which I have defined via F), we can reconstruct the entire spacetime, topology and all!Super cool! The techniques are based on domain theory, which was introduced by Scott in order to give a semantics to the lambda calculus. What the above paper shows is that techniques developed in theoretical computer science are applicable to something seemingly unrelated: general relativity. One point to note is that they drop the local finiteness condition on the "causal sets". This is because they work with continuous posets (well, bicontinuous posets actually), where one has a sort of interpolation condition on the order, which negates the possibility of local finiteness.

So, what is the global hyperbolicity condition anyway? If we have some spacetime M, then for each p and q in M, let I(p,q) be all the events in M that are in the "causal future" p as well as the "causal past of q". The "Alexandroff topology" (or rather, one topology with that name..) is obtained by taking as a basis all of the sets I(p,q) for p,q in M. We say that M is strongly causal if its Alexandroff topology is Hausdorff, which amounts to saying that its Alexandroff topology is the same as the manifold topology. The spacetime M is globally hyperbolic if it is strongly causal and for all a,b in M, the intersection of up(a) and down(b) is compact in the manifold topology on M. Here, up(a) are all those elements "above" a in the partial order and similarly for down(b).

Along the way, they show that every globally hyperbolic spacetime can be realised as a bicontinuous poset, where the order is the one I defined above. Moreover, the interval topology on the poset is the same as the original manifold topology.

Martin and Panangaden give a very convincing argument for swapping the "local finiteness" condition for a "bicontinuity" condition in the description of a causal set, though they remain diplomatic and don't go so far as to say this. Anyway, it's a pretty cool application of some ideas originally developed for "logic in computer science", so you should check it out!

NotYASS

2005-04-07T12:37:00.000+10:00

I have been organising a very informal gathering of assorted riff raff to discuss various things related to maths, logic, philosophy and whatnot. It is called NotYASS (Not Yet Another Seminar Series) and has a shiny new webpage over here. If you find youself in Canberra some time then why not lead a session or just come along for the ride?

Challenge!

2005-04-06T13:30:00.000+10:00

Here is a cute problem for you to think about.

Take the fragment of the sequent calculus for propositional logic over one propositional variable that consists of only the rules of weakening and contraction on the left and the right. That is, if the variable is x, then we start from x|-x and all we can do is add an x on either side or delete an x from one side, provided there are at least 2 x's on that side.

A theorem, T, of the system is just something that is derivable using the above rules. The depth of a theorem is the number of inferences in a proof of minimal length for T. For example, x,x |- x,x has depth 2, since the shortest proof is something like:

x |- x
--------
x,x |- x
--------
x,x |- x,x

The challenge is to give precise answers to the following...

Challenge 1 (easy): How many theorems are there of depth n in the above system?
Challenge 2 (trickier): How many theorems of depth n are there when we add cut to the above system?

Note that in the presense of cut, the depth of a proof, P, is defined to be the maximal length of a branch of P and the depth of a theorem, T, is defined to be the minimum depth over all proofs of T.

Also, note that we use an "additive" cut. That is, if we cut V |- x,W and X,x |- Y, we get V,X |- W,Y. Of course, in our case, the letters V,W,X and Y stand for multisets of our propositional variable (x).

If you do not know what cut is, or are rusty on formal proofs in general, then see this post.

Proof normal forms

2005-04-04T13:35:00.000+10:00

Normal forms for logical formulae are a simple, yet powerful tool. For instance, it is not hard to show that every propositional formula is equivalent to one which is in conjunctive normal form (CNF), that is a conjunction of disjunctions. This equivalence makes building software for satisfiability testing more streamlined, since one can consider only CNF formulae.

Similarly, one can study normal forms for proofs in sequent systems. For instance, one may assume without any loss of generality that a given proof in classical logic is cut free. This is all well and good, but it still does not give us a firm grip on how the proof behaves.

Considerations like this led Gentzen to his Sharpened Haupsatz or Midsequent Theorem. This theorem states that a proof in predicate logic may be rearranged so that all propositional inferences precede all quantifier inferences. The sequent resulting from the last propositional inference is known as the midsequent.

The midsequent theorem is a rather intuitive result. There is a more general phenomenon at play here, first expounded by Kleene:

Two Papers on the Predicate Calculus. S.C. Kleene. Memoirs of the American mathematical Society 10 (1952).

The first of the two papers concerns permutability of inferences in sequent calculi for classical and intuitionistic logic respectively. From the onset, Kleene works with a cut-free system. Hence, the whole paper may be seen as an exercise in finding out how much we can sharpen the cut elimination theorem. Kleene's first approach is to number each logical and nonlogical symbol appearing in the proof. This is sensible from an algorithmic point of view, as it allows one to trace where each symbol in the end sequent came from. By doing so, we can say slightly more. In particular, it turns out that for each logical symbol in the end sequent, there is only one possible type of inference that could have created it. That is, we can immediately point to a logical symbol in the end sequent and say whether it was introduced by the left or right introduction rule for that symbol.

Kleene's main result is a sort of generalised sharpened Haupsatz. In particular, look at the logical inferences that occur in a given proof of a sequent S. Now, partition this collection into C1, C2,...,Ck however you like, though satisfying a couple of natural conditions. Then, the proof of S can be rearranged so that on each branch no occurence of an inference in class j appears above an occurence of an inference in class i for i < j.

As a special case, we get the midsequent theorem. Quite easily in fact. Start by partitioning the inferences into two classes, the first of which contains all propositional inferences and the second of which all the quantifier inferences. Now, every predicate formula is equivalent to one in prenex normal form, that is, one which looks like Q1Q2...Qn(f) where each Qi is a quantifier and f is quantifier free (i.e. propositional). So, we may assume that the formula is prenex, from whence it is easy to verify the conditions of Kleene's theorem (Of course, by using prenex formulae, it is quite easy to prove the midsequent theorem without appealing to Kleene).

To cut or not to cut...

2005-03-18T16:30:00.000+11:00

In a Gentzen-like formulation of a logic, we take as axioms only those consecutions of the form A |- A. For a lot of sensible logics, we can even take A to be atomic. We then postulate a few rules for introducing connectives on both sides of |-. Most of these rules satisfy the subformula property, which is to say that any formula or structure appearing in the numerator (assumption) of the rule is a subformula of something appearing in the denominator (conclusion). Case in point, the contraction rule, one of whose variants is:

X, A, A |- Y
------------
X,A |- Y

In the above, X and Y are structures (multisets of formulae) and A is a formula. It says that if we can conclude Y from X and A and A, then we can conclude it from X and A also (this rule is present in classical logic but not in, say, linear logic).

One rule is a bit conniving and does not obey the subformula property: it is called cut, one version of which says that if you have X|- A and also A |- Y, then you can "cut out" A and conclude X |- Y (this is nothing but the transitivity of deduction).

But this is ok in sensible logics, for in these logics cut is admissable, which is to say that adding it as a rule does not give us anything new. This is quite an impressive result, since the cut rule is basically a rule which says that we can use lemmas. That it is admissable means that we do not need to use them. Actually, it says more than that. Good proofs of its admissability show how to explicitly transform a proof with cuts into one without. Crikey! To see cut elimination in action on a theorem from real analysis, look no further than the following (which also includes an introduction to sequent calculus and proof theory in general):

Making Proofs Without Modus Ponens A. Carbonne and S. Semmes

One very important consequence of cut elimination for a logic is consistency (although sometimes you need to use a bit of transfinite induction...). By eliminating the cut rule, we also ensure that (formal) proofs satisfy the subformula property. So, a proof of a formula (/structure/sequent/whatever) gives a method for constructing it. This leads, in one direction, to the field of logic programming, where one performs a backtrack search for a cut-free proof. See:

A Tutorial on Proof Theoretic Foundations of Logic Programming Paola Bruscoli and Alessio Guglielmi

The other side of the coin is that transforming a proof with cuts into one without cuts can lead to an exponential blowup in the length of the proof: obviously a bad thing.

So, what is a logician to do? One option is to only use a modified form of the cut rule, called an "analytic cut". In this version, we are only allowed to cut on a formula if it is a subformula of something in the conclusion. Ok, so this obviously lets us keep cut and still have the subformula property. So all is well right? Wrong! Surprisingly enough, there is trouble with this even in the case of propositional logic: a system with analytic cut is no better than truth tables. In technical terms, analytic tableaux cannot p-simulate truth tables.

Are Tableaux an Improvement on Truth-Tables? Marcello D'Agostino. Journal of Logic, Language and Information 1: 235 -- 252, 1992.

Although, this is not too surprising, since if a system with analytic cut did not give exponential length proofs of some propositional formulae, then we would have coNP = NP. More on this another time...

Semantics is (coNP) hard, syntax is (GI) easy

2005-03-15T15:48:00.000+11:00

It seems that posting regularly to a blog is harder than I thought. My excuse is that I have been quite busy learning a lot of background for what is essentially a new research area for me, as well as more mundane things such as furnishing a house. I am also organising a regular informal gathering of academics from across campus (maths, cs, philosophy, linguistics) to discuss the nature of proof. It should, hopefully, facilitate some interesting debates.

Anyway, enough of that. Let's get down to business. A little while ago I cleared up my understanding of symmetries of propositional logic. As it turns out, there are actually two notions of symmetry in the literature, and the authors of papers are not always at pains to clearly elucidate what they mean. This can be quite confusing! Let me try and settle things here. There are essentially two notions: a semantic one and a syntacitic one. Throughout, p is a propositional wff over n variables.

Semantics: We consider the boolean function f:(x1,x2,...,xn) -> {0,1} induced by p. A semantic automorphism is a permutation of the xi's that results in the same boolean function. That is, if f' results from f by merely twiddling around the arguments of f, then the "twiddle" is an automorphism if f' has the same truth table as f. The group of all automorphisms of f is denoted by Aut(f). Buried in a paper of Emerson and Sistla (Symmetry and Model Checking) is the result that the problem of determining whether Aut(f) is the full symmetric group, Sn, is coNP-Complete (recall that Sn is the group of *all* permutations of x1,x2,...,xn).

While their proof is not particularly difficult, there really is a much cleaner method. I'll just sketch the argument. First, determining whether a given permutation is in Aut(f) is coNP-hard. Why? Well, in order to determine if it is an automorphism, we need an efficient method for checking if truth tables are equivalent. If we had such a method, then we could use it to solve validity too. The problem is easily seen to be in coNP, so is coNP-Complete. Now, to see if all permutations are in Aut(f) is not too hard. It is an old piece of group theoretic folklore that an n-cycle and a transposition moving two consecutive points of that n-cycle generate Sn (an n cycle is a permutation which sends x1 to x2 to x3 to... to xn to x1 and a transposition is a permutation which just swaps two points). Now, pick an arbitrary n-cycle, test to see if it is an automorphism. If it is, then we need to check at mose n transpositions to see if we have Sn (all adjacent pairs in the n-cycle). So this problem is coNP-Complete also.

A natural question now is whether or not every finite group arises as the automorphism group of some boolean function. It turns out that the answer is no. I'll sketch the proof if anyone is interested, but will omit it for now.

Syntax: We assume that our formula f is given in conjunctive normal form. A syntactic automorphism is a permutation of the literals appearing in p, which preserves the syntactic structure (so, swapping two clauses counts as an automorphism). This is different from our previous notion of automorphism. For example, consider the CNF formula whose only clause is [x,-y]. Then, swapping x and y is a syntactic automorphism but not a semantic automorphism. I mentioned in the first post that it is possible to construct a coloured graph whose automorphism group is the same as the syntactic automorphism group of p. This can be done in polynomial time. Then, assume that we can compute generators for the automorphism group of this graph. This problem is equivalent in complexity to the graph isomorphism (GI) problem. This is interesting, because GI falls in NP but it is not known whether or not it isin NP-Complete, or P. Anyway, given these generators, we can use some group theoretic algorithms to solve the problems from before in polynomial time. That is, testing whether an arbitary permutation is a syntactic automorphisms and testing whether the syntactic automorphism group consists of all possible permutations.

The moral of the story is that the semantic aspecs of logical symmetry are inherently coNP-Complete, whereas the syntactic aspects are at most as hard as graph isomorphism. So, barring something unforseen like coNP= NP or P = NP, semantics is harder than syntax. Computationally speaking at least.

Sign me up

2005-03-03T15:58:00.000+11:00

For those who are interested in logic, but are not affiliated with a university, it can be quite expensive to keep up with things. After all, journal subscription prices are often out of the reach of individuals. The purpose of this post is to point out some options for individuals. Many are free, but you'll go a lot further by spending a little bit.

Of course, on the sidebar of this blog, are links to electronic resources which make their papers /articles available for free. This is a good thing. It promotes wider and faster dissemination of results. I'll briefly describe each of these below.

Australasian Journal of Logic: This is managed by the philosophy department at The University of Melbourne and is edited by Greg Restall. It is fully refereed and freely available and seeks to cover the breadth of modern pure and applied logic. Currently, the majority of the articles deal with philosophical logic.

ACM Transactions on Computational Logic: This is obviously put out by the Association for Computing Machinery. As such, its focus is predominantly computational. However, given the nature of the subject, many articles should be of interest to philosophical logicians as well. For instance, both proof theory and modal logic have philosophical and computational branches. While the concerns of each area are often quite distinct, one gets a fuller picture of the area by "seeing how the other half lives". The articles here are usually of a rather technical nature.

Bulletin of Symbolic Logic: This is put out quarterly by the Association for Symbolic Logic. It contains many helpful book and article reviews as well as many good expository papers. It is well worth browsing through the archives. While you are at it, why not join the association? As well as your very own print version of the bulletin, you recieve the Journal of Symbolic Logic and significantly reduced subscription rates for the Journal of Philosophical Logic. If you are a student, they also provide some funding support for attending ASL affiliated conferences.

arXiv.org: This is a major preprint server. By sending an email to math@arxiv.org with the body 'add LO' (without the quotes), you can receive updates on mathematical logic related preprints daily to your email address. By sending a message with the same body to cs@arxiv.org, you can sign up for computational logic as well.

The European Association for Theoretical Computer Science publishes a quarterly bulletin. It contains many interesting columns. For computational logicians, the logic in computer science, formal specification, computational complexity and formal language theory columns often contain interesting nuggets. You do need to pay an annual membership fee, but the bulletin is more than worth it (often running to a few hundred pages!). The sister publication, published by the ACM, is the Special Interest Group on Algorithms and Computation Theory News. It has recently rekindled its logic in computer science column. The two organisations currently have a reciprocal arrangement, whereby you receive a discount if you join both. Oh and if, like me, you live outside of Europe and/or the US, it is well worth spending the little bit extra for airmail.

An interesting quirk with the above publications is something that Richard Zach has mentioned in his blog. That is, Europeans seem to be a lot keener on logic than Americans. That is, American theoretical computer science tends to be very combinatorial, whereas its European counterpart is often a lot more logical. One certainly gets this impression when reading both publications.

Finally, there is a very good free online magazine devoted to philosophical logic and its applications: PhiNews.

Goodbye Syntax?

2005-02-22T10:30:00.000+11:00

I am now settled in, so can resume posting again. My goal is to average one post a week from now on, so there should be a bit more activity on this little piece of cyberspace.

Onto more interesting things. There are many different methods for performing proofs in logic. For instance, sequent calculi, natural deduction and related systems. However, they all have one thing in common: they manipulate syntax. This is fair enough, since a proof is a syntactic object, right? Well, yes. However, when we work in, say, propositional logic, we have access to a particularly perspicuous semantics and we know that the syntax matches up with the semantics very nicely. And, so, why not perform proofs in the semantics. Of course, the problem is that in order to find a tautology, we pretty much have to try out all possible valuations (barring something obscene like P=NP). Well, now there is a third way: combinatorics and, in particular, graph theory.

Proofs Without Syntax - Dominic Hughes

The above paper does a good job of explaining the necessary background, so I will only dwell on it briefly. The crux of the paper is in defining a "combinatorial" proof to be a special sort of graph homomorphism (map between graphs that preserves edges) between very special graphs. The main result is a soundness and completeness type of afair: if a proposition is a tautology, it has a combinatorial proof and vice versa. In other words, we have a bit more structure for performing "semantic" proofs. It remains to be seen whether this can be done reasonably efficiently.

Oligomorphic Magic

2005-02-09T22:32:00.000+11:00

I hadn't planned on making a new post until after moving but here we go. It seems that there are a few people with a philosophical bent reading this, so I will try and make a philosophical post soon. Today, however, is mathematical.

A couple of days ago, I was chatting with some group theorists and they mentioned the strange notion of an oligomorphic group. From a purely permutation group perspective, it does not seem like a particularly interesting object, so why has there been such a hubbub of late? The answer lies in logic and, in particular, model theory.

To make this post a manageable length, I assume familiarity with the definition of a group. Given a set X, the symmetric group on X, denoted Sym(X), is the group of all bijections mapping X to itself with function composition as the group operation. A permutation group, G, is a subgroup of Sym(X) for some X. Given a point x in X, the orbit of x is the set of all images of x under maps in G. It is a standard result that X is partitioned by the set of all orbits of G on X. The flavour of this area of group theory is markedly different depending upon whether X is finite or infinite. We shall deal with the infinite case here.

Now, a model, M, is a tuple consisting of a set m called the domain, together with a collection of (possibly no) functions from M^n to M and another collection of (possibly no) n-ary relations on M as well as some (possibly none) elements of m that are distinguished as constants. An automorphism of M is a permutation of m that preserves all functions and relations in M. For example, if (N,+,=) denotes the natural numbers together with addition and equality symbols, then an automorphism of this structure is just a semigroup automorphism. The collection of all automorphisms of M form a group under composition, the automorphism group of M, denoted by Aut(M). Given two models M and N, we say that they are isomorphic if there is a bijection mapping the domain of one to the domain of the other, which preserves functions and relations.

Much like in the first post of this blog, the automorphism group is going to tell us something logically interesting. Except, instaead of loooking at automorphisms of formulae, we are going to look at automorphisms of models. A set of sentences (quantifier-free formulae), S, is omega-categorical if every model of S with a countably infinite (omega) domain is isomorphic. Given a model M, the theory of M, denoted Th(M), is the set of all sentences true in M. Can we find omega-categorical theories?

It turns out that we can use the information about Aut(M) in order to find such theories. It is a result of Engeler, Ryll-Nardzewski and Svenonius that the following are equivalent for a countably infinite model M with domain m over a countable language:

1. Th(M) is omega-categorical
2. For each natural number k, there are only finitely orbits of Aut(M) on the set of k-tuples of elements of m.

This second condition is what is meant by an "oligomorphic" group: it has only finitely many orbits on the k-tuples of its permutation domain. We can also go the other way. Given an oligomorphic group, we can construct the so-called "canonical model" and this is going to have an omega-categorical theory.

Interesting flows of results start to go between model theory and permtuation group theory at this stage. For instance, from some elementary model theory, it follows that if a group G is the automorphism group of a model of an omega-categorical theory and H is any subgroup of G, then there are only finitely many groups between H and G (that is groups K such that H < K < G)

All of this is the starting point of the following wonderful book, which I, sadly, do not have the time to browse through properly before jetting off on Saturday:
Automorphisms of First Order Structures

Learning for Logic

2005-02-04T07:36:00.000+11:00

The long break in blogs is because I am preparing to move to another university next week, which happens to be a few thousand kilometers away. I am not sure how many people actually read this thing though - leave a comment to let me know you are here (If you wish to remain anonymous, then something like "Hi from anonymous person number n+1", where n is the number of the last anonymous person).

I'll hold off on the symmetry stuff for a while, because I am still absorbing a few references from some kindly local mathematicians, which may answer one of my questions from last time (at least partially). So, I'll talk about something else.

While browsing through the library the other day, the following caught my eye:

Donald N. Cohen: Knowledge Based Theorem Proving and Learning.

(no relation, honest). This turned out to be a copy of Cohen's PhD thesis, wherein he describes his admirable attempt to make an automated theorem prover that is less stupid than usual. Sadly, since the thesis dates from 1981 (making it older than me!), a large chunk of the work concerns efforts to make the program more memory efficient, despite his "large" 256kb memory space :) The basic premise is that humans hardly ever prove theorems starting from the axioms (the exception being when one is cleaning up the trivial consequences of a new definition, such as that of a group). However, this is something that has not been adopted much in the automated reasoning community, for some good reasons mind you.

Cohen first sets about creating a database that can store new theorems, as well as new *techniques*. The latter is particularly interesting, because anyone who has done tedious high school maths homework knows that once you learn the trick to solving a problem, you can just blindly follow the recipe when you notice a new instance of the problem, as opposed to solving the same problem again.

Cohen focuses his attention on something that often occurs in a backtriacking search - you end up solving the same subproblem over and over again. The computer science community has developed many heuristics for avoiding this situation, including backjumping (don't backtrack to the previous node, backtrack to the previous significant point) and look-ahead (what would happen if I picked this option?). Cohen's approach is to have the computer "learn" about the subproblem and how to solve it efficiently. A more recent approach, is the following:

Andrew Slater: Investigations into Satisfiability Search.

The basic approach there is to use relevant logic, which essentially says that when proving an implication, the assumptions should all be "relevant" to the conclusion. For example, while the statement "It is raining and I am wearing my leather shoes, so it is wet outside" is technically correct, what shoes I am wearing is not really relevant. Using this philosophy, Slater creates an algorithm for reordering a search tree, so that assumptions are relevant to "conclusions", thus sidestepping the problem of the computer re-solving subproblems.

The "learning" in Cohen's thesis is hard to spot. What he calls learning seems to be the ability for the program to remember succesful proof attempts and the pattern of the formulae that it worked on (he works with the typed lambda calculus, but this is not really important). The trick here is to then avoid a "combinatorial explosion", where the prover ahs too many options at any given stage, so spends far too much time trying different alternatives. Cohen makes some steps towards giving the prover "semantic" knowledge, so that it can reason with models of the formulae (for example, when trying to prove a statement in, say, topology, one usually has a stock of different spaces to test the statement out on, to see what makes it tick). Cohen does not make much progress on this area (and who can blame him, given the number of tasks he sets himself to complete!). A more recent piece of software along the last lines, is SCOTT (Semantically Constrained OTTer).

So, what more can be said about making automated theorem provers more intelligent, using all that we have discovered int he 24 years since Cohen's thesis? Certainly, machine learning has come on leaps and bounds with, for example, support vector machines proving to be very good at classification tasks. So too has knowledge representation and database theory. As far as building models of theories goes, there are now very powerful systems for doing modern algebra (groups, rings, fields,...), which can be used to generate as many models as you please. Thus, it seems that the time is ripe to develop software that reasons and learns a lot more like humans...

New Blog on the Spot

2005-01-17T22:36:00.000+11:00

For a while I have been wanting to get into the world of blogging. But what to do? I decided that I would follow the formula from John Baez's always interesting "column" This Weeks Finds in Mathematical Physics. That is, I will sporadically speak about stuff that I find interesting. Except, instead of mathematical physics, I'll speak about logic. I will not attempt to cover lots of different areas, merely those bits and pieces that I find interesting. So, it will most likely end up being mainly computational with a twist of mathematical.

Well, let's do something whacky for this first post. I'm going to speak about propositional logic. While many people may believe this to be a completely mined out and somewhat trivial area, this is not so. And no, I am not going to speak about propostitional proof complexity. I am going to speak about something I have been pontificating about for a while - symmetry. What do I mean by symmetry? Well, given a propositional formula, a "symmetry" (henceforth called an automorphism, in keeping with standard mathematical terminology) is any permutation of variables which preserve the valuation. For example, given the formula "a & b", we can swap the symbols a and b without affecting the valuation. The most general symmetry group for a formula of n variables seems to be the group S2 wr Sn, the so-called wreath product of the symmetric group on 2 elements with the symmetric group on n elements. Now, the symmetric group on n elements, Sn, is the collection of all permutations of an n-element set; in our case, the variables. How the wreath product works is like this: the top group (Sn) permutes the variables in the manner in which you would expect. The base group (S2) acts like a "light switch", flipping a variable to be either negative or positive (that is, either negated or not). So, here is the first open problem to chew on:

(OP1) What groups can arise as automorphism groups of propositional formulae?

Certainly, any such group will be a subgroup of our wreath product. We can get Sn for any n - just take the disjunction of n distinct variables (or, in the old language, n literals in such a way that no atom appears more than once). But, what others....?

Lets start having some real fun now. Recall that a formula is said to be in conjunctive normal form (CNF) if it is a conjunction of disjunctions. Given a formula in CNF, we build a "multicoloured graph" as follows: Make a vertex for each clause and one for each literal appearing in the formula. Paint the vertices corresponding to clauses black and the ones corresponding to literals white. Connect a black vertex to a white vertex if the (white) literal appears in the (black) clause. Connect literals to their negations (recall that to connect vertices in a graph, we just draw an edge between them). Then, an automorphism of the resulting graph is defined to be a permutation of the vertices that maps black vertices to black vertices, white vertices to white vertices and edges to edges. With a bit of squinting, we then see:

(1) Finding symmetries of a formula is a subcase of the coloured graph automorphism problem.

From some standard graph theory, we then see:

(2) As n goes to infinity, the probability that a random propositional formula has a trivial automorphism group tends to 1.

Now, the graph automorphism problem (GAP) is one of those black sheep of computational complexity. In other words, we don't have a clue what its actual complexity is. Even the complexity of finding a nontrivial automorphism is not known.

I'll leave the discussion there. There is a lot more I have to say about this area, including some more open problems and some tantalising links to the biggest open problem in theoretical computer science, but I will leave those to sequels if people are interested.