Changes

no edit summary
Line 1,048: Line 1,048:     
<br>
 
<br>
 +
 +
==Work Area==
 +
 +
<pre>
 +
Logical Translation Rule 1
 +
 +
If S is a sentence
 +
about things in the universe U
 +
 +
and P is a proposition : U -> B, such that:
 +
 +
L1a. [S]  =  P,
 +
 +
then the following equations hold:
 +
 +
L1b00. [False] = () = 0 : U->B.
 +
 +
L1b01. [Not S] = ([S]) = (P) : U->B.
 +
 +
L1b10. [S] = [S] = P : U->B.
 +
 +
L1b11. [True] = (()) = 1 : U->B.
 +
</pre>
 +
 +
<br>
 +
 +
<pre>
 +
Geometric Translation Rule 1
 +
 +
If X c U
 +
 +
and P : U -> B, such that:
 +
 +
G1a. {X}  =  P,
 +
 +
then the following equations hold:
 +
 +
G1b00. {{}} = () = 0 : U->B.
 +
 +
G1b10. {~X} = ({X}) = (P) : U->B.
 +
 +
G1b01. {X} = {X} = P : U->B.
 +
 +
G1b11. {U} = (()) = 1 : U->B.
 +
</pre>
 +
 +
<br>
 +
 +
<pre>
 +
Logical Translation Rule 2
 +
 +
If S, T are sentences
 +
about things in the universe U
 +
 +
and P, Q are propositions: U -> B, such that:
 +
 +
L2a. [S] = P  and  [T] = Q,
 +
 +
then the following equations hold:
 +
 +
L2b00. [False] = () = 0 : U->B.
 +
 +
L2b01. [Neither S nor T] = ([S])([T]) = (P)(Q).
 +
 +
L2b02. [Not S, but T] = ([S])[T] = (P) Q.
 +
 +
L2b03. [Not S] = ([S]) = (P).
 +
 +
L2b04. [S and not T] = [S]([T]) = P (Q).
 +
 +
L2b05. [Not T] = ([T]) = (Q).
 +
 +
L2b06. [S or T, not both] = ([S], [T]) = (P, Q).
 +
 +
L2b07. [Not both S and T] = ([S].[T]) = (P Q).
 +
 +
L2b08. [S and T] = [S].[T] = P.Q.
 +
 +
L2b09. [S <=> T] = (([S], [T])) = ((P, Q)).
 +
 +
L2b10. [T] = [T] = Q.
 +
 +
L2b11. [S => T] = ([S]([T])) = (P (Q)).
 +
 +
L2b12. [S] = [S] = P.
 +
 +
L2b13. [S <= T] = (([S]) [T]) = ((P) Q).
 +
 +
L2b14. [S or T] = (([S])([T])) = ((P)(Q)).
 +
 +
L2b15. [True] = (()) = 1 : U->B.
 +
</pre>
 +
 +
<br>
 +
 +
<pre>
 +
Geometric Translation Rule 2
 +
 +
If X, Y c U
 +
 +
and P, Q U -> B, such that:
 +
 +
G2a. {X} = P  and  {Y} = Q,
 +
 +
then the following equations hold:
 +
 +
G2b00. {{}} = () = 0 : U->B.
 +
 +
G2b01. {~X n ~Y} = ({X})({Y}) = (P)(Q).
 +
 +
G2b02. {~X n Y} = ({X}){Y} = (P) Q.
 +
 +
G2b03. {~X} = ({X}) = (P).
 +
 +
G2b04. {X n ~Y} = {X}({Y}) = P (Q).
 +
 +
G2b05. {~Y} = ({Y}) = (Q).
 +
 +
G2b06. {X + Y} = ({X}, {Y}) = (P, Q).
 +
 +
G2b07. {~(X n Y)} = ({X}.{Y}) = (P Q).
 +
 +
G2b08. {X n Y} = {X}.{Y} = P.Q.
 +
 +
G2b09. {~(X + Y)} = (({X}, {Y})) = ((P, Q)).
 +
 +
G2b10. {Y} = {Y} = Q.
 +
 +
G2b11. {~(X n ~Y)} = ({X}({Y})) = (P (Q)).
 +
 +
G2b12. {X} = {X} = P.
 +
 +
G2b13. {~(~X n Y)} = (({X}) {Y}) = ((P) Q).
 +
 +
G2b14. {X u Y} = (({X})({Y})) = ((P)(Q)).
 +
 +
G2b15. {U} = (()) = 1 : U->B.
 +
</pre>
 +
 +
<br>
 +
 +
<pre>
 +
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))
 +
</pre>
 +
 +
<br>
 +
 +
<pre>
 +
Value Rule 1
 +
 +
If v, w C B,
 +
 +
then the following are equivalent:
 +
 +
V1a. v = w.
 +
 +
V1b. v <=> w.
 +
 +
V1c. (( v , w )).
 +
</pre>
 +
 +
<pre>
 +
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
 +
 +
 +
Definition 2
 +
 +
