Unique homomorphic extension theorem

The unique homomorphic extension theorem is a result in mathematical logic which formalizes the intuition that the truth or falsity of a statement can be deduced from the truth values of its parts.

The lemma

Let A be a non-empty set, X a subset of A, F a set of functions in A, and [math]\displaystyle{ X_+ }[/math] the inductive closure of X under F.

Let be B any non-empty set and let G be the set of functions on B, such that there is a function [math]\displaystyle{ d:F\to G }[/math] in G that maps with each function f of arity n in F the following function [math]\displaystyle{ d(f):B^n\to B }[/math] in G (G cannot be a bijection).

From this lemma we can now build the concept of unique homomorphic extension.

The theorem

If [math]\displaystyle{ X_+ }[/math] is a free set generated by X and F, for each function [math]\displaystyle{ h:X\to B }[/math] there is a single function [math]\displaystyle{ \hat h:X_+\to B }[/math] such that:

[math]\displaystyle{ \forall x\in X, \hat h(x)= h(x); \qquad (1) }[/math]

For each function f of arity n > 0, for each [math]\displaystyle{ x_1,\ldots,x_n\in X^n_+, }[/math]

[math]\displaystyle{ \hat h(f(x_1, \ldots, x_n)) = g(\hat h(x_1),\ldots,\hat h(x_n)), \text{ where } g=d(f) \qquad (2) }[/math]

Consequence

The identities seen in (1) e (2) show that [math]\displaystyle{ \hat h }[/math] is an homomorphism, specifically named the unique homomorphic extension of [math]\displaystyle{ h }[/math]. To prove the theorem, two requirements must be met: to prove that the extension ([math]\displaystyle{ \hat h }[/math]) exists and is unique (assuring the lack of bijections).

Proof of the theorem

We must define a sequence of functions [math]\displaystyle{ h_i:X_i\to B }[/math] inductively, satisfying conditions (1) and (2) restricted to [math]\displaystyle{ X_i }[/math]. For this, we define [math]\displaystyle{ h_0=h }[/math], and given [math]\displaystyle{ h_i }[/math] then [math]\displaystyle{ h_{i+1} }[/math]shall have the following graph:

[math]\displaystyle{ {\{(f(x_1,\ldots,x_n),g(h_i(x_1),\ldots,h_i(x_n))) \mid (x_1,\ldots,x_n)\in X^n_i - X^n_{i-1},f\in F\}} \cup {\operatorname{graph}(h_i)} \text{ with } g=d(f) }[/math]

First we must be certain the graph actually has functionality, since [math]\displaystyle{ X_+ }[/math] is a free set, from the lemma we have  [math]\displaystyle{ f(x_1,\ldots,x_n)\in X_{i+1} - X_i }[/math] when [math]\displaystyle{ (x_1,\ldots,x_n)\in X^n_i - X^n_{i-1},(i\geq 0) }[/math], so we only have to determine the functionality for the left side of the union. Knowing that the elements of G are functions(again, as defined by the lemma), the only instance where [math]\displaystyle{ (x,y)\in graph(h_i) }[/math] and [math]\displaystyle{ (x,z)\in graph(h_i) }[/math] for some [math]\displaystyle{ x\in X_{i+1} - X_i }[/math] is possible is if we have  [math]\displaystyle{ x=f(x_1,\ldots,x_m)=f'(y_1,\ldots,y_n) }[/math]  for some [math]\displaystyle{ (x_1,\ldots,x_m)\in X^m_i - X^m_{i-1},(y_1,\ldots,y_n)\in X^n_i - X^n_{i-1} }[/math] and for some generators [math]\displaystyle{ f }[/math] and [math]\displaystyle{ {f'} }[/math] in [math]\displaystyle{ F }[/math].

Since [math]\displaystyle{ f(X^m_+) }[/math] and [math]\displaystyle{ {f'}(X^n_+) }[/math]  are disjoint when [math]\displaystyle{ f\neq {f'},f(x_1,\ldots,x_m) = f'(y_1,\ldots,Y_n) }[/math] this implies [math]\displaystyle{ f=f' }[/math] and [math]\displaystyle{ m=n }[/math]. Being all [math]\displaystyle{ f\in F }[/math] in [math]\displaystyle{ X^n_+ }[/math], we must have [math]\displaystyle{ x_j=y_j,\forall j,1\leq j\leq n }[/math].

