Metatheories of deductive systems

Simple item page
dc.contributor.advisor Clifford Bergman
dc.contributor.advisor Don Pigozzi
dc.contributor.author Babyonyshev, Sergei
dc.contributor.department Mathematics
dc.date 2018-08-24T23:31:53.000
dc.date.accessioned 2020-07-02T06:12:27Z
dc.date.available 2020-07-02T06:12:27Z
dc.date.copyright Thu Jan 01 00:00:00 UTC 2004
dc.date.issued 2004-01-01
dc.description.abstract <p>A deductive system (Hilbert-style) is an algebraic closure system over the set of formulas of given propositional language. Similarly, a Gentzen system is an algebraic closure system over the set of all sequents, i.e., finite sequences of formulas, of this language. The main feature of this work is a technique that allows us to adapt the methods, previously developed in the area of algebraic logic for work with Hilbert-style deductive systems, to the case of Gentzen systems. Using the properties of the Tarski congruence, a generalization of the Leibnitz congruence, we develop an algebraic hierarchy for Gentzen systems that closely parallels the well-known algebraic hierarchy of deductive systems. This approach allows us to unify in a single framework several previously known results about algebraizable and equivalential Gentzen systems. We also obtain a characterization of weakly algebraizable Gentzen systems. The significance of Gentzen systems and related axiomatizations by Gentzen rules is due in large part to the fact that various metatheoretical properties of deductive systems can be formulated in their terms. It was observed that a number of important non-protoalgebraic deductive system that have a natural algebraic semantics also have a so-called fully adequate Gentzen system associated with them, the conjunction-disjunction fragment of the classical propositional logic being a paradigmatic example. In this work, a general criterion for the existence of a fully adequate Gentzen system for non-protoalgebraic deductive systems is obtained, and it is shown that many of the known partial results can be explained based on this general criterion. This includes such cases as the existence of fully adequate Gentzen systems for self-extensional logics with conjunction or implication, and the criterions for the existence of a fully adequate Gentzen system for protoalgebraic and weakly algebraizable logics. In another vein, it is shown that the existence of a multiterm deduction-detachment theorem in a deductive system is equivalent to the fact that, so called, axiomatic closure relations for the deductive system form a Gentzen system.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/rtd/928/
dc.identifier.articleid 1927
dc.identifier.contextkey 6088651
dc.identifier.doi https://doi.org/10.31274/rtd-180813-8832
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath rtd/928
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/82361
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/rtd/928/r_3145628.pdf|||Sat Jan 15 02:30:43 UTC 2022
dc.subject.disciplines Mathematics
dc.subject.keywords Mathematics
dc.title Metatheories of deductive systems
dc.type article
dc.type.genre dissertation
dspace.entity.type Publication
relation.isOrgUnitOfPublication 82295b2b-0f85-4929-9659-075c93e82c48
thesis.degree.level dissertation
thesis.degree.name Doctor of Philosophy
File
Original bundle
Now showing 1 - 1 of 1
Name:
r_3145628.pdf
Size:
1.46 MB
Format:
Adobe Portable Document Format
Description:
Download
Collections
Theses and Dissertations