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

Hi,

Two more updates:


At 11:48 -0500 21/2/11, Giorgi Japaridze wrote:
>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.

Hi Giorgi, no, closure under substitution 
wouldn't do for me. I agree that, without it, 
what you have is odd and hard to deal with, but 
strict linearity is very important for us, as we 
are interested in the structure of the proof 
between A and B (see below), more than in the 
semantics of the formulae.


Lutz Strassburger reminds me of the presence of a 
combinatorial criterion on proof nets in his 
paper:

Naming Proofs in Classical Propositional Logic
François Lamarche and Lutz Straßburger
TLCA 2005, LNCS 3461, pp. 246-261
<http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf>


Ciao,

-Alessio


>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
>
>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.