If X, Y c U,
 +
 +
then the following are equivalent:
 +
 +
D2a. X = Y.
 +
 +
D2b. u C X  <=>  u C Y, for all u C U.
 +
 +
Definition 3
 +
 +
If f, g : U -> V,
 +
 +
then the following are equivalent:
 +
 +
D3a. f = g.
 +
 +
D3b. f(u) = g(u), for all u C U.
 +
 +
Definition 4
 +
 +
If X c U,
 +
 +
then the following are identical subsets of UxB:
 +
 +
D4a. {X}
 +
 +
D4b. {<u, v> C UxB : v = [u C X]}
 +
 +
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.
 +
 +
Given an indexed set of sentences, Sj for j C J, it is possible to consider the logical conjunction of the corresponding propositions.  Various notations for this concept are be useful in various contexts, a sufficient sample of which are recorded in Definition 6.
 +
 +
Definition 6
 +
 +
If Sj is a sentence
 +
about things in the universe U,
 +
for all j C J,
 +
 +
then the following are equivalent:
 +
 +
D6a. Sj, for all j C J.
 +
 +
D6b. For all j C J, Sj.
 +
 +
D6c. Conj(j C J) Sj.
 +
 +
D6d. ConjJ,j Sj.
 +
 +
D6e. ConjJj Sj.
 +
 +
Definition 7
 +
 +
If S, T are sentences
 +
about things in the universe U,
 +
 +
then the following are equivalent:
 +
 +
D7a. S <=> T.
 +
 +
D7b. [S] = [T].
 +
 +
Rule 5
 +
If X, Y c U,
 +
 +
then the following are equivalent:
 +
 +
R5a. X = Y. :D2a
 +
::
 +
R5b. u C X  <=>  u C Y, for all u C U. :D2b
 +
:D7a
 +
::
 +
R5c. [u C X] = [u C Y], for all u C U. :D7b
 +
:???
 +
::
 +
R5d. {<u, v> C UxB : v = [u C X]}
 +
=
 +
{<u, v> C UxB : v = [u C Y]}. :???
 +
:D5b
 +
::
 +
R5e. {X} = {Y}. :D5a
 +
 +
Rule 6
 +
 +
If f, g : U -> V,
 +
 +
then the following are equivalent:
 +
 +
R6a. f = g. :D3a
 +
::
 +
R6b. f(u) = g(u), for all u C U. :D3b
 +
:D6a
 +
::
 +
R6c. ConjUu (f(u) = g(u)). :D6e
 +
 +
Rule 7
 +
 +
If P, Q : U -> B,
 +
 +
then the following are equivalent:
 +
 +
R7a. P = Q. :R6a
 +
::
 +
R7b. P(u) = Q(u), for all u C U. :R6b
 +
::
 +
R7c. ConjUu (P(u)  =  Q(u)). :R6c
 +
:P1a
 +
::
 +
R7d. ConjUu (P(u) <=> Q(u)). :P1b
 +
::
 +
R7e. ConjUu (( P(u) , Q(u) )). :P1c
 +
:$1a
 +
::
 +
R7f. ConjUu (( P , Q ))$(u). :$1b
 +
 +
 +
Rule 8
 +
 +
If S, T are sentences
 +
about things in the universe U,
 +
 +
then the following are equivalent:
 +
 +
R8a. S <=> T. :D7a
 +
::
 +
R8b. [S] = [T]. :D7b
 +
:R7a
 +
::
 +
R8c. [S](u) = [T](u), for all u C U. :R7b
 +
::
 +
R8d. ConjUu ( [S](u)  =  [T](u) ). :R7c
 +
::
 +
R8e. ConjUu ( [S](u) <=> [T](u) ). :R7d
 +
::
 +
R8f. ConjUu (( [S](u) , [T](u) )). :R7e
 +
::
 +
R8g. ConjUu (( [S] , [T] ))$(u). :R7f
 +
 +
For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines (a, b, c), and these components of Rule 9 can be cited in future uses as "R9a", "R9b", "R9c", respectively.  Using Rule 7, annotated as "R7", to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as "R9d", "R9e", "R9f", "R9g".
 +
 +
Rule 9
 +
 +
If X, Y c U,
 +
 +
then the following are equivalent:
 +
 +
R9a. X = Y. :R5a
 +
::
 +
R9b. {X} = {Y}. :R5e
 +
:R7a
 +
::
 +
R9c. {X}(u) = {Y}(u), for all u C U. :R7b
 +
::
 +
R9d. ConjUu ( {X}(u)  =  {Y}(u) ). :R7c
 +
::
 +
R9e. ConjUu ( {X}(u) <=> {Y}(u) ). :R7d
 +
::
 +
R9f. ConjUu (( {X}(u) , {Y}(u) )). :R7e
 +
::
 +
R9g. ConjUu (( {X} , {Y} ))$(u). :R7f
 +
 +
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
 +
 +
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>
 +
 +
<pre>
 +
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
 +
///
 +
</pre>
12,080

edits