Subject: RE: Re: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-17 19:56:42 GMT (33 weeks, 3 days, 20 hours and 43 minutes ago)
Hello,
I elaborate a bit on why I see cirquents as a welcome advance.
Rhetorical question: what is the most natural representation of
boolean functions, formulae or circuits?
Many of us are in the business of eliminating bureaucracy from proofs
to get to their essence, so, why not eliminating bureaucracy also
from formulae and use circuits instead? Of course, one has to prove
that circuits are convenient enough for whatever purpose one wants to
use them, and we still have to see whether a proof theory can be
developed for them. But the fact remains that they are a more natural
starting point than formulae.
I thought about using them in the place of formulae in the past, but
did not do it because I had no further motivation than their
naturalness, and it was already difficult enough to make the
community accept deep inference. However, Giorgi now has external,
semantic justification for using circuits, and, in addition, he finds
that deep inference is the natural proof methodology for them. I see
this as a very welcome development.
I am convinced that this is not a slightly different syntax from the
calculus of structures. I remember very well when people were saying
the same about deep inference vs the sequent calculus, usually
without thinking much before talking.
Perhaps it will turn out that CoS + some extension can p-simulate
cirquents. I don't think that this will be easy, if at all possible.
Anyway, I insist that the point is that circuits are less
bureaucratic then formulae.
I would like to add that I find Lutz's argument in support of the
extension rule very unsatisfying. Perhaps he is right on a purely
technical level, and limited to the cirquent system that Giorgi shows
in his paper, but there is anyway a difficulty ahead, which I'll try
to explain here.
Let's start from the CoS derivation
[(B [A C] D) ([A C] D E)]
s -------------------------
[A (B [A C] D) (C D E)]
s -----------------------
[A A (B C D) (C D E)]
c^ --------------------- .
[A (B C D) (C D E)]
Let's see now how this derivation might look like with circuits:
A C
\ /
V D
\ /
B ^ E
\ / \ /
^ ^
\ /
V
---------- .
C D
\ /
B ^ E
\ / \ /
^ A ^
\|/
V
It should be clear that circuits can do in one shot and without
duplication what CoS does essentially in two steps with duplication.
This mechanism can obviously produce an exponential proof compression
in the circuits case, when subjected to recursion. If we try to
simulate circuits with Tseitin extension, and so, by giving a name to
the shared parts, we find ourselves with something like
B a a E C D
\| |/ \ /
^ A ^ a ^
\|/ \ /
V <-> .
\ /
\ /
\ /
^
How can we design a reasonable inference rule that carries A in a
disjunction next to C, without duplicating anything?
Perhaps I'm missing something, please correct me if I'm wrong.
There are pending questions by Giorgi. I'll set the good example and
think some more before answering.
Ciao,
-Alessio