Subject: RE: Re: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-18 02:20:00 GMT (33 weeks, 5 days, 20 hours and 37 minutes ago)
>> 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? Phi is there, and therefore so is psi because psi is a substitutional instance of phi. What is NOT there is, for example, -b OR (b AND b). > 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? Extended discussions of that class is given in “Introduction to cirquent calculus and abstract resource semantics”. A definition (but no discussions) can also be found in Section 5 of "Cirquent calculus deepened". Either paper can be downloaded from http://www.cis.upenn.edu/~giorgi/cl.html#3 If you read “Introduction to cirquent calculus…”, you will see the semantical motivation behind all this. In fact, my enthusiasm about cirquents is related to the fact that they can express and axiomatize things that other formalisms cannot. Despite the impression one could have gotten from our ongoing discussion, the possible speedup that cirquent calculus may (or may not) offer is only of a secondary importance for me personally. > Note that up to now we have two "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) > > 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), I can easily imagine that cirquents are in (2). > 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". Hard to say. But notice that all inferences used in my PHP proof take place not too far from the root, within a bounded depth. So, this looks like a “lucky case” even from the perspective of (not so) deep inference in general. Giorgi Japaridze http://www.csc.villanova.edu/~japaridz/