Necessarily Foreknown

There is an interesting argument on foreknowledge and free will at "Holy Cyclops"; I found it on a side journey while following links from the Philosophy Carnival. The argument is:

1. N(Kx—>x) (Premiss—to know that x will occur at t requires that x will occur at t)
2. N(Kx) (Premiss—it is necessarily foreknown that x will occur at t)
3. Nx (1, 2, modal modus ponens)

And to this the comment is added, "Anyone who thinks that God necessarily foreknows all events, including the outcomes of all human choices, will have to endorse the argument."

However, as Chad McIntosh notes in the comments, this appears to equivocate on what it means when people say "God necessarily foreknows all events"; the usual way of understanding it, and the one that is found in most traditional accounts of divine foreknowledge is not only not translated by N(Kx) but reject it.

N(Kx) basically says that it is necessary that x is known (by God, in this case). But this is not how "God necessarily foreknows all events" is usually understood; rather it's understood as something more like:

[A]
N(x -> Kx)

(Still confining the epistemic agents to God.) That is, It is necessary that if x, x is known by God. But this is consistent with the falsehood of N(Kx); x and Kx are both consistent with P~Kx, even though one is taken to entail the other.

I say we get something 'more like' [A] because strictly speaking we should probably be quantifying here, and this would seem to give us something along the lines of

(∀x) N ((∃x) -> Kx)

or

N (∀x) ((∃x) -> Kx)

or both, depending in part on what position we take with regard to the Barcan Formulas. (The difference between the two translations is the difference between "Every x is such that this is necessary: x is known by God if it occurs" and "This is necessary: every x is such that it is known by God if it occurs"; in many modal systems the two are interchangeable, but in others the former is a weaker claim.) But the interaction of modal operators and quantifiers is tricky stuff; best to avoid it when one can, and I think that on this subject we probably can.

UPDATE: Quantifiers wandering in where they shouldn't be! Mike Almeida helpfully points out in the comments that I muddled up things when adding the quantifiers. The ∃, which I put in without really thinking, shouldn't be there, so, minimally:

(∀x) N (x -> Kx)

and

N (∀x) (x -> Kx)

which both make more sense (since they make sense in the first place!); one could also used a truth predicate instead of the ∃ in the above.