Abstract EN:

Part I. Among the unsolvable terms of the lambda calculus, the mute ones are those having the highest degree of undefinedness. For each natural number n > 1, we introduce two infinite and recursive sets mn and gn. Their elements are called restricted regular mute and regular mute terms respectively. They are defined inductively and we prove that they are mute. Furthermore, we show that sets mn are graph-easy for any n : for any closed term t there exists a graph model equating all the terms of mn to t. We also provide a brief survey of the notion of undefinedness in lambda-calculus. Part II. We introduce factor algebras of first-order type and show that they can be used to provide an algebraic counterpart of ordinary first-order structures. We show that this translation can be extended to open formulas and equations between terms. By considering that propositional logic is a first-order logic on a particular type tcl , a new algebraic calculus for propositional logic is developed. Rules for the calculus are the axioms of the variety generated by the factor algebras of type tcl. We also provide a confluent and terminating term rewriting system for such calculus. Furthermore, we study the basic algebraic properties of factor algebras of first¬order type through the notion of splitting pair.