Structural recursion and definition of set of sub-formulas

64 Views Asked by At

Let $P\ne\emptyset$ and let $\mathcal{F}$ be the set of propositional formulas constructed from $P$: i.e. the smallest set containing $P$ and closed under $\neg, \Rightarrow,\lor,\land,\Leftrightarrow$.

We have the following result:

Let $\phi_0$ be a mapping from $P$ into a set $E$. Suppose $f\in E^E$ and $g,h,i,j\in E^{E\times E}$. Then there exists a unique mapping $\phi:\mathcal{F}\rightarrow E$ such that the following hold:

  • $\phi|_P=\phi_0$;
  • for $F\in\mathcal{F}$, $\phi(\neg F)=f(\phi(F))$;
  • for all $F,G\in\mathcal{F}$, $\phi(F\land G)=g(\phi(F),\phi(G))$;
  • for all $F,G\in\mathcal{F}$, $\phi(F\lor G)=h(\phi(F),\phi(G))$;
  • for all $F,G\in\mathcal{F}$, $\phi(F\Rightarrow G)=i(\phi(F),\phi(G))$;
  • for all $F,G\in\mathcal{F}$, $\phi(F\Leftrightarrow G)=j(\phi(F),\phi(G))$.

For $A\in P$, define $\phi_0(A):=\{A\}$. Then $\phi_0$ is a mapping from $P$ to $\mathfrak{P}(\mathcal{F})$. I want to use the above result to extend this map to all of $\mathcal{F}$ so that the following hold:

  • for $F\in\mathcal{F}$, $\phi(\neg F)=\phi(F)\cup\{\neg F\}$;
  • for $F,G\in\mathcal{F}$ and $\xi\in\{\Rightarrow,\lor,\land,\Leftrightarrow\}$, $\phi(F\xi G)=\phi(F)\cup\phi(G)\cup\{F\xi G\}$.

What should $f$ be in this case? Obviously it has to be a mapping from $\mathfrak{P}(\mathcal{F})$ into itself so that $$\phi(F)\cup\{\neg F\}=\phi(\neg F)=f(\phi(F))$$ for every $F\in\mathcal{F}$. I thought about $f:=H\mapsto H\cup\{H\}$ but this doesn't work since $f(\phi(F))=\phi(F)\cup\{\phi(F)\}$...

Any suggestions?