Logic Translations

An issue about translations came up in our Logic lecture earlier this week.  Consider the sentence S = "Either Fred will eat out and Martha will eat with him, or Fred will go home and eat alone".  How should this be translated into truth-functional logic?
 
The obvious approach is to simply go for (O & M) v (H & A), where O = Fred will eat out, M = Martha will eat with Fred, H = Fred will eat at home, A = Fred will eat alone.  Or something along those lines.
 
However, as another student pointed out, this seems incomplete, failing to capture the meaningful connections between elements of the sentence.  For example, it seems clear to us that A and M are mutually exclusive, as are O and H, yet the syntax of the simple translation offers no hint of this.
 
I think, then, a better translation may be:
[(O & M) v (H & A)] & (O → ~H) & (M → ~A) 
 
It might be objected that this unnecessarily complicates things.  Perhaps our basic translation should be kept as simple as possible, and any "extra information" or inferences between its parts, ought to be introduced as new premises if necessary.  Though if this principle were taken to extremes, we might be tempted to just offer the entire sentence S with no internal analysis whatsoever.  That would obviously not be helpful.
 
I would have thought that a translation should try to capture as much of the analytic/syntactical information provided in the sentence as possible.  That is, our translation should try to spell out the appropriate inferences between the words and phrases used.  However, we should avoid cramming in 'synthetic' or contextual information, for these might include unwarranted assumptions - far better to introduce them as new premises. 
 
In this case, however, I think the information added is best understood as analytic.  If Fred eats alone, then it is not the case that he eats with someone else (e.g. Martha).  This is a simple analytic truth that we can know from the words themselves, without having to reference contingent real-world facts.
 
To re-inforce this point, consider how we would translate the sentence into first-order logic.
We can do this with the single predicate - Wxyz: x will eat at (location) y with (person) z; 
We will also need the constants f = Fred; m = Martha; h = (Fred's) home.
Using 'E' as the existential quantifier ("there exists"), and 'V' for universal quantification (i.e. "for all..."), our translation of S could now be as follows:
 
Ex(Wfxm & x ≠ h ) v (Wfhf & VxVy(Wfyx → x = f))
 
This literally says "Either Fred will eat at somewhere that is not home, with Martha, OR Fred will eat at home (with himself), and he will eat with nobody but himself."
I think that captures the meaning of S reasonably well.  Notice that it includes the analytic implication that if Fred eats alone then there is no-one else he eats with - not even Martha.
 
However, this particular translation doesn't rule out the possibility of eating at several places, i.e. both at home and not and home.  This could be introduced easily enough with some more quantification, but it's starting to get a bit messy.  Also, the 3-place predicate might not be entirely faithful to the original syntax of S, which appeared to treat locations and companions quite separately.  This too is easily solved, this time by replacing it with two 2-place predicates, but that will make things messier yet. 
 
I think a better approach - solving both problems - might be to introduce a function, to map from a person to the place where that person "will eat" (at whatever particular time we're implicitly talking about). So here's a stronger translation...
 
Let px = the place where x will eat; f = Fred; m = Martha; h = (Fred's) home;
Wxy: x will eat with y.
(Wfm & pf ≠ h) v (pf = h & Vx(Wfx → x = f))
 
i.e. "Either Fred will eat with Martha, at a place which is not home, OR Fred will eat at home with nobody else".
 
Alternatively, we could lose the predicates altogether, and just use the function...
(pf = pm & pf ≠ h) v (pf = h & Vx (px = pf → x = f))
i.e. "Either Fred and Martha will eat at the same place, which is not home, OR the place where Fred will eat is home, and there is no-one but him at that place".
 
I quite like that last translation actually, though one might complain that there is a conceptual distinction to be made between eating with someone, and merely eating at the same place as them.
 
Anyway, my enthusiam about various translating strategies aside, the point is that these first-order logical translations seem to capture the meaning of S, better than the basic truth-functional one did.  These analytic implications can be captured truth-functionally, however, we just need to append them manually to the end of the basic translation.
 
The big question, then, is "should we?".  I think so, but I'm not entirely sure.  One could object that I've just assumed the sentence is talking about a single temporal period, and that this may not be so - perhaps the pairs are not mutually exclusive after all.  Fair enough.  But suppose I picked a better example to illustrate this point, one with no ambiguities here (e.g. reword the sentence to be entirely in the present tense).  The general question remains: How much detail should we seek to include in a logical translation?  Just the basic elements?  Or also the analytic implications we can draw between them?
 
As always, comments are most welcome.