We can construct informal proofs in first order logic in much the same way we did in zeroeth order logic, but asking how the given statement could be false and trying to show that none of these ways can actually occur.
As an example, consider the statement \[ \{ [ ∃ x . ( f x ) ] ⊃ [ ¬ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) ] \} . \] Suppose it were false in at least one interpretation. This is of the form \({ ( P ⊃ Q ) }\), where \({ P }\) is the expression \({ [ ∃ x . ( f x ) ] }\) is the expression \({ [ ¬ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) ] }\). We know that an expression of the form \({ ( P ⊃ Q ) }\) can only be false when \({ P }\) is true and \({ Q }\) is false, so \({ [ ∃ x . ( f x ) ] }\) should be true and \({ [ ¬ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) ] }\) should be false. We also know that an expression of the form \({ ( ¬ P ) }\) can only be false if \({ P }\) is true, so \({ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) }\) should be true. If \({ [ ∃ x . ( f x ) ] }\) is true then there is some \({ a }\) such that \({ f a }\). If \({ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) }\) is true then \({ \{ ¬ [ ( f a ) ∨ ( g a ) ] \} }\). Since this is true \({ [ ( f a ) ∨ ( g a ) ] }\) must be false. Then \({ ( f a ) }\) is also false. But we previously found \({ ( f a ) }\) to be true. So the assumption that \({ \{ [ ∃ x . ( f x ) ] ⊃ [ ¬ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) ] \} }\) was false is untenable. It is therefore a valid statement.
There was no branching in the proof above, or at least none worth making explicit, but sometimes there will be, just as there was in zeroeth order logic. As an example, consider the statement \[ \{ ( ∀ x . \{ ∀ y . [ ( f x ) ⊃ ( f y ) ] \} ) ⊃ ( \{ ∀ x . ( f x ) \} ∨ \{ ∀ x . [ ¬ ( f x ) ] \} ) \} . \] Suppose it were false in at least one interpretation. As before this is \({ ( P ⊃ Q ) }\) statement and for it to be false we’d need \({ P }\) to be true and \({ Q }\) to be false. So we take \({ ( ∀ x . \{ ∀ y . [ ( f x ) ⊃ ( f y ) ] \} ) }\) to be true and \({ ( \{ ∀ x . ( f x ) \} ∨ \{ ∀ x . [ ¬ ( f x ) ] \} ) }\) to be false. The second of these statements is of the form \({ ( P ∨ Q ) }\). For it to be false both \({ P }\) and \({ Q }\) must be, so in this case \({ \{ ∀ x . ( f x ) \} }\) and \({ \{ ∀ x . [ ¬ ( f x ) ] \} }\) must be false. For \({ \{ ∀ x . ( f x ) \} }\) to be false there must be an \({ a }\) such that \({ ( f a ) }\) is false. Similarly, for \({ \{ ∀ x . [ ¬ ( f x ) ] \} }\) there must be a \({ b }\) such that \({ [ ¬ ( f b ) ] }\) is false, and hence such that \({ ( f b ) }\) is true.
Note that we had to use a new name for this second parameter. It wouldn’t have been legitimate to call it \({ a }\) since \({ a }\) was the value that made \({ ( f a ) }\) false and while we know there are values which make each expression false individually there’s nothing to assure us that a single value will make \({ ( f a ) }\) false and make \({ ( f b ) }\) true. If you look back at the previous proof you’ll see a superficially similar situation, where we first said that if \({ [ ∃ x . ( f x ) ] }\) is true then there is some \({ a }\) such that \({ f a }\) and then said that if \({ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) }\) is true then \({ \{ ¬ [ ( f a ) ∨ ( g a ) ] \} }\). I used the same parameter \({ a }\) for both statements. That was legitimate though, since the second statement was about all values and so applies in particular to the value \({ a }\) chosen previously. So in that case I was allowed to reuse the parameter. I wasn’t required to though. I could have said that if \({ ( ∀ x . \{ ¬ [ ( f x ) ∨ ( g x ) ] \} ) }\) is true then \({ \{ ¬ [ ( f b ) ∨ ( g b ) ] \} }\). That would also have been legitimate, but it wouldn’t have led to the contradiction I was looking for.
After that digression let’s return to our proof. To summarise where we are, \({ ( ∀ x . \{ ∀ y . [ ( f x ) ⊃ ( f y ) ] \} ) }\) is true, \({ ( f a ) }\) is false, and \({ ( f b ) }\) is true. We use the first of these to conclude that \({ \{ ∀ y . [ ( f b ) ⊃ ( f y ) ] \} }\) is true. I’m allowed to reuse the parameter \({ b }\) here because the quantifier is universal and the statement is true. I could also have reused \({ a }\). That wouldn’t have accomplished much though since \({ ( f a ) }\) is false the statement \({ [ ( f a ) ⊃ ( f y ) ] }\) wouldn’t tell us anything. \({ ( f b ) }\) on the other hand is true, so the statement \({ [ ( f b ) ⊃ ( f y ) ] }\) does tell us something. I could also have chosen an entirely new parameter and concluded that \({ \{ ∀ y . [ ( f c ) ⊃ ( f y ) ] \} }\). That also wouldn’t have accomplished much though, so we’ll stick with \({ \{ ∀ y . [ ( f b ) ⊃ ( f y ) ] \} }\). From it we can derive \({ [ ( f b ) ⊃ ( f a ) ] }\). Again I had a choice of parameters and this time I chose \({ a }\) to substitute for \({ y }\). I could have chosen \({ b }\) instead, or an entirely new parameter. But I didn’t. It’s at this point that we need to branch the argument since there are two ways that \({ [ ( f b ) ⊃ ( f a ) ] }\) could be true. \({ ( f b ) }\) could be false or \({ ( f a ) }\) could be true. We’ve already seen though that \({ ( f b ) }\) is true and \({ ( f a ) }\) is false. So the assumption that \[ \{ ( ∀ x . \{ ∀ y . [ ( f x ) ⊃ ( f y ) ] \} ) ⊃ ( \{ ∀ x . ( f x ) \} ∨ \{ ∀ x . [ ¬ ( f x ) ] \} ) \} \] is false is seen to be untenable. It is therefore a valid formula.