Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

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.

Lambda abstraction algebras : coordinatizing models of lambda calculus

Pigozzi D., Salibra A.

Fundamenta Informaticae

1998

Vol. 33, nr 2

149-200

Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like combinatory algebras they can be defined by true identities and thus from a variety in the sense if universal algebra. One feature of lambda abstraction algebras that sts them apart from combinatory algebras is the way variables in the lambda calculus are abtracted; this provides each lambda abstraction algebra with an implicit coordinate system. Another peculiar feature in the algebraic reformulation of (b)-conversion as the definition of abstract substitution. Functional lambda abstraction algebras arise as the 'coordinatizations' of environment models or lambda models, the natural combinatory models of the lambda calculus. As in the case of cylindric and polyadic algebras, questions of the functional representation of various subclasses of lambda abstraction algebras are an important part of the theory. The main result of the paper is a stronger version of the functional representation theorem for locally finite lambda abstraction algebras, the algebraic analogue of the completeness theorem of lambda calculus. This result is used to study the connection between the combinatory models of the lambda calculus and lambda abstraction algebras. Two significant results of this kind are the existence of a strong categorical equivalence between lambda algebras and locally finite lambda abstraction algebras, and between lambda models and rich, locally finite lambda abstraction algebras.