Contexts, viewed as theories or modalities, have structural properties, and associated natural structural operations, such as union and intersection. These structural properties are most naturally captured by an algebra, reminiscent of relation or dynamic algebra , a set of operations that can be applied to contexts to form new contexts.

Thus we can have a larger space of modalities than just those that are explicitly named. We add quantifiers that range over modalities, so that we can state propositions like, ``no context with the property P exists'', or ``all contexts obey Q''. We give an axiomatization of these quantifiers which we show is complete with respect to a natural semantics.

We develop a self-dual algebra such that every point in the algebra is representable by some formula in the logic. This algebra arises as an instantiation of a Heyting algebra into several categorical constructions. In particular, we show that this algebra is an instantiation of the Chu construction applied to a Heyting algebra, the second Dialectica construction applied to a Heyting algebra, and as an algebra for the study of recursion and corecursion. Thus the algebra provides a common base for these constructions, and suggests itself as an important part of any constructive logical treatment of duality.

Implicit programming is suggested as a new paradigm for computing with constructible duality as its formal system. We show that all the operators that have computable least fixed points are definable explicitly and all operators with computable optimal fixed points are definable implicitly within constructible duality.

Implicit programming adds a novel definitional mechanism that allows functions to be defined implicitly. This new programming feature is especially useful for programming with co-recursively defined data-types such as circular lists.

Here we provide a method which computes the optimal fixed point when it is computable. To do this we use proofs of uniqueness in an extension of intuitionistic logic together with its associated Curry-Howard-De Bruijn isomorphism. Using this correspondence, we extract programs in a confluent strongly normalizable lambda calculus that computes the optimal fixed point of a recursively defined function. When this uniqueness proof exists, the optimal fixed point is computable.

We give several examples of where this fixed point gives intuitive answers. This new semantics is especially natural for functions on co-recursively defined data-types, like streams or circular lists.

We define a symmetrization of the Beth-Fitting construction which transforms an interval Kripke model in a self-dual algebra for the logic of constructible duality and back. We then show that every point in the algebra is representable by some formula in the logic.

This algebra arises as an instantiation of a pseudo-Boolean algebra into several categorical constructions. In particular, we show that this algebra is an instantiation of the $\Chu$ construction applied to a pseudo-Boolean algebra, the second Dialectica construction applied to a pseudo-Boolean algebra, and as posetal case of a suggestion by Pitts for the study of recursion and corecursion. Thus the algebra provides a common base for these constructions, and suggests itself as a necessary part of any logical treatment of constructive duality.

Using this insight, we are able to characterize validity in a Kripke structure in terms of {\em bisimilarity}.

Theorem 1 Let $K$ be a {\em finite} Kripke structure for propositional intuitionistic logic, then two worlds in $K$ are bisimilar if and only if they satisfy the same set of formulas.

This theorem lifts to structures in the following manner.

Theorem 2 Two finite Kripke structures $K$ and $K'$ are bisimilar if and only if they have the same set of valid formulas.

We then generalize these results to a variety of infinite structures; finite principal filter structures and saturated structures.

Girard \cite{Gir87} introduces an operator !$_l$ called an exponential, to add structural rules to linear logic\footnote{We use subscript $l$ to denote operators from linear logic.}. A formula !$_l A $ can be replicated or discarded. Thus the exponential removes the ``linearity'', the notion that assumptions should only be used once, from linear logic.

We show that a Girard exponential, that is a co-monad where ! distributes through the additive conjunction, can be added as a new operator to the logic of constructible falsity $N^-$; a conservative extension of intuitionistic logic.

This shows that we can naturally divide the exponential construction of Girard into two parts, one that deals with ``linearity'' or counting the occurrences of assumptions, and a second that captures the embedding of a intuitionistic logic in a paraconsistent logic.

The exponential is also used to embed intuitionistic logic in linear logic. Girard suggests that intuitionistic implication $A \iimp B$ can be represented as ! A --o B.

We suggest that these two uses can be separated. We look at how the second transformation can be carried out in $N-$ a logic which already contains all the structural rules of intuitionistic logic.

We show how exponentials arise from adding constants to the logic of constructible falsity $N-$. These two new units complete $N-$, in the sense that there is a representation theorem for $N-$ with these additional units onto $H \times H^{op}$ where $H$ is a Heyting algebra.

If $q$ and $p$ are interderivable, then the counter models contain each other. Thus we study {\em bisimulation} as a way of studying interderivability. Using bisimulation, we are able to characterize validity in a Kripke structure.

Theorem 1: Let $K$ be a finite Kripke structure for propositional intuitionistic logic, then two worlds in $K$ are bisimilar if and only if they satisfy the same set of formulas.

This theorem lifts to structures in the following manner.

Theorem 2: Two finite Kripke structures $K$ and $K'$ are bisimilar if and only if they have the same set of valid formulas.

This correspondence exists also for finite principal filter structures and saturated structures.

We give a Kripke model having only two truth values for which we show that $N$ is sound and complete. Truth is defined on intervals $(w_t, w_f)$ in the Kripke structure such that $w_f$ is accessible from $w_t$. Truth is judged from one end $w_t$, falsity from the other $w_f$. A formula $\varphi$ holds at an interval if and only if it holds at all non-trivial subintervals. We interpret strong negation as dualizing the Kripke structure with respect to both truth and accessibility.