Short version of my question.
What formal logical systems can represent, and seem robust against, the Liar Paradox?
N.B. I would like to avoid reference to truth-values, except inasmuch as they provide semantics for the formal system. Specifically, within the logic, I would like to say "P is true" if and only if P is derivable from whichever premisses we decide to grant in the formal system; and I would like only to say "P is false" if and only if ¬ P is similarly derivable. For instance, I accept that this means that Peano Arithmetic has statements where P ∨ ¬ P is true, but where neither P nor ¬ P are true (nor false). What I am concerned with is derivability.
I would like to make clear precisely what I'm asking. Apologies for the length of the question: please suggest a way that I might make this question more concise.
This question is about formal logical systems, which I will take (somewhat fuzzily) to mean a formal system of manipulating symbols, which we suppose to have some sort of meaningful semantics in terms of "truth" and/or "falsehood", and where we have some plausible rules of inference involving &, ∨, ¬, etc. in their familiar roles as logical connectives. That is: fragments of this system at least are clearly intelligible as representing logical reasoning — there is a transformation which would allow us to obtain a string similar to P ∨ Q from either P or Q, either of which we could obtain from P & Q, and so forth.
For a typical paradox X of logic, we shall say that a logical system represents the paradox X if we judge that the formal system can capture the syntactical elements of the paradox; and we shall say that it suffers from the paradox X if the logical system is inconsistent (we may derive absolutely any well-formed formula) essentially as a result of the fact that it represents X. We will say that the formal system is (or seems) robust against X if we cannot demonstrate that it suffers from X.
A simple formal model of self-reference
I want to consider formal logical systems in which we may represent the Liar Paradox, specifically in order to specify a way in which to treat the Liar Paradox as a feature (or a bug) of a formal logical system.
Consider a formal system in which propositions (i.e. strings of symbols) may be referred to by name. The names are labels which are allowed as propositions in well-formed formulae. The semantics of these labels being "names" arises from the fact that they are addressible in a straightforward way: the rules of inference allow for the name A of some proposition P to be substituted with the proposition P itself. (We might naively say that A ≡ P, though technically this would only be a tautology if we also allowed the substitution in reverse as well. We may consider systems in which this is allowed or not; I only assume that "expansion" is a valid transformation.)
The Liar Paradox
We consider a proposition ¬ L (which is well-formed in this system) which we then give the label L. This is then a simple and formalized realization of the Liar Paradox.*
The classic question is what to make of L: is it true or false? In a formal system, the question is instead whether our formal system "suffers". What makes the Liar a "Paradox" is that classical logic does suffer from it. Consider a typical formalization of classical sentential logic. If we grant the Law of Excluded middle, we have
L ∨ ¬ L
from which (by various applications of arguing by dilemma and double negation elimination) we may infer
L & ¬ L
which represents the classical crisis of truth values for L — or more to the point, from which we can infer whatever we like via reductio ad absurdum. In this case, we may say (we must say) that L is both true and false; and furthermore that everything is both true and false.
* Obviously, this is a circular reference, but as something realizable by a formal system it is impeccable — it is left for us to struggle with providing semantics for logical systems in which such things are possible. If one is really concerned about it one can serialize the logical system to preclude circular references, but this is not what this exercise is about.
Using the above (or a similar) system of self-referential logic:
What systems of inference rules (i.e. what formal systems of logic) seem to be robust to the Liar Paradox?
What works consider such rules of inference?
I already know of some obvious candidates — my derivation above already hints heavily at two such systems, for example — but I hope for some help with specific references, to specific formal logical systems, with "semantics" being quite subordinate to syntax.