Showing posts with label composition problem. Show all posts
Showing posts with label composition problem. Show all posts

Friday, July 1, 2011

Would you look at that!

OK, now this result does surprise me. I think I just found a ruleset that is not closed under modus ponens! D10+D12+D13+E:

  • validates ~~φ->φ.
  • validates (~~φ->φ)->(φv~&phi).
  • does not validate φv~φ.

And here are my proofs to double check my work, because this is very, very strange:

In fact, the same also holds of D10+D12+D13, without E:

Tuesday, August 10, 2010

Rule neutrality, rule naturality

Last week the website for the Workshop on Dialogues, Inference, and Proof - Logical and Empirical Perspectives (DIPLEAP) was distributed to the preliminary list of participants, which means Jesse and I need to start thinking about what we'll present there. One of us will certainly introduce N and cover the material in our ICLA paper, as sort of a test run. But since we've finished up the proof of the positive answer to the composition problem for N, I've been thinking about some more philosophical issues relating to the dialogical approach, and I might speak on these instead. Now that we have at least one example of a positive composition problem solution that was proved directly through semantic (that is, dialogical) means, the pot of gold at the end of the rainbow would be to be able to isolate what it was about the rules set N that allowed us to give this positive solution, so that we could then identify other rules sets where we can be sure a positive solution can be given, even if the proof strategy may differ. The composition problem proof for N relied crucially on our theorem characterizing the forms of valid implications in N, and this theorem in turn exploited the fact that when Felscher's rules E, D11, and D12 are dropped, Opponent can repeat defenses as many times as he want, and thus draw out a dialogue infinitely (meaning that Proponent cannot win). This fact is part of what made finding the proof for the composition problem so difficult: Neither of us have any clear intuition or understanding of what the connection is between Opponent's ability to repeat defenses and the theorems of N. There doesn't appear to be any fundamental fact grounding the connection, which means that it is extremely difficult to exploit, because working with N still feels like reaching out in the dark, blind. If we cannot pick out specifically something about the N rules that can be generalized or extrapolated to other rules sets, then perhaps it is still possible to say something general, to find a criterion/a for rule sets or a class of rule properties that have some connection, stronger or weaker, with a positive solution to the composition problem. That is, can we isolate some 'natural' feature of rules that is connected to the composition problem? One way to go about answering this is to look at rule sets where negative solutions to the composition problem can be given. We give an example in our paper on N, just to show that such examples can be given: Change the rules for CL so that Proponent is now allowed to also assert atoms in defense of disjunctions. Then, $\vDash p\vee\neg p$ and $\vDash(p\vee\neg p)\rightarrow p$, but $\nvDash p$, and thus the set of formulas generated by this rule set is not a logic. This example may seem somewhat trivial, but it actually displays an interesting property: The new rule fails to be neutral in the sense that it encodes an exception for a particular type of formula. This concept of neutrality seems like one that might be fruitfully exploited. First, we isolate three senses in which rules (both particle and structural) can be neutral:
  1. topic neutral (they do not favor one atom over another)
  2. connective neutral (they do not favor one connective over another)
  3. player neutral (they do not favor one player over another)
