Symmetric relations and logic

Suppose Alice and Bob are friends, and that friendship is a fundamental relation. Consider the facts expressed by these two sentences:

1. Alice and Bob are friends.

2. Bob and Alice are friends.

It is implausible that these are different facts. For if they were different facts, they would both be fundamental facts (otherwise, which of them would be the fundamental one?), and we would be multiplying fundamental facts beyond necessity—only one of the two is needed in the totality of fundamental facts.

Furthermore, I think that the propositions expressed by (1) and (2) are the same. Here’s one reason to think this. Imagine a three-dimensional written language where plural symmetric predicates like “are friends” are written (say, laser-inscribed inside a piece of glass) with “and are friends” on one horizontal layer, with “Alice” on a layer below the “and” and “Bob” on a layer above it. If (1) and (2) express different propositions, we would have to ask which of them is a better translation of the three-dimensional language. But surely there is no fact about that.

If this is right, then First Order Logic (FOL) fails to accurately represent propositions about fundamental relations, by having two atomic sentences, F(a,b) and F(b,a), where there is only one fundamental fact. Moreover, FOL will end up having non-trivial proofs whose conclusion expresses the same proposition as the premise, since we will presumably have an axiom like ∀x∀y(F(x,y)→F(y,x)) that lets us prove F(b,a) from F(a,b). This is not the only example of this phenomenon. Take the proof that ∀xF(x) follows from ∀yF(y), even though surely the two express the same proposition, namely that everything is F.

In particular, the logic of sentences appears to differ from the logic of propositions, since the proposition that Bob and Alice are friends follows by reiteration from the proposition that Alice and Bob are friends if they are the same proposition, but sentence (2) does not follow from sentence (1) by reiteration (nor is this true for the FOL versions).

If we think there is a One True Logic, it presumably will be a logic of propositions rather than sentences, then. But what it will be like is a difficult question, to answer which we will have to a worked out theory of when we have the same proposition and when we have different ones.