Given:
Rules R
Initial finite Quilder Q1
Desired finite Quilder Q2
Search for derivation of Q2 from Q1 using R
Defn: a Quilder consists of:
A porder P
Two sub-porders C and F
An equivalence relation W on P
Such that lifting holds:
o----->o o----->o
| __ /| | __ /|
c| /| |wf and wc| /| |f
v / | v v / | v
o----->o o----->o
Rules:
Decomposition:
If A-->B is unmarked, exists C s.t. A-wc->C-f->B
If A-->B is unmarked, exists C s.t. A-c->C-wf->B
(equiv (in porders): if A-->B is unmarked, exist C,D s.t.
A-wc->C-cf->D-wf->B)
If A-w->B, exists C s.t. A-wc->C-wf->B
Limits:
Can add infs and sups of arbitrary subsets of P;
C and WC are closed under pushouts, and F and WF under pullbacks.
Note subtlety - the fact that an object is an inf/sup is *not* just a
property of the given Quilder - so this data should form part of our
structure.
Note also that we may, after introducing a sup/inf, end up proving
that it is isomorphic aka equal to a pre-existing point.
Closedness:
Given an arrow, spawn a subinstance, add 2 new objects (and 3 arrows)
forming a lifting diagram, and try to prove existence of a lifting
arrow. If succeed, label the original arrow with c/wc/f/wf as
appropriate.
Alternatively: we can just add this new structure to our current
Quilder, and record the information that the new -wf-> is a 'test
arrow' for our potential -c->, i.e. that if ever we obtain a lifting,
we should mark it c.
Applying rules:
A rule produces a Quilder from a given Quilder by applying the rule then
closing off to form porders and equiv rels in obv ways.
A derivation of Q2 from Q1 consists of applying rules to Q1 to form some
super-Quilder of Q2.
So Q2 follows from Q1 iff Q2 is a sub-Quilder of the unique finite Quilder
generated from Q1 abiding by all the rules.
Stupid search algorithm: generate that finite Quilder, take all sub-Quilders.
This is pretty damned stupid.
Notes on implementing a Quilder as a data structure:
Can implement finite porders as "chainmerge" objects - store a chain
decomposition, and for each object x for each chain C_i the index of the
greatest element of C_i dominated by x. Then comparisons are constant
time, and, ju'ocu'i, adding objects and relations are efficient too.