existence of QSSs via term structure construction

Construction

We work in ${\mathcal{L}}_0$. For any nice term sequence $\bar{F}$, define the mapping \alpha_\trmseq{F} recursively as follows.

1. ${\alpha }_{\bar{F}}(C):=C$ for each constant $C\in {\Sigma }^{\sigma }$ other than ${\mathsf{E}!}_{\sigma }$;

2. ${\alpha }_{\bar{F}}({\mathsf{E}!}_{\sigma }):=F_{\sigma }$ if $F_{\sigma }$ is defined, ${\alpha }_{\bar{F}}({\mathsf{E}!}_{\sigma }):={\mathsf{E}!}_{\sigma }$ otherwise;[]{#tr-ex label=“tr-ex”}

3. ${\alpha }_{\bar{F}}(x):=x$ for each variable $x\in {Var}^{\sigma }$;

4. ${\alpha }_{\bar{F}}(MN):={\alpha }_{\bar{F}}(M){\alpha }_{\bar{F}}(N)$ whenever $M:\sigma \to \tau$ and $N:\sigma$;

5. ${\alpha }_{\bar{F}}(\lambda x.M):=\lambda x.{\alpha }_{\bar{F}}(M)$;

6. ${\alpha }_{\bar{F}}(QxP):=Qx{\alpha }_{\bar{F}}^t(P)$ whenever $x\in {Var}^{\sigma }$ and $Q\in \{\forall ,\exists \}$.

It is well known that ${\mathcal{L}}_0$ carries an applicative structure ${\mathcal{L}}_0:=({\mathcal{L}}_0,App)$, where ${App}^{\sigma \tau }(M,N):=MN$. Thus a domain over ${\mathcal{L}}_0$ is essentially a nice term sequence. More exactly, for each nice term sequence $\bar{F}$ there is a domain that assigns $F_{\sigma }$ to $\sigma$ whenever $F_{\sigma }$ is defined and is undefined otherwise. In view of this correspondence, I notate and speak of domains over ${\mathcal{L}}_0$ as if they were nice term sequences. Of course, nice term sequences that are mutual permutations of one another correspond to the same domain.

We define a typed family of equivalence relations ${\sim }_{\sigma }\subseteq {\mathcal{L}}_0^{\sigma }\times {\mathcal{L}}_0^{\sigma }$ on ${\mathcal{L}}_0$ by setting $M{\sim }_{\sigma }N⟺{\mathtt{H}}_0⊢{\alpha }_{\bar{F}}^{\sigma }(M)\bar{v}\leftrightarrow {\alpha }_{\bar{F}}^{\sigma }(N)\bar{v}\text{ for every nice term sequence Fˉ}.$ Intuitively, then, $M\sim N$ means that $M$ and $N$ are provably equivalent in H, and remain so under arbitrary translations. It is easy to see that $\sim$ is an applicative congruence of our term applicative structure $({\mathcal{L}}_0,App)$. We then let $\mathbf{A}:=(A,App)$ be the quotient of ${\mathcal{L}}_0$ through $\sim$.

To obtain a substitution structure, we can lift the mappings ${\alpha }_{\bar{F}}^{\sigma }$ to equivalence classes of terms. Write $[M]$ for the equivalence class of $M$ under $\sim$. A domain over $\mathbf{A}$ is then the result of lifting a domain over ${\mathcal{L}}_0$ to equivalence classes under $\sim$. This justifies notating domains in $\mathbf{A}$ as $[\bar{F}]:=([F_{\sigma }]{)}_{\sigma \in \bar{\sigma }}$, once more slightly abusing notation.

To each such domain $[\bar{F}]$ we assign a substitution $i_{[\bar{F}]}$ by setting $i_{[\bar{F}]}[M]:=[{\alpha }_{\bar{F}}(M)].$ It is not difficult to verify that $i_{[\bar{F}]}$ and $i_{[\bar{G}]}$ are identical whenever $[\bar{F}]=[\bar{G}]$.

It is then straightforward to check that $\mathfrak{A}:=(\mathbf{A},\mathbf{I},Sub,i_{(\cdot )})$ is a QSS, where $\mathbf{I}:=(I,\circ )$ with $\circ$ function composition, and $Sub$ is function application.

Limitations

This construction cannot be continued to build a model for a language with domain specifiers, since it is not rich enough to interpret syncategorematic quantification.