[FRIAM] TheoremDep

[Steven A Smith]

Glen -
> Yes, I can see that.  The answer(s) to the question, though, is still interesting.  I tried to allude to it by offering the 3 alternatives: chain, tree, mesh from the foundations up to "sophisticated" conclusions.  It seems to me that if one reacts to something like TheoremDep with a sense of "concatenation", then that implies they think about this sort of reasoning as a chain or, at least, a tree.
Reading ahead, I want to respond to this with anticipation toward what
you write in the next paragraph.  When I first saw the TheoremDep, I
thought of a tree which is pretty close to a DAG because of the obvious
constraint that we don't want circular dependencies/logic in our
proofs.   I didn't think of concatenation as much as composition.   In
principle, one could unroll or serialize all the dependencies of a
theorem and include them in the proof.   I remember when I took a
(belated?) course in the History of Mathematics near the end of my BS in
math.   I think I took it as credit toward a history course, though it
was at least 2nd year math in some of it's content.   One interesting
point was the clay-tablet records from Mesopotamia where algebraic
solutions of (all?) quadratics and many cubics were enumerated, but
redundantly across different contexts, expressed as "story problems".  
It may not have been as bad as offering the same solution to determining
crop yields for wheat and rye in separate story-problems, but less
immediate abstractions/analogies would have been redundantly "solved".
> For context, I have the same problem with what we've (I've?) come to call "physics-based biological modelers".  Their focus is on physically realistic simulation engines, upon which they implement chemically realistic reactions, upon which they implement biologically realistic mechanisms. 
I think there is good motivation for believing that Chemistry "emerges"
from physics and Biology "emerges from" Chemistry and Physics.   At the
same time, the point of emergent phenomena is that the governing
"forces" between entities are NOT directly or obviously based in the
next lower level of abstraction.   So, while Metabolic Networks *DO*
operate on Chemistry (and maybe some Physics like diffusion?), the
governing logic IS relational, as you point out.   Higher levels of
abstraction like protein expression networks and (as my last example on
Gene Ontologies represent) higher levels of abstraction have their own
logic which "emerges" from the lower levels.
>  I (being the soft-X type of person I am), tend to focus on *relational* modeling, which can be usefully applied at any layer of the heterarchy. 
I think that is the *point* (if we need to invoke a Final Cause here) of
these "layers" of emergent functionality.   To support more and more
complex types of relations (not just linear, heirarchical, etc.)...   I
haven't thought it through well, but I'm guessing that (for example),
metabolic networks, or gene expression networks have a qualitative
higher complexity than *most* physics phenomena (though Feynman diagrams
describe "relations" between subatomic particles, and there MAY be
known/interesting/relevant examples with similar complexity?)
>  Or, at least, I prefer a "middle out" method, starting at the layer where you understand/care the most.  The physics-based people tend to think in terms of chains and trees, whereas the relational people tend to think in terms of networks.  I call the phyics-based people "Grand Unified Modelers" because they're seeking the One True Model.  ... very Monistic.
I do believe that there is a conceit of Physics that if there is a place
for a Monistic GUT it would be in Physics,  but I think there is room
for the same in Chemistry, Biology, Sociology, Economics, etc...  within
the domain circumscribed by the "floor and ceiling" of emergence(s)?
>> The old fascination with why mathematics (as a pure abstraction) seems to line up so well with physical reality comes up again.   I think there is some kind of anthropic principle involved?   Do you have any parallax on this?
> I tend to believe it boils down to *attention*, intentionality, purposeful behavior.  It strikes me that math can unambiguously describe *anything*, real or fantasy.  And where non-ambiguity is required, math will be successful. 
I think this is accurate, maybe tautological...
>  Bands like Tool argue against me in some sense, because they use a lot of math in the creative composition of their tunes and lyrics.  But, then again, they're nerds and have high expectations for how tightly a performance hangs together ... which is, again, a requirement for non-ambiguity. 
I think the point in "interesting" endeavors is to provide enough
familiar structure to be "familiar" and then add to (abberate?) it
enough to be "surprising".  
>  My guess is math would be less successful if we tried to use it to, say, foster creativity in children ... at least for now.
I would claim that more than a little of my own personal creativity was
based IN mathematics as a child/adolescent.   It was the abstract
language of math that allowed me to see (and manipulate?) patterns
across more disparate domains than "natural language" allowed.   It
wasn't the lack of ambiguity (because my clumsy application
re-indroduced ambiguity) in Math that drew me, but the ease and
expressiveness of abstraction.
> The author of TheoremDep cites Metacademy (here's a good example: https://metacademy.org/graphs/concepts/incompleteness_of_set_theory#focus=mh2y5zs9&mode=explore).  That strikes me as a system amenable to edge weight adjustment.  E.g. How important is it to understand Russell's Paradox, really, for understanding how ZF fits into this "lineage of reasoning"?
I am working on a project involving the quantification and visualization
of uncertainty. In that it is implicit that we want to propogate
uncertainty through many different processes or models or scenarios.  It
seems somewhat to be a parallel to what you describe here around MetAcademy.
> the kind of graph I'm imagining, it may be better to imagine the lemmas as edges and the nodes as something else (conceptions of reality, maybe?).  Lemmas would, then, be transitions from one state to another.

I do see the (potential) value of considering this "dual" of the
dependency graph... a Lemma as you say, can be considered a transition
from one state of knowledge or conviction or proof to another state.

- Steve

>