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 order 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. One of its specifications, which is called the logic of \emph{spacetime} in \cite{amir} makes a dynamic reading of the Proof Interpretation for conditional statements possible. This reading does not suffer from the well-known impredicativity in the BHK interpretation.

In this paper, we will introduc a G3 style sequent-style calculus for the logic of spacetime, called $\stt$ along with an equivalent cut-free system, called $\gstt$. Then we will study some properties of thses systems such as subformula property, disjuction property, admissibility of the Visser's rule and existence of interpolants.