Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Reports on Mathematical Logic

1 2001

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: adequate Gentzen system

Sortuj według:

Ogranicz wyniki do:

Fully adequate Gentzen systems and the deduction theorem

Font J., Jansana R., Pigozzi D.

Reports on Mathematical Logic

2001

No. 35

115-165

A deductive system over an arbitrary language type A is a finitary and substitution-invariant consequence relation over the formulas of A. A Gentzen system is a finitary and substitution-invariant consequence relation over the sequents of A. A matrix model of a deductive system S is a pair (A,F) where A is A-algebra and F is an S-filter on A, i.e., a subset of A closed under all interpretations of the consequence relation of S in A. A generalized matrix is a pair (A,C) where C is an algebraic closed-set system over A; it is a model of a Gentzen system G if C is closed under all interpretations of the consequence relation of G in A. A Gentzen system G is fully adequate for a deductive system S if (roughly speaking) every reduced generalized matrix model of G is of the form (A, FisA), where FisA is the set of all S-filters on A. The existence of a fully adequate Gentzen system for a given protoalgebraic deductive system S is completely characterized in terms of the following variant of the standard deduction theorem of classical and intuitionistic logic. The main result of the paper is the following: Theorem. A protoalgebraic deductive system has a fully adequate Gentzen system if and only if it has a Leibniz-generating PGDD (a parameterized graded deduction-detachment) system over all Leibniz theories. Two corollaries: (I) A weekly algebraizable deductive system has a fully adequate Gentzen system iff it has the multiterm deduction-detachment theorem. (II) A finitely equivalential deductive system has a fully adequate Gentzen system iff it has a finite Leibniz-generating system for over all Leibniz S-filters. Several different variants of the deduction theorem arise in the course of the paper showing that this familiar notion is only one manifestation of a surprisingly complex phenomenon.