Cycling in proofs and feasibility

There is a common perception by which small numbers are considered more concrete and large numbers more abstract. A mathematical formalization of this idea was introduced by Parikh (1971) through an inconsistent theory of feasible numbers in which addition and multiplication are as usual but for which some very large number is defined to be not feasible. Parikh shows that sufficiently short proofs in this theory can only prove true statements of arithmetic. We pursue these topics in light of logical flow graphs of proofs (Buss, 1991) and show that Parikh's lower bound for concrete consistency reflects the presence of cycles in the logical graphs of short proofs of feasibility of large numbers. We discuss two concrete constructions which show the bound to be optimal and bring out the dynamical aspect of formal proofs. For this paper the concept of feasible numbers has two roles, as an idea with its own life and as a vehicle for exploring general principles on the dynamics and geometry of proofs. Cycles can be seen as a measure of how complicated a proof can be. We prove that short proofs must have cycles.

     

The uniquely embeddable planar graphs

Whitney [7] proved in 1932 that for any two embeddings of a planar 3-connected graph, their combinatorial duals are isomorphic. In this manner, the term “uniquely embeddable planar graph” was introduced. It is a well-known fact that combinatorial and geometrical duals are equivalent concepts. In this paper, the concept of unique embeddability is introduced in terms of special types of isomorphisms between any two embeddings of a planar graph. From this, the class U of all graphs which are uniquely embeddable in the plane according to this definition, is determined, and the planar 3-connected graphs are a proper subset of U. It turns out that the graphs in U have a unique geometrical dual (i.e., for any two embeddings of such a graph, their geometrical duals are isomorphic). Furthermore, the theorems and their proofs do not involve any type of duals.     

Proof complexity of propositional default logic

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen??s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti??s enhanced calculus for skeptical default reasoning.     

Some remarks on lengths of propositional proofs

We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depthd Frege proofs ofm lines can be transformed into depthd proofs ofO(m ^d+1) symbols. We show that renaming Frege proof systems are p-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed. Supported in part by NSF grant DMS-9205181     

Local computation in linear logic

This work deals with the exponential fragment of Girard's linear logic ([3]) without the contraction rule, a logical system which has a natural relation with the direct logic ([10], [7]). A new sequent calculus for this logic is presented in order to remove the weakening rule and recover its behavior via a special treatment of the propositional constants, so that the process of cut-elimination can be performed using only “local” reductions. Hence a typed calculus, which admits only local rewriting rules, can be introduced in a natural manner. Its main properties — normalizability and confluence — has been investigated; moreover this calculus has been proved to satisfy a Curry-Howard isomorphism ([6]) with respect to the logical system in question. MSC: 03B40, 03F05.     

A formalization of Sambins's normalization for GL

Sambin [6] proved the normalization theorem (Hauptsatz) for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini [1], on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45.     

Homology of proof-nets

This work defines homology groups for proof-structures in multiplicative linear logic (see [Gir1], [Gir2], [Dan]). We will show that these groups characterize proof-nets among arbitrary proof-structures, thus obtaining a new correctness criterion and of course a new polynomial algorithm for testing correctness. This homology also bears information on sequentialization. An unexpected geometrical interpretation of the linear connectives is given in the last section. This paper exclusively focuses onabstract proof-structures, i.e. paired-graphs. The relation with actual proofs is investigated in [Gir1], [Gir2], [Dan], [Ret] and [Tro].     

Ten questions and one problem on fuzzy logic

Recently, I had a very interesting friendly e-mail discussion with Professor Parikh on vagueness and fuzzy logic. Parikh published several papers concerning the notion of vagueness. They contain critical remarks on fuzzy logic and its ability to formalize reasoning under vagueness [10,11]. On the other hand, for some years I have tried to advocate fuzzy logic (in the narrow sense, as Zadeh says, i.e. as formal logical systems formalizing reasoning under vagueness) and in particular, to show that such systems (of many-valued logic of a certain kind) offer a fully fledged and extremely interesting logic [4, 5]. But this leaves open the question of intuitive adequacy of many-valued logic as a logic of vagueness. Below I shall try to isolate eight questions Parikh asks, add two more and to comment on all of them. Finally, I formulate a problem on truth (in)definability in Łukasiewicz logic which shows, in my opinion, that fuzzy logic is not just “applied logic” but rather belongs to systems commonly called “philosophical logic” like modal logics, etc.     

Subalternation and existence presuppositions in an unconventionally formalized canonical square of opposition

An unconventional formalization of the canonical (Aristotelian-Boethian) square of opposition in the notation of classical symbolic logic secures all but one of the canonical square’s grid of logical interrelations between four A-E-I-O categorical sentence types. The canonical square is first formalized in the functional calculus in Frege’s Begriffsschrift, from which it can be directly transcribed into the syntax of contemporary symbolic logic. Difficulties in received formalizations of the canonical square motivate translating I categoricals, ‘Some S is P’, into symbolic logical notation, not conjunctively as \({\exists x[Sx\wedge Px]}\), but unconventionally instead in an ontically neutral conditional logical symbolization, as \({\exists x[Sx\rightarrow Px]}\). The virtues and drawbacks of the proposal are compared at length on twelve grounds with the explicit existence expansion of A and E categoricals as the default strategy for symbolizing the canonical square preserving all original logical interrelations.     

A note on the characterization of domination perfect graphs

A graph G is domination perfect if for each induced subgraph H of G, γ(H) = i(H), where γ and i are a graph's domination number and independent domination number, respectively. Zverovich and Zverovich [3] offered a finite forbidden induced characterization of domination perfect graphs. This characterization is not correct, but the ideas in [3] can be used to weaken the known sufficient conditions for a graph to be domination perfect and to obtain short proofs of some results regarding domination perfect graphs. © 1993 John Wiley & Sons, Inc.     

