Subject: Linear inferences and derivations 1 Newsgroups: gmane.science.mathematics.frogs Date: Wednesday 26th September 2012 16:22:22 UTC (over 5 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 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 |
|||