Notes on the Tabularity of Polycontextural Logics

Bifunctoriality for transpositional and replicational Tableaux-Forest Calculi

Rudolf Kaehr Dr.phil@

Copyright ThinkArt Lab ISSN 2041-4358

 

Abstract

Some more stuff towards an adequate formalization of polycontextural logics. The tabular tableaux_forest approach. (Work in progress, v. 0.5, 25.July 2012 )

1.  Matrix Design for polycontextural Tableaux Logics

1.1.  Concept of matrix-distribution

1.1.1.  Bifunctoriality and tabular notation

Logic is easily connected with trees. Raymond Smullyan started the movement of “Logic with Trees” (Colin Howson), Melvin Fitting, the master of all trees dedicates his book “First-order Logic and Automated Theorem Proving" "To Raymond Smullyan who brought me into the trees".

The tree or tableaux method is highly elaborated by Melvin Fitting as the ultimate tableaux method, used today as a proof method for nearly all kinds of logical systems. There had been predecessors, as usual, like Evert Beth and Jaako Hintikka, or the Dialog Logic approaches of Paul Lorenzen and E. M. Barth.

Tree-thinking goes back to the Porphyry of Tyre with his Porphyrian tree. Tree-thinking is fundamental for Western thinking. Chinese thinking in contrast is based not on trees but on grids (Yang Hui (楊輝, c. 1238 - c. 1298)).
http://the-chinese-challenge.blogspot.co.uk/2007/03/chinese-centralism.html

The tableaux approach to logic seems to be very natural. Its emphasis is focussed on a structure with a singular beginning (root) and (mostly) binary decision procedures for the prolongations of the tree build on the base of such a root and its branching. The established hierarchy between the root and its nodes is perfectly stabilized by the success of its applications and its lucid rationality rooted in classical Western thinking of Porphyrian tree ontology and its re-invention in the Semantic Web, too.

It is believed, historically and actually, that non-rooted and non-hierarchical systems of thought and action are leading for short or long into chaos.

Postmodernist thinking believes that such arguments of and against hierarchical organizations are obsolete. Even the smallest kid experiences and knows how much we all are connected and taking part in massive networks where there is no beginning and no end and everything is nevertheless working fine. What’s a correct impression for kids is not necessary the truth of the adult game.

With or without clouds, the internet connections are strictly hierarchically mathematized, programmed, organized, regulated, governed and policed.

The mass of data and “contents” are blinding the fact of the covered simple hierarchical form of organization of the deep-structure of the Web. Not just ICANN and the reduction to uni-directional communication but also the reduction of any sign system to techniques and ideologies of digitalism is determining the structural poverty of the overwhelming possibilities on an informational data-level.

For whatever reasons I never could find any enthusiasm for such an ultimate tree.

To stay in the context of the established form of rationality I prefer to live with/in forests instead of singular trees. I don’t see any reason why a node might not change into a root and a root not becoming a node of a different, equally fundamental tree.

Traditional trees are not just defined by their uniqueness and hierarchy but by their definitive lack of interchangeability, chiasm or proemiality of the ‘fundamental’ terms, like nodes and root.

In fact, trees don’t come in plural. All the singular and factual trees, say of logic, are dominated by the concept and methods of a single, unique and ultimate idea of a tree.

A first, and simple approach to surpass such limitations is proposed with the idea and some elaborations of forest-based polycontextural logics.

Hence, nothing is wrong with “Logic with Trees”. I opt to just disseminate such ultimate trees. This, as such and alone, wouldn’t be specially interesting. What makes the forest approach interesting is the possibility of interactions between the plurality of such simultaneously existing ultimate trees. A forest is not the sum of singular trees but the interactivity between trees.

For the case of just one singular but ultimate tree we don’t have to know much about the structure of the place it is planted. Because of its uniqueness, the knowledge of its ground(ing) can freely be omitted. For a forest, the loci of the trees becomes crucial. Disseminated trees are indexed to localize them in the grid of the ground. A ground and locus of a tree is not itself a tree. Hence, any logical characterization of the loci of the trees, that is building of a matrix and a grid, is obsolete. The matrix of the dissemination of logic-trees is defined by a a-logical or pre-logical structure. This pre-logical and pre-semiotic structure is covered by the methods of kenogrammatics. Thus, the grid of the forest is the kenomic matrix.

Again, the game starts again. There is no necessity to suppose a static hierarchy between the grid and the forests.

Trees in formal languages are reduced to the simple structure of “append”  and “remove” of “items”. Hence, disseminated trees are indexed, in this case, double-indexed to define a matrix of trees, and are defined by the similarly simple operations of “leave” a tree, ‘horizontally’ for replications (reflection) and “leave” a tree vertically for transpositions (transjunctions).

Other operations between trees, like permutation, reduction and iteration of trees of a forest, are easily introduced and implemented into the formal game of forest-logics. Forests are not static. They might grow or shrink and change their patterns.

From a more mathematical point of view, forests and their interplays are well ruled by the polycontextural concept of interchangeability, i.e. a generalization and subversion of the category-theoretic concept of bifunctoriality.

Without any big deviations and dangerous revolutions a move from the tree-culture to a forest-world of thinking and acting seems to be a fairly save and sane step of evolution even for the timid Western searcher of truth and computational efficiency.

In earlier papers about tree-farming I proposed contextural forests as forests of colored trees. This time, coloring has to wait for the paint.

Tabular complexity in action

[Graphics:HTMLFiles/Notes on Polycontextural Logics_1.gif]

History and sketches of the tabular approach to polycontexturality
http://www.thinkartlab.com/pkl/lola/PolyLogics.pdf
http://www.thinkartlab.com/pkl/lola/AFOSR-Place-Valued-Logic.pdf
http://www.thinkartlab.com/pkl/lola/ConTeXtures.pdf
http://www.thinkartlab.com/pkl/media/SKIZZE-0.9.5-medium.pdf

1.1.2.  Why Smullyan’s analytical tree method?

"The tree method is one of several decision procedures available for classical propositionai logic and first-order functional calculus and for nonclassical logics, inducing intuitionistic propositional logic and intuitionistic first-order logic, modal logics, and multiple-valued logics The tree method provides exceptionally elegant proofs of the consistency and satisfiability of formulae.

Falsifiability trees allow easy testing of the validity of proofs and are a canonization of proof by contradiction for natural deduction systems, while truth trees allow easy derivation of theorems in these systems. Tree proofs permit graphical-geometric representations of logical relations, and appear to be of greater intuitive accessibility than either the axiomatic method or the method of natural deduction.

The proofs of the completeness and soundness of the tree method and its variants are also straightforward, and the method combines insights and results of model theory and proof theory in a fashion that clearly identifies the most basic concepts of proof involving such model-theoretic results as Craig's Interpolation Lemma, Beth's Definability Theorem, and Robinson's Consistency Theorem.” (Irving H. Anellis)
http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.rml/1204834539

1.1.3.  A wee 3x3-forest of tableaux_trees with bifunctoriality

    <br />       H5   =   (X laa Y)   iij   (X laa Y )  &nb ...              Semantic scheme for f3H5

