$ \def\imp{\Rightarrow} \def\celse{\ |\ } \def\prov{\vdash} \def\dns{{\downarrow}} \def\preq{\dashv\vdash} \def\sh{\#} $

Source Language

The source language is the small focused first-order logic FF described in Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic. Its syntax goes like this:

Negative $N$	$::=$	$P \imp N \celse N \land N \celse \top \celse \forall x . N(x) \celse a^-(t)$
Positive $P$	$::=$	$\dns N \celse a^+(t)$
Terms $t$	$::=$	$x \celse \cdots$

It has negative connectives, and both polarities of atoms. First-order terms can be built from variables and whatever term constructors you like.

Target Language

The target language is just ordinary unpolarized first-order intuitionistic logic, with one nonstandard connective, a U-quantifier:

Propositions $A,B,C$

$::=$

$A \imp A \celse A \land A \celse A \lor A \celse \top \celse \bot \celse \forall x . A(x) \celse \exists x . A(x)\celse Ux.A(x)\celse a(t)$

The rules for $U$ feature a distinguished atomic proposition $\sh$ that takes one term argument. $${ \Gamma, A(x) \prov \sh(x) \over \Gamma \prov Ux.A(x) }{\small(x\not\in\Gamma)}\qquad { \Gamma\prov A(t) \over \Gamma, Ux.A(x) \prov \sh(t) }$$ Naturally, it is easy to show that $Ux.A(x) \preq \forall x . A(x) \imp \sh(x)$, but the presentation of $U$ as a 'jumbo' connective is important for the isomorphism proof.

Abbrevs and Translation

We mutually recursively make the abbreviation $$N^\ast = Ux.N^x$$ and define $P^\ast$, $P^\circ$, $N^t$, $N^\circ$ by

$N$	$N^ t$	$N^\circ$
$P \imp N$	$P^\ast \land N^t$	$P^\circ \imp N^\circ$
$N_1 \land N_2$	$N_1^t \lor N_2^t$	$N_1^\circ \land N_2^\circ$
$\top$	$\bot$	$\top$
$\forall x . N(x)$	$\exists x . N^t(x)$	$\forall x . N^\circ(x)$
$a^-$	$a^-(t)$	$(a^-)^\ast$

$P$	$P^\ast$	$P^\circ$
$\dns N$	$N^\circ$	$N^\ast$
$a^+$	$a^+$	$a^+$

We're abusing notation a little by acting like that the $a^-$ and $a^+$ in the source language don't have arguments. What's really going on in the translation of $a^-$ is we're adding one more argument to the list, and with $a^+$ preserving the set of arguments.

Translation of sequents

$N_1\ldots, N_n\prov a^-$	$N_1^\ast, \ldots, N_n^\ast, a^-(x) \prov \sh(x)$
$N_1\ldots, N_n[N]\prov a^-$	$N^\ast_1, \ldots, N^\ast_n, a^-(x) \prov N^x$
$N_1\ldots, N_n\prov N$	$N^\ast_1, \ldots, N^\ast_n\prov N^\circ$
$N_1\ldots, N_n\prov [P]$	$N^\ast_1, \ldots, N^\ast_n\prov P^\ast$

Theorems

Proving these establishes cut and identity for FF, and are super easy to prove by induction:

$P^\ast \preq P^\circ$

$N^\ast \preq N^\circ$