( U | ( W | W ) ) , U |- W
for Cornejo and Viglizzo.
Given your comment, look up "differential ontology" and consider this as a "branch point" relative to the objectual ontologies of domains of discourse.
The first-order paradigm is not exactly metaphysics. If one is justifying the necessary truth of reflexive equality statements with the law of identity, it is metaphysical. But, the necessary truth of reflexive equality also follows from declaring mathematics to be analytical. A word ought to carry the same meaning (warrant for substitutivity in a logical calculus) with every occurrence.
So, you arrive at a second "branch point" by which the substitutivity warrant becomes the denial of distinctness. To make sense of this, you must distinguish between equality, discernibility, and distinctness. This requires an observation from first-order model theory regarding the persistence of truth for existential formulas with respect to model extensions (upward persistence) and the persistence of truth for universal formulas with respect to submodels (downward persistence). If one is not convinced by logicism and rejects the influence it has had on formalist foundations, this actually corresponds with the characterization of the consistency problem as described by Hilbert and Bernays. They interpreted intuitionistic criticisms in terms of a paradigm difference in which a "given" domain of discourse with well-construed (decidable) equality relations could not be assumed. Moreover, they explicitly understood the consistency question as obfuscating any role for existential import.
The paradigm difference expresses itself through description theory and the use of Tarski's transitivity axiom to embed existential import into equality statements.
It is possible to write a formal sentence "introducing" a discernibility relation that is irreflexive and symnetric with no quantifiers other than the two universal quantifiers with global scope.
It is possible to write a formal sentence "introducing" a distinctness relation whose two nested universal quantifiers carry no existential import. Related by a disjunction, the denied distinctness relation is expressed by the conjunction of existential subformulas.
The correlate to first-order formalism is to warrant substitutivity with a denied discernibility relation. Following the terminology in description theory (outside of received studies in mathematical logic) call this the attributive paradigm (Russellian).
Among the logics which manage existential import, one has free logics. In particular, there is a close connection between recursion theory and negative free logic because recursion theory admits a relation by which arbitrary expressions are comparable. Defined expressions are discernible from undefined expressions, and, all undefined expressions are indiscernible from one another. This corresponds with the principle of indiscernibility of non-existents in negative free logic.
Thoralf Skolem's paper on arithmetic and "the recursive mode of thought" has generally been interpreted as primitive recursive arithmetic relative to Goedel's effective (and platonistic) characterization of recursive arithmetic. Such an analysis is based on the comparison of "quantifier-free" methods. If, however, you read Skolem's paper, he is clearly critical of Russell's description theory. Much like Kant's call for the development of geometries different from Euclidean geometry (see Ewald's anthology), Skolem's criticism of Russellian description theory is lost in folklore.
It is well known that one can prove reflexiveness from transitivity and symmetry. If one takes Tarski's transitvity axiom for equality as the "symbol introduction" for the sign of equality, then one need only formulate a symmetry axiom to support a logic supportive of a non-Russellian description theory.
Implementing this, however. requires both discernibility and distinctness.
One criticism of the use of descriptions is that one cannot assure "singularity." So, if one can use a formula to introduce a constant using a description, one must first declare or otherwise prove that satisfying instances are indiscernible from one another. This is a different problem from how existential priority cannot be expressed within the first-order object languages.
What this also means is that a logic supporting non-Russellian descriptions does not even work like Russellian description.
A basic existential axiom will have two existential quantifiers
So that the first quantifier can become a universal quantifier,
Ax( x = a IFF Ey Phi(x,y) )
The quantifiers here are restricted with respect to reflexive equality statements,
IF a=a THEN Phi(a)
a=a AND Phi(a)
With regard to descrpition theory as discussed outside of received views for mathematical logic, these would more properly be called demonstrative descriptions. The kind of problematic description theory associated with Frege's idea that the word "the" is sufficient for "singular" reference is properly called referential description.
Consequently, this approach should be called the demonstrative paradigm as a contrast to the attributive paradigm of Russellian description.
As a "branch point" this is all motivated by the fact that the necessary truth of reflexive equality statements does not follow from Tarski's semantic conception of truth.
Analytical philosophy makes a knowledge claim--- "mathematics is analytic"--- before applying Tarski's truth analysis.
This is why a semi-intuitionist of Borel's persuasion would take issue with characterizing semi-intuitionism using formal systems. It is not a domain of discourse with decidable equality relations which is "given." It is the experiential continuum which is given. For Borel, at the time that he lived, this would have been equivalent to accepting real spaces as given through witnessability. This is why he is associated with problems in "descriptive set theory."
The development of these ideas on non-Russellian description can be traced to the inquiries into "slingshot arguments." I received some clarity on "demonstrative description" through Stephen Neale's work in fact theory.
Tarski had used the liar paradox to demonstrate that his conception of truth had correspondence with naive notions of how truth related to language. Frege had used a square of opposition to demonstrate correspondence with analyses of traditional logic such as Port Royal. Naturally, I have the proof schemes corresponding with Skolem's "descriptive function" explanation of numeric succession. So, while I am well aware that there may be fatal errors in my work because of the intrinsic difficulty, I am not making these remarks flippantly. Of course, my work will never see publication. I have no credentials and no one is interested in mathematical foundations that question analytical philosophy and its apparent determination to use mathematics to ground reductionism to physics as "truth."
Being the ever-competent dialectician, Russell actually discussed something similar to this paradigm in Chapter 19 of "Principles of Mathematics" under the classification "the relative view of quantity." It is similar with respect to the fact that the necessary truth of reflexive equality statements is not assumed.
Good luck in finding answers to your questions. Hopefully, you will not have to work as hard as I have.