Definition. Semantic Argument method (FOL) [0018]

In first order logic, the semantic argument method represents a proof by contradiction. The basic idea is as follows:

1. We assume that our formula \(F\) is not valid, i.e., \(\exists S, \sigma \nvDash F\)
2. Use the proof rules to derive a contradiction from this assumption.
3. If we can indeed derive a contradiction, we conclude that our initial assumption was false, and therefore \(F\) must be valid.

We can express the semantic argument method via the following inference rule:

So the idea here being that if we have a predicate and its negation both holding under the same interpretation and variable assignment, we can derive a contradiction. This allows us to conclude that our initial assumption (that the formula is not valid) must be false, thereby proving the validity of the formula.