introduction.tex

As a logical connective, \emph{the implication} is supposed to capture the higher order notion of \emph{logical entailment}. So it must reflect properties of the entailment relation in the language level. But we may have a broad meaning of an entailment relation in mind, to include different logics. Also we may choose which set of properties we expect the implication to reflect, and which structures we want it to internalize. This gives rise to many different instances of an implication; Indeed, for example, the implication in classical, intuitionistic, substructural or basic logic behave differently.

For a more particular example, observe the usual behaviour that we expect from the implication operator in intuitionistic or classical logic: It internalizes properties such as reflexivity, transitivity, and all other properties of the entailment relation which are common in both intuitionistic and classical settings, like how it deals with the meaning of operators like conjunction or disjunction. For example, both classical and intuitionistic entailments enjoy a \emph{deduction theorem}, i.e. for some propositions $A$ and $B$, the metalogical relation of entailment between $A$ and $B$ is equivalent to the truth of the proposition $A \rightarrow B$.

On the other hand, since there are intrinsic differences between what we intend by intuitionistic and classical entailments, their respecting implication connective also behaves differently in many ways. For instance, one can observe that the validity of $\varphi = \neg \neg A \rightarrow A$ can be interpreted as the internalization of RAA: If the negation of $A$ entails absurdity, then $A$ is true. So, contrary to classical implication, the intuitionistic implication must reflect the fact that RAA is not a valid rule of inference in intuitionistic setting by refuting $\varphi$.

This leaves us with the question that what is the essence of internalizing the entailment relation, whihc is a preorder relation in its most general form. The first author investigates this question in \cite{amir}, by introducing \emph{abstract implication}, a binary operator general enough to include the definitions of all the implication connectives for the logics that was mentioned above. An abstract implication is thus defined as an operator which internalizes the reflexive and transitive nature of the entailment.

Although the definition of the abstract implication captures the preorder structure of the entailment relation between the propositions, yet it does not require the operator to participate in the well-known adjunction between implication and conjunction. So abstract implication include not only the well-behaved implication operators of intuitionistic or classical logic, but also operators for which the mentioned \emph{deduction theorem} does not hold necessarily.

A smaller class of abstract implications are also studied in \cite{amir} which do not break the adjunction between implication and conjunction. These implications coincide with the natural notion of implication in \emph{dynamic locales}, which are point-free version of topological spaces with a topological automorphism.

In light of these observations, \cite{amir} introduces sequent style systems for dynamic locales, along with different semantics for them. An extensive investigation of these systems is done from an algebraic and topological point of view, while proof-theoretic approaches fail in absence of a reasonable \emph{analyticity} criterion. The systems in \cite{amir} are not analytic in the sense that a proof-tree can have formulas that are not subformulas of the formulas in the consequence.

In this paper we will talk about the logic of dynamic locals, $\ldl$, and some of its extensions. In the next section, we will see some preliminaries and the definition of a sequent style system for the logic of dynamic locales, along with its algebraic semantics, as it is defined in \cite{amir}.
In the third section, we will introduce a sequent style, conraction-free and cut-free system for the logic of dynamic locales.
In the fourth section, the admissibility of cut in this system will be proved. Then, in section five, we will use this theorem to deduce some results about the logic of dynamic locales and some of its extensions, such as subformula property, disjuction property and admissibility of the generalized Visser's rule.
And in the last section, we will show that some extensions of $\ldl$ have the Craig and deductive interpolation property.