Then we have [math]\displaystyle{ y=z=g(x_1,\ldots,x_n) }[/math] with [math]\displaystyle{ g=d(f) }[/math], displaying functionality.

Before moving further we must make use of a new lemma that determines the rules for partial functions, it may be written as:

 (3)Be [math]\displaystyle{ (f_n)_{n\geq 0} }[/math] a sequence of partial functions [math]\displaystyle{ f_n:A\to B }[/math] such that [math]\displaystyle{ f_n\subseteq f_{n+1},\forall n\geq 0 }[/math]. Then, [math]\displaystyle{ g=(A,\bigcup graph(f_n),B) }[/math] is a partial function. [1]

Using (3), [math]\displaystyle{ \hat h =\bigcup_{i\geq 0} h_i }[/math] is a partial function. Since  [math]\displaystyle{ dom(\hat h)=\bigcup dom(h_i)=\bigcup X_i=X_+ }[/math] then [math]\displaystyle{ \hat h }[/math] is total in [math]\displaystyle{ X_+ }[/math].

Furthermore, it is clear from the definition of [math]\displaystyle{ h_i }[/math] that [math]\displaystyle{ \hat h }[/math] satisfies (1) and (2). To prove the uniqueness of [math]\displaystyle{ \hat h }[/math], or any other function [math]\displaystyle{ {h'} }[/math] that satisfies (1) and (2), it is enough to use a simple induction that shows [math]\displaystyle{ \hat h }[/math] and [math]\displaystyle{ {h'} }[/math] work for [math]\displaystyle{ X_i,\forall i\geq 0 }[/math], and such is proved the Theorem of the Unique Homomorphic Extension.[2]

Example of a particular case

We can use the theorem of unique homomorphic extension for calculating numeric expressions over whole numbers. First, we must define the following:

[math]\displaystyle{ A=\Sigma^* }[/math] where [math]\displaystyle{ \Sigma= \mathrm{Variables} \cup \{0,1,2,\ldots,9\} \cup \{+,-,*\} \cup \{(,)\}, \text{ where }| *=\mathrm{Variables} \cup \{{0,\ldots,9}\} }[/math]

Be [math]\displaystyle{ F =\{{f-,f+,f*}\} }[/math]

[math]\displaystyle{ f:\Sigma^*\to \Sigma^*_{w\mapsto {-w}} }[/math]

[math]\displaystyle{ f:\Sigma^*x\Sigma^*\to \Sigma^*_{w_1,w_2\mapsto {w_1+w_2}} }[/math]

[math]\displaystyle{ f:\Sigma^*x\Sigma^*\to \Sigma^*_{w_1,w_2\mapsto {w_1*w_2}} }[/math]

Be [math]\displaystyle{ EXPR }[/math] he inductive closure of [math]\displaystyle{ X }[/math] under [math]\displaystyle{ F }[/math] and be[math]\displaystyle{ B=\Z, G={\{Soma(-.-),Mult(-,-),Menos(-)}\} }[/math]

Be [math]\displaystyle{ d:F\to G }[/math]

[math]\displaystyle{ d({f-})=menos }[/math]

[math]\displaystyle{ d({f+})=mais }[/math]

[math]\displaystyle{ d({f*})=mult }[/math]

Then [math]\displaystyle{ \hat h:X_+\to\{{0,1}\} }[/math] will be a function that calculates recursively the truth-value of a proposition, and in a way, will be an extension of the function [math]\displaystyle{ h:X\to\{{0,1}\} }[/math]that associates a truth-value to each atomic proposition, such that:

(1)[math]\displaystyle{ \hat h (\phi) = h(\phi) }[/math]

(2)[math]\displaystyle{ \hat h({(\neg\phi)})=NAO(\hat h(\psi)) }[/math] (Negation)

[math]\displaystyle{ \hat h({(\rho\land \theta)})= E(\hat h(\rho),\hat h(\theta)) }[/math] (AND Operator)

[math]\displaystyle{ \hat h({(\rho\lor \theta)})= OU(\hat h(\rho),\hat h(\theta)) }[/math] (OR Operator)

[math]\displaystyle{ \hat h({(\rho\to \theta)})= SE\,ENTAO(\hat h(\rho),\hat h(\theta)) }[/math] (IF-THEN Operator)

References

• Gallier, Jean (2003), Logic For Computer Science: Foundations of Automatic Theorem Proving, Philadelphia, http://phil.gu.se/logic/books/Gallier:Logic_For_Computer_Science.pdf, retrieved 2017-10-25