Features Download

From: Anupam Das <anupamdotdas-Re5JQEeQqe8AvxtiuMwx3w <at> public.gmane.org>
Subject: Linear inferences and derivations 1
Newsgroups: gmane.science.mathematics.frogs
Date: Wednesday 26th September 2012 16:22:22 UTC (over 6 years ago)
[This is the first of 3 emails to the Frogs list concerning linear 
inferences and derivations in deep inference. The first is about linear 
inferences that are independent of the usual basis {switch, medial}. The 
second concerns the size of linear derivations in deep inference, in the 
presence of units, and the third will present recent work towards 
efficiently automating the checking and search of new linear inferences.]

Linear inference rules are negation-free inferences where each variable 
appears exactly once in both the premiss and conclusion. In deep 
inference we often consider the following rules:

          A ^ [B v C]             (A ^ B) v (C ^ D)
switch --------------    medial -------------------
         (A ^ B) v C              [A v C] ^ [B v D]

But there are many more that one may consider, for example by composing 
the two rules above in various combinations. But as Strassburger shows 
in his paper Extension Without Cut, these two rules are not complete for 
the set of linear inferences, even when allowing composition of 
derivations by deep inference. His counterexample contains 36 variables, 
but is it possible to find smaller ones?

*Does anyone know any examples of such linear inferences, or whether 
there is any work related to the subject? *

In particular I would be interested to hear if there are any known for < 
10 variables, for reasons that are clear from what follows.

By the way, there are certain requirements here:

  * We consider formulae equivalent up to commutativity and associativity.
  * We allow basic unit manipulation in derivations.
  * We allow `deep' applications of rules, in the usual deep inference

(The first two requirements are equivalent to adding the usual = rule of 
deep inference.)

I propose here a new linear inference, on 10 variables, based on the 
pigeonhole principle for 3 pigeons and 2 holes, as well as an argument 
for it's soundness and independence from {switch, medial}. I conjecture 
that this is the minimal linear inference independent of {switch, 
medial}, though any brute force approach towards proving this is very 
computationally cumbersome. This is elaborated on in Part 3 of this 
email series.

The new inference is this:

     [a v (b ^ b')] ^ [(c ^ c') v (d ^ d')] ^ [(e ^ e') v f]
    ([c v e] ^ [a v (c' ^ e')]) v ([(b ^ d) v f] ^ [b' v d'])

or as formula trees:

              b   b'  c  c' d  d'  e   e'
               \ /     \ /  \ /     \ /
            a   ^       ^    ^       ^   f
             \ /          \ /         \ /
              v            v           v
               \________   |  _________/
                        \  | /
                   ______/   \______
                  /                 \
                 ^                   ^
               /   \               /   \
              v     v             v     v
             / \   / \           / \   / \
            c   e a   ^         ^   f b'  d'
                     / \       / \
                    c'  e'    b   d

(Soundness can readily be checked by any online theorem prover, though I 
am about to give an intuitive argument. For non-derivability in {switch, 
medial} see below.)

Essentially, this is a certain encoding of the pigeonhole principle with 
3 pigeons and 2 holes. Consider the following grid:

     |    a   |    b   |
     |    c   |    d   |
     |    e   |    f   |

The inference encodes the fact that, if we mark a box in each row, then 
some column has two marked boxes. To avoid repetition of variables we 
introduced new variables b', c', d', e' that live in the same respective 
boxes. If this is not clear, consider the following grid:

     |    a   |  b, b' |
     |  c, c' |  d, d' |
     |  e, e' |    f   |

Now the rule can just be interpreted as:

     if "each row contains a box whose variables are true"
     then "some column has two variables in distinct boxes that are true".

(in fact the conclusion only exhausts all combinations of boxes rather 
than variables)

For non-derivability notice that, working bottom up from the conclusion, 
any valid application of switch or medial leads to a formula not 
logically implied by the premiss (the above interpretation makes it 
easier to see this).

Furthermore, the rule is not even derivable in {switch, medial} using 
units. The argument is as follows:

Suppose it was, then some atom would have to be trivialised at some 
point (i.e. in the scope of a conjunction with falsum or disjunction 
with true) since otherwise we could just reduce every line by = to a 
unit-free formula. But then we can substitute 'true' for the atom in the 
premiss and 'falsum' in the conclusion and the resulting inference would 
remain sound. Inspection shows that no atom in the inference has this 

Both soundness and non-derivability have been checked by a computer 
program that will be introduced in Part 3 of this email series.

Kind regards,
CD: 14ms