ADDITIONAL THEOREM PROOFS
in MULTIPLE FORM LOGIC
version 2.0 - 5 Oct. 2007
(click here to see the previous version 1.01 -August 2007)
by Omadeon
Home page: http://multiforms.netfirms.com
Mirror site: http://omadeon.com/logic

DESCRIPTION:

Current list of theorem proofs:

1) Theorem ART-1 (about the "#" operator)
2) An algebraic proof of "Theorem 9"
3) Theorem ART-1 (alternative "demonstration" by Art Collings)
4) SLIDE-SHOW animated proof of the Third Axiom of Equality (in Tom Etter’s paper “The Expressive Power of Equality”)


(more to be included)
LINKS
  1. (blog article) The “Extended XOR Operator” as a Consistent interpretation of George Spencer-Brown’s "distinction"
  2. (blog article in Greek): Ενημέρωση από ΠΟΛΥ πιο σοβαρό Debate: ΠΩΣ Η Πολλαπλότητα εξάγεται από τη Μοναδική Μορφή
  3. (blog article) How Equality is embedded in Multiple Form Logic (Animated GIF Presentation of a Theorem Proof)
  4. (blog article)  The “Axiom of Perception” in Multiple Form Logic (brand new animated GIF slide-show presentation)


1) Theorem ART-1 (about the "#" operator)
Recently, Mr. Art Collings expressed some interesting doubts and objections about certain aspects of Multiple Form Logic, particularly with regard to the "#" operator (interpreted as logical "XOR"). E.g. he remarked:

"In LoF, the typical way to express XOR is via the form   ( ( A B )  ( ( A ) ( B ) ) )   [ which basically translates as 'A or B but not A and B'. It is easy to verify this expression corresponds to XOR].  In your notation, the corresponding expression is  (  ( A, B) #1  , ( A#1 , B#1)#1 ) #1 .  This being the case, we can easily prove arithmetically that the following theorem is true: 

A# B =  (  ( A, B) #1  , ( A#1 , B#1)#1 ) #1 

