version 2.0 - 5 Oct. 2007

DESCRIPTION:

• This web-page contains formal proofs of theorems in Multiple Form Logic, proposed by other people, or dictated by necessity.
• The new version of this page contains important updates, contributed by Mr. Art Collings in the "Laws of Form Forum"
• These updates arose from the new Formal Demonstration (by Art Collings) of Theorem Art-1 (using only re-write proof-steps)
• The latest (more fundamental) demonstration of theorem Art-1 by Mr. Art Collings is on-line here: http://homepage.mac.com/otter/XOR_demo_hybrid.pdf
• A copy of Art Collings' demonstration is also included here

Current list of theorem proofs:

1) Theorem ART-1 (about the "#" operator)
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)

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".

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 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): 4) SLIDE-SHOW animated proof of the Third Axiom of Equality (in Tom Etter’s paper “The Expressive Power of Equality”) (under construction - more theorems are to be included here, soon)