If you have been following the discussion in Plantinga on Free Will and Omiscience you will have seen that I have been struggling to construct a proof of (1), which says that if God knows that I will do some action before I actually do it then it is necessary that I actually do it, from (2), which says that it is necessary that if God knows what I will do some action in advance then I will actually do it.
(1) K(G,R,a) –> []D(R,a)
(2) [](K(G,R,a) –> D(R,a)
So far the two attempts that I have made have both been invalid because of some bonehead mistakes. This has been driving me crazy for the past couple of days, but now I think I got it, in fact it almost seems too simple (which probably means I made another bonehead mistake!)…
I thought that it would be easier if I did not include quantifiers, but I think that is what actually confused me. So, what I really want to prove is (1′), which says that for any action x if God knows that I will do it in advance then it is necessary that I actually do it, from (2′), which you can figure out for yourself.
(1′) (x)(K(G,R,x) –> [](D(R,x))
(2′) (x)[](K(G,R,x) –> D(R,x))
this actually turns out to be quite easy (I *think* 🙂 ).
1. ~(x)(K(G,R,x) –> []D(R,x)) assume as a theorem
2. (Ex)~(K(G,R,x) –> []D(R,x)) 1, by definition
3. (Ex)~~(K(G,R,x) & ~[]D(R,x)) 2, by def
4. (Ex) (K(G,R,x) & ~[]D(R,x)) 3, by def
5. K(G,R,a) & ~[]D(R,a) 4, EI
6. K(G,R,a) 5, CE
7. []K(G,R,a) 6, necessitation
8. ~[]D(R,a) 5, CE
9. (x)[] (K(G,R,x) –> D(R,x)) assumption (2′)
10. [](K(G,R,a) –> D(R,a)) 9, UI.
11. []K(G,R,a) –> []D(R,a) 10, distribution
12. ~[]D(R,a) –> ~[]K(G,R,a) 11, contraposition
13. ~[]K(G,R,a) 8,11 MP
14. []K(G,R,a) & ~[]K(G,R,a) 7,13 CI
15. (x)(K(G,R,x) –> [](D,R,x)) 1-14 reductio
What I didn’t notice before was that since we are assuming 1 as a theorem and we can get K(G,R,a) from that then we can use the rule of necessation, which says that if phi follows from a theorem then phi is necessary, to get []K(G,R,a).
So, free will is incompatible with God’s omniscience…
Richard Brown 
I’m a little on the tired side, so I might just be missing something obvious, but I’m not sure how necessitation is supposed to be working in order to get you (7) from (6); usually, I thought, this is restricted with regard to solutions not derived from necessary truths (even if the non-necessary truths are taken as axiomatic or derived from axioms). But all of (1)-(6) implicitly assume things that make it clear they are non-necessary truths (e.g., that Richard exists so as to be able to act and therefore to have his actions known by God). Am I just lapsing here?
Hi Brandon,
Thanks for the comment!
No, you are not just tired, that is the way the rule classicly works…but either those things are necerssary truths ( see here) or we can adopt Kripke’s position and make necessitation apply to anything that is or follows from a theorem (essentially making necessitation itself a logical axiom) so either way it seems to me that it is legitimate to apply it to get 7…
Hi Richard,
I’m also a bit on the tired side. But tell me why this is wrong:
You’ve unnecessarily complicated things. It seems to me what you are trying to prove is as simple as that from
1. [](P->Q)
it follows that
2 P->[]Q
Its easy to see that one could easily write a similar proof to the one you gave, (leaving out all the instantiations) of this “theorem” if your logic were sound.
but ([](P->Q))->(P->[]Q)
is clearly not a theorem of any modal logic. here is a counter model.
W1: P=1, Q=0
W2: P=0. Q=0
Make all worlds “see” all worlds, (so this is an S5 model).
The antecendent (your premise) comes out true, the consequent (your conclusion) false.
What am I missing.
Addendum:
Analogous Proof:
1. ~(P->[]Q) Assumption
2. P from 1. (a few skipped steps)
3. ~[]Q from 1 (ditto)
4 [](P->Q) (axiom 1)
5 []P->[]Q 4, dist
6 ~[]Q->~[]P 5, cont
7 ~[]P 3,7mp
8. []P 2, nec.
The faulty step, of course, as brandon says, is 8.
Its also easy to see how you can extend my counter model to one of your more complicated theorem. Just make the domain 1 element, call it a, and let my P= …. , well, you get the idea.
I am indeed tired.
I meant, of course, that in world 1, (the real world) P and Q are both true. In world 2 they are both false.
Just for kicks, here is the counter model to your version.
Domain {g,r,a}
Interpretation of constants: G=g, R=r
Interpretation of relations:
Real world: all ordered triples are in K, all ordered doubles are in D.
Possible world 2: K and D are both empty.
All worlds see all worlds (so its a countermodel for S5).
2′ comes out true since (for any substitution) the antecedent is false in world 2, and the consequent is true in world 1.
1′: for any substitution, the consequent is false since there is a world that the real world can see (world 2) where the boxed quantity is false.
Hi Eric,
Thanks for the comment! I mean comments 🙂
I agree with your worries about [](P –> Q) –> (P –> []Q) being a theorem. But in your proof step 7 applies necessitation to something that was not derived from necessary truths, so that is an invalid application of the rule. This is as it should be because we would not want to be able to prove that any old contingent truth was a necessary truth! From the fact that I belong to the indepenent party we shouldn’t be able to prove that it is necessary that I belong to it…but in my proof I assume that either 6 follows from necessary truths (classical modal logic) or, if one rejects that kind of modal semantics, a kripe-ish semantics that treats necessitation as itself an axiom, so that if phi follows from an axiom then phi is necessary…In either case necessitation of 7 is valid, and it seems to me that this covers all the cases…so those models aren’t counter-examples.
I guess one might try to push this objection by claiming that my 1 is not itself necessary and so, even though it depends on things which are themselves necessary, it is still wrong to apply necessitation to 7. If so, I guess I would respond I would then start the proof one step back and have 0,
0. []~(x)(Kx –> []Dx)
and we could still generate the contradiction assuming 9. Granted, the conclusion of the arg. would be different. It would only show that it was possible that If I am free then God can’t know what I will do in advance, not that it was actually the case…wich I think I could live with…
Sorry, I dont get it. 1st: My proof EXACTLY parallels yours. The thing I Nec on, just like you, follows from the thing I have assumed for reductio. That’s the no-no. 2nd: How can you say that your 6 follows from something “necessary” when in the end you show that the thing it follows from is false??? I agree that if something follows from an axiom, you can nec it, but your thing follows from an assumption for reductio. 3rd: What about the plain fact that I have given you a counter model to the ‘theorem’ (x)[](K(G,R,x) –> D(R,x))->(x)(K(G,R,x) –> [](D(R,x))?
Hi Eric,
Thanks for the response. Let me see if this helps.
If I am right then your proof does not exactly parallel mine. The difference between them, I say, is that yours, and the counter model that you construct, assume that 1-6 are not necessary truths. In standard S5, though, it is easy to prove that everything necessarily exists (see the link in teh reply to Brandon), simarly the actions that I perform, if they can be quantified over, also necessarily exist, etc, so in that way the truth of 6 follows from things that are necessary…
You ask “How can you say that your 6 follows from something “necessary” when in the end you show that the thing it follows from is false???”
We assume for the proof that 1 is in fact an axiom. If it is then anything that follows from it will also be necessary. So, you are right that it does not actually follow from something that is necessary, but at that step in the proof, under the assumptions of the proof, it is the case that if 1 were an axiom then 6 would follow from an axiom. So, yes, it does follow from an assumption for reductio, but the assumption is that 1 is an axiom, that is the very reason that we reject it as an axiom at the end of the proof. We can show that if it were it would lead to a contradiction! To deny that this is a legitimate move seems to me to deny that reductio is a valid way of proving theorems…So either way I just don’t see that there is any reason to suspect 7.
So, the counter model is not a counter model…
I’m not seeing why this is a legitimate move either. You were wanting to show that (2) entailed (1). The way to do this is to show that (2) is inconsistent with the denial of (1). Why is it ok to take as your assumption |- ~(1)? I’m not seeing any motivation for this, aside from it supposedly licensing necessitation at the crucial point in the proof.
Hi Aidan,
I think I may not be getting the force of your objection, but isn’t it the case that either |- P or |- ~P for any P? I want to show |- P and so I assume |- ~P and show that we can generate a contradiction and then conclude |- P like I wanted…what’s illigitimate or unmotivated about this?
Its simple. You cant use the NEC rule inside a conditional proof, or a proof by reductio. If you do, you can prove all sorts of crazy things. Moreover, work through the semantics with the model I gave in my third post. You will see that 2′ comes out true, and 1′ comes out false. (and notice that I give only one domain for all worlds, so the point about everything existing in every possible world–(which is btw controversial)–is moot)
“isn’t it the case that either |- P or |- ~P for any P?”
Why would this hold?
Hi Eric, thanks for the response.
Sorry for the delay getting back to you, but I was away from the computer for a day and when I got back, I was having problems with my wordpress account…
Anyways, I have never heard of that restriction on nec…so you have a source?
As for the model, I am not sure what you mean when you say K and D are empty, but if what you mean is that in that world no one knows anything and no one does anything then the point about necessary existence is anything but moot…and I am aware that the claim is contravesial, but if one is using S5, as you said you were, then it is indeed the case that anything that exists does so necessarily…so that means that God exists in w2 and so do I, which means that K and D cannot be empty (unless I misunderstand what you mean by that)…now of course what you are pointing out is that you do not think that if I perform some action then it is necessary that I perform that action, and so at w2 I do not perform that action and that falsifies the consequent…but let us say that the event in question is mowing my lawn, and let us say that I actually do mow my lawn…then that event exists and if it does we can prove that it must via the same kind of argument that we gave for my necessary existence…so that means that I do perform the act at w2 and so your model neglects the claim about necessary existence…Now if you want to reject that, as I do and I take it, you, do we can adopt Kripke’s strategy and make nec an axiom (i.e. accept p –> []p as an axiom)….
I guess that what is ultimately at issue here is actualism…if actualism is true then all God has to know in order to be omniscient is what the truths actually are, and what they could have been….but knowing what they could have been is just knowing of the things that are possible, that they are in fact possible…but if actualism is wrong, knowing what they could have been means knowing that they are in fact (possibly) the case…which means that if He knows something then He must necessarily know it….this might even be true on a kind of actualism that allows for actual possibilities (like, I think, Plantinga does).
While I don’t think that p –> []p is generally true, it is true for some predicates (like the existence predicate) and also I think of ‘knows’ when applied to God (and one has a particular view of possible worlds)…so, thanks, this discussion has been very helpful to me
Sorry Aidan, I meant ~ |- P or ~ |- ~P….
Richard,
I dont have a reference. But notice, e.g. that H&C state NEC as: if a is a theorem, then []a is a theorem. When you assume something for CP, it is not necessarily a theorem, so it is illegitimate to apply NEC.
A very trivial example shows this.
1. P (assumption for CP)
2. []P 1. Nec
3 P->[]P 1-2, CP
But P->[]P is clearly not a theorem of K, whereas Nec is a rule of K.
As for my model, its a formal model–I dont care whether its about you mowing your lawn, or the moon being made of green cheese. The only thing that matters is that the domain is the same in both worlds. The DOMAIN is the same. The interpretations of the predicates are, of course, different. In the second world, no entities stand in either of the two relations to any other entities. (that’s what I mean, of course, by saying K and D are the empty set.) The beauty of logic is that I dont have to get into discussions about whether this is true of lawnmowers or moons. I can just give you an a formal model to test whether your FORMulae are true in every model. Yours arent.
Anyway, since you seem to admit in your latest post that the proof is invalid, we should probably drop the matter.
Hi Eric,
That’s not quite what I admitted, 🙂
The proof is valid in S5….it is just that I do not accept S5 so I don’t really care if it is valid in S5 or not…what I want is a proof that is valid for Kripke’s kind of quantified modal logic…
As for the ‘counter-proof’ it doesn’t show that there is anything wrong with mine…in fact it is perfectly good for some predicates, as I said before. If we are assuming that P is itself a theorem then step 2 is perfectly fine…that just what H&C say…we are assuming that P is a theorem ans so we can get []P…that should be fine as long as P (or ~P as the case may be) is a candidate for a theorem…but THIS JUST IS why the proof is valid in S5 since the events and individuals we are talking about are all necessary…
Finally then, as for your model, you seem to be missing the point. I know it is a formal model, but it assumes something that you can’t assume, which is that K and D are empty..this assumption only works if we ARE NOT talking about neccesary existents…so w2 is not possible in that kind of semantics…it is clearly NOT required that a formula be valid in every model, that’s quite silly actually. Take the Barcan formula. It is not valid in every model, but so what? It is valid in S5…..
[…] obsessed with this stuff about God’s omniscience and Free Will. I have been having some very interesting, and helpful, discussion about whether Plantinga’s defense, which I take it is the standard defense, of their […]