I am not sure what you are trying to do here. Are you saying that "c causes e iff..." is a theory and the same sentence with x and y standing for c and e is its Ramsey sentence?

I am examining correct formalization of Lewis' counterfactual analysis of causation. Lewis gives a semi-formal analysis, a combination of schematic letters (e.g. c, e, ...) and English expressions (e.g. causes, ...). What I am looking for is a formal analysis of causation symbolized completely down to schema.

By formal analysis do you mean specifically the positivist approach of defining all theoretical terms through observable properties? I think it would be problematic to define counterfactuals this way. And that makes me think of a problem with this definition of causation:

If c is not the case, then something else is the case, right? What could be the case then? And couldn't some alternate state of affairs result in the same effect? Suppose we see a red ball strike a yellow ball and then the yellow ball rolls into a pocket. We would normally say that the red ball striking the yellow ball (c) caused the latter to roll into a pocket (e). But what would be a counterfactual to that? Suppose that a blue ball struck the yellow ball instead of the red ball, with the same consequences. (c) is not the case, but (e) occurred anyway. Does this mean that (c) was not the cause of (e) after all? It seems that on this definition of causation either there is no multiple realizability of effects or there is no causation - either option is implausible.

As Sophisticat points out, as soon as we start considering counterfactuals, we get into the devil of a mess. And counterfactuals is what's going on when we write 'if (something that we have observed to have happened) were not the case, then ....'

A less troubled approach is to define cause in terms of agreed initial conditions and scientific theories. Try reading this for an approach that does it that way.

I am interested in logical forms of analyses. Or, I am interested in how to construct definitions in symbolic logic precisely.

xCy = x causes y
xRy = x is correlates with y
xNy = x is correlated coincidentally with y

1. xRy
2. ~yCx
3. ~(Ez)(zCx AND zCy)
4. ~xNy

Then

xCy <-> 1 & 2 & 3 & 4

:P

1. Rxy
2. ~Cyx
3. ~(∃z)(Czx & Czy)
4. ~Nxy
5. Show Cxy ↔ (Rxy & ~Cyx & ~(∃z)(Czx & Czy) & ~Nxy)
6. Show Cxy → (Rxy & ~Cyx & ~(∃z)(Czx & Czy) & ~Nxy)
7. Cxy A
8. Show Rxy & ~Cyx & ~(∃z)(Czx & Czy) & ~Nxy
9. Rxy & ~Cyx & ~(∃z)(Czx & Czy) & ~Nxy 1, 2, 3, 4, Add
10. Show (Rxy & ~Cyx & ~(∃z)(Czx & Czy) & ~Nxy) → Cxy
11. Rxy & ~Cyx & ~(∃z)(Czx & Czy) & ~Nxy A
12. Show Cxy
13. (∀z)~(Czx & Czy) 3, QN
14. ~(Cxx & Cxy) 13, UI
15. ~Cxx ∨ ~Cxy 14, DM
INVALID
TheMadFool, your argument is not valid as shown above.

But I'm not making an argument. Perhaps the ''then'' misled you.

I'm defining causation.

Ah, you defined causation by biconditional (or necessary and sufficient condition) ... I got it.

However, your analysis includes free variables x and y, which is not allowed in first-order predicate logic. Of course, if you used them as names, no troubles here.

(Ex)(Ey)(xCy <-> xRy & ~yCx & ~(Ez)(zCx & zCy) & ~xNy)

Thanks for pointing out the mistake. My logic is rusty. How's the above formulation

Or...

aCb <-> (aRb & ~bCa & ~(Ex)(xCa & xCb) & ~aNb)

Two formulations are well-formed fomulae.