Symbolic Logic:Programming:Value Set Proof

From Knowino

Pending changes are displayed on this page

Unchecked

Jump to: navigation, search

[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,

A1 is true

A3

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

$(\bigcup_{z\in S} : \{x = z\}) = \{x \in S\}= \{true\} \!$

A4

$\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

Symbolic Logic:Programming:Value Set Proof

Contents

[edit] Set Membership Equivalence

[edit] Proof

[edit] Functions of a Value Set

[edit] Proof

[edit] Step 1

[edit] Step 2

[edit] Step 3

[edit] Function of Multiple Parameters

[edit] Step 1

[edit] Step 2

[edit] Step 3

[edit] Function of Vector of Parameters

[edit] Proof

[edit] Assertions on Value Sets

[edit] Proof

[edit] Pruning Empty Worlds

[edit] Resolution

[edit] Proof

[edit] Links

Personal tools

Namespaces

Variants

Views

Actions

Search

Navigation

Community

Toolbox