On logical flow graphs.
Item
-
Title
-
On logical flow graphs.
-
Identifier
-
AAI9325075
-
identifier
-
9325075
-
Creator
-
Carbone, Alessandra.
-
Contributor
-
Adviser: Rohit Parikh
-
Date
-
1993
-
Language
-
English
-
Publisher
-
City University of New York.
-
Subject
-
Mathematics
-
Abstract
-
The key topic of this thesis is the notion of proof. This research considers proofs as objects, measures their complexity with the number of lines and studies the logical relations among the occurrences of formulas in them. We develop a theory of how the influence of a formula spreads through a proof, based on the notion of logical flow graph (introduced by S. Buss in 1991) and we study how the logical flow graph of a proof behaves with respect to two basic results in proof theory: the Cut Elimination Theorem and the Craig Interpolation Theorem.;The results are used to obtain lower bounds on the number of lines in a proof. Namely, we applied them to the following context of Peano Arithmetic: postulating that large numbers are not finite leads to an inconsistent extension of arithmetic which is, however, conservative for proofs of low complexity. Thus an inconsistent theory can prove true results, as long as the proofs are not too long. This was first proved by Parikh in 1971. In 1985, Dragalin improves Parikh lower bounds on the complexity of the proofs of true sentences. In this work we improve Parikh's statement showing that if a sentence is proved using the fact that large numbers are not finite by means of a proof with low complexity, then one can find a proof of it with lower complexity and not using the postulate on large numbers. Our lower bounds are the best possible bounds and considerably improve the ones obtained by both Parikh and Dragalin. We then consider the consistent theory of large numbers asserting the existence of some large number and show that not only is a conservative extension of Peano Arithmetic but also that there is no speed-up by this theory over arithmetic.;Results on the complexity (intended as number of symbols) of the interpolant C for a given sequent A {dollar}\to{dollar} B and on the complexity (intended as number of lines) of the proofs A {dollar}\to{dollar} C and C {dollar}\to{dollar} B are also studied and proofs of the classical and intuitionistic Craig's Interpolation Theorem based on logical flows are given.
-
Type
-
dissertation
-
Source
-
PQT Legacy CUNY.xlsx
-
degree
-
Ph.D.
