Modal logic formulation

Question

Introduction

So, I want to prove that the decisions that any being makes are either predetermined or are chosen at random - basically, disproving libertarianism. I have already formulated it using words, and, in fact, I have also attempted at formulating it using modal logic, but, since this is the first time I ever used it, it is very likely that a big chunk of the proof will be wrong, ambiguous, unclear, or just plain gibberish. So, I want to see what exactly it is, if not everything, that can be improved in my modal logic formulation and how.

Verbal formulation

1. Either an action is the same in all possible worlds, or it is not.
2. If it is not, it must depend on a variable that is not the same in all worlds.
3. Similarly, that variable itself must depend on a variable that is not the same in all worlds.
4. I demand that the variable composition is not infinite, as that would result in an infinite regress.
5. Therefore, there must eventually be a variable that doesn't depend on anything. Since, if $a$ depends on $b$ that depends on $c$, $a$ depends on $c$, the action itself must depend on nothing.
6. I define a thing to be predetermined if it is the same in all worlds and random if it depends on nothing but is not predetermined.
7. Therefore, an action at any given instant is either predetermined or random.

Mathematical formulation

In this theorem, I will consider an action taken at a particular instant by a particular individual;

• $f[x]$ represents that $f$ depends on $x$/the (set) of value(s) of $f$ at $x$
• $c$ represents a constant
• $a$ is the action taken

• $f^n[x]$, in this context, will be taken to mean $f\circ f \circ \cdot \cdot \cdot \circ f$ with $f$ repeated n times

  1. $Df. 1:D(y,x_1,x_2,…x_n):\Leftrightarrow (y[x_1,x_2,…x_n]\wedge \neg \exists z:y[z])$
  2. $Df. 2:(\forall v:(f[v]\Leftrightarrow v\in V[f]))\wedge \forall f:\neg (V[f]=\emptyset)$
  3. $Th. 1:D(a,V[a])\oplus \square a=c$
  4. $Th. 2:(\forall n\in ℕ:D(V^n [a],V^{n+1} [a]))\oplus \exists Max[n]\oplus \square a=c$
  5. $Ax. 1:\exists Max[n]$
  6. $Th. 4:D(a,\emptyset )\oplus \square a=c$
  7. $Df. 3:f\in Pre:\Leftrightarrow \square f=c$
  8. $Df. 4:f\in Ran:\Leftrightarrow (D(f,\emptyset )\wedge \neg (f\in Pre))$
  9. $Th. 5:a\in Ran\oplus a\in Pre$

Can anyone help me with this?