Then, we can ask: how much neutrality (a) is good and (b) can be had and obtain a logic? If neutrality turns out to be the right property to exploit, the latter question is the same as asking whether we can characterise when a rules set will have a positive solution to the composition problem on the basis of the neutrality of the rules involved. There are a few remarks that can be made at the outset. First, structural rules which are wholly player neutral will result in the inconsistent logic: Proponent has a winning strategy for every atom p, so at least some asymmetry/nonneutrality in the rules is required. This raises a question that I first became interested in in the cafe above the cafeteria on the campus in Ponta Delgada, which is how little player nonneutrality do we need in order to ensure that this does not follow? We already have reason to believe that D10 can be weakened, at least somewhat; Jesse has been investigating a variant of the D rules where Proponent can assert an atom if the corresponding literal has already been asserted by Opponent. The resulting rule set validates WEM but not LEM. (Thus, if this rule set generates a logic, then it is an SI-logic.) It is also likely that the particle rules cannot be wholly neutral: The fact that negations can only be attacked and not defended seems to be crucial. Investigating rule neutrality in these three ways has the advantage that neutrality is simply expressible, easy to determine, and has nice symmetry properties. However, the connection between neutrality of rules and their naturality is something which is much less clear, at this point. People working in the dialogical tradition who have tried to give philosophical justifications for the approach have appealed to the 'naturalness' of the rules (particularly the particle rules), and have argued that there is a connection between the dialogical rules and the way that people actually debate (see, for example, the first few pages of chapter 6 of Lorenzen's Constructive Philosophy), and that therefore the dialogical approach is philosophically preferable to others because it is somehow more natural. But what is 'natural'? Barthe & Krabbe, in From Axiom to Dialogue, after they have introduced rules for systematic dialectics and realistic dialectics (and before they discuss thoroughgoing dialectics, orderly dialectics, and dynamic dialectics), discuss the naturalness of the rules they've suggested:
In each case where we expect that the large majority of people can be brought to agree upon a certain rule as part of a formal_3 dialectics (provided they are explicitly confronted with it and made acquainted with the motivation given for it here or with a similar motivation), we shall say, for short, that we think it is a natural rule [p. 75].
If it is agreed that this is a reasonable definition of 'natural', then I think it can be argued that none of the dialogical rule sets are in fact natural. The motivation for many of the dialogical rule sets in the literature to date essentially boils down to "they work" -- a formal proof can be given showing that the rules do in fact correspond to the desired logic (or, in the case of N, that they correspond to a logic, even if that logic is one that was not set out in advance). The majority of people when confronted with this motivation are going to balk at being asked to accept the rules on that basis alone: They're going to ask, "Why do they work?" What is it about the rules that makes them correspond to a logic, much less the target logic isolated in advance? And now we're back to the original question: Are there any properties of rule or rule sets that correspond to positive solutions to the composition problem, and if so, what are they? And then neutrality of certain types presents itself again as a natural starting point for investigating answers.

Friday, July 30, 2010

NCL goes to India?

Despite our initial doubts that we'd be able to say anything of much interest about NCL, Sara and I managed to actually solve its composition problem: we now know that
If φ and φ→ψ are NCL-valid, then so is ψ.
The proof didn't turn out to be hard, but it does involve some rather curious lemmas that hardly resemble anything like what I've seen before in my study of mathematical logic. It really feels like exploring a whole new world. Sara discovered a crucial feature of valid NCL-implications:
If φ→ψ is NCL-valid, then either
  • φ is an atom,
  • φ is a negation, or
  • ψ is already NCL-valid.
I confess that I was skeptical when Sara shared this conjecture with me; it felt too ham-fisted and alien. But the conjecture in fact holds, and it paves the way toward a positive solution of the composition problem. (The other principal lemma in the proof is a characterization of NCL-valid negations.) Just today we submitted a joint paper about all this (“A curious dialogical logic and its composition problem”) to the upcoming Indian Conference on Logic and its Applications, to be held in Delhi in January, 2011. We expect to learn in about a month whether it will be accepted. (In the paper we call NCL simply “N”. The name NCL comes from a more benighted time when we thought, based on a priori reasoning about rulesets, that since NCL is only slightly different from a ruleset that characterizes classical logic, it would correspondingly give rise to a logic that might be different from classical logic but “close” to it.) We were restricted to 12 pages, but we have lots more to say about NCL and couldn't pack it all in. We expect to produce a fuller account in a journal article.

Wednesday, July 14, 2010

Meta

Having not yet had any time to write a proper blog post, I thought I would take a few minutes to at least write a post about posts I am going to write when said time magically appears. The first question Jesse and I considered, and the one that eventually led him to think of and formulate the composition problem, was one that I thought was relatively simple: Given a classically valid formula $\phi$ and the Gödel-Gentzen translation $\phi^n$ of $\phi$, is there a (uniform) way of translating the winning strategy for $\phi$ in the classical game into a winning strategy for $\phi^n$ in the intuitionistic game? What the composition problem has shown us is that this is not an easy question to answer partly because it is not clear what a "winning strategy in the classical game" is. So answering that question will be a long time off and in the meantime I'm going to be much more modest in my aims, and I've come up with a number of much, much more basic questions that I hope to answer, whose answering I also hope will help me come up with some intuitions about how dialogical proofs work (since currently I have none). These are the issues I hope to explore in future blog posts: - The "solution" to the "weakening" problem: We discussed this in Ponta Delgada and I think convinced ourselves that the weakening problem does indeed have a solution, but for now the scare quotes are necessary because we haven't anything like a proof. - Why DN is so important in differentiating classical logic from intuitionistic logic. - What would particle rules for TONK look like? - Is there anyway to get an inconsistent logic other than dropping the requirement that P cannot assert an atomic formula unless O has already asserted it? - How symmetric can you make the structural rules (so that they treat O and P the same) and still get a logic? Some tantalizing topics for future discussion...