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 X + {\displaystyle X_{+}} 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 d : F → G {\displaystyle d:F\to G} in G that maps with each function f of arity n in F the following function d ( f ) : B n → B {\displaystyle d(f):B^{n}\to B} in G (G cannot be a bijection). From this lemma we can now build the concept of unique homomorphic extension.
The theorem If X + {\displaystyle X_{+}} is a free set generated by X and F, for each function h : X → B {\displaystyle h:X\to B} there is a single function h ^ : X + → B {\displaystyle {\hat {h}}:X_{+}\to B} such that:
∀ x ∈ X , h ^ ( x ) = h ( x ) ; ( 1 ) {\displaystyle \forall x\in X,{\hat {h}}(x)=h(x);\qquad (1)}
For each function f of arity n > 0, for each x 1 , … , x n ∈ X + n , {\displaystyle x_{1},\ldots ,x_{n}\in X_{+}^{n},}
h ^ ( f ( x 1 , … , x n ) ) = g ( h ^ ( x 1 ) , … , h ^ ( x n ) ) , where g = d ( f ) ( 2 ) {\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)}
Consequence The identities seen in (1) e (2) show that h ^ {\displaystyle {\hat {h}}} is an homomorphism, specifically named the unique homomorphic extension of h {\displaystyle h} . To prove the theorem, two requirements must be met: to prove that the extension ( h ^ {\displaystyle {\hat {h}}} ) exists and is unique (assuring the lack of bijections).
Proof of the theorem We must define a sequence of functions h i : X i → B {\displaystyle h_{i}:X_{i}\to B} inductively, satisfying conditions (1) and (2) restricted to X i {\displaystyle X_{i}} . For this, we define h 0 = h {\displaystyle h_{0}=h} , and given h i {\displaystyle h_{i}} then h i + 1 {\displaystyle h_{i+1}} shall have the following graph:
{ ( f ( x 1 , … , x n ) , g ( h i ( x 1 ) , … , h i ( x n ) ) ) ∣ ( x 1 , … , x n ) ∈ X i n − X i − 1 n , f ∈ F } ∪ graph ( h i ) with g = d ( f ) {\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_{i}^{n}-X_{i-1}^{n},f\in F\}}\cup {\operatorname {graph} (h_{i})}{\text{ with }}g=d(f)}
First we must be certain the graph actually has functionality, since X + {\displaystyle X_{+}} is a free set, from the lemma we have f ( x 1 , … , x n ) ∈ X i + 1 − X i {\displaystyle f(x_{1},\ldots ,x_{n})\in X_{i+1}-X_{i}} when ( x 1 , … , x n ) ∈ X i n − X i − 1 n , ( i ≥ 0 ) {\displaystyle (x_{1},\ldots ,x_{n})\in X_{i}^{n}-X_{i-1}^{n},(i\geq 0)} , 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 ( x , y ) ∈ g r a p h ( h i ) {\displaystyle (x,y)\in graph(h_{i})} and ( x , z ) ∈ g r a p h ( h i ) {\displaystyle (x,z)\in graph(h_{i})} for some x ∈ X i + 1 − X i {\displaystyle x\in X_{i+1}-X_{i}} is possible is if we have x = f ( x 1 , … , x m ) = f ′ ( y 1 , … , y n ) {\displaystyle x=f(x_{1},\ldots ,x_{m})=f'(y_{1},\ldots ,y_{n})} for some ( x 1 , … , x m ) ∈ X i m − X i − 1 m , ( y 1 , … , y n ) ∈ X i n − X i − 1 n {\displaystyle (x_{1},\ldots ,x_{m})\in X_{i}^{m}-X_{i-1}^{m},(y_{1},\ldots ,y_{n})\in X_{i}^{n}-X_{i-1}^{n}} and for some generators f {\displaystyle f} and f ′ {\displaystyle {f'}} in F {\displaystyle F} . Since f ( X + m ) {\displaystyle f(X_{+}^{m})} and f ′ ( X + n ) {\displaystyle {f'}(X_{+}^{n})} are disjoint when f ≠ f ′ , f ( x 1 , … , x m ) = f ′ ( y 1 , … , Y n ) {\displaystyle f\neq {f'},f(x_{1},\ldots ,x_{m})=f'(y_{1},\ldots ,Y_{n})} this implies f = f ′ {\displaystyle f=f'} and m = n {\displaystyle m=n} . Being all f ∈ F {\displaystyle f\in F} in X + n {\displaystyle X_{+}^{n}} , we must have x j = y j , ∀ j , 1 ≤ j ≤ n {\displaystyle x_{j}=y_{j},\forall j,1\leq j\leq n} . Then we have y = z = g ( x 1 , … , x n ) {\displaystyle y=z=g(x_{1},\ldots ,x_{n})} with g = d ( f ) {\displaystyle g=d(f)} , 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 ( f n ) n ≥ 0 {\displaystyle (f_{n})_{n\geq 0}} a sequence of partial functions f n : A → B {\displaystyle f_{n}:A\to B} such that f n ⊆ f n + 1 , ∀ n ≥ 0 {\displaystyle f_{n}\subseteq f_{n+1},\forall n\geq 0} . Then, g = ( A , ⋃ g r a p h ( f n ) , B ) {\displaystyle g=(A,\bigcup graph(f_{n}),B)} is a partial function. [1] Archived 2017-07-12 at the Wayback Machine
Using (3), h ^ = ⋃ i ≥ 0 h i {\displaystyle {\hat {h}}=\bigcup _{i\geq 0}h_{i}} is a partial function. Since d o m ( h ^ ) = ⋃ d o m ( h i ) = ⋃ X i = X + {\displaystyle dom({\hat {h}})=\bigcup dom(h_{i})=\bigcup X_{i}=X_{+}} then h ^ {\displaystyle {\hat {h}}} is total in X + {\displaystyle X_{+}} . Furthermore, it is clear from the definition of h i {\displaystyle h_{i}} that h ^ {\displaystyle {\hat {h}}} satisfies (1) and (2). To prove the uniqueness of h ^ {\displaystyle {\hat {h}}} , or any other function h ′ {\displaystyle {h'}} that satisfies (1) and (2), it is enough to use a simple induction that shows h ^ {\displaystyle {\hat {h}}} and h ′ {\displaystyle {h'}} work for X i , ∀ i ≥ 0 {\displaystyle X_{i},\forall i\geq 0} , and such is proved the Theorem of the Unique Homomorphic Extension.[2] Archived 2017-07-12 at the Wayback Machine
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:
A = Σ ∗ {\displaystyle A=\Sigma ^{*}} where Σ = V a r i a b l e s ∪ { 0 , 1 , 2 , … , 9 } ∪ { + , − , ∗ } ∪ { ( , ) } , where | ∗ = V a r i a b l e s ∪ { 0 , … , 9 } {\displaystyle \Sigma =\mathrm {Variables} \cup \{0,1,2,\ldots ,9\}\cup \{+,-,*\}\cup \{(,)\},{\text{ where }}|*=\mathrm {Variables} \cup \{{0,\ldots ,9}\}}
Be F = { f − , f + , f ∗ } {\displaystyle F=\{{f-,f+,f*}\}}
f : Σ ∗ → Σ w ↦ − w ∗ {\displaystyle f:\Sigma ^{*}\to \Sigma _{w\mapsto {-w}}^{*}}
f : Σ ∗ x Σ ∗ → Σ w 1 , w 2 ↦ w 1 + w 2 ∗ {\displaystyle f:\Sigma ^{*}x\Sigma ^{*}\to \Sigma _{w_{1},w_{2}\mapsto {w_{1}+w_{2}}}^{*}}
f : Σ ∗ x Σ ∗ → Σ w 1 , w 2 ↦ w 1 ∗ w 2 ∗ {\displaystyle f:\Sigma ^{*}x\Sigma ^{*}\to \Sigma _{w_{1},w_{2}\mapsto {w_{1}*w_{2}}}^{*}}
Be E X P R {\displaystyle EXPR} he inductive closure of X {\displaystyle X} under F {\displaystyle F} and be B = Z , G = { S o m a ( − . − ) , M u l t ( − , − ) , M e n o s ( − ) } {\displaystyle B=\mathbb {Z} ,G={\{Soma(-.-),Mult(-,-),Menos(-)}\}}
Be d : F → G {\displaystyle d:F\to G}
d ( f − ) = m e n o s {\displaystyle d({f-})=menos}
d ( f + ) = m a i s {\displaystyle d({f+})=mais}
d ( f ∗ ) = m u l t {\displaystyle d({f*})=mult}
Then h ^ : X + → { 0 , 1 } {\displaystyle {\hat {h}}:X_{+}\to \{{0,1}\}} will be a function that calculates recursively the truth-value of a proposition, and in a way, will be an extension of the function h : X → { 0 , 1 } {\displaystyle h:X\to \{{0,1}\}} that associates a truth-value to each atomic proposition, such that: (1) h ^ ( ϕ ) = h ( ϕ ) {\displaystyle {\hat {h}}(\phi )=h(\phi )}
(2) h ^ ( ( ¬ ϕ ) ) = N A O ( h ^ ( ψ ) ) {\displaystyle {\hat {h}}({(\neg \phi )})=NAO({\hat {h}}(\psi ))} (Negation)
h ^ ( ( ρ ∧ θ ) ) = E ( h ^ ( ρ ) , h ^ ( θ ) ) {\displaystyle {\hat {h}}({(\rho \land \theta )})=E({\hat {h}}(\rho ),{\hat {h}}(\theta ))} (AND Operator)
h ^ ( ( ρ ∨ θ ) ) = O U ( h ^ ( ρ ) , h ^ ( θ ) ) {\displaystyle {\hat {h}}({(\rho \lor \theta )})=OU({\hat {h}}(\rho ),{\hat {h}}(\theta ))} (OR Operator)
h ^ ( ( ρ → θ ) ) = S E E N T A O ( h ^ ( ρ ) , h ^ ( θ ) ) {\displaystyle {\hat {h}}({(\rho \to \theta )})=SE\,ENTAO({\hat {h}}(\rho ),{\hat {h}}(\theta ))} (IF-THEN Operator)
References
Gallier, Jean (2003), Logic For Computer Science: Foundations of Automatic Theorem Proving (PDF), Philadelphia, archived from the original (PDF) on 2017-07-12, retrieved 2017-10-25{{citation}}: CS1 maint: location missing publisher (link)