Difference between revisions of "Directory talk:Jon Awbrey/Papers/Syntactic Transformations"

MyWikiBiz, Author Your Legacy — Sunday November 17, 2024
Jump to navigationJump to search
(→‎Other Rules: del merged text)
Line 162: Line 162:
 
: f(u) = [u C X], for all u C U.
 
: f(u) = [u C X], for all u C U.
 
</pre>
 
</pre>
 
======Other Rules======
 
 
<pre>
 
Rule 10
 
 
If X, Y c U,
 
 
then the following are equivalent:
 
 
R10a. X = Y. :D2a
 
 
::
 
 
R10b. u C X  <=>  u C Y, for all u C U. :D2b
 
 
:R8a
 
 
::
 
 
R10c. [u C X] = [u C Y]. :R8b
 
 
::
 
 
R10d. For all u C U,
 
 
[u C X](u) = [u C Y](u). :R8c
 
 
::
 
 
R10e. ConjUu ( [u C X](u)  =  [u C Y](u) ). :R8d
 
 
::
 
 
R10f. ConjUu ( [u C X](u) <=> [u C Y](u) ). :R8e
 
 
::
 
 
R10g. ConjUu (( [u C X](u) , [u C Y](u) )). :R8f
 
 
::
 
 
R10h. ConjUu (( [u C X] , [u C Y] ))$(u). :R8g
 
</pre>
 
 
<pre>
 
Rule 11
 
 
If X c U
 
 
then the following are equivalent:
 
 
R11a. X = {u C U : S}. :R5a
 
 
::
 
 
R11b. {X} = { {u C U : S} }. :R5e
 
 
::
 
 
R11c. {X} c UxB
 
 
: {X} = {< u, v> C UxB : v = [S](u)}. :R
 
 
::
 
 
R11d. {X} : U -> B
 
 
: {X}(u) = [S](u), for all u C U. :R
 
 
::
 
 
R11e. {X} = [S]. :R
 
</pre>
 
 
An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result.  Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time.  More often than not, though, a rule is applied in only a few of its possible ways.  The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows:
 
 
a.  R11a marks the usual starting place for an application of the Rule, that is, the standard form of antecedent condition that is likely to lead to an invocation of the Rule.
 
 
b.  R11b records the trivial consequence of applying the spiny braces to both sides of the initial equation.
 
 
c.  R11c gives a version of the indicator function with {X} c UxB, called its "extensional form".
 
 
d.  R11d gives a version of the indicator function with {X} : U->B, called its "functional form".
 
  
 
======Facts======
 
======Facts======

Revision as of 02:42, 11 September 2010

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
Definitions
Definition 5

If	X	c	U,

then the following are identical propositions:

D5a.	{X}.

D5b.	f	:	U -> B

:	f(u)	=	[u C X], for all u C U.
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 

///
1.3.12.2. Derived Equivalence Relations
1.3.12.3. Digression on Derived Relations