RE: Re: Deep cirquent calculus

On Sun, 16 Sep 2007, Giorgi Japaridze wrote:

> > I guess you mean balanced tautologies where each
> > atom occurs once positive and once negative.
>
> Tautologies where each atom has *at most* one positive
> and *at most* one negative occurrence,

OK. Then

   phi = a OR -a OR b

is in, whereas

   psi = "b OR -b OR b"

should be out.

> and also substitutional instances of such tautologies.

But psi is a substitutional instance of phi? Am I missing something here?

> > Then, what do you mean by "capturing these objects"?
>
> Capturing = axiomatizing (in some reasonable, natural
> way).

I still don't get what you mean. Probably I should look at some paper 
where you have this written up. Can you please give the reference?

> Sure not  polynomial. Just a proof system. Other
> formalisms do not have that. Could you axiomatize
> binary tautologies in CoS+extension? POINT 1 was
> about expressiveness and not at all about proof
> complexities, so coNP-completeness is irrelevant.

OK, that's some relief.

> Let us call *proof width* (in CoS) the maximal size of
> formulas involved in the proof. And call *proof length*
> the number of formulas in the proof. Sharing generally
> allows us to reduce both width and length. Width is
> reduced at the expense of merging identical parts in
> formulas. And length is reduced at the expense of
> merging identical steps in the proof (that could
> otherwise have to be performed over an over again
> within different occurrences of identical subformulas).
> As for extension, it only reduces width, at the expense
> of abbreviating large subformulas. Sure every
> polynomial size cirquent can be represented as a
> polynomial size formula, by introducing abbreviations
> for all nodes of the cirquent and then indicating who
> is whose parent/child. But this does not help when those
> abbreviations have to be disabbreviated later to
> perform transformations on (inside) them. Alessio
> expressed very well what else I wanted to say:

I principle, I can agree with that. However, there are two things that I 
am not (yet) convinced of:

1) can you use cirquents to exponentially reduce the *proof length* ?

2) If yes, why can extension not do the same?

The real problem here is, that we do not have any examples to exhibit the 
problems.

> Alessio Guglielmi wrote:
>   "I have a comment about the possibility of
>    p-simulating deep cirquents by CoS + some extension.
>    I cannot rule out entirely the possibility of this
>    simulation by some extension, but I doubt that this
>    can be Tseitin's extension; in any case this has to
>    be really awkward (so, I agree with Giorgi and am
>    sure that Lutz also agrees). That said, I think that
>    the main point is not really to achieve the maximum
>    speed-up `somehow', but to do it naturally."

Well, the question is always, what do "maximum speed-up" and "naturally" 
mean. Note that up to now we have to "classes" of proof systems:

(1) ordinary Frege, which is equivalent (wrt p-simulation) to sequent 
calculus with cut.

(2) Frege (or CoS with cut) plus extension (or substitution)

Note that it is not at all obvious that, for example, extension is as 
powerful as substitution. The proof is quite technical.

I am claiming that we can open up a third group, namely

(3) CoS without cut, but with extension

I have no clue whether this is as good as (2), or weaker.

But I strongly conjecture that your cirquents are either in (2) 
or in (3), and that proving this is not more complicated than proving that 
substitution and extension are equally good for Frege.

I do not make any claims with respect to which one, "cirquents" or "CoS 
with extension", is more "natural".

> > I don't think PHP is so "particular" in that respect.
>
> Its particularity is that, morally, it only has a proof
> breadth problem (in CoS without extension) but not a
> proof length problem. Sharing is only used in it to merge
> large identical parts in formulas, but not to merge identical
> steps in the proof: no transformations are taking place
> within shared components in that proof, which is quite
> a ?lucky case?.

I agree. However, I am not aware of an example which is not such a ?lucky 
case?. Maybe it is inherent to the problem that we cannot find an "unlucky 
case".

-Lutz