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 x1
, 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 x1
and 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 A
.
- conjunction elimination right: If
A and B
, then B
.
- contradiction introduction: If
A
and not A
, then ⊥
(= contradiction).
- negation introduction: If
A
leads to ⊥
, then not A
.
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 S1
.
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 x1
, 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 B
, then if A then B
.
- universal introduction: If
A
holds for arbitrary x
, then 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 6.
:
...
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 y
, x1
and 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 y
and x1
, 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 x1
, x2
, if x1
and x2
are different, then the position of y
can not be x1
and x2
at the same time.