Symbolic Logic:Programming:Value Set Proof

From Knowino
Jump to: navigation, search

Contents

[edit] Set Membership Equivalence

x \in S \iff V(x) = v(\{ z\in S : z :: \{x = z\} \}) \!

[edit] Proof

Firstly v(\{ z\in S : z :: \{x = z\} \}) \! is a Value Set because,

W(v(\{ z\in S : z :: \{x = z\} \})) = \{z\in S : \{x = z\}\} \!
(\bigcup_{z\in S} : \{x = z\}) = \{x \in S\}= \{true\} \!
\forall z \in {V(x)}_t : z_p \subset \{ x = z_v \} \!

is,

\forall z \in \{ z\in S : z :: \{x = z\} \} : z_p \subset \{ x = z_v \} \!

simplifies to,

\forall z \in S : \{x = z\} \subset \{ x = z \} \!

which is true,

Secondly using A2,

S(v(\{ z\in S : z :: \{x = z\} \})) = S \!

so every Value Set Y with S(Y) = Y must equal v(\{ z\in S : z :: \{x = z\} \})\!

[edit] Functions of a Value Set

The following theorem gives the function on a value set of a type using the function of the type.

(B1) f(X) = v(\{y\in X_t: f(y_v)::y_p\})\!

[edit] Proof

Let,

K = v(\{y\in X_t: f(y_v)::y_p\}) \} \!

firstly we need to prove that K satisfies the axioms of a Value Set, if X is a value set,

[edit] Step 1

To prove that axiom A3 holds,

W(K) = W(v(\{y\in X_t: f(y_v)::y_p\})) = \{y\in X_t: y_p\} = W(X) \!

so,

 \bigcup_{w \in W(K)} : w = \bigcup_{w \in W(X)} : w = \alpha \!

[edit] Step 2

From (A4) applied to X,

\forall z \in X : z_p \subset \{ x = z_v \} \!

which implies,

\forall z \in X : z_p \subset \{ f(x) = f(z_v) \} \!

Which is (A4) applied to K.

[edit] Step 3

As K\! obeys the definition of a Value Set now prove that it equals f(X)\!. Let X = V(x)\!.

From A6,

V(f(x)) = f(V(x)) \!

From A1,

x \in S(V(x))\!

which implies,

f(x) \in \{y \in S(V(x)):f(y)\} \!

so,