(f1 .1 : <br /> t1 .1 : (X l Y) <br /> f1 .1 : (X l Y) <br /> stop(1.1)                        ... p;         Closing semantic tableaux_forest for f3H5 Null

f1H5                                                                                           ... bsp;    xx = stop(3.3)           

<br /> Bifunctoriality of H5

<br /> (1)      t2 .1 :   (X laa Y)     (0)   &nb ...      (2.2 ) ,     t1 .2   : Y      (2.2 ) <br />

General scheme <br />  (sf1 && sf2 && sf3 && sf4) // < (t1 &&am ... mp;& : junction, <br /> //       : transfunction <br />   

     Diagram <br /> <br /> Overscript[    |   &nb ...  />      | <br />     sf4 <br />      

<br /> Formal   characterization   for   f1H5 : <br /> (                                       ...                                                      [empty]       <br />

<br /> Multi - processor model for f1H5 :

Multi-Processor-System for matrix-distribution of tableaux_forests =
(intra-process: {append, remove, leave}, inter-process: {send, receive}).

(                                                                                              ...                                                                                                  -

2.  From a tableaux to a matrix presentation

2.1.  TreeDefinition

2.1.1.  Fitting Smullyan trees

TreeDefinition in Prolog by Fitting, p. 156.

/* member(Item, List) := Item occurs in List
*/
member(X, [X |  _]).
member(X, [_ | Tail]) :- member(X, Tail).

/* remove(Item, List, Newlist) :-
         Newlist is the result of removing all occurrences of Item from List.
*/
remove(X, [ ], [ ]).
remove(X, [Y | Tail], Newtail) :-
      X == Y
remove(X, [Y | Tail], [Y | Newtail]) :-
      X \= Y
remove(X, Tail, Newtail).

/*  append(ListA, ListB, Newlist) :-
           Newlist is the result of appending ListA and ListB.
*/
append([ ], List, List).
append([Head | Tail], [Head | Newlist]) :-
   append(Tail, List, Newlist).

Conceptual structure of Fitting’s TreeDefinition
Mono-Contexturality: Prolog, Logic.
TreeDefinition = (Operators, Elements):
Elements = {Item, List, Newlist; Head, Tail, Newtail, ListA, ListB} with  
operators= {member, remove, append}.

Forests of Trees
Distribution of TreeDefiniton.
Method: Indexed categories (Pfalzgraf)
Junctional logical operations.
Transjunctions as semantically indexed mono-contextural mappings.

Mediated Forests of Trees
Weak polycontexturality. Category theory.
Distribution and mediation of TreeDefiniton.
Method: Single-indexed categories (Pfalzgraf) with proemial interchangeability and chiasms.
Junctional and transjunctional logical operations.
LOLA: lists of mediated tableaux trees.

Matrix of Trees
Polycontexturality, Polycontextural Logics, Morphogrammatics.
Interactionally and reflectionally distributed and mediation of TreeDefinition.
Double-indexed categories and processors.

MAT = {{term, list, append, remove} ∪ {replication, transposition}, N}.
replication = leaveV, (vertical)
transposition = leaveH, (horizontal).

2.1.2.  TreeDefinition of TabDefSig in SML by LOLA1993

(*$TabDefSig*)
signature TABDEF =
    sig
    type var
    type truval
    type operator
    type formula
    type tableau_tree
    exception TabDefError of string
    val fmls2fmls:  (formula list) -> (formula list)
    val defs2rules: (operator * (int * (var list) * formula)) list  -> unit
    val tabs2rules: (operator * (int * (var list) * ((truval*tableau_tree) list))) list  -> unit
    end;

http://www.thinkartlab.com/pkl/lola/LOLA.pdf

2.1.3.  Sketch of a matrix definition for forests of tableaux trees

(*$MatDefSig*)
signature MATRIXDEF =
    sig
           type matrix
           type matrix_super-operators
           type tableaux_forest              
  sig
       tableaux-forest
       val tab2tab: (tableaux_tree list) --> (tableaux_tree list)

val tableaux - forest2tableaux - forrest : <br /> ID :       &nb ... x_forest) ^(i, j) -> (tableaux_forest) ^(i, j  _ 1 ... j  _ k)

signature TABDEFtypeset structure =
    sig
           type var
    type truval
    type operator
    type formula
    type tableau_tree
           type tableaux_forrest

    exception TabDefError of string
    val fmls2fmls:  (formula list) -> (formula list)
    val defs2rules: (operator * (int  *(var list) * formula)) mat  -> unit
    val tabs2rules: (operator * (int  *(var list) * ((truval*tableau_tree) list))) list  -> unit
    end;

signature TAB2MATRDEF =

2.2.  Bivariat functors

2.2.1.  Unary and binary indexed functors

Unary indexed functors for LOLA1993
The unary indexed approach to polycontextural tableaux trees takes the distribution over different places into account. But it is not yet considering the matrix distribution necessary for an understanding of the full polycontextural approach with transpositions and replications defining a 2-dimensional grid.

Infixes
||:   disjunctive              
&&: conjunctive
///: transjunctive branching.

Operators
o: disjunction,
a: conjunction,
i, j: implication,
t: transjunction.

Examples
oao :   [t1:  t1:X || t1:Y ]
        [f1:  f1:X && f1:Y ]
        [t2:  t2:X && t2:Y ]
        [f2:  f2:X || f2:Y ]
        [t3:  t3:X && t3:Y ]
        [f3:  f3:X || f3:Y ]

ijj :  [t1:  f1:X || t1:Y]
       [f1:  t1:X && f1:Y]
       [t3:  (f2:X || t2:Y) /// (f3:X || t3:Y)]    
       [f3:  (t2:X && f2:Y) /// (t3:X && f3:Y)]
       [t2:  f2:X && t2:X]
       [f2:  f2:X && t2:X]

oto :  [t1:   t1:X && t1:Y /// (f2:X && t2:Y)||(t2:X && f2:Y)]
        [f1:   f1:X && f1:Y /// (t2:X && t2:Y)                           ]
        [t2:   t2:X && t2:Y ]
        [f2:   f2:X && f2:Y ]
        [t3:   t3:X || t3:Y /// (f2:X && t2:Y)||(t2:X && f2:Y)]
        [f3:   f3:X && f3:Y /// (f2:X && f2:Y)                        ]

http://www.thinkartlab.com/pkl/lola/VERSIONT/DATA/TABLEAU.RUL

Double-indexed functors for MATRIX-LOLA
The double-indexed functors are distibuted and mediated over the kenomic matrix. Its 2-dimensionality enables, together with permutations, reductions and iterations, a proper managment of transjunctional and replicational functors.

Junctional distribution
oao
:   [t1.1:  t1.1:X || t1.1:Y ]
        [f1.1:  f1.1:X && f1.1:Y ]
        [t2.2:  t2.2:X && t2.2:Y ]
        [f2.2:  f2.2:X || f2.2:Y ]
        [t3.3:  t3.3:X && t3.3:Y ]
        [f3.3:  f3.3:X || f3.3:Y ]

Replicational distribution
ijj :
[t1.1:  f1.1:X || t1.1:Y]
       [f1.1:  t1.1:X && f1.1:Y]
       [t3.3: (f1.2:X || t1.2:Y)\\\ (f3.3:X || t3.3:Y)]    
       [f3.3: (t1.2:X && f1.2:Y)\\\ (t3.3:X && f3.3:Y)]
       [t2.2:  f2.2:X && t2.2:X]
       [f2.2:  f2.2:X && t2.2:X]    =[]

iij:   [t1.1: (f1:X || t1:Y) /// (f1.2:X || t1.2:Y)]
       [f1.1: (t1:X && f1:Y) /// (t1.2:X && f1.2:Y)]
       [t3.3:  f1.3:X || t1.3:Y]    
       [f3.3:  t1.3:X && f1.3:Y]
       [t2:  f2.2:X && t2.2:X]     =[]
       [f2:  f2.2:X && t2.2:X]

Transjunctional distribution
oto :  [t1.1:   t1.1:X && t1.1:Y /// (f2.1:X && t2.1:Y)||(t2.1:X && f2.1:Y)]
        [f1.1:   f1.1:X && f1.1:Y /// (t2.1:X && t2.1:Y)                               ]
        [t2.2:   t2.2:X && t2.2:Y ]
        [f2.2:   f2.2:X && f2.2:Y ]
        [t3.3:   t3.3:X || t3.3:Y /// (f2.1:X && t2.1:Y)||(t2.1:X && f2.1:Y)]
        [f3.3:   f3.3:X && f3.3:Y /// (f2.1:X && f2.1:Y)                        ]

2.2.2.  Distribution tables

Total functions: Ftot: (i, j) --> (i, j)

Ftypeset structure:
o1.1: (1, 2) --> (1, 2;1)
atypeset structure: (2, 3) --> (2, 3;2)
o3.3: (1, 3) --> (1, 3;3).

typeset structure =>  typeset structure : typeset structure

Ftypeset structure:
o1.1: (1, 2) --> (1, 2;1)
atypeset structure: (2, 3) --> (2, 3;2)
o3.3: (1, 3) --> (1, 3;1).

typeset structure =>  typeset structure : typeset structure

Partial functions Ftypeset structure
Transjunctions: Ftrans: (i, j) --> ((i, j1),  (i,jtypeset structure,..., (i,jn)
Foto:
o1.1: (1, 2) --> (1,2;1)
ttypeset structure (2, 3) --> (2, 3;1), (2, 3;2), (2, 3;3)),
o3.3: (1, 3) --> (1, 3;3)

typeset structure  =>  typeset structure :  typeset structure

Mediation scheme t3 .3 ≡ t1 .1 --> f1 .1    ↓      ... ;         ↕ <br /> f3 .3 ≡ f2 .2 <-- t2 .2


Ftypeset structure:
i1.1: (1, 2) --> (1, 2;1)
itypeset structure: (2, 3) --> (1, 3;1)
j3.3: (1, 3) --> (1, 3;3).

typeset structure =>  typeset structure , ijj = i1.1 i1.3 i3.3


typeset structure  typeset structure

typeset structure  typeset structure

neg1(ijj):
[t1.1, f1.1] = [t1,f1]:pos(1,1)    [f1.1, t1.1] = [t1, f1]:pos(1,1)
[t1.3, f1.3] = [t1,f1]:pos(1,3)    typeset structure = [t2, f2]:pos(2,2)
[t3.3, f3.3] = [t3,f3]:pos(3,3)    typeset structure = [t2, f2]:pos(2,3)


typeset structure =>  typeset structure , iij = i1.1 i1.2 i3.3    

typeset structuretypeset structure



typeset structure =>  typeset structure :  typeset structure    

2.2.3.  Polyvariat functors

Decomposibility of m-valued n-ary functions into its two-valued parts is disturbed by the fact that an extensional m-valued n-ary function receives more different values as necessary for a decomposition into binary states. Hence, a 3-valued 3-ary function with {1,2,3}3 gets constellations like (1,2,3) that are not as such decomposable as such into 2-valued parts.

val((X o Y ) o Z) != val(val(X o Y), Z))

Example

 <br />     val ^(3) (   X ∧ ∨ ∧ Y)  & ...  ∨ ∨ Z) . <br /> | val ^(3, 3) (X, Y, Z) | = 3 ^(3 ) - 3 = 24

                             O                    O                    O༺ ...           3   -                            -                            [{t3 .3, f3 .3}  ]

Tableaux - Rules 1. {t  _ i, f  _ i} ∈ Contradiction, i ∈ (m/2) 2. ... le {f  _ 2.3 , t  _ 1.3, f  _ 1 ≡ t  _ 2 } ∉ VB  Null

H = (X ∨ ∨ ∨ ¬  _ 1 Y) ∨ ∨ ∨ ¬  _  ... sp; t1 .1 Y <br /> {f1 .1, f1 .1, f3 .3}, {   t2 .2, t3 .3, f2 .2 } ∉ VB . <br />

     H =  ¬  _ 1((¬  _ 1 ∨ ∨ ∨ & ... 4; ∨ ¬  _ 1 Z) . ijj . ((X ∧ ∨ ∨ Y) ∧ ∨ ∨ Z)

 H                                                                                             ...               1                                       1                                          1

2.3.  Matrix distribution

Infixes
||:   disjunctive,              
&&: conjunctive,
///: transjunctive,
\\\: replicative branching.


oao: [||, &&]:

typeset structure

iij: [||, &&, \\\]:

typeset structure


typeset structure

oto: [||, &&, ///]:

typeset structure     


oto : [t1.1:   t1.1:X || t1.1:Y  /// [] /// (f2.1:X && t2.1:Y) || (t2.1:X && f2.1:Y)  /// [] ]
        [f1.1:   f1.1:X && f1.1:Y   /// []  /// t2.1:X && t2.1:Y                                    /// [] ]
        [t2.2:   t2.2:X && t2.2:Y ]
        [f2.2:   f2.2:X && f2.2:Y ]
        [t3.3:   t3.3:X || t3.3:Y ///  [] /// (f2.1:X && t2:Y) || (t2.1:X && f2.1:Y)  /// [] ]
        [f3.3:   f3.3:X && f3.3:Y /// []  /// f2.1:X && f2.1:Y                                  /// [] ]

Iterations

                             O                    O                    O༺ ...                         3                3.2           3                                   2 Null

ii ''' j                                                                                       ...                           [t3 .3 : (f3 : X || t3 : Y)] <br /> [f3 .3 : (t3 : X && f3 : Y)]

Example: Disambiguation of the implication “j” in “ooj”       

ooj :  [t1:  t1: X || t1:Y /// f2:X && f2:Y /// f3:X || t3:Y ]
         [f1:  f1:X && f1:Y /// t2:X || t2:Y /// t3:X && f3:Y ]

ooj' :  [ t1:  t1: X || t1:Y /// f2:X && f2:Y ]
         [f1:  f1:X && f1:Y /// t2:X || t2:Y  ]
         [t3:  f3:X || t3:Y  ]
         [f3:  t3:X && f3:Y ]

<br />     (ooj   O     O     O  )    => (                         ...                                          O                                                     3.3

Result : <br /> The specially distinguished implication " j ' " is nothing more than ... the place (1, 3) . The abstract implication " j " is represented by the morphogram [j] .

2.3.1.  Distributivity and Bifunctoriality of terms

Among the main rules to organize logical proof are the principle of distributivity for classical logic and bifunctoriality for polycontextural logics.

typeset structure


typeset structure

Some transjunctional rules Underscript[X taa Y, _] Y    taa X <br /> Underscript[X l ... script[<br /> (X taa U) aaa (Y taa V)   , _]     (X aaa Y) taa (U aaa V)

An extension in classical logic of Distr(X, Y, Z; a, o) to Distr(X, Y, U, V; a, o) is trivially achieved by substitution. In other words, Distr(X, Y, U, V, a, o) in classical logic is trivially reduced to Distr(X, Y, Z; a, o).  Therefore, there is no genuine ‘bifunctiorial’ principle for classical logic. For polycontextural logics with their transjunctions ‘bifunctoriality’ is crucial.
BIF(X, Y, U, V; a, t) is not reducible to Distr(X, Y, U, V; a, o). Transjunctional operators are not definable in terms of junctional  operators. Therefore, the rules for transjunctions and their interplay with junctions has to be established separately.

[Graphics:HTMLFiles/Notes on Polycontextural Logics_65.gif]
http://www.thinkartlab.com/pkl/lola/Transjunctions/Tale%20of%20Transjunctions.pdf

2.3.2.  Negation and permutation

LOLA-definitions
n1
3 (X):=
[T1: F1: X] [F1: T1:X]
[T2: T3: X] [F2: F3:X]
[T3: T2: X] [F3: F2:X]

n2  3 (X) :=
[T1: T3: X] [F1: F3: X]
[T2: F2: X] [F2: T2:X]
[T3: T1: X] [F3: F1:X]

Matrix definitions of negations

typeset structure      

typeset structure


typeset structure

typeset structure


typeset structure


typeset structure


typeset structure     

Matrix indices, again

taa : [t1:  t1:X && t1:Y ]
        [f1:   f1:X && f1:Y ]
        [t2:   t2:X && t2:Y /// f1:X && f1:Y                             /// [] /// [] ]
        [f2:   f2:X || f2:Y /// (f1:X && t1:Y) || (t1:X && f1:Y) /// [] /// [] ]
        [t3:   t3:X && t3:Y /// t1:X && t1:Y                             /// [] /// [] ]
        [f3:   f3:X || f3:Y /// (f1:X && t1:Y) || (t1:X && f1:Y)  /// [] /// [] ]


typeset structure

πi.j : i=place, j=value, hence t2.1: value t1 at place locus2.

2.4.  Forest-tableaux proofs

Another example; without negation

H5 = ((X laa Y) iij (X laa Y))


typeset structure   


Bifunctoriality
( A simul C) et (B simul D) = (A et B) simul (B et C):

typeset structure et typeset structure= typeset structure typeset structure     

H5 =  ((X laa Y) iij (X laaY))

typeset structure


1LOLA-1993-proof of f1H5

f1: ((X laa Y) iij (X laa Y))
                                 |                                   
              +---------------  ///  ---------------+  : this branching is replicational \\\ in Matrix.
              |                                     |               
              |                      +------------------------------+        
      +------ && ------+             |              |               |
      |                |             |      +------ && ------+      |
t1: (X laa Y)    f1: (X laa Y)       |      |                |      |
                                     |t2: (X laa Y)    f2: (X laa Y)|
                                     +------------------------------+
                                                     |                                   
                                 +----------------  ///  ---------------+  : this branching is transjunctional.           
                                 |                                      |                
                                 |                       +------------------------------+
               +---------------- && ------+              |              |               |
               |                          |              |      +------ && ------+      |
               |                          |              |      |                |      |
      +------- || ------+             +-- && --+         |t2: (X laa Y)    f2: (X laa Y)|
      |                 |             |        |         +------------------------------+
      |                 |           f1: X    f1: Y                                       
  +-- && --+        +-- && --+                                                           
  |        |        |        |                                                           
t1: X    t1: Y    t1: X    f1: Y              


The proof ends with:


|                    
+-  ///  --------+         : replicational  
|                |        
+-+       +---------------+
|$|       |      |        | : transjunctional.
+-+       | +-  ///  --+  |
          | |          |  |
          |+-+       +---+|
          ||$|       |+-+||
          |+-+       ||$|||
          |          |+-+||
          |          +---+|
          +---------------+

2.4.1.  Bifunctoriality in action

f1 H1 = f1 ((X taa Y) .iij. n5(n5 X oto n5 Y)

The clean separation of the transjunctional and the junctional parts of the tableaux is ruled by the bifunctorial term rule R1 based on the matrix representation.

Again, without a strict tabular matrix-scheme of the distribution of tableaux_trees, an application of the bifunctorial term rule wouldn’t be possible.
On the other hand, an intuitive approach as shown in the colored term development would be helplessly lost in higher complexity. The example shows at least a first step of a distribution of different loci, S1 and S2.

In fact, the concept of a tabular dissemination was clearly stateted but the bifunctorial term rules had still been missing for h conceptual and manual approach. Nevertheless, bifunctoriality was at the base of the implementation of the theorem prover LOLA (1993).

        [Graphics:HTMLFiles/Notes on Polycontextural Logics_80.gif]

[Graphics:HTMLFiles/Notes on Polycontextural Logics_81.gif]

Sub-systems S1 and S2 are closing directly, S1 at step 8 and S2 at step 9. This would be enough to close the tableaux for S1 and S2. But there is an additional part of the formula which is closing separately in S1, closing at step 13, encircled in red.

The analysis on the base of the bifunctorial term rule R1 gives a conceptually and technically clear result and eliminates the adhocism of the “red” results.

[Graphics:HTMLFiles/Notes on Polycontextural Logics_82.gif]

[Graphics:HTMLFiles/Notes on Polycontextural Logics_83.gif]

f1 H1 = f1 ((X taa Y) .iij. n5(n5 X oto n5Y)

typeset structure

2.4.2.  Negation and permutation in proofs


H6 = (n1(n1X ooo n1Y) iij (X aoo Y)

typeset structure

typeset structure

2.4.3.  Negations and permutations

<br /> H7   = n1(n2(n1(n2(n1(n2(X)))))) iij (X) <br />

(f1 .1 : H7                                                                   negation cycle   ...                  -                                                                            xxx

<br /> (f3 .3 : H7                                                                             ...                                                                                                xxx

<br /> neg1(ijj) : <br /> [t1 .1, f1 .1] = [t1, f1] : pos(1, 1)     =>   ... f3] : pos(3, 3)     =>    [t2 .3, f2 .3] = [t2, f2] : pos(2, 3) <br />

H7 =  ((XooaY) laa (X aao Y)) iij ((YooaX) laa (Y aao X))


typeset structure

2.5.  Decision mechanisms

2.5.1.  Intra-contextural logical proofs

From an environment of a complex system Systtypeset structure a request might be addressed, asking to check if the logical formula H5 is valid for all its subsystems. In short: Does the complex tableaux prover LOLAplusproof the validity of H5? In other words: Are all subsystem tableaux closing in all branches of the tree-development of the formula H5 for f1 and f3?

Firstly, it is supposed that the formula H5 is syntactically well-formed, then questions arises about its semantic and its proof-theoretic properties.

input   question   for   Syst ^(3, 3) :   H5 ∈ tautology ? : <br />    ... <br /> xx    Result :   f1   H5   and   f3H5 ∈ tau t, hence H5   ∈   taut .

2.5.2.  Polycontextural transformations

How to define or represent matrix-constellations of logical operators out of other existing constellations?
In classical logic this reduces to the question, how to represent, say, conjunction by disjunction? There is no need to ask for more. Classical junctions are ‘one-place’ operations in the matrix. That is, classical junctions are not distributed but appear at singular not marked place.
De Morgan is at its place. Completeness of definability by say the Sheffer stroke is secured.

Definability for polycontextural logics (pcl) is more intricate. How to define, a pcl-constellation by means of other pcl-constellations? Is there a Sheffer analogon? Are transjunctional functions definable by junctional functions?
It is well known that transjunctional logical functions are not definable by junctional functions and negations.

This has a structural equivalent: Bifunctoriality is not definable by functorial distributivity, and other junctional rules.

Furthermore, a new abstraction is achieved with the consideration of the matrix-constellations of functions only. Neither decidablity and definability of distributed contextural logical formulas is here in the focus but just the different places in the matrix where the parts of the complex formulas are taking place.

Hence, how to define constellations?

One answer is given by the introduction of the super-operators sops = {id, perm, red, repl, iter, bif}.
Hence, the question transforms to the question of the logical definability of the super-operator transformation in the domain of logic..

From the point of view of matrix-distribution, constellations like “laa” and “raa” are equivalent. But also “taa” as “laa.” “aaa”. “raa” are equivalent too. And more: the conjunctions “aa” might be replaced by disjunctions “oo”, or even by a combination of “a” and “o”, “ao” and “oa”.

A chain of abstractions
Matrix pattern(Mtypeset structure ) --> [α,β,γ,δ]-distribution --> π-value distribution.

A further abstraction leads directly to the value independent constellations of morphogrammatics. On a morphogrammatic level, combinatorial questions had been elaborated in extenso.

Example

pattern(Mtypeset structure):

typeset structure

The constellation pattern(M) has at least three unified main realizations: unif(raa), unfi(raa) and unif(taa), and additionally the secondary junctional combinations, like “tao”, “toa”, “too”, etc.

[α,β,γ,δ]-distribution:

typeset structure        typeset structure    

Again, α-β-constellations have different value realisations π (α, β). Nevertheles, their combinations, say conjunctions with implications, have to consider their mediation rules.

π-value distribution:

typeset structure


typeset structure

The constellations [raa] and [laa] are equivalent on the unificational level but different on the value level of the concrete formulas. Hence,
[laa]:typeset structure[raa]: typeset structure, and [laa]: typeset structure != typeset structure.

Transformations
How to transform constellation M1 into constellation M2?:
Formaly, it is a reduction: red2.3 : M1 --> M2.
How is this reduction realized on the logicl level?

typeset structure =>  typeset structure


Take Xtypeset structure =  typeset structure     


with (Xtypeset structure ooo neg1(Xtypeset structure)) we get [ag1.1, X3.1, X3.3]

                                             typeset structure,   
               
and with ((Xtypeset structure ooo neg1(Xtypeset structure)) ooo neg3(Xtypeset structureag1.3, ag3.3]

                                                     typeset structure .

2.6.  Abstractions: Matrix, super-operators, unification, tableaux

2.6.1.  Matrix abstractions

H = (X laa Y) iij (X laaY) f1 : H5                                                             ...                                                  Sys 3.3       <br /> xx

2.6.2.  Activity patterns

<br />    (O   O   O)     =>  _ f1 : H5    (R ...                          3                    3.1                          3.2                 3.3

<br /> Processor   model   for   f1H5 : <br /> Multi - Processor - System for matrix - distrib ...  <br /> ( intra - process : {append, remove, leave}, inter - process : {send, receive}  ) . <br />

(                                                                                              ...                                                                                             <br />

<br /> The   matrix   development   as   a   concurrent   procedure   with   spawn <br /> &nbs ... TeXtures, An application 2005 <br /> Available at : http : // works . bepress . com/thinkartlab/21

2.6.3.  Extended Smullyan unification

Unification                                                                                    ...                                     trans -                                         junctive Null

f1H5 = (X laa Y) iij (X laaY)         (0)

    f1H5                                                                                       ...                                                                                                 []


typeset structure

2.7.  Extension mechanism for polycontextural logics

2.7.1.  Modular compositions

The inversion of decomposition of logical functions is the action of composition. Both are based on the principle of polycontextural modularity.

2.7.2.  Example of a 4-contextural constellation

H = X <> ∧ ∨ ⊃ ∨ <> Y : (X taoiot Y) H   = X ^(3)  ...                      -                                             3.6                        4.6

<br /> (ta oiol                                                1                               ...          -                     4   3                 -                     -                     -

<br />                              O                    O                     ...           [t3 .6, f3 .6]               [t4 .6, f4 .6]               O                            O

<br /> Distributed   formulas : <br /> <br /> (X <>     Y)                       ...                     3.6                                                                        4.6

2.8.  Metatheoretical laws for polycontextural logics

2.8.1.  Distributed duality laws

Metatheory of polycontextural logics is just in its beginnings. Nevertheless, there are many insights, elaborations and results been published in earlier work, beginning with my Materialien 1976.

An important metatheoretical principle in classical formal theories and logics is the “duality principle”.

"The Duality Principle for Categories states
Whenever a property P holds for all categories, then the property Pop holds for all categories.” (Herrlich, 2004, p. 27)
http://katmat.math.uni-bremen.de/acc/acc.pdf

Mario José Caccamo, A Formal Calculus for Categories, gives a classical definition of Herrlich’s category-theoretical principle of “get two for the price of one":

"Duality
A category C gives rise to another category by just reversing all the arrows. This new category called the dual or opposite is denoted by Cop. The composition of the arrows in Cop can be expressed in terms of the arrows in C by reading the composition
in the reverse order: g o f in Cop uniquely corresponds to f o g in C. In the same spirit, a functor F : C -> D can be dualised to obtain a functor Fop: Cop -> Dop.
More generally a statement S involving a category C automatically gives a dual statement Sop obtained by reversing all the arrows. This is known as the duality principle.”
http://www.brics.dk/DS/03/7/BRICS-DS-03-7.pdf

A simple application of the duality principle is known in classical logic as the De Morgan laws. As much as logical functions are disseminated, De Morgan too is not escaping its matrix-dissemination (Kaehr, Materialien, 1976).

2.8.2.  Hierarchic and heterarchic understanding of duality

The hierarchy of duality
Also duality means that the dual-parts are of equal value (meaning, relevance) there is nebvertheless a clear hierarchy set between the first and the second of a duality.
"Buy one, get one for free”: this implies a succession and therefore a herarchy. And equally by dual ‘inversion’:
"Get one for free, buy one”.

C = (Cop)op:
C--> Cop --> (Ctypeset structure --> C, equally,
Cop --> (Ctypeset structure --> C --> Cop.

The heterarchy of duality

C ∐ Cop -->  typeset structure .
The categories or processes of “buy” and “get” are interacting simultaneously together. Its simultaneity is reflected or conceived from a third position as a triadicity of “neither-nor” or of “both-and” as [C, Ctypeset structure.

Quadralectics of the duality
A further concretization of the duality of C and Ctypeset structureis achieved with the full ‘quadralectics’ of  Q = (C, Cop, [C, Cop], {C, Cop}), with
C             : position,
Cop          : opposition,
[C, Cop]   : neither-nor, rejection
{C, Cop}  : both-and, acception.
http://www.thinkartlab.com/pkl/lola/Quadralectic%20Diamonds/Quadralectic%20Diamonds.pdf

2.8.3.  Trans-contextural duality principle

But a much more interesting question, based on the insights of categorial interchangeability, arises: Is there a duality between composition and dissemination? That is, is there a kind of a duality between the “operators” “o” and “∐”? A positive answer would establish a new kind of duality:the trans-contextural duality between composition and dissemination. A further transclassical duality principle is established between transpositional  and replicational combinations of polycontextural complexions.

As far as there is systematically no “position”, C, without its (dual) "opposition”, Cop, and vice versa, there are no compositions without disseminations, and vice versa, there are no disseminations without compositions. Hence, there is a systematic, i.e. a meta-theoretical duality established between intra-contextural compositions (combinations) and inter-contextural disseminations of a polycontextural complexion.

This kind of trans-contextural duality is staged by the interplay of proemiality.

Trans-duality of combination and dissemination:

D (o, ∐) = typeset structure <==> typeset structure .

Trans-duality is not less self-referential, i.e. proemial, than De Morgan duality but well-reflected in its super-additivity.

Duality in the mono-contextural sense as the duality principle is achieved by a dissemination into itself, i.e. a option or positioning (Setzung, Fichte) of the epistemé to uniqueness.

D (o , ∐ = 1) = d (o) = (o) : <br /> d (o) ≡ d (X) o d (Y) = d (X o Y) : mono - contextural duality principle .

3.  Remarks on a more mathematical formalization

3.1.  Pfalzgraf’s fiber bundle approach: linear-indexed fibered bundles

3.1.1.  Free and Derived Logical Fiberings

Some citations:

"Logical Fibering can be seen as a methodology in symbolic computation. We have thus a direct link between symbolic computation and AI.
http://www.tmrfindia.org/ijcsa/v9i24.pdf

A Logical Fibering is a triple (E, π, B). E is called total space, B base space, and π : E --> B is called projection map. For b ∈ B the preimage set of all x ∈ E such that π (x) = b, is called Fiber over b (Pfalzgraf, 1991).

"The global set of truth values, hence, is Ω = {a, b, c}. This global logic shall be decomposed to the three classical two valued logics Li, i=1,2,3 (with local values {Ti, Fi})The total universe of available local values is Ω3 = {T1, T2, T3, F1, F2, F3}. The decomposition is done by finding suitable equivalence relations on Ω3 such that the set of residue classes Ω:= Ω3/≡ yields the global truth value set Ω = {a, b, c}. The respective logical connectives (the “AND” operation in the current case) shall be implemented by local logical connectives in the subsystems.

[Graphics:HTMLFiles/Notes on Polycontextural Logics_137.gif]

"The decomposition method is illustrated by Figure 2-13 (adapted from [PFA95]). Firstly, from thetruth table in L we derive three sub matrixes (defined by their limits): the {1,2}-sub matrix, the {2, 3}-sub matrix and the {1, 3}-sub matrix, considering that the {i, j}-sub matrix consists of the elements {(i, i), (i, j), (j, i), (j, j)}.

In the above case it may be observed that each sub matrix gives the values of a classical conjunction truth table, which may be expressed by xtypeset structure respectively. The present relation may furthermore be modeled by the mediation scheme in Figure 2-11 as the encountered relation follows T1≡ T3; F1≡ T2; typeset structure≡ F3 (see above). Finally, it may be expressed by the bivariate operation X typeset structureY [PFA95]."
http://www.iks.kit.edu/fileadmin/User/Calmet/dissertationen/diss_Schneider.pdf

"Remark: The compatibility condition with respect to the three suboperations (submatrices) can be expressed as follows (cf. [20]): The three 2x2-matrices have to be merged to a 3x3-matrix scheme along the diagonal of the 3x3-matrix such that the corresponding diagonal elements match (i.e. the 2x2-matrices are the suitable submatrices). In this sense our decomposition method is the reverse process to this merge.”
http://www.rac.es/ficheros/doc/00158.pdf
[20]: J. Pfalzgraf. Logical fiberings and polycontextural systems. In Fundamentals of Artificial Intelligence Research,
Ph.Jorrand, J.Kelemen (eds.). Lecture Notes in Computer Science 535, Subseries in AI, Springer Verlag, 1991.

3.2.  Matrix formalization: tabular-indexed fibre bundles

3.2.1.  Notes on a natural extension of Pfalzgraf’s approach

Translation table (  Pfalzgraf ' s linear - Fibre bundle       & ... ;                

"A Logical Fibering is a triple (E, π, B). E is called total space, B base space, and π : E --> B is called projection map. For b ∈ B the preimage set of all x ∈ E such that π (x) = b, is called Fiber over b (Pfalzgraf, 1991)."

3.2.2.   Tabular examples

Total functions: Ftot: (i, j) --> (i, j)

F  _ oao : : o  _ 1.1 : (1, 2) --> (1, 2 ; 1) a  _ 2.2  : (2, 3) --> (2, 3 ; 2) o  _ 3.3 : (1, 3) --> (1, 3 ; 3) .

(oao                                                    1                                      ...                                                                (1, 3)    -         -         1   3

Ftypeset structure:
o1.1: (1, 2) --> (1, 2;1)
atypeset structure: (2, 3) --> (2, 3;2)
o3.3: (1, 3) --> (1, 3;1).

(oio                                                    1                                      ...                                                                       (1, 3)   1   2    -        -

Partial functions Ftypeset structure
Transjunctions: Ftrans: (i, j) --> ((i, j1),  (i,jtypeset structure,..., (i,jn)
Foto:
o1.1: (1, 2) --> (1,2;1)
ttypeset structure (2, 3) --> (2, 3;1), (2, 3;2), (2, 3;3)),
o3.3: (1, 3) --> (1, 3;3)

(oto                                                    1                                      ...                      (1, 3)                  -                       -                       1   3

4.  Logic programming in the field

4.1.  Logic and programming

"Many AI practitioners have shied away from using standard logic programming languages as the knowledge representation language in AI systems, partly due to the diffculty associated with representing uncertain, incomplete, or conflicting information in such languages. The root of these diffculties is the inherent limitations of first-order logic as the basis of the standard logic programming systems. One such limitation is the monotoniciy of first-order logic which makes it unsuitable as a mechanism for revisable reasoning. Another important limitation stems from the all-or-nothing nature of classical first-order logic: statements can be evaluated to be completely true or completely false. Intelligent agents, however, must often deal with information which is uncertain, or incomplete.

"The above brief discussion suggests that such systems must have two common characteristics: they must rely on the expressive power of an underlying multi-valued logic which can deal with contradictory as well as incomplete or uncertain information, and secondly, such systems should be able to interpret statements not only based on their truth or falsity, but also based on some measure of the knowledge or information contained within those statements.”
Bamshad Mobasher et al, Algebraic Semantics for Knowledge-based Logic Programs
http://maya.cs.depaul.edu/mobasher/papers/wudds94.pdf

The statement in the citation “interpret statements not only based on their truth or falsity, but also based on some measure of the knowledge or information contained within those statements.” hints to another chance of modeling, especially if connected with its first part ”they must rely on the expressive power of an underlying multi-valued logic which can deal with contradictory as well as incomplete or uncertain information”.

It seems not to be a too wild decision to opt for a polycontextural interpretation of the proposed situation.
The “the measure of knowledge” shall correspond to the measure of the dissemiantion of contextures. And the “power of multi-valued logic” gets a modeling by the polycontextural logic of the disseminated contextures. But that’s not working without some subversion. Contextures are corresponding to “workspaces” in the sense of Fitting’s theories of logic and computation. And, obviously, there is just one and only one ‘workspace’ accepted by Fitting’s approach.

Hence, each contexture contains ‘knowledge’, and each contexture is ruled by its logic. The dissemination, i.e. distribution and mediation, of logics is defined by the pylycontextural ‘multi-valuedness’ of the complexion of contextural logics. The minimum logic of a contexture is a 2-valued logic. The ‘multi-valuedness’ of the complexion is build by the mediation of the distributed 2-valued logics. Negation in polycontextural logics is intra-contextural  negation and inter-contextural  permutation.
M Fitting, Negation As Refutation
http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/NegAsRef.pdf

4.2.  Polycontextural logical programming: The SCHELLING turn

"Seine [Schelling, rk] These, es gäbe weder die ´eine Wahrheit´ noch die ´eine Wirklichkeit‘, sondern das Universum sei vielmehr als ein ´bewegliches Gewebe´ aufeinander nicht zurückführbarer Einzelwelten zu denken,  formulierte die entscheidende Aufgabe der
Philosophie der Zukunft: eine Theorie bereitzustellen, die es gestattet, die Strukturgesetze des organischen Zusammenwirkens der je für sich organisierten Teilwelten aufzudecken.“
Gotthard Günther, Nachlass „GG“, 15. Juni 1980

The universe of polycontextural programming is a poly-verse. A poly-verse is an interactional complexion of universes (general domains) of logic and logical programming.

In contrast to a TARSKI-world, such a polyverse of interactivity is called a SCHELLING-world. Tarski-worlds goes back to Leibniz, and Schelling-worlds had been discovered for logic by Gotthard Gunther.

A TARSKI-world is defined by classical logic and programmed by logical programming languages like Prolog.

A simple, and first-step implementation of the dynamic SCHELLING-worlds and their polycontextural logics has been achieved with the tabular matrix-approach of the dissemination, i.e. distribution and mediation, of formal languages, logics, semiotics and arithmetics.
http://memristors.memristics.com/Mereotopology/Mereotopology%20and%20Polycontexturality.pdf
http://memristors.memristics.com/Polyverses/Polyverses.pdf


SCHELLINGtypeset structure = typeset structure


5.  Tabular dissemination of kenomic cellular automata

5.1.  Explicit tabular notation of distributed CAs

As shown in earlier papers, composed cellular automata might be constructed as mediations of classical elementary CAs.
http://memristors.memristics.com/CA-Compositions/Memristive%20Cellular%20Automata%20Compositions.pdf

5.1.1.  Homogeneous compositions

General composition scheme for mediation

typeset structure

Homogeneous compositions
typeset structuretypeset structure” : mediation
typeset structure   

typeset structure


typeset structure=> typeset structure

5.1.2.  Replicational distributions

typeset structure

Replicational example

typeset structure   

typeset structure
                 

Tabular notation:

typeset structure

typeset structure=> typeset structure

5.1.3.  Transpositional distributions

Some transpositional rules <br />             ...  •   -       -         •   -       -         •   -       -          •    -

   <br /> General scheme <br /> c     c     c   => R12  c ...        4   -                     -                                         4                     -

Subsystems : S _ 1^1 = {•, O},    S _ 1^2    = {• ,   O}, &nbs ...                         -         O         -                               -         -         -

<br />    (                                                                          ...                             -         •   -           -                                    -

Tabular notation of kenoCA=1.8.11.13.14 = [10222]

typeset structure

typeset structure

Notes

1 LOLA-proof
         f1: ((X laa Y) iij (X laa Y))


                                 |                                   
              +---------------  ///  ---------------+                
              |                                     |                
              |                      +------------------------------+
      +------ && ------+             |              |               |
      |                |             |      +------ && ------+      |
t1: (X laa Y)    f1: (X laa Y)       |      |                |      |
                                     |t2: (X laa Y)    f2: (X laa Y)|
                                     +------------------------------+
                                                     |                                   
                                 +----------------  ///  ---------------+                
                                 |                                      |                
                                 |                       +------------------------------+
               +---------------- && ------+              |              |               |
               |                          |              |      +------ && ------+      |
               |                          |              |      |                |      |
      +------- || ------+             +-- && --+         |t2: (X laa Y)    f2: (X laa Y)|
      |                 |             |        |         +------------------------------+
      |                 |           f1: X    f1: Y                                       
  +-- && --+        +-- && --+                                                           
  |        |        |        |                         

                                  
t1: X    t1: Y    t1: X    f1: Y                                                         
                                                                       |                                   
                                             +----------------------  ///  ---------------+                
                                             |                                            |                
                                             |                             +------------------------------+
                     +---------------------- && ---------+                 |              |               |
                     |                                   |                 |      +------ && ------+      |
                     |                                   |                 |      |                |      |
         +---------- || ---------+                 +---- && ---+           |t2: (X laa Y)    f2: (X laa Y)|
         |                       |                 |           |           +------------------------------+
         |                       |              +------+    +------+                                       
   +---- && ---+           +---- && ---+        |[f1:X]|    |[f1:Y]|                                       
   |           |           |           |        +------+    +------+                                       
+------+    +------+    +------+    +------+                                                               
|[t1:X]|    |[t1:Y]|    |[t1:X]|    |[f1:Y]|
+------++------+   +------+    +------+         

                                                            
                                                     |                                   
                                 +----------------  ///  ---------------+                
                                 |                                      |                
                                 |                       +------------------------------+
               +---------------- && ------+              |              |               |
               |                          |              |      +------ && ------+      |
               |                    +------------+       |      |                |      |
      +------- || ------+           |[f1:X, f1:Y]|       |t2: (X laa Y)    f2: (X laa Y)|
      |                 |           +------------+       +------------------------------+
+------------+    +------------+                                                         
|[t1:X, t1:Y]|    |[t1:X, f1:Y]|   
+------------+    +------------+                                                         
                                   |                                   
               +----------------  ///  ---------------+                
               |                                      |                
               |                       +------------------------------+
      +------- && ------+              |              |               |
      |                 |              |      +------ && ------+      |
+------------+    +------------+       |      |                |      |
|[t1:X, f1:Y]|    |[f1:X, f1:Y]|       |t2: (X laa Y)    f2: (X laa Y)|
|[t1:X, t1:Y]|    +------------+       +------------------------------+
+------------+                                                         
      |                                   
+-  ///  ---------------+                
|                       |                
+-+       +------------------------------+
|$|       |              |               |
+-+       |      +------ && ------+      |
          |      |                |      |
          |t2: (X laa Y)    f2: (X laa Y)|
          +------------------------------+


      |                                                                                   
+-  ///  ---------------------------------------+                                        
|                                               |                                        
+-+       +------------------------------------------------------------------------------+
|$|       |                                      |                                       |
+-+       |                 +------------------- && -----------------+                   |
          |                 |                                        |                   |
          |                 |                                        |                   |
          |      +-------  ///  -------+                  +-------  ///  -------+        |
          |      |                     |                  |                     |        |
          |      |              +--------------+          |              +--------------+|
          |  +-- && --+         |      |       |      +-- || --+         |      |       ||
          |  |        |         |  +-- && --+  |      |        |         |  +-- && --+  ||
          |t2: X    t2: Y       |  |        |  |    f2: X    f2: Y       |  |        |  ||
          |                     |f1: X    f1: Y|                         |f1: X    t1: Y||
          |                     +--------------+                         +--------------+|
          +------------------------------------------------------------------------------+
      |                                                                                               
+-  ///  ---------------------------------------------+                                              
|                                                     |                                              
+-+       +------------------------------------------------------------------------------------------+
|$|       |                                                                      |                   |
+-+       |                     +---------------------------------------------  ///  -------+        |
          |                     |                                                           |        |
          |                     |                                                    +--------------+|
          |         +---------- && -----------------------+                          |      |       ||
          |         |                                     |                          |  +-- && --+  ||
          |         |                                     |                          |  |        |  ||
          |   +---- && ---+                 +----------  ///  -------+               |f1: X    f1: Y||
          |   |           |                 |                        |               +--------------+|
          |+------+    +------+             |                 +--------------+                       |
          ||[t2:X]|    |[t2:Y]|       +---- || ---+           |      |       |                       |
          |+------+    +------+       |           |           |  +-- && --+  |                       |
          |                        +------+    +------+       |  |        |  |                       |
          |                        |[f2:X]|    |[f2:Y]|       |f1: X    t1: Y|                       |
          |                        +------+    +------+       +--------------+                       |
          +------------------------------------------------------------------------------------------+
    

       |                                                                             
+-  ///  ------------------------------------+                                     
|                                            |                                     
+-+       +------------------------------------------------------------------------+
|$|       |                                                    |                   |
+-+       |                             +-------------------  ///  -------+        |
          |                             |                                 |        |
          |                             |                          +--------------+|
          |               +----------  ///  -------+               |      |       ||
          |               |                        |               |  +-- && --+  ||
          |               |                 +--------------+       |  |        |  ||
          |      +------- && ---+           |      |       |       |f1: X    f1: Y||
          |      |              |           |  +-- && --+  |       +--------------+|
          |+------------+    +------+       |  |        |  |                       |
          ||[t2:X, t2:Y]|    |[f2:Y]|       |f1: X    t1: Y|                       |
          |+------------+    |[f2:X]|       +--------------+                       |
          |                  +------+                                              |
          +------------------------------------------------------------------------+
     

      |                                                 
+-  ///  ----------------------+                       
|                              |                       
+-+       +--------------------------------------------+
|$|       |      |                                     |
+-+       | +-  ///  ----------------+                 |
          | |                        |                 |
          |+-+       +--------------------------------+|
          ||$|       |               |                ||
          |+-+       |      +------- && ------+       ||
          |          |      |                 |       ||
          |          |      |                 |       ||
          |          |  +-- && --+        +-- && --+  ||
          |          |  |        |        |        |  ||
          |          |f1: X    f1: Y    f1: X    t1: Y||
          |          +--------------------------------+|
          +--------------------------------------------+
      |                                                 
+-  ///  ----------------------+                       
|                              |                       
+-+       +--------------------------------------------+
|$|       |      |                                     |
+-+       | +-  ///  ----------------+                 |
          | |                        |                 |
          |+-+       +--------------------------------+|
          ||$|       |               |                ||
          |+-+       |      +------- && ------+       ||
          |          |      |                 |       ||
          |          |      |                 |       ||
          |          |  +-- && --+        +-- && --+  ||
          |          |  |        |        |        |  ||
          |          |f1: X    f1: Y    f1: X    t1: Y||
          |          +--------------------------------+|
          +--------------------------------------------+
     

      |                                                             
+-  ///  ----------------------------+                             
|                                    |                             
+-+       +--------------------------------------------------------+
|$|       |      |                                                 |
+-+       | +-  ///  ----------------------+                       |
          | |                              |                       |
          |+-+       +--------------------------------------------+|
          ||$|       |                     |                      ||
          |+-+       |         +---------- && ---------+          ||
          |          |         |                       |          ||
          |          |         |                       |          ||
          |          |   +---- && ---+           +---- && ---+    ||
          |          |   |           |           |           |    ||
          |          |+------+    +------+    +------+    +------+||
          |          ||[f1:X]|    |[f1:Y]|    |[f1:X]|    |[t1:Y]|||
          |          |+------+    +------+    +------+    +------+||
          |          +--------------------------------------------+|
          +--------------------------------------------------------+
      |                                                 
+-  ///  ----------------------+                       
|                              |                       
+-+       +--------------------------------------------+
|$|       |      |                                     |
+-+       | +-  ///  ----------------+                 |
          | |                        |                 |
          |+-+       +--------------------------------+|
          ||$|       |               |                ||
          |+-+       |      +------- && ------+       ||
          |          |      |                 |       ||
          |          |+------------+    +------------+||
          |          ||[f1:X, f1:Y]|    |[f1:X, t1:Y]|||
          |          |+------------+    +------------+||
          |          +--------------------------------+|
          +--------------------------------------------+
    

      |                    
+-  ///  --------+        
|                |        
+-+       +---------------+
|$|       |      |        |
+-+       | +-  ///  --+  |
          | |          |  |
          |+-+       +---+|
          ||$|       |+-+||
          |+-+       ||$|||
          |          |+-+||
          |          +---+|
          +---------------+
eof