OK, so this is going to be confusing, and it's kind of unfortunate we've learned proofs using trees instead of boxes/lines because it makes things really unclear, but here goes:

So far, I've kind of been letting things slide in terms of you guys rigorously understanding what's going on in these proofs. The proofs have been mostly pattern matching; I've told you guys you can basically look for rules that have the same kind of conclusion, and apply them backwards until you've discharged all your assumptions, and voila, you'll have a complete proof tree.

Unfortunately, we've moved into First Order Logic now, and in First Order Logic, you have to worry about the scoping of your variables; that is, when we talk about variables, we have to think about what they actually represent and for what section of the proof tree they represent that.

Consider this statement:

P [u/t]

If this appears somewhere in your homework, I get what you're trying to do: you're trying to apply ∀ introduction. The problem is, the ∀ introduction rule doesn't make a lick of sense unless we really understand the condition on the rule, and unfortunately I've been kind of shit at explaining it, because it's honestly not at all intuitive the way we're doing things (it's much clearer using the boxes-and-lines method, but too late now!)

From the notes:


"Here, u must be a variable that does not occur free in any of the propositions in Γ or in ∀tP. The notation P[u/t] stands for the result of substituting u for all free occurrences of t in P."

That is some seriously unintuitive shit here! Instead, think of it this way: think of what ∀tP actually means. It means the statement P is true for EVERY possible value that t could take on. To be able to conclude that, we have to let t range over ALL possible values in the domain. That's what u represents. We try to come up with a deduction from some premises down to P[u/t], where u is a standin for any possible value that t could take on. If we can show that that deduction is valid with no constraints on u, then we can say ∀tP.

In the above proof, though, you make the assumption P[u/t] is true, which means you've found a SINGLE u in the domain that makes the statement P true. Clearly, from this single example, you can't extrapolate over ALL possible u's and say P is true for all of them.

If, as part of your deduction, you can show that P[u/t] is true for EVERY possible value of u, then you can conclude ∀tP. For example, say you somehow arrive at a contradiction in your proof. From that contradiction, you can say P[u/t] is true for ALL the possible values of u (obviously, because from contradiction, EVERY statement is provable). So, from that, you could say ∀tP.
Allons-y! Back to CIS160 Page