Equivalences and the complete hierarchy of intersection graphs of paths in a tree

An (h,s,t)-representation of a graph G consists of a collection of subtrees of a tree T, where each subtree corresponds to a vertex in G, such that (i) the maximum degree of T is at most h, (ii) every subtree has maximum degree at most s, (iii) there is an edge between two vertices in the graph G if and only if the corresponding subtrees have at least t vertices in common in T. The class of graphs that have an (h,s,t)-representation is denoted by [h,s,t]. It is well known that the class of chordal graphs corresponds to the class [3, 3, 1]. Moreover, it was proved by Jamison and Mulder that chordal graphs correspond to orthodox-[3, 3, 1] graphs defined below.In this paper, we investigate the class of [h,2,t] graphs, i.e., the intersection graphs of paths in a tree. The [h,2,1] graphs are also known as path graphs [F. Gavril, A recognition algorithm for the intersection graphs of paths in trees, Discrete Math. 23 (1978) 211-227] or VPT graphs [M.C. Golumbic, R.E. Jamison, Edge and vertex intersection of paths in a tree, Discrete Math. 55 (1985) 151-159], and [h,2,2] graphs are known as the EPT graphs. We consider variations of [h,2,t] by three main parameters: h, t and whether the graph has an orthodox representation. We give the complete hierarchy of relationships between the classes of weakly chordal, chordal, [h,2,t] and orthodox-[h,2,t] graphs for varied values of h and t.     

A new functional calculus for noncommuting operators

In this paper we use the notion of slice monogenic functions [F. Colombo, I. Sabadini, D.C. Struppa, Slice monogenic functions, Israel J. Math., in press] to define a new functional calculus for an n-tuple T of not necessarily commuting operators. This calculus is different from the one discussed in [B. Jefferies, Spectral Properties of Noncommuting Operators, Lecture Notes in Math., vol. 1843, Springer-Verlag, Berlin, 2004] and it allows the explicit construction of the eigenvalue equation for the n-tuple T based on a new notion of spectrum for T. Our functional calculus is consistent with the Riesz-Dunford calculus in the case of a single operator.     

Circular proofs for the Gödel-Löb provability logic

Sequent calculus for the provability logic GL is considered, in which provability is based on the notion of a circular proof. Unlike ordinary derivations, circular proofs are represented by graphs allowed to contain cycles, rather than by finite trees. Using this notion, we obtain a syntactic proof of the Lyndon interpolation property for GL.     

A cut-free sequent system for two-dimensional modal logic,and why it matters

The two-dimensional modal logic of Davies and Humberstone (1980) [3] is an important aid to our understanding the relationship between actuality, necessity and a priori knowability. I show how a cut-free hypersequent calculus for 2D modal logic not only captures the logic precisely, but may be used to address issues in the epistemology and metaphysics of our modal concepts. I will explain how the use of our concepts motivates the inference rules of the sequent calculus, and then show that the completeness of the calculus for Davies–Humberstone models explains why those concepts have the structure described by those models. The result is yet another application of the completeness theorem.     

The Cayley graphs of ℤ<Superscript>d</Superscript> and the limits of vertex-primitive graphs of <Emphasis Type="Italic">HA</Emphasis>-type

We study the limits of the finite graphs that admit some vertex-primitive group of automorphisms with a regular abelian normal subgroup. It was shown in [1] that these limits are Cayley graphs of the groups ?^d. In this article we prove that for each d > 1 the set of Cayley graphs of ?^d presenting the limits of finite graphs with vertex-primitive and edge-transitive groups of automorphisms is countable (in fact, we explicitly give countable subsets of these limit graphs). In addition, for d < 4 we list all Cayley graphs of ?^d that are limits of minimal vertex-primitive graphs. The proofs rely on a connection of the automorphism groups of Cayley graphs of ?^d with crystallographic groups.     

Corrections of proofs for Hansen and Mélot's two theorems

The Randi? index R(G) of a (chemical) graph G is also called connectivity index. Hansen and Mélot [Variable neighborhood search for extremal graphs 6: analyzing bounds for the connectivity index, J. Chem. Inf. Comput. Sci. 43 (2003) 1-14] in their paper, characterized the chemical trees of given order and number of pendent vertices which have the minimum and maximum Randi? index, respectively. In this note, we point out the mistakes in the proofs of their results Theorems 8 and 10, while we still believe that the two theorems are true, and then we give their corrected proofs.     

A new coloring theorem of Kneser graphs

In 1997, Johnson, Holroyd and Stahl conjectured that the circular chromatic number of the Kneser graphs KG(n,k) is equal to the chromatic number of these graphs. This was proved by Simonyi and Tardos (2006) [13] and independently by Meunier (2005) [10], if χ(KG(n,k)) is even. In this paper, we propose an alternative version of Kneser's coloring theorem to confirm the Johnson-Holroyd-Stahl conjecture.     

Computation paths logic: An expressive,yet elementary,process logic

A new process logic is defined, called computation paths logic (CPL), which treats formulas and programs essentially alike. CPL is a pathwise extension of PDL, following the basic process logic of Harel, Kozen and Parikh and is close in spirit to the logic R of Harel and Peleg. It enjoys most of the advantages of previous process logics, yet is decidable in elementary time. We also offer extensions for modeling asynchronous/synchronous concurrency and infinite computations. All extensions are also shown to be decidable in elementary time.