What is the metamathematical interpretation of knot diagrams?  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".  
 A: Knot diagrams are a special sort of tangle diagrams, so I will reinterpret your question as being about tangle diagrams. Tangle diagrams are a "planar algebra" generated by $\{\text{overcrossing},\text{undercrossing}\}$, so every tangle can be drawn by taking a finite collection of generators, arranging them in a plane, and connecting each of the four "loose ends" on each generator by "bridge arcs" to another of the "loose ends" (of the same or a different generator), or leaving "the loose end" "loose". The relations are Reidemeister relations. If you allow "bridge arcs" to cross (and allow virtual Reidemeister moves), you get virtual tangles, and if not, you get usual tangles.
This is already algebra, but it's algebra in a different sense from "x+3=2" because it takes place in the plane. You could introduce a height function and translate tangles into "algebra" in the old sense, as some other answers suggest, but surely to do so would constitute an act of violence. Maybe it's better (philosophically at least) to widen one's perspective on what constitutes "algebra".
I certainly think that yes, "there are important theorems with no known proof except via diagrams, and nobody knows why". Anything proven by using skein relations fits the bill. Nobody really knows what quantum invariants have to do with 3d topology (other than the Alexander polynomial for links, but the tangle version of the Alexander polynomial also fits the bill), but it's quite clear what they have to do with diagram algebras if they are defined via linear skein relations. 
Surely more than that is true- many invariants of knots extend naturally to invariants of more general "diagrammatic algebras", and maybe this wider context is where we can understand those invariants and where they make more conceptual sense. Maybe coming to terms with "the metamathematics of diagrams" (tangle diagrams, and more general classes of diagrams as well) as a brave new algebra is a fruitful direction of research. I interpret current work of Dror Bar-Natan in this vein.
As a concrete example of where this concept has proven useful, see Zsuzsanna Dancso's thesis, which (building on ideas of Bar-Natan and D. Thurston) explains how considering diagrams of knotted trivalent graphs (a larger "brave new algebra") helps us to understand how the Kontsevich invariant of a framed link changes under handle slides (Kirby 2 moves). Even more so, Bar-Natan and Dancso's forthcoming w-knotted objects project is an example of a setting in which taking "the metamathematics of diagrams" seriously, treating them with respect as a genuine form of algebra, motivates the project and yields substantial dividends, at least in the form of better understanding the Alexander polynomial of tangles.
A: I don't know what you mean by "substitutability a la planar algebras," since I don't know anything about planar algebras, but here's my take. Knot diagrams can be interpreted as (representatives of) certain morphisms in the category $\text{Tang}$ of tangles, which can be succinctly described as the free braided monoidal category with duals on a self-dual unframed object. More precisely, this category has a distinguished set of generators given by all of the structure I just described (the braiding, the self-duality, etc.), and a knot diagram is a description of a certain type of morphism $0 \to 0$ in terms of these generators. 

they are relation-like, relating segments of a link to each other.

The category of tangles is analogous in some ways to the category $\text{Rel}$ of sets and relations; in particular, they are both dagger categories. 

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

I admit I don't really know what you mean by this either. The Reidemeister moves describe certain relations that hold in $\text{Tang}$ between the generators. 

Finally, there's the standard trick of calculating invariants by recursively applying certain skein relations to get to the unknot.

By the universal property of $\text{Tang}$, any self-dual unframed object in a braided monoidal category gives rise to a braided monoidal functor from $\text{Tang}$, which imposes some relations (such as skein relations) on the generators. 
From my perspective the situation is at heart no more complicated than describing a group by generators and relations and naming elements of that group in terms of products of the generators (provided that you've accepted Reidemeister's theorem). 
A: I see this as a general problem in higher dimensional algebra, that there will need to be "higher dimensional rewriting".  John Baez has illustrated the higher dimensional thinking by displaying the picture
$$ ||| \;\; ||| ||  $$
$$||| \;\; ||||| $$ 
which is easily seen to illustrate $2 \times (3+5)= 2 \times 3 + 2 \times 5$ but  the 1-dimensional formula involves various conventions, and is less transparent. We have found diagrammatic rewriting useful in dealing with rotations in double groupoids (with connections), and there is a 3-dimensional rewriting argument in Section 5 of 
F.-A. Al-Agl,  R. Brown, R. Steiner,  `Multiple categories: the
equivalence between a globular and cubical approach', Advances in
Mathematics, 170 (2002) 71-118.
which proves a key braid relation (Theorem 5.2).  
So there is the interesting question of how to cope say with a 5-dimensional rewrite? Maybe computers could handle it? 
These situations could well occur in algebras with partial operations whose domains are defined by geometric conditions, and with strict axioms. 
A: If you want to consider knot diagrams as finitistic algebraic objects, it is not hard to show that they can be encoded as sets.  For example, you may choose to label crossings and line segments between them, then encode the over/under behavior, incidence, orientations, and other decorations using tuples, and finally introduce a notion of equivalence under relabelings.  Any proof using diagrams then has a translation into the algebraic world, but often that translation is too cumbersome to reproduce, and in the real world, you may encounter incomplete proofs.
I agree with your first option in your list, but I feel that the phrase "just a convenience" does not do justice to the power of linguistic and notational choices.  It is often very difficult to find proofs of theorems, and it helps to use any tool available to ease the mental burden.
A: It seems that you may trust algebra more as a solid foundation for how to describe a mathematical object, so you may be interested in the classification of knot diagrams by knot polynomials, such as the Jones Polynomial. 
Additionally, you can note by Alexander's Theorem that every knot can be created by the closure of some braid. Since braids can be defined by a braid group "word", we can describe a particular knot diagram by a word in this language. For example, if we have $\sigma_{1} \sigma_{2}^{-1} \sigma_{1} \sigma_{1} \sigma_{2}$, then it describes some knot diagram and is easier to work with algebraically.
These are, to my understanding, two common approaches to employing the power of algebra to analyze knots by converting knot diagrams into some algebraic representation.