S(V(f(x)) = \{y \in S(V(x)):f(y)\} \!

but also by simplifying,

S(K) = S(v(\{y\in X_t: f(y_v)::y_p\})) = \{y \in S(X): f(y)\} \!

so from A2,

S(V(f(x)) = S(K) \implies V(f(x)) = K \!

gives,

V(f(x)) = f(V(x)) = f(X) = K \!

[edit] Function of Multiple Parameters

If F is a value set of functions on a value set of a values,

(B2) F(X) = v(\{f\in F_t, x\in X_t: f_v(x_v)::f_p\cap x_p\}) \!

Let,

K = v(\{f\in F_t, x\in X_t: f_v(x_v)::f_p\cap x_p\}) \} \!

firstly we need to prove that K satisfies the axioms of a Value Set, if X is a value set,

[edit] Step 1

To prove that axiom A3 holds,

W(K) = W(v(\{f\in F_t, x\in X_t: f_v(x_v)::f_p\cap x_p\})) = \{f\in F_t, x\in X_t: f_p\cap x_p\} \!

so,

 (\bigcup_{w \in W(K)} : w) = (\bigcup_{f\in F_t, x\in X_t}: f_p\cap x_p) \!

gives,

 \bigcup_{w \in W(K)} : w = (\bigcup_{f\in F_t}: f_p)\cap(\bigcup_{x\in X_t}: f_p\cap x_p) = \alpha \cap \alpha = \alpha \!

which is A3 applied to K.

[edit] Step 2

From (A4) applied to F and X,

\forall y \in F_t : y_p \subset \{ f = y_v \} \!
\forall z \in X_t : z_p \subset \{ x = z_v \} \!

combining them,

\forall y \in F_t, x \in X_t : y_p \subset \{ f = y_v \} \and x_p \subset \{ x = z_v \} \!

gives,

\forall y \in F_t, z \in X_t : y_p \cap x_p \subset \{ f = y_v \and x = z_v \} \!

as,

f = y_v \and x = z_v \implies f(x) = y_v(z_v) \!
\{f = y_v \and x = z_v\} \subset \{f(x) = y_v(z_v)\} \!

then

\forall y \in F_t, z \in X_t : y_p \cap x_p \subset \{ f(x) = y_v(z_v) \} \!

which is A4 applied to K.

[edit] Step 3

As K\! satisfies the definition of a Value Set now prove that it equals F(X)\!. Let F = V(f)\! and X = V(x)\!. Then F(X) = V(f)(V(x))\!.

From A6,

V(f(x)) = V(f)(V(x)) \!

From A1,

f \in S(V(f))\!
x \in S(V(x))\!

which implies,

f(x) \in \{y \in S(V(f))\and z \in S(V(x)):y(z)\} \!

so,

S(V(f(x)) = \{y \in S(V(f))\and z \in S(V(x)):y(z)\} \!

but also,

S(K) = S(v(\{f\in F_t, x\in X_t: f_v(x_v)::f_p\cap x_p\})) = \{y \in S(F)\and z \in S(X):y(z) \!

so from A2,

S(V(f(x)) = S(K) \implies V(f(x)) = K \!

so,

V(f(x))= V(f)(V(x)) = F(X) = K \!

[edit] Function of Vector of Parameters

If x is a vector, and X is a vector of Value Sets (representing multiple parameters) then,

(B4) F(X) = v(\{ f(x_v)::\bigcap_{j \in J} x_p[j] : x\in X \}) \!

[edit] Proof

Use induction. Firstly B1 gives the case for a scalar (n = 1).

Assume that B4 holds for a vector of size n then prove it holds for a vector of size n+1. Start with,

(B3) g(X, Y) = v(\{ g(x_v, y_v)::x_p\cap y_p : x\in X \and y\in Y \})\!

Let X\! be a scalar and Y = Y(n)\! is a vector of size n. Also let x\in X \and y(n) \in Y(n)\!.

Let,

y(n+1)_v = [x_v|y(n)_v] \!
y(n+1)_p = [x_p|y(n)_p] \!

then,

\bigcap_{j \in [1..n+1]} y(n+1)_p[j] = x_p \cap \bigcap_{j \in [1..n]} y(n)_p[j] \!

and,

y(n+1) \in Y(n+1) = x\in X \and y(n)\in Y(n) \!

Also let,

g(X, Y(n)) = h([X|Y(n)] = h(Y(n+1)) \!
g(x_v, y(n)_v) = h([x_v|y(n)_v]) = h(y(n+1)_v]) \!

in,

(B3) g(X, Y(n)) = v(\{ g(x_v, y(n)_v)::x_p\cap y(n)_p : x\in X \and y(n)\in Y(n) \})\!

becomes,

h(Y(n+1)) = v(\{ h(y(n+1)_v)::y(n+1)_p : y(n+1) \in Y(n+1) \})\!

Which is B4 for n+1, so by induction B4 holds for any number of parameters >= 1.

[edit] Assertions on Value Sets

(C1) x_V \implies \forall z \in V(x)_t: z_v \or (z_p = \empty) \!

[edit] Proof

From A5

V(x) \iff x \!

And, x \in \{ true \}  \! .

Using,

(A1) x \in \{ z \in {V(x)}_t \and z_p \ne \empty : z_v \} \!

gives,

\{ z \in V(x)_t \and z_p \ne \empty : z_v \} = \{ true \} \!

and,

\forall z \in V(x)_t \and z_p \ne \empty : z_v = true \!

or,

\forall z \in V(x)_t: z_v \or z_p = \empty \!

[edit] Pruning Empty Worlds

(C2) X = v(\{x \in X \and x_p \neq \empty : x \}) \!
S(X) = \{ z \in X_t \and z_p \ne \empty : z_v \} \!

also,

S(v(\{x \in X \and x_p \neq \empty : x \})) = \{ z \in \{x \in X \and x_p \neq \empty : x \} \and z_p \ne \empty : z_v \} \!

which simplifies to,

S(v(\{x \in X \and x_p \neq \empty : x \})) = \{ z \in X_t \and z_p \ne \empty : z_v \} \!

so using A2,

S(X) = S(v(\{x \in X \and x_p \neq \empty : x \})) \implies X = v(\{x \in X \and x_p \neq \empty : x \}) \!

[edit] Resolution

The standard form for Possible Worlds is defined as,

X = f(Y, Z) \!
\forall x_p \in X, y_p \in Y: x_p \subset y_p or x_p \cap y_p = \empty \!

Then the resolution rule is,

If X \!, Y \! and Z \! are a Value Sets, where

X = f(Y, Z) \!

then,

(y_p \in S(Y) \and (\forall x_p \in S(X): x_p \not \subset y_p )) \implies y_p = \empty \!

[edit] Proof

x_p \subset y_p \or x_p \cap y_p = \empty

therefore,

\forall x_p \in S(X): x_p \not \subset y_p )) \implies \!
\forall x_p \in S(X): x_p \cap y_p = \empty )) \implies \!
\bigcup_{x_p \in S(X)} x_p \cap y_p = \empty \!

but,

\bigcup_{x_p \in S(X)} x_p \cap y_p = (\bigcup_{x_p \in S(X)} x_p) \cap y_p = \alpha \cap y_p = y_p\!

so,

y_p = \empty \!

[edit] Links

Personal tools
Variants
Actions
Navigation
Community
Toolbox