Abstract

The dissertation deals with problems in "logic", more precisely, it deals with particular formal systems aiming at capturing patterns of valid reasoning. Sequent calculi were proposed to characterize logical connectives via introduction rules. These systems customarily also have structural rules which allow one to rearrange the set of premises and conclusions. In the "structurally free logic" of Dunn and Meyer the structural rules are replaced by combinatory rules which allow the same reshuffling of formulae, and additionally introduce an explicit marker for the application of the rule---the combinator. The dissertation gives syntactic extensions of such systems introducing conjunction and disjunction . Cut elimination is proved for these systems. ;Syntactic systems as a rule are accompanied by a semantics which interprets them. The extended systems are supplied with semantics using algebraic methods. First, the Lindenbaum algebras are formed, and then these algebras are represented in an algebra of sets. This gives a so called Kripke-style semantics for the systems. The representation for the distributive extension utilizes well-known techniques; it uses sets of prime filters and set theoretical operations on them to deal with conjunction and disjunction, plus a ternary accessibility relation to accommodate the intensional operators as fusion and implication. The representation theorem is proven generally, i.e., for arbitrary sets of combinators using the "squeeze lemma" of Routley and Meyer. ;The non-distributive calculi require a different representation since union and intersection are distributive. Two previous representations for lattices are overviewed, and a modification of the Hartonas-Dunn representation is successfully augmented with the intensional operations. Instead of sets of filters, sets of pairs of minimally inconsistent filters and ideals are used and the representation theorem is proven. The representation results provide soundness and completeness for the systems. The dissertation also investigates properties of dual combinators , proving a series of lemmas about dual combinatory systems not being Church-Rosser and being inconsistent. Combinatorially definable classes of lambda-terms are considered as well.