Directory talk:Jon Awbrey/Papers/Syntactic Transformations

Alternate Version : Needs To Be Reconciled

1.3.12. Syntactic Transformations ✔

1.3.12.1. Syntactic Transformation Rules

Value Rules

Value Rule 1

If	v, w	C	B

then	"v = w" is a sentence about <v, w> C B2,

	[v = w] is a proposition : B2 -> B,

and the following are identical values in B:

V1a.	[ v = w ](v, w)

V1b.	[ v <=> w ](v, w)

V1c.	((v , w))

Value Rule 1

If	v, w	C	B,

then the following are equivalent:

V1a.	v = w.

V1b.	v <=> w.

V1c.	(( v , w )).

A rule that allows one to turn equivalent sentences into identical propositions:

(S <=> T) <=> ([S] = [T])

Consider [ v = w ](v, w) and [ v(u) = w(u) ](u)

Value Rule 1

If	v, w	C	B,

then the following are identical values in B:

V1a.	[ v = w ]

V1b.	[ v <=> w ]

V1c.	(( v , w ))

Value Rule 1

If	f, g	:	U -> B,

and	u	C	U

then the following are identical values in B:

V1a.	[ f(u) = g(u) ]

V1b.	[ f(u) <=> g(u) ]

V1c.	(( f(u) , g(u) ))

Value Rule 1

If	f, g	:	U -> B,

then the following are identical propositions on U:

V1a.	[ f = g ]

V1b.	[ f <=> g ]

V1c.	(( f , g ))$

Evaluation Rule 1

If	f, g	:	U -> B

and	u	C	U,

then the following are equivalent:

E1a.	f(u) = g(u).	:V1a

				::

E1b.	f(u) <=> g(u).	:V1b

				::

E1c.	(( f(u) , g(u) )).	:V1c

				:$1a

				::

E1d.	(( f , g ))$(u).	:$1b

Evaluation Rule 1

If	S, T	are sentences

		about things in the universe U,

	f, g	are propositions: U -> B,

and	u	C	U,

then the following are equivalent:

E1a.	f(u) = g(u).	:V1a

				::

E1b.	f(u) <=> g(u).	:V1b

				::

E1c.	(( f(u) , g(u) )).	:V1c

				:$1a

				::

E1d.	(( f , g ))$(u).	:$1b

Facts

Applying Rule 9, Rule 8, and the Logical Rules to the special case where S <=> (X = Y), one obtains the following general fact.

Fact 1

If	X,Y	c	U,

then the following are equivalent:

F1a.	S	<=>	X = Y.	:R9a

				::

F1b.	S	<=>	{X} = {Y}.	:R9b

				::

F1c.	S	<=>	{X}(u) = {Y}(u), for all u C U.	:R9c

				::

F1d.	S	<=>	ConjUu ( {X}(u) = {Y}(u) ).	:R9d

				:R8a

				::

F1e.	[S]	=	[ ConjUu ( {X}(u) = {Y}(u) ) ].	:R8b

				:???

				::

F1f.	[S]	=	ConjUu [ {X}(u) = {Y}(u) ].	:???

				::

F1g.	[S]	=	ConjUu (( {X}(u) , {Y}(u) )).	:$1a

				::

F1h.	[S]	=	ConjUu (( {X} , {Y} ))$(u).	:$1b

///

	{u C U : (f, g)$(u)}

	=	{u C U : (f(u), g(u))}

	=	{u C 

///