Linear inferences and derivations 1
Anupam Das <[email protected]> Wed, 26 Sep 2012 17:22:22 +0100
| Newsgroups | gmane.science.mathematics.frogs |
|---|---|
| Message-ID | <[email protected]> |
This is a multi-part message in MIME format.
--------------040507070302080607000506
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
[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
style.
(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 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
property.
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,
Anupam
--------------040507070302080607000506
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
<html>
<head>
<meta http-equiv="content-type" content="text/html;
charset=ISO-8859-1">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<tt>[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.]</tt><tt><br>
</tt> <br>
<br>
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:<br>
<br>
<tt> A ^ [B v C] (A ^ B) v (C ^ D)<br>
switch -------------- medial -------------------<br>
(A ^ B) v C [A v C] ^ [B v D]<br>
<br>
<br>
</tt>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?<br>
<br>
<b>Does anyone know any examples of such linear inferences, or
whether there is any work related to the subject? </b><br>
<br>
In particular I would be interested to hear if there are any known
for < 10 variables, for reasons that are clear from what follows.<br>
<br>
By the way, there are certain requirements here:<br>
<ul>
<li>We consider formulae equivalent up to commutativity and
associativity.</li>
<li>We allow basic unit manipulation in derivations.</li>
<li>We allow `deep' applications of rules, in the usual deep
inference style.</li>
</ul>
<p>(The first two requirements are equivalent to adding the usual =
rule of deep inference.)<br>
</p>
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.<br>
<br>
The new inference is this:<br>
<tt><br>
</tt><tt> [a v (b ^ b')] ^ [(c ^ c') v (d ^ d')] ^ [(e ^ e') v f]
</tt><tt><br>
</tt><tt>
-----------------------------------------------------------
</tt><tt><br>
</tt><tt> ([c v e] ^ [a v (c' ^ e')]) v ([(b ^ d) v f] ^ [b' v
d'])
</tt><tt><br>
</tt>
<tt><br>
</tt>
<tt><br>
</tt>or as formula trees:
<tt><br>
</tt>
<tt><br>
</tt>
<tt><br>
</tt><tt> b b' c c' d d' e e'
</tt><tt><br>
</tt><tt> \ / \ / \ / \ /
</tt><tt><br>
</tt><tt> a ^ ^ ^ ^ f
</tt><tt><br>
</tt><tt> \ / \ / \ /
</tt><tt><br>
</tt><tt> v v v
</tt><tt><br>
</tt><tt> \________ | _________/
</tt><tt><br>
</tt><tt> \ | /
</tt><tt><br>
</tt><tt> ^
</tt><tt><br>
</tt><tt> ----------------------------------------------
</tt><tt><br>
</tt><tt> v
</tt><tt><br>
</tt><tt> ______/ \______
</tt><tt><br>
</tt><tt> / \
</tt><tt><br>
</tt><tt> ^ ^
</tt><tt><br>
</tt><tt> / \ / \
</tt><tt><br>
</tt><tt> v v v v
</tt><tt><br>
</tt><tt> / \ / \ / \ / \
</tt><tt><br>
</tt><tt> c e a ^ ^ f b' d'
</tt><tt><br>
</tt><tt> / \ / \
</tt><tt><br>
</tt><tt> c' e' b d
</tt><tt><br>
</tt>
<tt><br>
</tt>
<tt><br>
</tt>(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.)
<br>
<br>
Essentially, this is a certain encoding of the pigeonhole principle
with 3 pigeons and 2 holes. Consider the following grid:
<br>
<tt><br>
</tt><tt> _________________
</tt><tt><br>
</tt><tt> | a | b |
</tt><tt><br>
</tt><tt> |________|________|
</tt><tt><br>
</tt><tt> | c | d |
</tt><tt><br>
</tt><tt> |________|________|
</tt><tt><br>
</tt><tt> | e | f |
</tt><tt><br>
</tt><tt> |________|________|
</tt><tt><br>
</tt>
<tt><br>
</tt>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:
<tt><br>
</tt>
<tt><br>
</tt><tt> _________________
</tt><tt><br>
</tt><tt> | a | b, b' |
</tt><tt><br>
</tt><tt> |________|________|
</tt><tt><br>
</tt><tt> | c, c' | d, d' |
</tt><tt><br>
</tt><tt> |________|________|
</tt><tt><br>
</tt><tt> | e, e' | f |
</tt><tt><br>
</tt><tt> |________|________|
</tt><tt><br>
</tt>
<tt><br>
</tt>Now the rule can just be interpreted as:
<tt><br>
</tt>
<tt><br>
</tt><tt> if "each row contains a box whose variables are true"
</tt><tt><br>
</tt><tt> then "some column has two variables in distinct boxes
that are true".
</tt><tt><br>
</tt>
<tt><br>
</tt>(in fact the conclusion only exhausts all combinations of boxes
rather than variables)
<br>
<br>
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).
<br>
<br>
Furthermore, the rule is not even derivable in {switch, medial}
using units. The argument is as follows:
<br>
<br>
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 property.<br>
<br>
Both soundness and non-derivability have been checked by a computer
program that will be introduced in Part 3 of this email series.<br>
<br>
Kind regards,<br>
Anupam<br>
</body>
</html>
--------------040507070302080607000506--