An appropriate formalization (with natural language terminology instead of logic symbols) of your sentences in a language of predicate logic with term equality
=, a function symbol
pos, a variable
y for the object and two variables
x2 for the two positions is
S1: (pos(y) = x1) and (pos(y) = x2)
S2: not(x1 = x2)
Your usage of "the position" justifies the translation as a function expression that has exactly one value. One could question now whether or not "position" is indeed something that behaves as a function -- this may be more of a question for physics than for philosophy, and if the answer is no, then already the initial wording of the situation would have been inadequate and the conclusion will not be provable with the methods used here. But for the sake of demonstrating from a logical point of view how a semi-formal proof can be carried out with the premises as you worded them, as per your request, let's assume that this formalization is indeed adequate.
The set of premises is not immediately contradictory: To be able apply the law of non-contradiction, which states that
not(P and not P), one of the two
and-ed statements in S1 would have to be the direct negation of the other, so that
S1 has the form
P and not P; but
pos(y) = x1 and
pos(y) = x2 are just two independent formulas that are not immediately visible as contradictory.
So if we want to prove the argument rigorously, we need a few additional inference steps. The idea will be that if we have equality statements
=, then we are free to combine any of the terms between the equality symbols, which eventually leads to the observation that if the first assumption is true, we must have
x1 = x2, which contradicts the second assumption that
x2 are different positions.
More precisely, we are exploiting the following two properties of equality:
- symmetry: If
A = B , then
B = A.
- transitivity: If
A = B and
B = C, then
A = C.
In addition, we need
- conjunction elimination left: If
A and B, then
- conjunction elimination right: If
A and B, then
- contradiction introduction: If
not A, then
⊥ (= contradiction).
- negation introduction: If
A leads to
With these rules, we can prove the validity of your argument formally:
1. pos(y) = x1 and pos(y) = x2 (assumption S1)
2. pos(y) = x1 (conjunction elimination left on line 1)
3. x1 = pos(y) (symmetry on line 2)
4. pos(y) = x2 (conjunction elimination right on line 1)
5. x1 = x2 (transitivity on lines 3 and 4)
6. not (x1 = x2) (assumption S2)
7. ⊥ (contradiction introduction on lines 5 and 6)
8. not (pos(y) = x1 and pos(y) = x2) (negation introduction on lines 1 to 7)
Note that the contradiction arises not between the two position assertions, but between
not (x1 = x2) and
(x1 = x2), the latter of which is derived from the assumption
If we are convinced that the initial formalization of your situation is adequate, and accept the individual inference rules, then the above reasoning indeed proves that the object can not be at positions x1 and x2 at the same time. The key of the proof lies in the implicit assumption that "position" is indeed a function, in the sense that every object can only have one position, so that we can use
= and argue about how equality works.
We can now actually go a step further. Up until now, we only proved that the set of premises given, with the concrete positions
x2 and object
y is inconsistent. But we may want to prove something more general:
For any object y and positions x1, x2, if x1 and x2 are different, then y can not be at x1 and x2 at the same time.
To do this, we need two more inference rules:
- conditional introduction: If
A leads to
if A then B.
- universal introduction: If
A holds for arbitrary
for all x: A.
In the proof above, the assumption
6. not(x1 = x2) led to the conclusion
8. not(pox(y) = x1 and pos(y) = x2. So we can do a conditional introduction and state that
if not(x1 = x2), then not(pox(y) = x1 and pos(y) = x2), thereby resolving the dependency on the assumption
9. if not(x1 = x2) then not(pox(y) = x1 and pos(y) = x2) (conditional intoduction on lines 6 to 8)
At this point, conclusion
9. does no longer depend on any assumptions about
x2: The second premise
S2 is discharged because we now said more generally that if
not(x1 = x2), then
not (...), which no longer depends on whether or not
not(x1 = x2) is actually true. And the first premise
S1 was discharged in line
8. where we concluded that this assumption must have been wrong since it led to a contradiction. So
x2 are indeed arbitrary objects and positions, the conclusion does not depend on what exactly these variables look like, so the proof should work for any object and positions. This is why we are allowed to a final universal introduction:
10. for all y, x1, x2: if not(x1 = x2) then not(pox(y) = x1 and pos(y) = x2) (3x universal introduction on line 9)
We now formally proved that for all objects
y and all positions
x2 are different, then the position of
y can not be
x2 at the same time.