The question then becomes whether you can demonstrate this as a consequence in your algebra. GSB proves that LoF is complete by proving that any theorem that is true in the arithmetic can be demonstrated as a consequence in the Algebra. In order for your algebra to be complete in the same sense as LoF, it must be the case that expression such as this can be demonstrated as a consequence from your three axioms: (1. A,1 = 1 ;   2.  A#A = 0;  3.  A, (A, B)#X = A, B#X.  [ i.e., 'demonstrated', as distinct from 'proved'! ] 

I don't have a proof (at the moment), but instinctively my guess is that such a demonstration is not possible from your axiom set (or from other equivalent axiom sets for that matter). "

(- Art  Collings, http://tech.groups.yahoo.com/group/lawsofform/message/1709)


ANSWER: Evidently, the 'instinctive guess that such a demonstration is not possible from the axiom set" (etc.) is wrong.

Here is a complete algebraic proof:

To prove:

A# B =  (  ( A, B) #1  , ( A#1 , B#1)#1 ) #1


Here is an (exclusivey "algebraic") proof, in two stages:


1) First stage, to show that the Left-hand-side of this equation, implies the Right-hand side:

[ i.e. LHS -> RHS, translated into  (LHS)#1, RHS ]

LHS->RHS becomes:

(A# B)#1,  ( ( A, B) #1 , ( A#1, B#1)#1) #1 by substituting the actual values into "LHS#1,RHS"
A#B#1,  ( ( A, B, A#B#1) #1  , ( A#1, B#1)#1) #1 by axiom 3 (internalisation of "(A#B)#1" inside "(A,B)#1")
A#B#1,  ( ( A, B, 1) #1  , ( A#1, B#1)#1) #1 by axiom 3 (cancelling out A, B inside "A#B#1")
A#B#1,  ( ( A#1, B#1)#1) #1 by axiom 1 and axiom 2 (inside "(A,B,1)#1".)
A#B#1,  ( A#1, B#1) by axiom 2 (in "((A#1, B#1)#1) #1")
A#B#1#A#1, A#1, B#1
 by axiom 3 (internalisation of "A#1" inside "A#B#1")
A#B#A, A#1, B#1 by axiom 2 (applied to "A#B#1#A#1" , to remove 1)
B, A#1, B#1 by axiom 2 (applied to "A#B#A" , to remove A)
..., 1 ...  = TRUE
 by axiom 3 (cancelling out B inside "B#1") and -finally- axiom 1

2) Second stage, to show that the Right-hand-side of this equation, implies the Left-hand side:

[ i.e. RHS -> LHS, translated into  (RHS)#1, LHS ]

RHS->LHS becomes:

(((A,B) #1, (A#1, B#1)#1)#1)#1, A#B  =               
by substituting the actual values into "RHS#1,LHS"
(A,B) #1, (A#1, B#1)#1, A#B = by axiom 2  (generally: X#Y#Y = X)
(A,B)#1, (A#1, B#1, A#B)#1, A#B =
by axiom 3 (in reverse;"internalising" A#B inside the second sub-expression)
(A,B)#1, (A#1, A#B#B#1, A#B)#1, A#B = by axiom 3...
(A,B)#1, (A#1, A#B)#1, A#B = by axioms 2 and 1
(A,B)#1, (A#1)#1, A#B = by axiom 3
(A,B)#1, A, A#B = by axiom 2 (applied to "(A#1)#1" )
(B)#1, A, B = by axiom 3 (cancelling out A inside "(A,B)#1" and also in "A#B")
1, ...  = TRUE
 by axiom 2 ( cancelling out B inside "(B)#1" ) and -finally- axiom 1

(the proof is now complete)

2) An algebraic proof of "Theorem 9"

- Also requested by Art Collings, who remarked: 

The same issue in fact arises with your Theorem 9:  ( A # 1, B) = ( A , B ) # B # 1. This is clearly true, which you prove by cases, substituting A = 0 and A = 1.
However, employing substitution while acceptable as an arithmetic proof does not constitute an algebraic demonstration. 


Well, here is a complete ALGEBRAIC DEMONSTRATION:

( A # 1, B) = ( A , B ) # B # 1 


1) First stage, to show that the Left-hand-side of this equation, implies the Right-hand side:

[ i.e. LHS -> RHS, translated into  (LHS)#1, RHS ]

LHS->RHS becomes:
(A#1,B)#1, (A,B)#B#1 =
 by substituting the actual values into "RHS#1,LHS"
(A#1,B)#1, (A,B)#(B, (A#1,B)#1 )#1 = by axiom 3  (internalising "(A#1,B)#1" inside "B" to get "(B, (A#1,B)#1)")
(A#1,B)#1, (A,B)#(B, (A#1)#1 )#1 = by axiom 3 (cancelling-out the 2nd appearance of "B" inside "(B, (A#1,B)#1)")
(A#1,B)#1, (A,B)#(B,A)#1 = by axiom 2 (reducing "(A#1)#1" to "A")..
(A#1,B)#1, 1 = by axiom 2 (reducing "(A,B)#(B,A)#1" to "1")
1 = TRUE
 by axiom 1 (i.e. "anything ,1 =1")

2) Second stage, to show that the Right-hand-side of this equation, implies the Left-hand side:

[ i.e. RHS -> LHS, translated into  (RHS)#1, LHS ]

RHS->LHS becomes:
((A,B)#B#1)#1, (A#1,B) =
 by substituting the actual values into "RHS#1,LHS"
(A,B)#B, (A#1,B) =
 by axiom 2  (applied to "...#1#1")
(A,B,(A#1,B))#B, (A#1,B) = by axiom 3 (internalising "(A#1,B)" inside the first term)
(A,B,1,B)#B, (A#1,B) = by axiom 3 (cancelling-out "A" inside "A#1" because it exists "outside it")
(1)#B, (A#1,B) = by axiom 1 (reducing "A,B,1,B" "to "1")
1#B, A#1,1#B#B = by axiom 3 (internalising "1#B" inside "B" to get "1#B#B")
1 = TRUE
 by axiom 2 (in "1#B#B") and then ax iom 1 (i.e. "anything ,1 =1")


(the proof is now complete)

Art Collings also said:
"You might add these as a new axioms of course, but my position would be that adding the # operation could introduce other such true but non-demonstrable consequences, but you might end up with a really big axiom set. Overcoming these problems with respect to completeness may well prove non-trivial, and it definitely could be the case that introducing the binary # operator actually precludes completeness".

ANSWER:

I  really do not think so...

The operation "#" has NOT been"added" to the system. It ALREADY exists in the system (in a certain way).

1) In this page, I have shown that these theorems are derivable by purely algebraic demonstrations.
There is absolutely, provably, NO need to "add them as new axioms"!

2) A couple of years ago, I also proved that William Bricken's "Boundary Algebra" is only a special instance of Multiple Form Logic:
http://multiforms.netfirms.com/more_theorems.html

3) Other results include evidence (theorems T4, T6) that George Spencer Brown's LoF algebra is ALSO a special instance of Multiple Form Logic:
 Theorem T4)   George Spencer Brown’s algebraic axiom J1 proved as a theorem

Theorem T5)   George Spencer Brown’s algebraic axiom J2 proved as a theorem

4) A proof that Multiple Form Logic is equivalent to a Boolean Algebra, with respect to the operations "  , " and X’ = X # 1 , has already been given in
http://multiforms.netfirms.com/mflogic_proofs.html#theorem_T6

5) My intent for the near future is to also show that Multiple Form Logic is consistent & complete (in conventional terms).

3) An alternative demonstration of "ART-1" by Mr. Art Collings:
(click on the image, to see the original PDF document, in his site):
DEMONSTRATION by Art Collings
4) SLIDE-SHOW animated proof of the Third Axiom of Equality (in Tom Etter’s paper “The Expressive Power of Equality”)

Third Axiom of Equality (proof as a theorem in MF Logic)


(under construction - more theorems are to be included here, soon)