I am not a geometric topologist, but from looking over papers in the field, it's clear that knot diagrams are a major tool and we know how to use them in a way that is rigorous and trustworthy. My background is in model theory and I am having trouble fitting them into that framework. I'm hoping for pointers to references or a quick sketch of the logical status of these things.

Specific points that I'm hung up on: knot diagrams have nice properties analogous to terms in formulas, like substitutability *a la* planar algebras. On the other hand, they are relation-like, relating segments of a link to each other. On the third hand, the Reidemeister moves seem like a set of formulas in a model-theoretic interpretation (of a "theory" of knot isotopy into a "theory" of graphs.) Finally, there's the standard trick of calculating invariants by recursively applying certain skein relations to get to the unknot.

In other words, I can't see that a knot diagram is always being used as a relation, term, formula, or substructure - it seems like none of these is adequate to fully describe their use.

I can see this playing out in a number of ways:

- Knot diagrams are a tool that can be completely subsumed by algebra in an algorithmic way, and are just a convenience;
- There is a theorem that says proofs using diagrams can be "un-diagrammed", but it's an existence proof
- People keep finding new ways to use knot diagrams in proofs, often by decorating the diagrams with new features like orientations - reproving via alternate techniques is then a useful contribution, but always tends to work out; e.g., we don't completely understand the metamathematics of knot diagrams, but the general shape of things is clear;
- There are important theorems with no known proof except via diagrams, and nobody knows why;
- It will somehow all become obvious if I take the right course on planar algebras, or o-minimal structures, or category theory;
- It's subtle, but was all cleared up by Haken in the 70's;
- Dude, it's just Reidemeister's Theorem, and you need to go away and think about it some more.

Community wiki, in case the right answer is a matter of opinion.

**Update** - Just to be clear, this is not in any way a brief for eliminating knot diagrams - quite the opposite. Knot diagrams are honest mathematical objects, while also serving as syntax for other objects. That seems like a ripe area for mathematical logic.

Also, I'm including partial diagrams, as in skein relations, when I use the phrase "knot diagram".