I agree with the commentators that the question is rather too broad, but here's an attempt to answer it anyway.
Readers of MO will likely have less familiarity with non-mathematical logic, so it might help to begin by skimming the tables of contents of the 18-volume (!) Handbook of Philosophical Logic to get some feeling for what people mean by "philosophical logic." [Edit: The preceding link no longer works; one can find some content using Google Books and the Wayback Machine.] It includes many topics that will likely be unfamiliar to mathematicians, such as temporal logic, multi-modal logic, non-monotonic reasoning, labelled deductive systems, and fallacy theory.
Roughly speaking, philosophical logic is the general study of reasoning and related topics. As in other areas of philosophy, this study is not necessarily formal. However, the success of formal methods in mathematical logic has led philosophers to try to formalize many other kinds of reasoning. Formalized modal logics are perhaps the best known of these. These are not always classified as "mathematical logic" because in mathematics one does not typically reason formally about concepts such as possibility, necessity, belief, etc. On the other hand, once a system of logic has been made sufficiently formal, it can of course be subject to mathematical study. Thus the boundary between (for example) formal modal logic and traditional mathematical logic is somewhat blurry. A notable example of the cross-fertilization that is possible here is Fitting and Smullyan's book on Set Theory and the Continuum Problem, which develops the (highly mathematical) subject of forcing from the perspective of modal logic, providing a fresh and completely rigorous approach to a now-classical mathematical subject.
If I had to summarize in one sentence, I would say that mathematical logic is the subfield of philosophical logic devoted to logical systems that have been sufficiently formalized to admit mathematical study. This is a slightly broader definition of mathematical logic than is customary, but I think it's a good definition in the context of this MO question, which tacitly seems to be asking if mathematicians have anything to learn from so-called "philosophical logic."
I don't mean to give this as a complete answer, but regarding question 2, there have been a great deal of negative results surrounding this problem.
In fact, most of them take the form of showing that any ''reasonably constructive'' (read ''effectively generated'') subrecursive hierarchy of computable functions indexed by paths through Kleene's $\mathcal O$ suffer from definability issues. At the core of each argument, these negative results exploit some variation of Spector's $\Sigma^1_1$-boundedness principle. To illustrate an example, Sacks (located in his Higher Recursion Theory) explored an effective version of this principle as follows:
There is a computable function $\varphi$ such that, for every $x \in 2^{\omega}$, we have that
$x \subseteq \mathcal O \iff \varphi(x) \in \mathcal O$ and $x \subseteq \mathcal O_{\varphi(x)}$
where $\mathcal O_{\varphi(x)} := \left\{ y \in \mathcal O : rnk(y) \leq rnk(\varphi(x))\right\}$, and $rnk(x)$ denotes the rank of $x$, and is measured as an ordinal.
Applying this to our problem (or some variation thereof), any inductive classification of the computable functions on some $\Pi^1_1$-path $\mathcal P \subseteq \mathcal O$ will ultimately "collapse" before all the computable functions have been exhausted at some countable level, which is typically measured as the ordinal height of $\mathcal P$.
As an aside, I think it's interesting to note that Sacks himself gave a lecture where he recalls his conversations with Godel toward the end of his life. In particular, he mentioned a conversation where Godel outlined a list of outstanding problems in mathematical logic which he thought would enliven the subject as a whole. On the list, he suggested the problem of proving the existence of an exhuastive hierarchy of computable functions, and believed that such a hierarchy should exist.
Sacks then goes on to conclude that there is not a lot of evidence supporting Goedel's belief, in view of the negative partial results hinted above. However, Sacks did go on to say that no one has been able to give a real proof that no such hierarchy exists, and so one is left with the feeling that a final solution of this problem is out of reach with current methods.
Best Answer
Yes, this still occurs in modern type theory; in particular, you'll find it in the calculus of constructions employed by the Coq language.
Consider the type called
Prop, whose inhabitants are logical propositions (which are in turn inhabited by proofs). The typePropdoes not belong toProp-- this means thatPropexhibits stratification:However, note that
(forall a:Prop, a)does have typeProp. So althoughPropdoes not belong toProp, things which quantify over all ofPropmay still belong toProp. So we can be more specific and say thatPropexhibits unramified stratification.By contrast, consider
Set, whose inhabitants are datatypes (which are in turn inhabited by computations and the results of computations).Setdoes not belong to itself, so it too exhibits stratification:Unlike the previous example, things which quantify over all of
Setdo not belong toSet. This means thatSetexhibits ramified stratification.So, in short, "ramification" in Russell's type hierarchy is embodied today by what Coq calls "predicative" types -- that is, all types except
Prop. If you quantify over a type, the resulting term no longer inhabits that type unless the type was impreciative (and Prop is the only impredicative type).The higher levels of the Coq universe (
Type) are also ramified, but Coq hides the ramification indices from you unless you ask to see them:Think of
Top.15as a variable, like $\alpha_{15}$. Here, Coq is telling you that if you quantify over the $\alpha_{15}^{th}$ universe to produce a result in the $\alpha_{16}^{th}$ universe, the resulting term will fall in the $max(\alpha_{15}+1, \alpha_{16}+1)^{th}$ universe -- which is at least "one level up" from what you're quantifying over.Just as it was later discovered that Russell's ramification was unnecessary (for logic), it turns out that predicativity is unnecessary for the purely logical portion of CiC (that is,
Prop).