abstract.tex

A generalization of the notion of implication is introduced in \cite{amir}, as a binary operator which internalizes the reflexive and transitive properties of the provability relation on the set of all propositions. This generalization gives rise to a classification of some sub-intuitionistic and sub-structural logics with various behaviors of their respecting implication operators. The canonical instance of this generalization, which is \emph{the dynamic locale}, can be thought of as an algebraic model for \emph{dynamic topological systems}.

In this paper we will introduce a cut-free G3-style sequent calculus for the logic of dynamic locales and its extension with intuitionistic implication. Then we will study some properties of this system such as subformula property, disjuction property, admissibility of the Visser's rule and Craig's and deductive interpolation.