RE: [PT] Update: Question on a class of tautologies

Alessio,

Are you willing to consider the closure of X under substitution instead of X as you described it? 
Otherwise,  X contains p&q->p&q but not p&p->p&p, which makes it rather odd and hard to deal with.  

Giorgi Japaridze
http://www.csc.villanova.edu/~japaridz/
________________________________________
From: Alessio Guglielmi [[email protected]]
Sent: Monday, February 21, 2011 11:03 AM
To: Proof Theory List
Subject: [PT] Update: Question on a class of tautologies

Hello,

Many thanks to those who answered the question I posted a few days
ago. Here it is again, with a bit of clarification (I hope to get
more answers). I collect below some of the answers I've got (beyond
Lutz Strassburger's one, already posted to the list and reprised by
Tom Gundersen).


PROBLEM   Characterise the set X of classical propositional
tautologies of the form A -> B such that:

* all and only the variables in A appear in B;
* no variable appears twice in A (and so in B);
* there is no negation in A and in B: the only allowed connectives are ^ and V.


Note that a rather closely related object is the monotone sequent
calculus MLK, which is LK where no negation appears. This calculus is
studied in proof complexity, in the hope of finding lower bounds,
following the relative success of monotone circuits. There is a
strict relation between MLK and cut-free proofs in deep inference
(whence my interest). It is conceivable that a linear version of MLK
would be able to capture X in terms of provability.

I am mainly motivated by the question: how much can we prove in
classical logic if we stay linear? We have shown, with atomic flows
(see <http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf>), that
we can decompose any classical propositional proof into two parts: a
structural one and a linear one. We also have shown that the
structural part contains sufficient information to normalise the
proof.

We have a characterisation of the linear part (it is generated by the
two inference rules switch and medial). However, this
characterisation is unsatisfactory: we know that `it works' but we
don't know why (perhaps I should just speak for myself and not my
coauthors?).

I hope to find alternative definitions of the set X of tautologies,
in the hope to better understand the switch-medial fragment (which is
certainly smaller than X). So, I'm looking for anything that can
generate the set X: combinatorially, or perhaps via criteria on proof
nets, whatever really. If you have something like this, let me have a
look, please.

Ciao,

-Alessio

--------------------------------------------------------------------

From: Tom Gundersen <[email protected]>
Date: Thu, 17 Feb 2011 21:43:05 +0100
Subject: Re: [PT] Question on a class of tautologies
To: Lutz Strassburger <[email protected]>, Alessio Guglielmi
<[email protected]>

On Thu, Feb 17, 2011 at 2:51 PM, Lutz Strassburger
<[email protected]> wrote:
>
>  Hello Alessio,
>
>  I do not fully understand what you mean by "characterize". But the set can
>  easily be shown to be coNP-complete:
>
>  There is a polytime function f, such that for every formula C of size n, we
>  have that f(C) is a formula of shape A->B having the three *-properties
>
>   * all and only the variables in A appear in B;
>   * no variable appears twice in A (and so in B);
>   * there is no negation in A and in B.
>
>  and having size smaller than 2n^2, and such that f(C) is a tautology if and
>  only if C is a tautology.

For the sake of completeness:

The function f can be defined as follows:

Let a_1,...,a_n and their duals be the atoms occurring in C. Let a_i
occur k_i times, and -a_i occur l_i times.

B is obtained from C by replacing each occurrence of a_i (resp., -a_i)
by a new atom a_i^j (resp., b_i^j) such that no atom occurs twice in
B.

A=AND_{i=1}^n [ AND_{j=1}^k_i a_i^j   or   AND_{j=1}^l_i b_i^j]

 From a KS proof of C we can then build an SKS derivation from A to B
and from an SKS derivation from A to B we can build an SKS proof of C.

Cheers,

Tom

--------------------------------------------------------------------

Date: Fri, 18 Feb 2011 08:36:16 +0100 (CET)
From: Lutz Strassburger <[email protected]>
To: Tom Gundersen <[email protected]>
cc: Alessio Guglielmi <[email protected]>, [email protected]
Subject: Re: [PT] Question on a class of tautologies

On Thu, 17 Feb 2011, Tom Gundersen wrote:

>For the sake of completeness:
>
>The function f can be defined as follows:
>
>Let a_1,...,a_n and their duals be the atoms occurring in C. Let a_i
>occur k_i times, and -a_i occur l_i times.
>
>B is obtained from C by replacing each occurrence of a_i (resp., -a_i)
>by a new atom a_i^j (resp., b_i^j) such that no atom occurs twice in
>B.
>
>A=AND_{i=1}^n [ AND_{j=1}^k_i a_i^j   or   AND_{j=1}^l_i b_i^j]
>
>>From a KS proof of C we can then build an SKS derivation from A to B
>and from an SKS derivation from A to B we can build an SKS proof of C.

The construction of B is in my paper "Extension without cut".

L.

--------------------------------------------------------------------

From: Tom Hirschowitz <[email protected]>
To: Alessio Guglielmi <[email protected]>
Subject: Re: [PT] Question on a class of tautologies
Date: Thu, 17 Feb 2011 13:29:14 +0100

Hi Alessio,

Sequents with exactly two occurrences of each variable, one negative
and one positive, are called "linearly balanced" in Murawski and
Ong's "Fast verification of MLL proof nets via IMLL".

Does this count as a tiny bit of information? Not sure, just in case.

Cheers,
Tom