Tuesday, February 17, 2026

Logic of Law

I am not sure whether Frank Van Dun’s stated justifications for developing his formal theory of law hold much water. He says he is using formal logic to avoid the ambiguities in natural language, but the only semantics provided for his logic is to give a natural-language interpretation of each predicate. And obviously, the central words in the theory, namely the relation of “belonging”, are certainly understood differently by different cultures. If Van Dun wanted to avoid such issues, it may have been desirable to give a semantics that translates these relations into less loaded terms, which may be cashed out into positivistic “observation-sentences” or something of the sort.

Nevertheless, Van Dun’s theory is very interesting in its own right. I feel an aesthetic attraction to it. Hence, this blog post redevelops the formal elements of The Logic of Law, by Frank van Dun, in a new notation, and with proofs given (Van Dun gave no proofs, only theorem statements). I have replaced Van Dun’s idiosyncratic quantifiers with standard ones, and in every instance where variable names were used to implicitly distinguish domains (such as the variable name $p$ used to imply that it is restricted to persons), I have replaced that with restricted quantification over explicitly-defined sets. I have also replaced many of Van Dun’s predicates and relations with infix-notated symbols, because I thought that looked nicer. Although I added proofs of each of the propositions, at least one of them was not provable as stated, as you will see.

The same labels are used for propositions as far as possible, so you can easily compare this blog post to Van Dun’s paper; but Van Dun wrote many propositions without labels, so it might not be very easy to compare, anyway, especially since I preferred to add a new natural-language paraphrase of each of the formal statements instead of reusing his paraphrase.

Illustration of Van Dun’s legal system as notated by this blog post, made with Nano Banana.

Contents

Section I: The General Theory

Persons

Primitive vocabulary (system \(\mathbf L_0\))

  • Domain of discourse: $\mathcal D$ (objects).
  • Primitive binary relation: $<\ \subseteq \mathcal D\times\mathcal D$ (“belongs to”).
  • Primitive unary predicate: $I:\mathcal D\to{\text{T},\text{F}}$ (“is innocent”).
  • Identity: $=$.

Syntactic/domain definitions (SD)

$SD1$: $\mathcal P \;\:=\; {p\in\mathcal D \mid \exists o\in\mathcal D\ (o<p)}
\qquad\text{(persons)}$
A “Person” is defined as any object that has at least one other object belonging to it. (To be a person is to be an owner).

$SD2$: $\mathcal M \;\:=\; {x\in\mathcal D \mid \exists o\in\mathcal D\ (x<o)}
\qquad\text{(means)}$
A “Means” is defined as any object that belongs to another object. (To be a means is to be owned).

A “mere object” (outside the law, in Van Dun’s sense) may be captured as:
$SD3$: $\mathcal O \;\:=\; {o\in\mathcal D \mid \neg\exists u\in\mathcal D\ (u<o)\ \wedge\ \neg\exists v\in\mathcal D\ (o<v)}$
A “Mere Object” is something that neither owns anything nor belongs to anything. It exists outside the legal structure of persons and means.

Immediate consequences of SD1–SD2

$T0.1$: $\forall p\in\mathcal P\ \exists x\in\mathcal M\ (x<p)$
Every Person possesses at least one Means. (You cannot be an owner without owning something).
Proof. Fix $p\in\mathcal P$. By $SD1$, $\exists o\in\mathcal D\ (o<p)$. Let $x:=o$. Then $x<p$, hence by $SD2$ (since $\exists o'\,(x<o')$ is witnessed by $o'=p$) we have $x\in\mathcal M$. Therefore $\exists x\in\mathcal M\ (x<p)$. $\square$

$T0.2$: $\forall x\in\mathcal M\ \exists p\in\mathcal P\ (x<p)$
Every Means belongs to at least one Person. (If something is owned, the thing that owns it must be a Person).
Proof. Fix $x\in\mathcal M$. By $SD2$, $\exists o\in\mathcal D\ (x<o)$. Let $p:=o$. Then $x<p$, and by $SD1$ (since $\exists o'\,(o'<p)$ is witnessed by $o'=x$) we get $p\in\mathcal P$. Hence $\exists p\in\mathcal P\ (x<p)$. $\square$

Axioms constraining (<) (A)

$A_{01}$: $\forall p\in\mathcal P\ \exists q\in\mathcal P\ (p<q)$
Every Person belongs to at least one Person. (This implies that everyone is either self-owned or owned by others; no person is unowned).

$A_{02}$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\ \bigl((x<p\ \wedge\ p<q)\ \rightarrow\ x<q\bigr)$
If a Means belongs to Person A, and Person A belongs to Person B, then the Means also belongs to Person B.

Person-status definitions (DP)

Real person. A person who belongs to themselves (is self-owning).
$DP1$: $\operatorname{Real}(p)\ \:=\ (p<p)\qquad(p\in\mathcal P)$

Free person. A person who belongs to themselves and only to themselves.
$DP2$: $\operatorname{Free}(p)\ \:=\ (p<p)\ \wedge\ \forall q\in\mathcal P,(p<q\rightarrow q=p)$

Sovereign person. A person who, if they belong to anyone, belongs only to themselves.
$DP3$: $\operatorname{Sov}(p)\ \:=\ \forall q\in\mathcal P,(p<q\rightarrow q=p)$

Autonomous person. A person with the following trait: if they belong to someone else, that other person must also belong to them. (A relationship of mutuality).
$DP4$: $\operatorname{Aut}(p)\ \:=\ \forall q\in\mathcal P,(p<q\rightarrow q<p)$

Heteronomous person. A person who is not Autonomous. (They belong to someone who does not belong back to them).
$DP5$: $\operatorname{Het}(p)\ \:=\ \neg\operatorname{Aut}(p)$

Strictly autonomous person. A person who is Autonomous but not Sovereign. (They are involved in mutual ownership arrangements but are not exclusively self-owned).
$DP6$: $\operatorname{SAut}(p)\ \:=\ \operatorname{Aut}(p)\ \wedge\ \neg\operatorname{Sov}(p)$

(Relational notions stated informally in the paper, made explicit:)

Master / serf (of a master). A Serf is a Heteronomous person who belongs to a Master, where the Master does not belong to the Serf.
$D_{ms}$: $\operatorname{Master}(b,a)\ \:=\ a\in\mathcal P\wedge b\in\mathcal P\wedge \operatorname{Het}(a)\wedge (a<b)\wedge \neg(b<a)$
(“$a$” is a serf of “$b$” iff $\operatorname{Master}(b,a)$.)

Ruler / subject. A Subject is a person who belongs to a Ruler, provided that the Ruler is an Autonomous person.
$D_{rs}$: $\operatorname{Subject}(a,b)\ \:=\ a\in\mathcal P\wedge b\in\mathcal P\wedge (a<b)\wedge \operatorname{Aut}(b)$
(“$b$” is a ruler iff $\operatorname{Aut}(b)$.)

Theorems about persons (TP)

(These correspond to the ones listed in the paper\; I’ve silently normalized a couple obvious typos in the paper’s displayed TP1/TP2.)

$TP1$: $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\rightarrow \operatorname{Real}(p)\bigr)$
If a person is Free, they are necessarily a Real person (they own themselves).
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Free}(p)$. By $DP2$, $\operatorname{Free}(p)$ includes $(p<p)$. By $DP1$, $\operatorname{Real}(p)\equiv (p<p)$. Hence $\operatorname{Real}(p)$. $\square$

$TP2$: $\forall p\in\mathcal P\ \bigl(\neg\operatorname{Real}(p)\rightarrow \neg\operatorname{Free}(p)\bigr)$
If a person is not Real (does not own themselves), they cannot be Free.
Proof. Fix $p\in\mathcal P$ and assume $\neg\operatorname{Real}(p)$. Suppose for contradiction that $\operatorname{Free}(p)$. Then by $TP1$, $\operatorname{Real}(p)$, contradicting the assumption. Hence $\neg\operatorname{Free}(p)$. $\square$

A person is Free if and only if they are Sovereign. These concepts are logically equivalent in this system:

$TP3$: $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\rightarrow \operatorname{Sov}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Free}(p)$. By $DP2$, we have $\forall q\in\mathcal P\,(p<q\rightarrow q=p)$. By $DP3$ this is exactly $\operatorname{Sov}(p)$. $\square$

$TP4$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow \operatorname{Free}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Sov}(p)$, i.e. $\forall q\in\mathcal P\,(p<q\rightarrow q=p)$.
By $A_{01}$, $\exists q\in\mathcal P\,(p<q)$. Let such $q$ be given. Then $\operatorname{Sov}(p)$ yields $q=p$, hence $p<p$.
So $(p<p)\wedge \forall q\in\mathcal P\,(p<q\rightarrow q=p)$ holds, i.e. $\operatorname{Free}(p)$ by $DP2$. $\square$

$TP5$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\leftrightarrow \operatorname{Free}(p)\bigr)$
Proof. Immediate from $TP3$ and $TP4$. $\square$

$TP6$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow \operatorname{Real}(p)\bigr)$
If a person is Sovereign, they are necessarily a Real person.
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Sov}(p)$. By $TP4$, $\operatorname{Free}(p)$; then by $TP1$, $\operatorname{Real}(p)$. $\square$

Autonomy results

Van Dun reuses TP5/TP6 numbers here; I mark them with primes.

Autonomy implies Reality (self-ownership), and Sovereignty implies Autonomy. (If you are sovereign, you are automatically autonomous).

$TP5′$: $\forall p\in\mathcal P\ \bigl(\operatorname{Aut}(p)\rightarrow \operatorname{Real}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Aut}(p)$, i.e. $\forall q\in\mathcal P\,(p<q\rightarrow q<p)$ by $DP4$.
By $A_{01}$, choose $q\in\mathcal P$ with $p<q$. Then $\operatorname{Aut}(p)$ gives $q<p$.
From $p<q$ we have $p\in\mathcal M$ by $SD2$ (witness $o:=q$).
Now apply $A_{02}$ with $x:=p$ (note $x\in\mathcal M$), $p:=q$, $q:=p$:
$$
(x<p\ \wedge\ p<q)\ \rightarrow\ x<q
$$
becomes
$$
(p<q\ \wedge\ q<p)\ \rightarrow\ p<p.
$$
Since $p<q$ and $q<p$, conclude $p<p$, i.e. $\operatorname{Real}(p)$ by $DP1$. $\square$

$TP6′$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow \operatorname{Aut}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Sov}(p)$.
First show $p<p$: by $A_{01}$ pick $q\in\mathcal P$ with $p<q$; then $\operatorname{Sov}(p)$ yields $q=p$, hence $p<p$.
Now to show $\operatorname{Aut}(p)$, let any $r\in\mathcal P$ and assume $p<r$. By $\operatorname{Sov}(p)$ we get $r=p$, so $r<p$ is just $p<p$, which holds. Thus $\forall r\in\mathcal P\,(p<r\rightarrow r<p)$, i.e. $\operatorname{Aut}(p)$. $\square$

Heteronomy

$TP7$: $\forall p\in\mathcal P\ \bigl(\operatorname{Aut}(p)\ \vee\ \operatorname{Het}(p)\bigr)$
Every person is either Autonomous (relationships are mutual) or Heteronomous (relationships are one-sided). Proof. By $DP5$, $\operatorname{Het}(p)\equiv \neg\operatorname{Aut}(p)$. So the formula is $\operatorname{Aut}(p)\vee\neg\operatorname{Aut}(p)$, an instance of classical excluded middle. $\square$

$TP8$: $\forall p\in\mathcal P\ \bigl(\neg\operatorname{Real}(p)\rightarrow \operatorname{Het}(p)\bigr)$
If a person is not Real (does not own themselves), they must be Heteronomous. Proof. Fix $p\in\mathcal P$ and assume $\neg\operatorname{Real}(p)$. If $\operatorname{Aut}(p)$ held, then by $TP5′$ we would have $\operatorname{Real}(p)$, contradiction. Hence $\neg\operatorname{Aut}(p)$, i.e. $\operatorname{Het}(p)$ by $DP5$. $\square$

$TP9$: $\forall p\in\mathcal P\ \bigl(\operatorname{Het}(p)\rightarrow \neg\operatorname{Free}(p)\bigr)$
If a person is Heteronomous, they cannot be Free. Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Het}(p)$, i.e. $\neg\operatorname{Aut}(p)$.
If $\operatorname{Free}(p)$, then by $TP3$ $\operatorname{Sov}(p)$, hence by $TP6′$ $\operatorname{Aut}(p)$, contradiction. Therefore $\neg\operatorname{Free}(p)$. $\square$

Strict autonomy

$TP10$: $\forall p\in\mathcal P\ \bigl(\operatorname{Aut}(p)\rightarrow (\operatorname{Sov}(p)\ \vee\ \operatorname{SAut}(p))\bigr)$
If a person is Autonomous, they are either Sovereign (independent) or Strictly Autonomous (interdependent).
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Aut}(p)$.
By classical excluded middle, either $\operatorname{Sov}(p)$ or $\neg\operatorname{Sov}(p)$.

  • If $\operatorname{Sov}(p)$, done.
  • If $\neg\operatorname{Sov}(p)$, then $\operatorname{Aut}(p)\wedge\neg\operatorname{Sov}(p)$ holds, i.e. $\operatorname{SAut}(p)$ by $DP6$.
    Thus $\operatorname{Sov}(p)\vee \operatorname{SAut}(p)$. $\square$

$TP11$: $\forall p\in\mathcal P\ \bigl(\operatorname{SAut}(p)\rightarrow \exists q\in\mathcal P\ (p<q\ \wedge\ q\neq p)\bigr)$
A Strictly Autonomous person always belongs to at least one other person who is not themselves.
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{SAut}(p)$. By $DP6$, $\operatorname{SAut}(p)$ implies $\neg\operatorname{Sov}(p)$.
By $DP3$, $\operatorname{Sov}(p)\equiv \forall q\in\mathcal P\,(p<q\rightarrow q=p)$.
So $\neg\operatorname{Sov}(p)$ is
$$
\neg\forall q\in\mathcal P\,(p<q\rightarrow q=p).
$$
Classically, $\neg\forall q\,\varphi(q)\ \Rightarrow\ \exists q\,\neg\varphi(q)$, so we get
$$
\exists q\in\mathcal P\ \neg(p<q\rightarrow q=p),
$$
equivalently
$$
\exists q\in\mathcal P\ (p<q\ \wedge\ q\neq p).
$$
$\square$

$TP12$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \Bigl((\operatorname{SAut}(p)\ \wedge\ p<q)\rightarrow (\operatorname{SAut}(q)\ \wedge\ q<p)\Bigr)$
Proof (classical, by cases on $q=p$).
Strict Autonomy is reciprocal. If Person A is Strictly Autonomous and belongs to Person B, then Person B must also be Strictly Autonomous and belong to Person A.
Fix $p,q\in\mathcal P$ and assume $\operatorname{SAut}(p)\wedge p<q$. Then $\operatorname{Aut}(p)$ and $\neg\operatorname{Sov}(p)$ by $DP6$.

  1. Show $q<p$. Since $\operatorname{Aut}(p)$ means $\forall r\in\mathcal P\,(p<r\rightarrow r<p)$ (by $DP4$), applying it to $r:=q$ and $p<q$ yields $q<p$.
  2. Show $\operatorname{Aut}(q)$. Let $r\in\mathcal P$ and assume $q<r$.
    From $p<q$ we have $p\in\mathcal M$ by $SD2$. Then $A_{02}$ with $x:=p$, $p:=q$, $q:=r$ gives $p<r$.
    Now $\operatorname{Aut}(p)$ and $p<r$ yield $r<p$. Hence $r\in\mathcal M$ by $SD2$.
    Apply $A_{02}$ with $x:=r$, $p:=p$, $q:=q$ to $(r<p\wedge p<q)$ to conclude $r<q$.
    Thus $q<r\rightarrow r<q$, and since $r$ was arbitrary, $\operatorname{Aut}(q)$.
  3. Show $\neg\operatorname{Sov}(q)$ (classical split). By excluded middle, either $q=p$ or $q\neq p$.
  • Case (i): $q=p$. From $p<q$ we get $p<p$. Since $\operatorname{SAut}(p)$ already gives $\neg\operatorname{Sov}(p)$, and $q=p$, we have $\neg\operatorname{Sov}(q)$.
  • Case (ii): $q\neq p$. We show $\neg\operatorname{Sov}(q)$ by exhibiting a counterexample to the $\forall$ in $DP3$.
    We have $q<p$ from (1). Also $p\in\mathcal P$. So $(q<p\ \wedge\ p\neq q)$ holds, i.e. $\exists r\in\mathcal P\,(q<r\wedge r\neq q)$ (witness $r:=p$).
    But $\operatorname{Sov}(q)$ would imply $\forall r\in\mathcal P\,(q<r\rightarrow r=q)$, contradicting the witness $r=p$. Hence $\neg\operatorname{Sov}(q)$.
  1. Conclude $\operatorname{SAut}(q)$. From (2) $\operatorname{Aut}(q)$ and (3) $\neg\operatorname{Sov}(q)$, we get $\operatorname{SAut}(q)$ by $DP6$.
    Therefore $\operatorname{SAut}(q)\wedge q<p$, as required. $\square$

$TP13$: $\forall p\in\mathcal P\ \bigl(\operatorname{SAut}(p)\rightarrow \neg\operatorname{Free}(p)\bigr)$
A Strictly Autonomous person is not Free (because they are partially owned by others). Proof. Fix $p\in\mathcal P$ and assume $\operatorname{SAut}(p)$. Then by $DP6$, $\neg\operatorname{Sov}(p)$.
If $\operatorname{Free}(p)$, then by $TP3$ we have $\operatorname{Sov}(p)$, contradiction. Hence $\neg\operatorname{Free}(p)$. $\square$

Partition results

$TP14$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\ \vee\ \operatorname{SAut}(p)\ \vee\ \operatorname{Het}(p)\bigr)$
Every person falls into exactly one of three categories: Sovereign, Strictly Autonomous, or Heteronomous.
Proof. Fix $p\in\mathcal P$. By excluded middle, either $\operatorname{Aut}(p)$ or $\neg\operatorname{Aut}(p)$.

  • If $\neg\operatorname{Aut}(p)$ then $\operatorname{Het}(p)$ by $DP5$.
  • If $\operatorname{Aut}(p)$ then by $TP10$, $\operatorname{Sov}(p)\vee\operatorname{SAut}(p)$.
    Thus $\operatorname{Sov}(p)\vee\operatorname{SAut}(p)\vee\operatorname{Het}(p)$. $\square$

These three categories (Sovereign, Strictly Autonomous, or Heteronomous) are mutually exclusive. No person can be in two categories at once:

$TP15$: $\neg\exists p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\ \wedge\ \operatorname{SAut}(p)\bigr)$
Proof. Suppose $\exists p\in\mathcal P\ (\operatorname{Sov}(p)\wedge\operatorname{SAut}(p))$. Then for that $p$, $\operatorname{SAut}(p)$ implies $\neg\operatorname{Sov}(p)$ by $DP6$, contradicting $\operatorname{Sov}(p)$. Hence no such $p$ exists. $\square$

$TP16$: $\neg\exists p\in\mathcal P\ \bigl(\operatorname{SAut}(p)\ \wedge\ \operatorname{Het}(p)\bigr)$
Proof. Suppose $\exists p\in\mathcal P\ (\operatorname{SAut}(p)\wedge\operatorname{Het}(p))$. Then $\operatorname{SAut}(p)$ implies $\operatorname{Aut}(p)$ by $DP6$, while $\operatorname{Het}(p)$ is $\neg\operatorname{Aut}(p)$ by $DP5$. Contradiction. $\square$

$TP17$: $\neg\exists p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\ \wedge\ \operatorname{Het}(p)\bigr)$
Proof. Suppose $\exists p\in\mathcal P\ (\operatorname{Sov}(p)\wedge\operatorname{Het}(p))$. From $\operatorname{Sov}(p)$, $TP6′$ gives $\operatorname{Aut}(p)$. But $\operatorname{Het}(p)$ is $\neg\operatorname{Aut}(p)$. Contradiction. $\square$

Quantitative/“company” result

$TP18$: $\forall p\in\mathcal P\ \Bigl(\neg\operatorname{Sov}(p)\rightarrow \exists q\in\mathcal P\ (p<q\ \wedge\ q\neq p)\Bigr)$
If a person is not Sovereign, they must belong to someone other than themselves.
Proof. Fix $p\in\mathcal P$ and assume $\neg\operatorname{Sov}(p)$.
Unfold $DP3$: $\operatorname{Sov}(p)\equiv \forall q\in\mathcal P\,(p<q\rightarrow q=p)$.
Then $\neg\operatorname{Sov}(p)$ is $\neg\forall q\in\mathcal P\,(p<q\rightarrow q=p)$, which classically implies
$\exists q\in\mathcal P\,\neg(p<q\rightarrow q=p)$, i.e. $\exists q\in\mathcal P\,(p<q\wedge q\neq p)$. $\square$

Uniqueness/solipsism results

$TP19$: $\forall p\in\mathcal P\ \Bigl(\bigl(\operatorname{Aut}(p)\ \wedge\ \forall q\in\mathcal P(\operatorname{Aut}(q)\rightarrow q=p)\bigr)\rightarrow \operatorname{Sov}(p)\Bigr)$
If a person is Autonomous, and they are the only Autonomous person in existence, they must be Sovereign.
Proof. Fix $p\in\mathcal P$ and assume:
(i) $\operatorname{Aut}(p)$, and
(ii) $\forall q\in\mathcal P(\operatorname{Aut}(q)\rightarrow q=p)$.

To show $\operatorname{Sov}(p)$, let $q\in\mathcal P$ and assume $p<q$. We must prove $q=p$.

First, from (i) and $p<q$, we have $q<p$ (by $DP4$).
We now prove the auxiliary claim: $\operatorname{Aut}(q)$.

Auxiliary claim: $\operatorname{Aut}(q)$.
Let $r\in\mathcal P$ and assume $q<r$. We show $r<q$.

  • From $p<q$ and $q<r$, note $p\in\mathcal M$ because $p<q$ (by $SD2$). Apply $A_{02}$ with $x:=p$, $p:=q$, $q:=r$ to get $p<r$.
  • Using (i) $\operatorname{Aut}(p)$ and $p<r$, we get $r<p$.
  • Since $r<p$, we have $r\in\mathcal M$ (by $SD2$). Apply $A_{02}$ with $x:=r$, $p:=p$, $q:=q$ to get $r<q$ from $(r<p \wedge p<q)$.
    Thus $q<r\rightarrow r<q$, and since $r$ was arbitrary, $\operatorname{Aut}(q)$ holds. (End auxiliary claim.)

Now apply (ii) to $q$: since $\operatorname{Aut}(q)$, we conclude $q=p$.
Therefore $\forall q\in\mathcal P\,(p<q\rightarrow q=p)$, i.e. $\operatorname{Sov}(p)$ by $DP3$. $\square$

$TP20$: $\forall p\in\mathcal P\ \Bigl(\bigl(\forall q\in\mathcal P\ (q=p)\bigr)\rightarrow \operatorname{Sov}(p)\Bigr)$
If only one person exists in the universe, that person must be Sovereign.
Proof. Fix $p\in\mathcal P$ and assume $\forall q\in\mathcal P\,(q=p)$.
To show $\operatorname{Sov}(p)$, let $q\in\mathcal P$ and assume $p<q$. By the assumption, $q=p$. Hence $p<q\rightarrow q=p$, and since $q$ was arbitrary, $\forall q\in\mathcal P\,(p<q\rightarrow q=p)$, i.e. $\operatorname{Sov}(p)$ by $DP3$. $\square$

“Meta-theorems” about finiteness/infinity (MT)

These aren’t first-order consequences expressible inside $\mathbf L_0$ without extra machinery (because “finite/infinite” is metalanguage here), so our rendering is in terms of cardinality $|\mathcal P|$; we will use the derived lemma that $<$ is transitive on $\mathcal P$.

Lemma (Transitivity on persons). For all $a,b,c\in\mathcal P$, if $a<b$ and $b<c$, then $a<c$.
Proof. If $a<b$, then $a\in\mathcal M$ by $SD2$ (witness $o:=b$). Apply $A_{02}$ with $x:=a$, $p:=b$, $q:=c$ to get $a<c$. $\square$

$MT3$: $(|\mathcal P|<\infty)\ \rightarrow\ \exists p\in\mathcal P\ \operatorname{Aut}(p)$
If the number of people is finite, there must be at least one Autonomous person. (You cannot have an endless chain of masters without looping back or stopping).
Proof (metalanguage). Assume $|\mathcal P|<\infty$. Consider the preorder on $\mathcal P$ given by $<$; by the lemma it is transitive.
Define an equivalence relation on $\mathcal P$ by $u\sim v$ iff $(u<v)\wedge(v<u)$. Transitivity of $<$ ensures $\sim$ behaves as the standard “mutual reachability” relation for a preorder.
Let $\mathcal P/{\sim}$ be the finite set of equivalence classes, partially ordered by $[u]\le [v]$ iff $u<v$.
A finite poset has a maximal element; pick a maximal class $[p]$.
We claim $\operatorname{Aut}(p)$. Take any $q\in\mathcal P$ with $p<q$. Then $[p]\le [q]$, so maximality forces $[q]=[p]$, hence $q\sim p$, i.e. $q<p$. Therefore $\forall q\in\mathcal P\,(p<q\rightarrow q<p)$, i.e. $\operatorname{Aut}(p)$. $\square$

$MT1$: $\bigl(\forall p\in\mathcal P\ \operatorname{Het}(p)\bigr)\ \rightarrow\ (|\mathcal P|=\infty)$
If every single person is Heteronomous (a serf), then there must be an infinite number of people. (An endless chain of serfs belonging to masters who are themselves serfs).
Proof (metalanguage). Suppose $\forall p\in\mathcal P\ \operatorname{Het}(p)$, i.e. $\forall p\in\mathcal P\ \neg\operatorname{Aut}(p)$.
If $|\mathcal P|<\infty$, then by $MT3$ there exists $p\in\mathcal P$ with $\operatorname{Aut}(p)$, contradiction.
Hence $|\mathcal P|\not<\infty$, i.e. $|\mathcal P|=\infty$. $\square$

$MT4$: $\bigl((|\mathcal P|<\infty)\ \wedge\ \exists a\in\mathcal P\ \operatorname{Het}(a)\bigr)\ \rightarrow\ \exists a\in\mathcal P\ \exists b\in\mathcal P\ \bigl(\operatorname{Het}(a)\wedge \operatorname{Aut}(b)\wedge a<b\bigr)$
If the population is finite and there is at least one Heteronomous person (serf), there must be a chain of ownership leading up to an Autonomous person (a Ruler or Sovereign).
Proof (metalanguage). Assume $|\mathcal P|<\infty$ and pick $a\in\mathcal P$ with $\operatorname{Het}(a)$.
Starting from $a$, iteratively choose $p_{n+1}\in\mathcal P$ with $p_n<p_{n+1}$ using $A_{01}$. Because $\mathcal P$ is finite, some equivalence class (under $\sim$ as in $MT3$) among the $p_n$ is maximal among those reachable from $a$; choose $b$ in such a maximal reachable class.
Then $a<b$ (reachability gives $a<b$ by repeated transitivity), and the same maximality argument as in $MT3$ shows $\operatorname{Aut}(b)$.
Thus $\exists b\in\mathcal P\,(\operatorname{Aut}(b)\wedge a<b)$ with the chosen $a$ still satisfying $\operatorname{Het}(a)$. $\square$

$MT2$: $\bigl(\exists a\in\mathcal P\ \operatorname{SerfNotSubject}(a)\bigr)\ \rightarrow\ (|\mathcal P|=\infty)$
If there exists a “Serf who is not a Subject” (meaning they are a serf owned by someone who is not Autonomous), then the population must be infinite.
Proof (metalanguage). Assume $\exists a\in\mathcal P\ \operatorname{SerfNotSubject}(a)$, so for some $a\in\mathcal P$:
(1) $\operatorname{Het}(a)$, and
(2) $\neg\exists b\in\mathcal P(\operatorname{Aut}(b)\wedge a<b)$.

If $|\mathcal P|<\infty$, then by $MT4$ (using the same $a$ from (1)) we would get some $b\in\mathcal P$ with $\operatorname{Aut}(b)\wedge a<b$, contradicting (2).
Therefore $|\mathcal P|\not<\infty$, i.e. $|\mathcal P|=\infty$. $\square$

Collectives

Definition

We define a special relationship ($\sim$) between two persons, $p$ and $q$. This relationship exists when $p$ is a Strictly Autonomous person who belongs to $q$. Note: Since Strict Autonomy involves mutual ownership, this definition sets the stage for a group of people who all belong to one another.

$DP7$: $p\sim q \;\:=\; \bigl(p\in\mathcal P \wedge q\in\mathcal P \wedge \operatorname{SAut}(p)\wedge (p<q)\bigr)$

(So $p\sim q$ reads: “$p$ is strictly autonomous and belongs to $q$”—exactly Van Dun’s DP7, just with $\sim$ and $<$.)

Theorems

$TP21$ (No Solitary Members): $\forall p\in\mathcal P\ \Bigl(\operatorname{SAut}(p)\rightarrow \exists q\in\mathcal P\ (q\neq p\ \wedge\ p\sim q)\Bigr)$
If a person is Strictly Autonomous, there must be at least one other person to whom they belong. You cannot be “strictly autonomous” all by yourself.
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{SAut}(p)$. By $TP11$, $\exists q\in\mathcal P\,(p<q\ \wedge\ q\neq p)$. Choose such a $q$.
By $DP7$, $p\sim q$ abbreviates $(p\in\mathcal P\wedge q\in\mathcal P\wedge \operatorname{SAut}(p)\wedge (p<q))$, all of which hold for our $p,q$. Hence $q\neq p\ \wedge\ p\sim q$. Therefore $\exists q\in\mathcal P\,(q\neq p\ \wedge\ p\sim q)$. $\square$

$TP22$ (Membership Implies Status): $\forall p\in\mathcal P\ \Bigl(\bigl(\exists q\in\mathcal P\ (p\sim q)\bigr)\rightarrow \operatorname{SAut}(p)\Bigr)$
Conversely, if a person stands in this collective relationship with anyone else, they are by definition Strictly Autonomous.
Proof. Fix $p\in\mathcal P$ and assume $\exists q\in\mathcal P\,(p\sim q)$. Choose such $q$. By $DP7$, $p\sim q$ implies $\operatorname{SAut}(p)$. $\square$

$TP23$ (Self-Membership): $\forall p\in\mathcal P\ \bigl(\operatorname{SAut}(p)\rightarrow p\sim p\bigr)$
Every Strictly Autonomous person belongs to themselves (they are part of the collective that owns them).
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{SAut}(p)$. Then $\operatorname{Aut}(p)$ by $DP6$. By $TP5'$, $\operatorname{Aut}(p)\rightarrow \operatorname{Real}(p)$, hence $\operatorname{Real}(p)$. By $DP1$, $\operatorname{Real}(p)\equiv (p<p)$, so $p<p$.
Now $DP7$ gives $p\sim p$ since $p\in\mathcal P$, $p\in\mathcal P$, $\operatorname{SAut}(p)$, and $p<p$. $\square$

$TP24$ (Reciprocity): $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \bigl((p\sim q)\rightarrow (q\sim p)\bigr)$
The collective relationship is symmetrical. If $p$ belongs to $q$ in this way, then $q$ must also belong to $p$.
Proof (uses $TP12$). Fix $p,q\in\mathcal P$ and assume $p\sim q$. By $DP7$, $\operatorname{SAut}(p)$ and $p<q$. Applying $TP12$ to $(\operatorname{SAut}(p)\wedge p<q)$ yields $\operatorname{SAut}(q)$ and $q<p$. Then by $DP7$ (with roles swapped), $q\sim p$. $\square$

$TP25$ (Transitivity): $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall r\in\mathcal P\ \bigl((p\sim q\ \wedge\ q\sim r)\rightarrow (p\sim r)\bigr)$
The relationship extends through the group. If $p$ is connected to $q$, and $q$ is connected to $r$, then $p$ is connected to $r$. The collective is a unified web of mutual ownership.
Proof. Fix $p,q,r\in\mathcal P$ and assume $p\sim q\ \wedge\ q\sim r$. From $p\sim q$ and $DP7$ we get $\operatorname{SAut}(p)$ and $p<q$. From $q\sim r$ and $DP7$ we get $q<r$ (and $r\in\mathcal P$).
Since $p<q$, by $SD2$ we have $p\in\mathcal M$ (witness $o:=q$). Now apply $A_{02}$ with $x:=p$, $p:=q$, $q:=r$: \[ ((p<q)\wedge(q<r))\rightarrow (p<r). \] Hence $p<r$. Finally, by $DP7$, $p\sim r$ holds because $p\in\mathcal P$, $r\in\mathcal P$, $\operatorname{SAut}(p)$, and $p<r$. $\square$

$TP26$ (Communism of Means): $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M\ \Bigl((p\sim q)\rightarrow\bigl((x<p)\leftrightarrow(x<q)\bigr)\Bigr)$
Within a collective, ownership of external objects (means) is shared. If $p$ and $q$ are members of the same collective, any means that belongs to $p$ necessarily belongs to $q$, and vice versa.
Proof. Fix $p,q\in\mathcal P$ and $x\in\mathcal M$, and assume $p\sim q$. By $DP7$, $\operatorname{SAut}(p)$ and $p<q$. Also $\operatorname{SAut}(p)\rightarrow \operatorname{Aut}(p)$ by $DP6$.
($\Rightarrow$) Assume $x<p$. Since $x\in\mathcal M$ and $p<q$, apply $A_{02}$ (with $p:=p$, $q:=q$) to get $x<q$.
($\Leftarrow$) Assume $x<q$. From $\operatorname{Aut}(p)$ and $p<q$, we have $q<p$ by $DP4$. Since $x\in\mathcal M$ and $q<p$, apply $A_{02}$ with $p:=q$ and $q:=p$ to get $x<p$.
Thus $(x<p)\leftrightarrow(x<q)$. $\square$

Rousseau-style formal suppositions

These are not derived theorems, but specific assumptions used to model the “Social Contract” theory of Jean-Jacques Rousseau using this logic.

New concepts:

  • Civic Persona ($c(p)$): The artificial “citizen” version of a natural person.
  • Legal Belonging ($<_L$): A distinct type of ownership defined by positive law rather than natural reality.

Introduce a function $c:\mathcal P\to\mathcal P$ (“civic persona”), and a second “legal belonging” relation $<_{L}\subseteq\mathcal D\times\mathcal D$.

$R1$ (Alienation): $\forall p\in\mathcal P\ \bigl(\operatorname{SAut}(p)\rightarrow c(p)\neq p\bigr)$
For a Strictly Autonomous person (a member of the State), their “Civic Persona” is a distinct entity from their natural self. They are not identical.

$R2$ (The General Will): $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \bigl((p\sim q)\rightarrow c(p)=c(q)\bigr)$
If two people are in the same collective, they share the exact same Civic Persona. The “Citizen” is a singular collective abstract, not a unique individual.

$R3$ (Subordination to the State): $\forall p\in\mathcal P\ \Bigl(\operatorname{SAut}(p)\rightarrow \bigl(p<_{L}c(p)\ \wedge\ \neg(c(p)<_{L}p)\bigr)\Bigr)$
A member of the collective legally belongs to their Civic Persona, but the Civic Persona does not belong to them. The relationship is hierarchical, not mutual.

$R4$ (State Property): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \Bigl((\operatorname{SAut}(p)\wedge x<p)\rightarrow x<_{L}c(p)\Bigr)$
Any means (property) owned by a member of the collective naturally is considered to legally belong to the Civic Persona (the State).

And the later “aspect person” schema (with $\varepsilon:\mathcal P\to\mathcal P$):

$E1$: $\forall p\in\mathcal P\ \bigl(\varepsilon(p)<p\ \wedge\ \neg(p<\varepsilon(p))\bigr)$
This encodes the “natural” direction you’d expect for fictions/roles: the persona depends on (and is subordinate to) the real person who generates/occupies it. Van Dun argues Rousseau reverses this.

Rights

Definitions (DR)

Right to deny

$DR1$ (Right to Deny): $p\uparrow q/x \;\:=\; \bigl((x<p)\ \vee\ (q<p)\bigr)\ \wedge\ \neg(p<q)
\qquad(p,q\in\mathcal P,\ x\in\mathcal M)$

That is, Person $p$ has the right to deny Person $q$ the use of Object $x$ if:

  • Person $p$ owns Object $x$ (or owns Person $q$), AND
  • Person $p$ is not owned by Person $q$.

More briefly: I can say “no” if I own the thing, and you don’t own me.

$DR2$ (Freedom to Use): $p/x\downarrow q \;\:=\; \neg\bigl(q\uparrow p/x\bigr)
\qquad(p,q\in\mathcal P,\ x\in\mathcal M)$
Person $p$ is “free to use” Object $x$ with respect to Person $q$ if Person $q$ does not have the right to deny them.

$DR3$ (Right to Use): $p/x\Downarrow q \;\:=\; (x<p)\ \wedge\ \neg\bigl(q\uparrow p/x\bigr)
\qquad(p,q\in\mathcal P,\ x\in\mathcal M)$

That is, Person $p$ has a positive “right to use” Object $x$ against Person $q$ if:

  • Person $p$ actually owns $x$, AND
  • Person $q$ has no standing to deny them.

Absolute right to use

$DR4$ (Absolute Right): $p/x\Downarrow\Downarrow \;\:=\; \forall q\in\mathcal P\ \bigl(p/x\Downarrow q\bigr)
\qquad(p\in\mathcal P,\ x\in\mathcal M)$
Person $p$ has an Absolute Right to Object $x$ if they have the right to use it against every other person in existence.

Theorems (TR)

Immediate consequences of DR1

$TR1a$: $\forall p\in\mathcal P\ \neg\bigl(p\uparrow p/p\bigr)$
A person cannot deny themselves the use of themselves. (Logically impossible).
Proof. Fix $p\in\mathcal P$. By $DR1$ (with $q:=p$ and $x:=p$),
\[
p\uparrow p/p \;\equiv\; \bigl((p<p)\ \vee\ (p<p)\bigr)\ \wedge\ \neg(p<p),
\]
i.e.
\[
p\uparrow p/p \;\equiv\; (p<p)\wedge \neg(p<p),
\]
which is impossible. Hence $\neg(p\uparrow p/p)$. $\square$

$TR1b$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \Bigl(\operatorname{Sov}(p)\rightarrow (q\neq p\rightarrow (p\uparrow q/p))\Bigr)$
A Sovereign person (who owns themselves exclusively) has the right to deny everyone else the use of their person.
Proof. Fix $p,q\in\mathcal P$ and assume $\operatorname{Sov}(p)$ and $q\neq p$.
First, $\operatorname{Sov}(p)$ implies $p<p$: by $A_{01}$ pick $r\in\mathcal P$ with $p<r$, then $\operatorname{Sov}(p)$ yields $r=p$, hence $p<p$.
Second, if $p<q$ then $\operatorname{Sov}(p)$ gives $q=p$, contradicting $q\neq p$; thus $\neg(p<q)$.
Now by $DR1$ (with $x:=p$),
\[
p\uparrow q/p \;\equiv\; \bigl((p<p)\ \vee\ (q<p)\bigr)\wedge \neg(p<q).
\]
The left disjunct $p<p$ holds, and we have $\neg(p<q)$, so $p\uparrow q/p$. $\square$

If a person could deny themselves the use of a means, that person would have to be “imaginary” (not a Real Person). Real people cannot validly deny themselves their own property in this structure:

$TR2a$: $\forall p\in\mathcal P\ \forall x\in\mathcal M\ \Bigl((p\uparrow p/x)\rightarrow (x<p)\Bigr)$
Proof. Fix $p\in\mathcal P$ and $x\in\mathcal M$, and assume $p\uparrow p/x$.
By $DR1$,
\[
p\uparrow p/x \;\equiv\; \bigl((x<p)\ \vee\ (p<p)\bigr)\ \wedge\ \neg(p<p).
\]
So $(x<p)\vee(p<p)$ and $\neg(p<p)$ both hold; hence $x<p$. $\square$

$TR2b$: $\forall p\in\mathcal P\ \forall x\in\mathcal M\ \Bigl((p\uparrow p/x)\rightarrow \neg(p<p)\Bigr)$ (i.e. only non-real/“imaginary” persons satisfy $p\uparrow p/x$.)
Proof. Fix $p\in\mathcal P$ and $x\in\mathcal M$. From $DR1$,
\[
p\uparrow p/x \;\Rightarrow\; \neg(p<p)
\]
since $\neg(p<p)$ is a conjunct of the defining formula. $\square$

Relations between “right” and “free”

$TR3$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M\ \Bigl((p/x\Downarrow q)\rightarrow (p/x\downarrow q)\Bigr)$
If you have a right to use something, you are automatically free to use it.
Proof. Fix $p,q\in\mathcal P$ and $x\in\mathcal M$, and assume $p/x\Downarrow q$.
By $DR3$, $p/x\Downarrow q$ implies $\neg(q\uparrow p/x)$.
By $DR2$, $p/x\downarrow q \;\equiv\; \neg(q\uparrow p/x)$.
Therefore $p/x\downarrow q$. $\square$

Rights to the use of oneself

$TR4$: $\forall p\in\mathcal P\ \bigl((p<p)\rightarrow (p/p\Downarrow p)\bigr)$
If you are a Real Person (you exist and own yourself), you have the right to use yourself.
Proof. Fix $p\in\mathcal P$ and assume $p<p$.
By $DR3$,
\[
p/p\Downarrow p \;\equiv\; (p<p)\ \wedge\ \neg(p\uparrow p/p).
\]
The first conjunct is our assumption, and the second holds by $TR1a$. Hence $p/p\Downarrow p$. $\square$

Let $\operatorname{Real}(p)\:= (p<p)$ as before. Then:

$TR5$: $\forall p\in\mathcal P\ \Bigl((p/p\Downarrow p)\leftrightarrow \operatorname{Real}(p)\Bigr)$
Possessing the right to use oneself is logically equivalent to being a Real Person.
Proof. Fix $p\in\mathcal P$.
($\Rightarrow$) Assume $p/p\Downarrow p$. By $DR3$ with $x:=p$, we get $(p<p)$ as the first conjunct. By $DP1$, $\operatorname{Real}(p)\equiv(p<p)$, so $\operatorname{Real}(p)$.
($\Leftarrow$) Assume $\operatorname{Real}(p)$. By $DP1$, this means $p<p$. Then $TR4$ gives $p/p\Downarrow p$.
Thus $(p/p\Downarrow p)\leftrightarrow \operatorname{Real}(p)$. $\square$

Absolute right to the use of oneself for autonomous/sovereign persons

$TR6$: $\forall p\in\mathcal P\ \bigl(\operatorname{Aut}(p)\rightarrow (p/p\Downarrow\Downarrow)\bigr)$
Autonomous persons (whether Sovereign or strictly autonomous) have an absolute right to use themselves. No one can legitimately stop them.
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Aut}(p)$.
We show $\forall q\in\mathcal P\ (p/p\Downarrow q)$.
Let $q\in\mathcal P$ be arbitrary. By $DR3$,
\[
p/p\Downarrow q \;\equiv\; (p<p)\ \wedge\ \neg(q\uparrow p/p).
\]
First, $\operatorname{Aut}(p)\rightarrow \operatorname{Real}(p)$ by $TP5'$, so $p<p$ by $DP1$.
For the second conjunct, suppose $q\uparrow p/p$. By $DR1$,
\[
q\uparrow p/p \;\equiv\; \bigl((p<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p),
\]
i.e. $(p<q)\wedge \neg(q<p)$. But $\operatorname{Aut}(p)$ (via $DP4$) gives $(p<q)\rightarrow (q<p)$, contradiction. Hence $\neg(q\uparrow p/p)$.
Therefore $p/p\Downarrow q$, and since $q$ was arbitrary, $p/p\Downarrow\Downarrow$. $\square$

$TR7$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow (p/p\Downarrow\Downarrow)\bigr)$
Sovereign persons specifically have an absolute right to use themselves.
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Sov}(p)$. By $TP6'$, $\operatorname{Aut}(p)$. Then by $TR6$, $p/p\Downarrow\Downarrow$. $\square$

$TR8$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M\
\Bigl((x<q\ \wedge\ \neg(q<p))\rightarrow \neg(p/x\Downarrow q)\Bigr)$
If an object belongs to someone ($q$) who does not belong to you, you do not have the right to use that object against their will.
Proof. Fix $p,q\in\mathcal P$ and $x\in\mathcal M$, and assume $x<q$ and $\neg(q<p)$.
Then by $DR1$ (with first person $q$, second person $p$),
\[
q\uparrow p/x \;\equiv\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p).
\]
The left disjunction holds since $x<q$, and $\neg(q<p)$ holds by assumption, so $q\uparrow p/x$.
But $p/x\Downarrow q$ (by $DR3$) would imply $\neg(q\uparrow p/x)$, contradiction. Hence $\neg(p/x\Downarrow q)$. $\square$

A fortiori for sovereign:

$TR9$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M
\Bigl((\operatorname{Sov}(q)\ \wedge\ x<q\ \wedge\ p\neq q)\rightarrow \neg(p/x\Downarrow q)\Bigr)$
Specifically, no one has the right to use the property of a Sovereign person (except the Sovereign themselves).
Proof. Fix $p,q\in\mathcal P$ and $x\in\mathcal M$, and assume $\operatorname{Sov}(q)$, $x<q$, and $p\neq q$.
We claim $\neg(q<p)$: if $q<p$, then by $\operatorname{Sov}(q)$ we would have $p=q$, contradicting $p\neq q$.
Thus $x<q\wedge \neg(q<p)$ holds, and $TR8$ yields $\neg(p/x\Downarrow q)$. $\square$

Two structurally important “propagation” theorems

$TR10$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\
\Bigl((p<q)\rightarrow (q/p\Downarrow p)\Bigr)$
If you belong to someone else (if you are a serf and they are a master), they have the right to use you.
Proof. Fix $p,q\in\mathcal P$ and assume $p<q$.
By $DR3$,
\[
q/p\Downarrow p \;\equiv\; (p<q)\ \wedge\ \neg(p\uparrow q/p).
\]
The first conjunct is the assumption. For the second, note that by $DR1$,
\[
p\uparrow q/p \;\Rightarrow\; \neg(p<q),
\]
but $p<q$ holds, so $p\uparrow q/p$ is impossible; hence $\neg(p\uparrow q/p)$.
Therefore $q/p\Downarrow p$. $\square$

$TR11$ (Propagation of Rights): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall r\in\mathcal P
\Bigl((p/x\Downarrow q\ \wedge\ r<q)\rightarrow (p/x\Downarrow r)\Bigr)$
If you have the right to use an object against a Master, you automatically have the right to use it against that Master’s serfs. (Rights against the owner extend to the owned).
Proof. Fix $x\in\mathcal M$ and $p,q,r\in\mathcal P$, and assume $p/x\Downarrow q$ and $r<q$.
From $p/x\Downarrow q$ and $DR3$ we get $x<p$ and $\neg(q\uparrow p/x)$.
To prove $p/x\Downarrow r$, by $DR3$ it suffices to show $x<p$ (already have it) and $\neg(r\uparrow p/x)$.

Suppose for contradiction that $r\uparrow p/x$. By $DR1$,
\[
r\uparrow p/x \;\equiv\; \bigl((x<r)\ \vee\ (p<r)\bigr)\ \wedge\ \neg(r<p).
\]
We derive $q\uparrow p/x$.

  1. Show $(x<q)\ \vee\ (p<q)$:
  • If $x<r$, then since $x\in\mathcal M$ and $r<q$, $A_{02}$ gives $x<q$.
  • If $p<r$, then $p\in\mathcal M$ by $SD2$, and with $r<q$, $A_{02}$ gives $p<q$.
    Hence $(x<q)\vee(p<q)$.
  1. Show $\neg(q<p)$:
    Because $r\in\mathcal P$, by $A_{01}$ choose $s\in\mathcal P$ with $r<s$, so $r\in\mathcal M$ by $SD2$.
    If $q<p$, then using $r<q$ and $r\in\mathcal M$, $A_{02}$ yields $r<p$, contradicting $\neg(r<p)$.
    Therefore $\neg(q<p)$.

Combining (1) and (2), $DR1$ yields
\[
q\uparrow p/x \;\equiv\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p),
\]
so $q\uparrow p/x$, contradicting $\neg(q\uparrow p/x)$.
Hence $\neg(r\uparrow p/x)$, and thus $p/x\Downarrow r$. $\square$

Connections to collectives and heteronomy

(Using $p\sim q$ from DP7 in the “collectives” section.)

$TR12$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M
\Bigl((p\sim q\ \wedge\ x<p)\rightarrow (q/x\Downarrow p)\Bigr)$
In a collective (where members belong to each other), if one member owns an object, the other members have a right to use it.
Proof. Fix $p,q\in\mathcal P$ and $x\in\mathcal M$, and assume $p\sim q$ and $x<p$.
By $DP7$, $p\sim q$ implies $p<q$ (and $p,q\in\mathcal P$).
First, from $x<p$ and $p<q$ with $x\in\mathcal M$, apply $A_{02}$ to obtain $x<q$.
Second, to show $\neg(p\uparrow q/x)$: by $DR1$,
\[
p\uparrow q/x \;\equiv\; \bigl((x<p)\ \vee\ (q<p)\bigr)\ \wedge\ \neg(p<q).
\]
But $p<q$ holds, so $\neg(p<q)$ is false, hence $p\uparrow q/x$ is false and $\neg(p\uparrow q/x)$ holds.
Therefore, by $DR3$, $q/x\Downarrow p$ (since $x<q$ and $\neg(p\uparrow q/x)$). $\square$

$TR13$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\
\bigl((p\sim q)\rightarrow (p/q\Downarrow q)\bigr)$
In a collective, members have the right to use each other. (Since they belong to one another).
Proof. Fix $p,q\in\mathcal P$ and assume $p\sim q$. By $DP7$, $\operatorname{SAut}(p)$ and $p<q$.
From $\operatorname{SAut}(p)$ we have $\operatorname{Aut}(p)$ by $DP6$, hence from $p<q$ we get $q<p$ by $DP4$.
Now by $DR3$,
\[
p/q\Downarrow q \;\equiv\; (q<p)\ \wedge\ \neg(q\uparrow p/q).
\]
The first conjunct $q<p$ holds. For the second, by $DR1$,
\[
q\uparrow p/q \;\equiv\; \bigl((q<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p).
\]
But $q<p$ holds, so $\neg(q<p)$ is false, hence $q\uparrow p/q$ is false and $\neg(q\uparrow p/q)$ holds.
Therefore $p/q\Downarrow q$. $\square$

$TR14$: $\forall p\in\mathcal P\ \forall x\in\mathcal M
\Bigl((\operatorname{Het}(p)\ \wedge\ x<p)\rightarrow \exists q\in\mathcal P\ (q/x\Downarrow p)\Bigr)$
If you are Heteronomous (owned by others), there is always someone else who has the right to use your property.
Proof. Fix $p\in\mathcal P$ and $x\in\mathcal M$, and assume $\operatorname{Het}(p)$ and $x<p$.
By $A_{01}$, choose $q\in\mathcal P$ such that $p<q$.
Then from $x<p$ and $p<q$ with $x\in\mathcal M$, $A_{02}$ yields $x<q$.
Also, by $DR1$,
\[
p\uparrow q/x \;\equiv\; \bigl((x<p)\ \vee\ (q<p)\bigr)\ \wedge\ \neg(p<q),
\]
but $p<q$ holds, so $p\uparrow q/x$ is false and $\neg(p\uparrow q/x)$ holds.
Thus by $DR3$, $q/x\Downarrow p$. Hence $\exists q\in\mathcal P\ (q/x\Downarrow p)$. $\square$

$TR15$: $\forall p\in\mathcal P\ \forall x\in\mathcal M
\Bigl((\operatorname{Het}(p)\ \wedge\ x<p)\rightarrow \exists q\in\mathcal P\ \neg(p/x\Downarrow q)\Bigr)$
If you are Heteronomous, there is always someone against whom you cannot assert a right to use your own property.
Proof. Fix $p\in\mathcal P$ and $x\in\mathcal M$, and assume $\operatorname{Het}(p)$ and $x<p$.
Since $\operatorname{Het}(p)\equiv \neg\operatorname{Aut}(p)$ (by $DP5$) and $\operatorname{Aut}(p)\equiv \forall q\in\mathcal P\,(p<q\rightarrow q<p)$ (by $DP4$), we obtain
\[
\exists q\in\mathcal P\ \bigl(p<q\ \wedge\ \neg(q<p)\bigr).
\]
Choose such $q\in\mathcal P$. Then by $DR1$,
\[
q\uparrow p/x \;\equiv\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p).
\]
Here $p<q$ holds, and $\neg(q<p)$ holds, so $q\uparrow p/x$ holds.
But $p/x\Downarrow q$ (by $DR3$) would imply $\neg(q\uparrow p/x)$, contradiction. Hence $\neg(p/x\Downarrow q)$.
Therefore $\exists q\in\mathcal P\ \neg(p/x\Downarrow q)$. $\square$

$TR16$: $\forall p\in\mathcal P
\Bigl(\operatorname{Het}(p)\rightarrow \exists q\in\mathcal P\ (q/p\Downarrow p)\Bigr)$
If you are Heteronomous, there is someone who has the right to use you.
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Het}(p)$. By $A_{01}$ choose $q\in\mathcal P$ with $p<q$.
By $DR3$,
\[
q/p\Downarrow p \;\equiv\; (p<q)\ \wedge\ \neg(p\uparrow q/p).
\]
The first conjunct holds. For the second, $DR1$ gives $p\uparrow q/p \Rightarrow \neg(p<q)$, contradicting $p<q$; hence $\neg(p\uparrow q/p)$.
Thus $q/p\Downarrow p$, and so $\exists q\in\mathcal P\ (q/p\Downarrow p)$. $\square$

Property

Definitions (DY)

Ownership

There is a distinction between an object simply “belonging” to someone ($x < p$) and someone “owning” that object ($x \ll p$).

$DY1$ (Ownership): $x\ll p \;\:=\; (x<p)\ \wedge\ \forall q\in\mathcal P\bigl((x<q)\rightarrow(q<p)\bigr)
\qquad(x\in\mathcal M,\ p\in\mathcal P)$

That is, Person $p$ Owns Object $x$ if:

  • The object belongs to $p$, AND
  • Anyone else to whom the object belongs must effectively belong to $p$.

Meaning: Ownership is the “highest title.” If you hold the object, but you belong to me, then I am the owner of the object.

Common property

$DY2$ (Common Property): $x<p,q \;\:=\; (x<p)\ \wedge\ (x<q)
\qquad(x\in\mathcal M,\ p,q\in\mathcal P)$
An object is “Common Property” simply if it belongs to Person $p$ and also belongs to Person $q$. (Simple co-possession).

Communal property

$DY3$ (Communal Property): $(p\Downarrow q)/x \;\:=\; (p/x\Downarrow q)\ \wedge\ (q/x\Downarrow p)
\qquad(x\in\mathcal M,\ p,q\in\mathcal P)$
An object is “Communal Property” if both Person $p$ and Person $q$ have a recognized right to use it against one another. (This is a stronger legal claim than simple possession).

Theorems (TY)

Owners must be real/autonomous; heteronomous persons own nothing

(Recall $\operatorname{Real}(p)\:= (p<p)$.)

$TY1$ (Owners must be Real): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \bigl((x\ll p)\rightarrow \operatorname{Real}(p)\bigr)$
If a person owns anything at all, they must be a Real Person (they must own themselves). A person who does not own themselves cannot validly own external objects in the ultimate sense.
Proof. Fix $x\in\mathcal M$ and $p\in\mathcal P$, and assume $x\ll p$. By $DY1$, we have:

  1. $x<p$, and
  2. $\forall q\in\mathcal P\bigl((x<q)\rightarrow(q<p)\bigr)$.

By $A_{01}$ choose $q\in\mathcal P$ with $p<q$. Since $x\in\mathcal M$, from $x<p$ and $p<q$ we get $x<q$ by $A_{02}$. Then (2) yields $q<p$.

Now $p<q$ implies $p\in\mathcal M$ by $SD2$ (witness $o:=q$). Apply $A_{02}$ with $x:=p$, $p:=q$, $q:=p$:
\[
((p<q)\wedge(q<p))\rightarrow (p<p).
\]
Thus $p<p$, i.e. $\operatorname{Real}(p)$ by $DP1$. $\square$

$TY2$ (Owners must be Autonomous): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \bigl((x\ll p)\rightarrow \operatorname{Aut}(p)\bigr)$
If a person owns anything, they must be Autonomous. Proof. Fix $x\in\mathcal M$ and $p\in\mathcal P$, and assume $x\ll p$. By $DY1$, $x<p$ and
\[
\forall q\in\mathcal P\bigl((x<q)\rightarrow(q<p)\bigr).
\]
To prove $\operatorname{Aut}(p)$ (i.e. $DP4$), let $q\in\mathcal P$ and assume $p<q$. Since $x\in\mathcal M$, from $x<p$ and $p<q$ we get $x<q$ by $A_{02}$. Then the universal condition in $DY1$ yields $q<p$. Hence $\forall q\in\mathcal P\,(p<q\rightarrow q<p)$, so $\operatorname{Aut}(p)$. $\square$

$TY3$ (Serfs Own Nothing): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \bigl(\operatorname{Het}(p)\rightarrow \neg(x\ll p)\bigr)$
A Heteronomous person (a serf) cannot own anything. Since a serf belongs to a master who does not belong to the serf, any object the serf holds ultimately belongs to the master (by the logic of DY1).
Proof. Fix $x\in\mathcal M$ and $p\in\mathcal P$, and assume $\operatorname{Het}(p)$. Suppose for contradiction that $x\ll p$. Then by $TY2$, $\operatorname{Aut}(p)$. But $\operatorname{Het}(p)\equiv \neg\operatorname{Aut}(p)$ by $DP5$. Contradiction. Hence $\neg(x\ll p)$. $\square$

Self-ownership characterizations

Both Sovereign persons and Autonomous persons own themselves:

$TY4$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow (p\ll p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Sov}(p)$. We show $p\ll p$, i.e. by $DY1$:
\[
(p<p)\ \wedge\ \forall q\in\mathcal P\bigl((p<q)\rightarrow(q<p)\bigr).
\]
First, $p<p$ follows from $\operatorname{Sov}(p)$: by $A_{01}$ pick $q\in\mathcal P$ with $p<q$, then $\operatorname{Sov}(p)$ gives $q=p$, hence $p<p$.
Next, let $q\in\mathcal P$ and assume $p<q$. Then $\operatorname{Sov}(p)$ yields $q=p$, so $q<p$ is $p<p$, already shown. Thus the universal condition holds, and $p\ll p$. $\square$

$TY5$: $\forall p\in\mathcal P\ \bigl(\operatorname{Aut}(p)\rightarrow (p\ll p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\operatorname{Aut}(p)$. By $TP5'$, $\operatorname{Real}(p)$, hence $p<p$ by $DP1$.
Also $\operatorname{Aut}(p)$ is exactly $\forall q\in\mathcal P\,(p<q\rightarrow q<p)$ (by $DP4$).
Therefore $DY1$ (with $x:=p$) holds, so $p\ll p$. $\square$

Conversely, if a person owns themselves, they are by definition Autonomous:

$TY6$: $\forall p\in\mathcal P\ \bigl((p\ll p)\rightarrow \operatorname{Aut}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $p\ll p$. By $DY1$ (with $x:=p$),
\[
p\ll p \;\Rightarrow\; \forall q\in\mathcal P\bigl((p<q)\rightarrow(q<p)\bigr),
\]
which is $\operatorname{Aut}(p)$ by $DP4$. $\square$

Ownership inside autonomous collectives

Here I render Van Dun’s “$A!p \wedge Bpq$” as $\operatorname{SAut}(p)\wedge (p<q)$, equivalently $p\sim q$ in our earlier convention. To stay closest to his TY7, I keep it expanded:

$TY7$ (The Upward Flow of Ownership): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(\operatorname{SAut}(p)\wedge (x\ll p)\wedge (p<q)\ \rightarrow\ (x\ll q)\Bigr)$
In a strict collective (where Person $p$ is strictly autonomous and belongs to Person $q$), if $p$ owns an object, then $q$ essentially acquires ownership of that object as well. That is, in a collective structure, you cannot keep property private from the collective that owns you.
Proof. Fix $x\in\mathcal M$ and $p,q\in\mathcal P$, and assume $\operatorname{SAut}(p)$, $x\ll p$, and $p<q$.
From $x\ll p$ (by $DY1$) we have $x<p$ and
\[
\forall r\in\mathcal P\bigl((x<r)\rightarrow(r<p)\bigr). \tag{$\ast$}
\]
To show $x\ll q$ we need (by $DY1$):

  1. $x<q$, and
  2. $\forall r\in\mathcal P\bigl((x<r)\rightarrow(r<q)\bigr)$.

(1) Since $x\in\mathcal M$, from $x<p$ and $p<q$ we get $x<q$ by $A_{02}$.

(2) Let $r\in\mathcal P$ and assume $x<r$. Then by ($\ast$), $r<p$. Hence $r\in\mathcal M$ by $SD2$ (witness $o:=p$). With $r<p$ and $p<q$, apply $A_{02}$ (with $x:=r$) to get $r<q$.

Thus $x\ll q$. $\square$

(So: if a strictly autonomous $p$ owns $x$ and $p$ belongs to $q$, then $q$ owns $x$.)

Communal vs common property theorems

$TY8$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(((p\Downarrow q)/x)\rightarrow (x<p,q)\Bigr)$
If property is Communal (rights are shared), it is necessarily Common (possessed by both).
Proof. Fix $x\in\mathcal M$ and $p,q\in\mathcal P$, and assume $(p\Downarrow q)/x$. By $DY3$,
\[
(p\Downarrow q)/x \;\Rightarrow\; (p/x\Downarrow q)\ \wedge\ (q/x\Downarrow p).
\]
By $DR3$, $p/x\Downarrow q$ implies $x<p$, and $q/x\Downarrow p$ implies $x<q$.
Therefore $(x<p)\wedge(x<q)$, i.e. $x<p,q$ by $DY2$. $\square$

$TY9$ (The Requirement of Mutuality): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(((p\Downarrow q)/x)\rightarrow \bigl(p<q\ \wedge\ q<p\bigr)\Bigr)$
You can only have Communal Property with someone if you belong to them and they belong to you. That is, true communal rights cannot exist between strangers; they require a relationship of mutual ownership (a collective).
Proof. Fix $x\in\mathcal M$ and $p,q\in\mathcal P$, and assume $(p\Downarrow q)/x$. By $DY3$ we have both $p/x\Downarrow q$ and $q/x\Downarrow p$.

From $q/x\Downarrow p$ and $DR3$, we have $\neg(p\uparrow q/x)$. But by $DR1$,
\[
p\uparrow q/x \;\equiv\; \bigl((x<p)\ \vee\ (q<p)\bigr)\ \wedge\ \neg(p<q).
\]
Also, from $p/x\Downarrow q$ and $DR3$ we get $x<p$. Hence if $\neg(p<q)$ were true, then $p\uparrow q/x$ would be true (since $(x<p)\vee(q<p)$ would hold), contradicting $\neg(p\uparrow q/x)$. Therefore $p<q$.

Similarly, from $p/x\Downarrow q$ we have $\neg(q\uparrow p/x)$. By $DR1$,
\[
q\uparrow p/x \;\equiv\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p).
\]
From $q/x\Downarrow p$ we get $x<q$. Hence if $\neg(q<p)$ were true, then $q\uparrow p/x$ would be true, contradicting $\neg(q\uparrow p/x)$. Therefore $q<p$.

So $p<q\wedge q<p$. $\square$

$TY10$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl((p<q\ \wedge\ \neg(q<p))\rightarrow \neg((p\Downarrow q)/x)\Bigr)$
If the relationship is one-sided (e.g., Master and Serf), there can be no Communal Property. A Master may use the Serf’s goods, but the Serf has no right to use the Master’s goods.
Proof. Fix $x\in\mathcal M$ and $p,q\in\mathcal P$, and assume $p<q$ and $\neg(q<p)$. If $(p\Downarrow q)/x$ held, then by $TY9$ we would have $q<p$, contradicting $\neg(q<p)$. Hence $\neg((p\Downarrow q)/x)$. $\square$

Van Dun’s theorem TY11 is not provable as stated, since it lacked $p\neq q$ in the antecedent, which meant that there is a countermodel to it. However, similarly to how Van Dun took the variable name $p$ to implicitly be a person, he most likely took the variable name $q$ to implicitly mean a distinct person. After all, it is a theorem about communal property, which was certainly meant as holding between distinct persons. Hence, I give only the corrected version of TY11 with its proof.

$TY11$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\
\Bigl(((p\Downarrow q)/x\ \wedge\ p\neq q)\rightarrow \bigl(\neg\operatorname{Sov}(p)\ \wedge\ \neg\operatorname{Sov}(q)\bigr)\Bigr)$
If two distinct people share Communal Property, neither of them can be a Sovereign person. (Sovereignty requires exclusive self-ownership. Communal property requires mutual ownership. Therefore, to enter a communal property arrangement, one must surrender Sovereignty.) Proof. Fix $x\in\mathcal M$ and $p,q\in\mathcal P$, and assume $(p\Downarrow q)/x$ and $p\neq q$.

From $(p\Downarrow q)/x$ and $DY3$, we have both $p/x\Downarrow q$ and $q/x\Downarrow p$.
By $TY9$, this implies
\[
p<q\ \wedge\ q<p. \tag{1}
\]

We show $\neg\operatorname{Sov}(p)$. Suppose for contradiction that $\operatorname{Sov}(p)$.
By $DP3$, $\operatorname{Sov}(p)$ means $\forall r\in\mathcal P\,(p<r\rightarrow r=p)$.
Applying this with $r:=q$ and using $p<q$ from (1), we obtain $q=p$, contradicting $p\neq q$.
Hence $\neg\operatorname{Sov}(p)$.

Similarly, to show $\neg\operatorname{Sov}(q)$, suppose $\operatorname{Sov}(q)$.
Then $\forall r\in\mathcal P\,(q<r\rightarrow r=q)$, and with $r:=p$ and $q<p$ from (1), we get $p=q$, again contradicting $p\neq q$.
Hence $\neg\operatorname{Sov}(q)$.

Therefore $\neg\operatorname{Sov}(p)\ \wedge\ \neg\operatorname{Sov}(q)$. $\square$

And the autonomous-collective result (replacing $\mathrm{SACpq}$ with $p\sim q$):

$TY12$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M
\Bigl((p\sim q\ \wedge\ x<p)\rightarrow ((p\Downarrow q)/x)\Bigr)$
In a strictly autonomous collective (where members belong to one another), any object belonging to a member automatically becomes Communal Property between them and the collective.
Proof. Fix $p,q\in\mathcal P$ and $x\in\mathcal M$, and assume $p\sim q$ and $x<p$.
By $DP7$, $p\sim q$ implies $\operatorname{SAut}(p)$ and $p<q$. From $\operatorname{SAut}(p)$ we get $\operatorname{Aut}(p)$ by $DP6$, hence from $p<q$ we get $q<p$ by $DP4$.

We show both conjuncts of $DY3$.

  1. $p/x\Downarrow q$: By $DR3$, it suffices that $x<p$ (given) and $\neg(q\uparrow p/x)$.
    But $q\uparrow p/x$ (by $DR1$) entails $\neg(q<p)$ as a conjunct. Since $q<p$ holds, $\neg(q<p)$ is false, so $q\uparrow p/x$ is false; hence $\neg(q\uparrow p/x)$. Therefore $p/x\Downarrow q$.

  2. $q/x\Downarrow p$: By $DR3$, it suffices that $x<q$ and $\neg(p\uparrow q/x)$.
    From $x<p$ and $p<q$ with $x\in\mathcal M$, $A_{02}$ yields $x<q$.
    Also $p\uparrow q/x$ (by $DR1$) entails $\neg(p<q)$ as a conjunct, but $p<q$ holds, so $p\uparrow q/x$ is false; hence $\neg(p\uparrow q/x)$.
    Thus $q/x\Downarrow p$.

Therefore $(p/x\Downarrow q)\wedge(q/x\Downarrow p)$, i.e. $(p\Downarrow q)/x$ by $DY3$. $\square$

Actions (system $\mathbf L_1$)

Domains and primitives

We reuse the objects domain from $\mathbf L_0$: $\mathcal D$ $with $\mathcal P\subseteq\mathcal D$, $\mathcal M\subseteq\mathcal D$$. But here we expand it.

We expand our view of reality to include a new domain: Actions ($\mathcal A$). The expanded domain is $\mathcal D_1 \:= \mathcal D ,\dot\cup, \mathcal A$ (disjoint union).

We introduce two new primitive relations linking actions to means:

  • Use ($i/x$): Action $i$ uses object $x$ (direct employment). $i/x$ is a primitive predicate with $i\in\mathcal A,\ x\in\mathcal M$.
  • Affect ($i//x$): Action $i$ affects object $x$ (consequences/side effects). $i//x$ is a primitive predicate with $i\in\mathcal A,\ x\in\mathcal M$.

That is, $i/x$ corresponds to Van Dun’s $Uix$, and $i//x$ to $Vix$.

Axioms for actions ($A_1$)

$A_{11}$ (Usage implies Effect): $\forall i\in\mathcal A\ \forall x\in\mathcal M\ \bigl((i/x)\rightarrow (i//x)\bigr)$
If an action uses an object, it necessarily affects that object.

Every action uses at least one means, and every means is used by at least one action. There are no “ghost” actions using nothing, and no “useless” objects:

$A_{12}$: $\forall i\in\mathcal A\ \exists x\in\mathcal M\ (i/x)$

$A_{13}$: $\forall x\in\mathcal M\ \exists i\in\mathcal A\ (i/x)$

If an action affects an object, and that object belongs to Person $p$, then the action is considered to affect Person $p$. (Touching my property counts as touching me).

$A_{14}$ (The Transitivity of Effect): $\forall i\in\mathcal A\ \forall x\in\mathcal M\ \forall p\in\mathcal P
\bigl((i//x\ \wedge\ x<p)\rightarrow (i//p)\bigr)$

Notice that this axiom extends $//$ to persons; $i//p$ is similarly read as “$i$ affects person $p$”.

Action-rights definitions (DA)

Right to deny doing an action

$DA1$ (Right to Deny): $p\uparrow q/i \;\:=\; \exists x\in\mathcal M\ \bigl(i//x\ \wedge\ (p\uparrow q/x)\bigr)
\qquad(p,q\in\mathcal P,\ i\in\mathcal A)$
Person $p$ has the right to deny Person $q$ from performing an action if that action affects something $p$ has a right to deny $q$ from using. (I can stop you if your action touches my stuff).

$DA2$ (Right to Do): $p/i\Downarrow q \;\:=\; \forall x\in\mathcal M\ \bigl((i//x)\rightarrow (p/x\Downarrow q)\bigr)
\qquad(p,q\in\mathcal P,\ i\in\mathcal A)$
Person $p$ has a right to perform an action against Person $q$ only if $p$ has the right to use every single object that the action affects. (You need “clearance” for all affected items).

“Property of actions” definitions (DA)

Action belongs to a person

$DA3$ (Belonging): $i<p \;\:=\; \forall x\in\mathcal M\ \bigl((i//x)\rightarrow (x<p)\bigr)
\qquad(i\in\mathcal A,\ p\in\mathcal P)$
An action “belongs” to Person $p$ if every object affected by that action belongs to $p$.

Person owns an action

$DA4$ (Ownership): $i\ll p \;\:=\; \forall x\in\mathcal M\ \bigl((i//x)\rightarrow (x\ll p)\bigr)
\qquad(i\in\mathcal A,\ p\in\mathcal P)$
Person $p$ “owns” an action if every object affected by that action is owned by $p$. This implies that to truly own an action, one must own the entire sphere of its consequences.

Theorems (TA)

$TA1$: $\forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall x\in\mathcal M
\Bigl((i//x\ \wedge\ x<q)\rightarrow\bigl((p/i\Downarrow q)\rightarrow (q<p)\bigr)\Bigr)$
If Person $p$ has a right to perform an action that affects Person $q$’s property, it implies that $q$ actually belongs to $p$. (Only a master has a right to actions that affect a serf’s property without consent).
Proof. Fix $i\in\mathcal A$, $p,q\in\mathcal P$, $x\in\mathcal M$, and assume $i//x$ and $x<q$.
Assume moreover $p/i\Downarrow q$. By $DA2$, from $p/i\Downarrow q$ and $i//x$ we get $p/x\Downarrow q$.
If $\neg(q<p)$ held, then $TR8$ (applied to $p,q,x$) would yield $\neg(p/x\Downarrow q)$ from $(x<q\wedge \neg(q<p))$, contradicting $p/x\Downarrow q$.
Hence $q<p$. $\square$

Property of actions: exclusivity against sovereign owners

$TA2$: $\forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl((i<p\ \wedge\ \operatorname{Sov}(p)\ \wedge\ q/i\Downarrow p)\rightarrow q=p\Bigr)$
If an action belongs to a Sovereign person (who owns themselves), no one else has the right to perform that action against the Sovereign.
Proof. Fix $i\in\mathcal A$ and $p,q\in\mathcal P$, and assume $i<p$, $\operatorname{Sov}(p)$, and $q/i\Downarrow p$.
By $A_{12}$ choose $x\in\mathcal M$ with $i/x$. Then by $A_{11}$, $i//x$.
From $i<p$ and $DA3$ we have $\forall y\in\mathcal M((i//y)\rightarrow (y<p))$, so in particular $x<p$.

Apply $TA1$ with the roles $(p,q)$ there replaced by $(q,p)$ here:
since $i//x$ and $x<p$, from $q/i\Downarrow p$ we infer $p<q$.
But $\operatorname{Sov}(p)$ means $\forall r\in\mathcal P\,(p<r\rightarrow r=p)$ ($DP3$), hence from $p<q$ we get $q=p$. $\square$

Owning an action implies an absolute right to do it (as stated)

(As written by Van Dun, the quantification over $q$ is implicit; I make it explicit.)

$TA3$: $\forall i\in\mathcal A\ \forall p\in\mathcal P
\Bigl((i\ll p)\rightarrow \forall q\in\mathcal P\ (p/i\Downarrow q)\Bigr)$
If you own an action, you have an Absolute Right to perform it. (Because owning it means you own all the affected means, so no one has standing to deny you).
Proof. Fix $i\in\mathcal A$ and $p\in\mathcal P$, and assume $i\ll p$.
Let $q\in\mathcal P$ be arbitrary; we prove $p/i\Downarrow q$.

By $DA2$, it suffices to show: for every $x\in\mathcal M$, if $i//x$ then $p/x\Downarrow q$.
So fix $x\in\mathcal M$ and assume $i//x$.

From $i\ll p$ and $DA4$, $(i//x)\rightarrow (x\ll p)$, hence $x\ll p$.
By $DY1$, $x\ll p$ implies $x<p$ and $\forall r\in\mathcal P((x<r)\rightarrow (r<p))$. ($\ast$)

Also $x\ll p\rightarrow \operatorname{Aut}(p)$ by $TY2$. Hence $(p<r)\rightarrow (r<p)$ for all $r\in\mathcal P$. ($\ast\ast$)

To show $p/x\Downarrow q$ we use $DR3$: it suffices that $x<p$ (already) and $\neg(q\uparrow p/x)$.
But by $DR1$,
\[
q\uparrow p/x \;\equiv\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p).
\]
If $x<q$ then $q<p$ by ($\ast$); if $p<q$ then $q<p$ by ($\ast\ast$). Either way $\neg(q<p)$ is impossible. Hence $\neg(q\uparrow p/x)$.
Thus $p/x\Downarrow q$, and therefore $p/i\Downarrow q$. Since $q$ was arbitrary, $\forall q\in\mathcal P\,(p/i\Downarrow q)$. $\square$

Heteronomous persons own no actions

$TA4$: $\forall i\in\mathcal A\ \forall p\in\mathcal P
\bigl(\operatorname{Het}(p)\rightarrow \neg(i\ll p)\bigr)$
Heteronomous persons (serfs) own no actions. (Since they do not own themselves, they cannot own the means affected by their actions).
Proof. Fix $i\in\mathcal A$ and $p\in\mathcal P$, and assume $\operatorname{Het}(p)$.
Suppose for contradiction that $i\ll p$. By $A_{12}$ choose $x\in\mathcal M$ with $i/x$, hence $i//x$ by $A_{11}$.
Then $DA4$ and $i\ll p$ give $x\ll p$, and $TY2$ gives $\operatorname{Aut}(p)$.
But $\operatorname{Het}(p)\equiv \neg\operatorname{Aut}(p)$ by $DP5$. Contradiction. Hence $\neg(i\ll p)$. $\square$

Autonomous collectives and “perfect communism” for actions

(Replace $\mathrm{SACpq}$ with $p\sim q$ as before.)

$TA5$: $\forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall r\in\mathcal P
\Bigl((p\sim q\ \wedge\ p/i\Downarrow r)\rightarrow (q/i\Downarrow r)\Bigr)$
In a strictly autonomous collective (where members belong to each other), if one member has the right to do an action, the other members automatically have that right too.
Proof. Fix $i\in\mathcal A$ and $p,q,r\in\mathcal P$, and assume $p\sim q$ and $p/i\Downarrow r$.
We show $q/i\Downarrow r$, i.e. by $DA2$:
\[
\forall x\in\mathcal M\bigl((i//x)\rightarrow (q/x\Downarrow r)\bigr).
\]
So fix $x\in\mathcal M$ and assume $i//x$. From $p/i\Downarrow r$ and $DA2$, we have $p/x\Downarrow r$.
By $DR3$, $p/x\Downarrow r$ implies $x<p$ and $\neg(r\uparrow p/x)$. \ ($\dagger$)

Since $p\sim q$ implies $p<q$ ($DP7$), and $x\in\mathcal M$, from $x<p$ and $p<q$ we get $x<q$ by $A_{02}$. ($\ddagger$)

It remains to show $\neg(r\uparrow q/x)$, so that $q/x\Downarrow r$ holds by $DR3$ using ($\ddagger$).
Assume for contradiction $r\uparrow q/x$. Then by $DR1$,
\[
\bigl((x<r)\ \vee\ (q<r)\bigr)\ \wedge\ \neg(r<q). \ (\star)
\]
From $\neg(r<q)$ and $p<q$ we infer $\neg(r<p)$: if $r<p$, then $r\in\mathcal M$ by $SD2$ (witness $o:=p$), and with $p<q$ axiom $A_{02}$ would yield $r<q$, contradicting $\neg(r<q)$.

Also, from $p\sim q$ we have $p<q$, hence $p\in\mathcal M$ by $SD2$ (witness $o:=q$). If $q<r$ holds (the second disjunct in ($\star$)), then by $A_{02}$ with $x:=p$ we get $p<r$ from $(p<q\wedge q<r)$.

Thus in all cases, $(x<r)\vee(p<r)$ holds, and we have $\neg(r<p)$; therefore by $DR1$ we obtain $r\uparrow p/x$.
This contradicts $\neg(r\uparrow p/x)$ from ($\dagger$). Hence $\neg(r\uparrow q/x)$, and so $q/x\Downarrow r$.
Since $x$ was arbitrary, $q/i\Downarrow r$. $\square$

$TA6$: $\forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl((p\sim q\ \wedge\ i\ll p)\rightarrow (i\ll q)\Bigr)$
If an action is owned by one member of the collective, it is owned by the others.
Proof. Fix $i\in\mathcal A$ and $p,q\in\mathcal P$, and assume $p\sim q$ and $i\ll p$.
To show $i\ll q$, use $DA4$: we must show
\[
\forall x\in\mathcal M\bigl((i//x)\rightarrow (x\ll q)\bigr).
\]
So fix $x\in\mathcal M$ with $i//x$. From $i\ll p$ and $DA4$, we have $x\ll p$.
Also $p\sim q$ implies $\operatorname{SAut}(p)$ and $p<q$ ($DP7$).
Thus $TY7$ (ownership inside autonomous collectives) yields $x\ll q$ from $\operatorname{SAut}(p)\wedge (x\ll p)\wedge (p<q)$.
Hence $i\ll q$. $\square$

$TA7$: $\forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\bigl((p\sim q)\rightarrow \neg(p\uparrow q/i)\bigr)$
Members of a collective cannot deny each other the right to perform actions. (The right to deny is based on exclusive ownership, which does not exist in the collective).
Proof. Fix $i\in\mathcal A$ and $p,q\in\mathcal P$, and assume $p\sim q$. Then $p<q$ by $DP7$.
By $DA1$, $p\uparrow q/i$ means $\exists x\in\mathcal M\,(i//x\wedge (p\uparrow q/x))$.
But for any $x$, $DR1$ gives $(p\uparrow q/x)\Rightarrow \neg(p<q)$ (since $\neg(p<q)$ is a conjunct of $p\uparrow q/x$).
This contradicts $p<q$. Hence no such $x$ exists and $\neg(p\uparrow q/i)$. $\square$

Action-right equivalence (analogue of the earlier $p/x\Downarrow q$ normal form)

I modernize Van Dun’s “$R^a$” statement into our action-right notation and his “$B^a$” notation into $i<p$.

$TA8$: $\forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl((p/i\Downarrow q)\ \leftrightarrow\ \bigl(i<p\ \wedge\ ((i<q\ \vee\ p<q)\rightarrow (q<p))\bigr)\Bigr)$
Having the right to perform an action against someone is logically equivalent to the action belonging to you (or the affected person belonging to you).
Proof. Fix $i\in\mathcal A$ and $p,q\in\mathcal P$.

($\Rightarrow$) Assume $p/i\Downarrow q$.

  1. Show $i<p$. Let $x\in\mathcal M$ and assume $i//x$. By $DA2$, from $p/i\Downarrow q$ we get $p/x\Downarrow q$. By $DR3$, $p/x\Downarrow q\rightarrow (x<p)$. Since $x$ was arbitrary, $\forall x\in\mathcal M((i//x)\rightarrow (x<p))$, i.e. $i<p$ by $DA3$.

  2. Show $((i<q\ \vee\ p<q)\rightarrow (q<p))$. Assume $(i<q\ \vee\ p<q)$.

  • If $p<q$: by $A_{12}$ choose $x\in\mathcal M$ with $i/x$, hence $i//x$ by $A_{11}$. As above, $p/i\Downarrow q$ gives $p/x\Downarrow q$, hence $x<p$ by $DR3$. Since $x\in\mathcal M$ and $p<q$, axiom $A_{02}$ yields $x<q$. Now $TA1$ (with this $x$) gives $(i//x\wedge x<q)\rightarrow((p/i\Downarrow q)\rightarrow(q<p))$, so $q<p$.

  • If $i<q$: again choose $x\in\mathcal M$ with $i/x$ (so $i//x$). From $i<q$ (i.e. $DA3$ with $q$ in place of $p$) we get $x<q$. Then $TA1$ with $i//x$ and $x<q$ yields $q<p$.

Thus $((i<q\ \vee\ p<q)\rightarrow (q<p))$ holds.

So the right-hand side holds.

($\Leftarrow$) Assume $i<p\ \wedge\ ((i<q\ \vee\ p<q)\rightarrow (q<p))$. We prove $p/i\Downarrow q$.

By $DA2$, it suffices to show: for all $x\in\mathcal M$, if $i//x$ then $p/x\Downarrow q$. So fix $x\in\mathcal M$ and assume $i//x$.

From $i<p$ and $DA3$, we get $x<p$. It remains (by $DR3$) to show $\neg(q\uparrow p/x)$.

Suppose for contradiction that $q\uparrow p/x$. By $DR1$, \[ q\uparrow p/x \;\Rightarrow\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p). \] So either (a) $p<q$, or (b) $x<q$; in both cases we derive $q<p$, contradicting $\neg(q<p)$.

(a) If $p<q$, then $(i<q\ \vee\ p<q)$ holds, so the assumed implication yields $q<p$.

(b) If $x<q$, then by $A_{14}$, $(i//x\wedge x<q)\rightarrow i//q$, hence $i//q$. Also, since $q\in\mathcal P$, axiom $A_{01}$ gives $\exists r\in\mathcal P\ (q<r)$, so by $SD2$ we have $q\in\mathcal M$. Now instantiate $DA3$ (the assumption $i<p$) at $x:=q$: \[ q\in\mathcal M\ \wedge\ i//q \ \Rightarrow\ q<p. \] So again $q<p$.

Thus $\neg(q\uparrow p/x)$. Therefore $p/x\Downarrow q$ (since $x<p$ and $\neg(q\uparrow p/x)$), and since $x$ was arbitrary, $p/i\Downarrow q$.

Hence the equivalence holds. $\square$

(Here $i<q$ is shorthand for “action $i$ belongs to $q$” i.e. $i<q \equiv i<q$ as defined in DA3.)

Rights, obligations, freedoms

Generic-action predicates

We now move from specific actions ($i$) to “Kinds” of actions ($Z$), such as “Speech” or “Walking.”

Let $Z$ be any unary predicate on actions: $Z:\mathcal A\to{\text{T},\text{F}}$.
Write $Z(i)$ $or simply $Zi$$ for “action $i$ is of kind $Z$”.

Define negation of kinds pointwise:
$$
(\neg Z)(i)\;\:=\;\neg Z(i).
$$

Rights to do a kind of action

Weak right (exists some permissible instance)

$DA5$ (Weak Right): $p/Z\downarrow q \;\:=\; \exists i\in\mathcal A\ \bigl(Z(i)\ \wedge\ (p/i\Downarrow q)\bigr)
\qquad(p,q\in\mathcal P)$
You have a “weak right” to do action $Z$ if there is at least one instance of $Z$ you are allowed to do. (e.g., “I have a right to walk” = I can walk in my own house).

Strong right (all instances are permissible)

$DA6$ (Strong Right): $p/Z\Downarrow q \;\:=\; \forall i\in\mathcal A\ \bigl(Z(i)\rightarrow (p/i\Downarrow q)\bigr)
\qquad(p,q\in\mathcal P)$
You have a “strong right” to do action $Z$ if you are allowed to do every instance of $Z$. (e.g., “I have a right to walk” = I can walk anywhere).

Some derived facts stated in the text

Weak right “against everyone” implies autonomy

(“without anybody’s consent” = for all persons $q$.)

$T_{W\to Aut}$: $\forall p\in\mathcal P\ \Bigl(\bigl(\forall q\in\mathcal P\ (p/Z\downarrow q)\bigr)\rightarrow \operatorname{Aut}(p)\Bigr)$
Autonomy: If you have a weak right to do an action kind $Z$ “against everyone,” you must be an Autonomous person.
Proof. Fix $p\in\mathcal P$ and assume $\forall q\in\mathcal P\ (p/Z\downarrow q)$.
To show $\operatorname{Aut}(p)$, let $q\in\mathcal P$ and assume $p<q$; we prove $q<p$.

From the assumption, $p/Z\downarrow q$ holds. By $DA5$, choose $i\in\mathcal A$ such that $Z(i)$ and $p/i\Downarrow q$.
By $A_{12}$ choose $x\in\mathcal M$ with $i/x$, hence $i//x$ by $A_{11}$.
From $p/i\Downarrow q$ and $DA2$, $p/x\Downarrow q$, so by $DR3$ we get $x<p$.
Since $x\in\mathcal M$ and $p<q$, $A_{02}$ yields $x<q$ from $(x<p\wedge p<q)$.
Now apply $TA1$ to $(i//x\wedge x<q)$ and $p/i\Downarrow q$ to conclude $q<p$.
Thus $p<q\rightarrow q<p$, so $\operatorname{Aut}(p)$. $\square$

Specialization to the predicates (U) and (V)

Treat “uses $x$” as a kind $U_x$ defined by $U_x(i)\equiv (i/x)$, and “affects (x)” as a kind $V_x$ defined by $V_x(i)\equiv (i//x)$. Then Van Dun’s stated equivalence becomes the following. This is the first time that we reach a theorem given by Van Dun which really isn’t provable from his stated definitions and axioms, and which does not seem to be a mere oddity of his notation, as explained next.

$T_{WU\leftrightarrow R}$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(p/U_x\downarrow q\ \leftrightarrow\ (p/x\Downarrow q)\Bigr)$
This theorem would claim that having a right to use a specific object ($U_x$) is always the same as having the right to perform an action that affects that object.
Explanation (the $\Leftarrow$ direction generally needs an extra assumption).
($\Rightarrow$) If $p/U_x\downarrow q$, then by $DA5$ there exists $i\in\mathcal A$ with $U_x(i)$ and $p/i\Downarrow q$.
By definition $U_x(i)\equiv (i/x)$, hence $i//x$ by $A_{11}$.
Then $DA2$ gives $(i//x)\rightarrow (p/x\Downarrow q)$, so $p/x\Downarrow q$.

($\Leftarrow$) Conversely, from $p/x\Downarrow q$ one can use $A_{13}$ to pick an action $i$ with $i/x$.
But to conclude $p/i\Downarrow q$ one must show that for every $y$ with $i//y$, $p/y\Downarrow q$ holds (by $DA2$),
which does not follow from $p/x\Downarrow q$ unless one assumes (for instance) that actions with $i/x$ do not affect any other means,
or more generally that all means affected by $i$ are also means for which $p$ has the corresponding right.
So the equivalence as stated is not derivable from $A_{11}$–$A_{14}$ and $DA2$ alone; it becomes correct with a suitable “single-means” or “no extra affected means” constraint. $\square$

Van Dun seems to actually agree that the leftward direction is not provable, when he says afterwards in the text that “ownership is a necessary (but it is not a sufficient) condition for the right to use a means without anybody’s consent. It is not a sufficient condition because there may be no action that uses the means one owns that does not have significant side effects on other means (and other persons).” But it still seems odd that he claimed that this formula (stated in the text as $(\triangle x) (\triangle p) (\triangle q) (\mathbb{W}^a p U x q \leftrightarrow R p x q)$) was provable. We all make mistakes, I suppose.

And the “weak right to use $x$ against everyone implies ownership” becomes:

$T_{WU\to Own}$: $\forall x\in\mathcal M\ \forall p\in\mathcal P
\Bigl(\bigl(\forall q\in\mathcal P\ (p/U_x\downarrow q)\bigr)\rightarrow (x\ll p)\Bigr)$
Ownership: If you have a weak right to use object $x$ against everyone, you must Own object $x$.
Proof. Fix $x\in\mathcal M$ and $p\in\mathcal P$, and assume $\forall q\in\mathcal P\,(p/U_x\downarrow q)$.
We prove $x\ll p$, i.e. by $DY1$: (i) $x<p$ and (ii) $\forall q\in\mathcal P((x<q)\rightarrow(q<p))$.

(i) Take $q:=p$. Then $p/U_x\downarrow p$, so by $DA5$ choose $i$ with $i/x$ and $p/i\Downarrow p$.
From $i/x$ we get $i//x$ by $A_{11}$, and then $DA2$ gives $p/x\Downarrow p$.
By $DR3$, $p/x\Downarrow p$ implies $x<p$.

(ii) Let $q\in\mathcal P$ and assume $x<q$. By assumption, $p/U_x\downarrow q$, so choose $i$ with $i/x$ and $p/i\Downarrow q$.
As above, $i/x\Rightarrow i//x$, and $DA2$ yields $p/x\Downarrow q$.
Unfold $p/x\Downarrow q$ via $DR3$ and $DR1$: it implies $\neg(q\uparrow p/x)$, while
\[
q\uparrow p/x \;\equiv\; \bigl((x<q)\ \vee\ (p<q)\bigr)\ \wedge\ \neg(q<p).
\]
Since $x<q$, the left disjunction holds; therefore $\neg(q\uparrow p/x)$ forces $\neg\neg(q<p)$, hence $q<p$ (classically).
Thus $(x<q)\rightarrow (q<p)$ for all $q\in\mathcal P$.

So $x\ll p$. $\square$

Rights Regarding “Not-Doing” (Negative Rights)

Define the “non-$Z$” kind $\neg Z$ by $(\neg Z)(i)\equiv \neg Z(i)$. Then having a right to “Not-$Z$” (not do a specific kind of action) means there exists some action you can do that is not $Z$:

$T_{\neg Z,\exists}$: $\forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(p/(\neg Z)\downarrow q\ \leftrightarrow\ \exists i\in\mathcal A\ \bigl((p/i\Downarrow q)\wedge \neg Z(i)\bigr)\Bigr)$
Proof. By $DA5$,
\[
p/(\neg Z)\downarrow q \;\equiv\; \exists i\in\mathcal A\bigl((\neg Z)(i)\wedge (p/i\Downarrow q)\bigr).
\]
By definition of pointwise negation, $(\neg Z)(i)\equiv \neg Z(i)$, so this is exactly
\[
\exists i\in\mathcal A\bigl(\neg Z(i)\wedge (p/i\Downarrow q)\bigr),
\]
equivalently $\exists i\in\mathcal A\bigl((p/i\Downarrow q)\wedge \neg Z(i)\bigr)$. $\square$

Equivalently (the text’s second formulation):

$T_{\neg Z,\forall}$: $\forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(\neg\bigl(p/(\neg Z)\downarrow q\bigr)\ \leftrightarrow\ \forall i\in\mathcal A\ \bigl((p/i\Downarrow q)\rightarrow Z(i)\bigr)\Bigr)$
Proof. From $T_{\neg Z,\exists}$,
\[
p/(\neg Z)\downarrow q \;\leftrightarrow\; \exists i\in\mathcal A\bigl((p/i\Downarrow q)\wedge \neg Z(i)\bigr).
\]
Negating both sides and using classical quantifier laws yields
\[
\neg\bigl(p/(\neg Z)\downarrow q\bigr) \;\leftrightarrow\; \forall i\in\mathcal A\ \neg\bigl((p/i\Downarrow q)\wedge \neg Z(i)\bigr).
\]
But $\neg(A\wedge \neg B)\equiv (A\rightarrow B)$, so the right side becomes
\[
\forall i\in\mathcal A\ \bigl((p/i\Downarrow q)\rightarrow Z(i)\bigr).
\]
$\square$

“Not having the strong right to not-$Z$” (another obligation-shaped form)

$T_{S,\neg Z}$: $\forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(\neg\bigl(p/(\neg Z)\Downarrow q\bigr)\ \leftrightarrow\ \exists i\in\mathcal A\ \bigl(\neg Z(i)\ \wedge\ \neg(p/i\Downarrow q)\bigr)\Bigr)$
Obligations: Not having the strong right to refrain from $Z$ means there is some specific way of not doing $Z$ that is forbidden to you.
Proof. By $DA6$,
\[
p/(\neg Z)\Downarrow q \;\equiv\; \forall i\in\mathcal A\bigl((\neg Z)(i)\rightarrow (p/i\Downarrow q)\bigr).
\]
Negating and using classical quantifier laws:
\[
\neg\bigl(p/(\neg Z)\Downarrow q\bigr) \;\leftrightarrow\; \exists i\in\mathcal A\ \neg\bigl((\neg Z)(i)\rightarrow (p/i\Downarrow q)\bigr).
\]
But $\neg(A\rightarrow B)\equiv (A\wedge \neg B)$, and $(\neg Z)(i)\equiv \neg Z(i)$, so this becomes
\[
\exists i\in\mathcal A\bigl(\neg Z(i)\wedge \neg(p/i\Downarrow q)\bigr).
\]
$\square$

Freedom to do a kind of action (several strengths)

Recall: $p\uparrow q/i$ means “$p$ has a right to deny $q$ doing $i$”.
So “$p$ is free from $q$’s denial for $i$” is $\neg(q\uparrow p/i)$.

The text distinguishes between “Freedom” (absence of denial) and “Rights” (positive authority), with three levels of strength:

  • F1/R1: Freedom/Right to do some instance of the action kind.
  • F2/R2: For every person, there is some instance of the action I can do against them.
  • F3/R3 (Strongest): I can do any instance of the action against anyone.

Freedom defined via absence of others’ denial-rights (three strengths)

$F1$: $\exists i\in\mathcal A\ \Bigl(Z(i)\ \wedge\ \forall q\in\mathcal P\bigl(q\neq p\rightarrow \neg(q\uparrow p/i)\bigr)\Bigr)$

$F2$: $\forall q\in\mathcal P\ \Bigl(q\neq p\rightarrow \exists i\in\mathcal A\ (Z(i)\ \wedge\ \neg(q\uparrow p/i))\Bigr)$

$F3$: $\forall i\in\mathcal A\ \forall q\in\mathcal P\ \Bigl((Z(i)\ \wedge\ q\neq p)\rightarrow \neg(q\uparrow p/i)\Bigr)$

Freedom defined as a (positive) right rather than mere absence of another’s right (three strengths)

$R1$: $\exists i\in\mathcal A\ \Bigl(Z(i)\ \wedge\ \forall q\in\mathcal P\bigl(q\neq p\rightarrow (p/i\Downarrow q)\bigr)\Bigr)$

$R2$: $\forall q\in\mathcal P\ \Bigl(q\neq p\rightarrow \exists i\in\mathcal A\ (Z(i)\ \wedge\ (p/i\Downarrow q))\Bigr)$

$R3$: $\forall i\in\mathcal A\ \forall q\in\mathcal P\ \Bigl((Z(i)\ \wedge\ q\neq p)\rightarrow (p/i\Downarrow q)\Bigr)$

Relevant harms and wrongs

“Produces a state of affairs”

Let $\Sigma$ be a set of state-descriptions. We introduce a primitive relation between an action ($i$) and a state ($S$): $$
\Vdash\ \subseteq \mathcal A\times \Sigma,
$$
We say action $i$ produces state $S$.

For object-parameterized states, let $\Phi(\cdot)$ be a state-former producing a state $\Phi(x)\in\Sigma$ for each $x\in\mathcal D$. That is, a state can be defined relative to an object, such as “Object $x$ is broken”; we write this as $\Phi(x)$. Then $i\Vdash \Phi(x)$ abbreviates “$i$ puts $x$ in state $\Phi$”.

Given any state $S$, define the corresponding “kind predicate” on actions:
$$
Z_S(i)\ \:=\ (i\Vdash S).
$$
Then weak right to produce $S$ without $q$’s consent is exactly:
$Def$ (Weak Right to Produce): $p/S\downarrow q\ \:=\ \exists i\in\mathcal A\ \bigl((i\Vdash S)\wedge (p/i\Downarrow q)\bigr).$
Person $p$ has a “weak right” to put Person $q$ (or object $x$) into state $S$ if there is at least one permissible action $p$ can perform that results in state $S$.

Forbidden (F-)states

Van Dun’s condition for “$\Phi$ is an F-state for $x$” is: any action that produces $\Phi(x)$ relevantly affects $x$. Using our affect notation $i//x$:

$DF$ (Forbidden State): $F(\Phi,x)\ \:=\ \forall i\in\mathcal A\ \bigl((i\Vdash \Phi(x))\rightarrow (i//x)\bigr).$
A state $\Phi$ is considered a Forbidden State for object $x$ if every possible action that produces this state necessarily affects object $x$.

Intuition: You cannot put my car in the state of “being painted” without touching (affecting) my car. Therefore, “being painted” is an F-state for the car.

Theorems (F-states block)

Using the same “weak right” notation $p/Z\downarrow q$, and taking $Z_{\Phi(x)}(i)\equiv(i\Vdash\Phi(x))$:

$TF1$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(F(\Phi,x)\ \wedge\ x<p\ \wedge\ \neg(p<q)\ \rightarrow\ \neg\bigl(q/\Phi(x)\downarrow p\bigr)\Bigr)$ (Reads: if $\Phi$ is forbidden-for-$x$, and $x$ belongs to $p$, and $p$ does not belong to $q$ $so $p$ is “independent of $q$” in the sense used in DR1$, then $q$ has no weak right to put $x$ into $\Phi$ without $p$’s consent.)
If a state is Forbidden for an object (requires touching it), and that object belongs to Person $p$, and Person $p$ is independent of Person $q$ (not $q$’s serf), then $q$ has no right to put the object into that state without $p$’s consent. (That is, you can’t paint my car without asking me, because you can’t paint it without touching it, and you have no right to touch my property.)
Proof. Fix $x\in\mathcal M$ and $p,q\in\mathcal P$, and assume:
(1) $F(\Phi,x)$, i.e. $\forall i\in\mathcal A\,((i\Vdash \Phi(x))\rightarrow (i//x))$,
(2) $x<p$,
(3) $\neg(p<q)$.
We show $\neg(q/\Phi(x)\downarrow p)$.

Suppose for contradiction that $q/\Phi(x)\downarrow p$. By the weak-right definition,
\[
q/\Phi(x)\downarrow p \;\equiv\; \exists i\in\mathcal A\bigl((i\Vdash \Phi(x))\wedge (q/i\Downarrow p)\bigr).
\]
Choose $i\in\mathcal A$ such that $i\Vdash \Phi(x)$ and $q/i\Downarrow p$.

From (1) and $i\Vdash \Phi(x)$ we obtain $i//x$.
Then $q/i\Downarrow p$ and $DA2$ yield: since $i//x$, we have $q/x\Downarrow p$.
Now apply $TA1$ with the roles $(p,q)$ there replaced by $(q,p)$ here:
because $i//x$ and $x<p$, we get $(q/i\Downarrow p)\rightarrow (p<q)$, hence $p<q$.
This contradicts (3) $\neg(p<q)$. Therefore $\neg(q/\Phi(x)\downarrow p)$. $\square$

Likewise for persons (replacing $x\in\mathcal M$ by $p\in\mathcal P$ as the affected object), at this point in the text, Van Dun states this statement (“No one has a right to put an independent person in F-state Φ without his consent”):

$TF2$: $\forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(F(\Phi,p)\ \wedge\ \neg(p<q)\ \rightarrow\ \neg\bigl(q/\Phi(p)\downarrow p\bigr)\Bigr)$

This is not provable as stated. Staying close to his intent, I state and prove a version restricted to real persons (persons that belong to themselves):

$TF2'$ (Real Persons): $\forall p,q\in\mathcal P\Bigl(F(\Phi,p)\wedge \operatorname{Real}(p)\wedge \neg(p<q)\rightarrow \neg(q/\Phi(p)\downarrow p)\Bigr)$
If a state is Forbidden for a Real Person (requires touching them), and they do not belong to you, you have no right to put them in that state. (That is, you cannot perform surgery on me without my consent, because surgery requires touching me.)
Proof. Fix $p,q\in\mathcal P$ and assume:

  1. $F(\Phi,p)$, i.e. $\forall i\in\mathcal A\,\bigl((i\Vdash \Phi(p))\rightarrow (i//p)\bigr)$,
  2. $\operatorname{Real}(p)$, i.e. $p<p$ by $DP1$,
  3. $\neg(p<q)$.

Suppose for contradiction that $q/\Phi(p)\downarrow p$. By definition of weak right,
\[
q/\Phi(p)\downarrow p \;\equiv\; \exists i\in\mathcal A\ \bigl((i\Vdash \Phi(p))\wedge (q/i\Downarrow p)\bigr).
\]
Choose $i\in\mathcal A$ with $i\Vdash \Phi(p)$ and $q/i\Downarrow p$.

From (1) and $i\Vdash \Phi(p)$, we get $i//p$.

Now note that in this framework persons are means: since $p\in\mathcal P$, by $A_{01}$ there exists $r\in\mathcal P$ with $p<r$, hence $p\in\mathcal M$ by $SD2$. Thus we may instantiate $TA1$ with the “affected means” variable $x:=p$.

Apply $TA1$ with substitutions: action $i$ as chosen, actor-person $p:=q$, consent-person $q:=p$, and affected means $x:=p$. The antecedent becomes $(i//p\ \wedge\ p<p)$, which holds by $i//p$ and (2). Therefore $TA1$ yields
\[
(q/i\Downarrow p)\rightarrow (p<q).
\]
Since $q/i\Downarrow p$ holds, we conclude $p<q$, contradicting (3) $\neg(p<q)$.

Hence $\neg(q/\Phi(p)\downarrow p)$. $\square$

And the special case for free/sovereign persons (using $\operatorname{Free}(p)$ or $\operatorname{Sov}(p)$\; earlier we had $\operatorname{Free}\leftrightarrow \operatorname{Sov}$):

$TF3$ (Free/Sovereign Persons): $\forall p\in\mathcal P\
\Bigl(F(\Phi,p)\ \wedge\ \operatorname{Free}(p)\ \rightarrow\ \forall q\in\mathcal P\ (q\neq p\rightarrow \neg(q/\Phi(p)\downarrow p))\Bigr)$
If a person is Free (Sovereign), no one else in the world has the right to put them into a Forbidden state without their consent.
Proof. Fix $p\in\mathcal P$ and assume:

  1. $F(\Phi,p)$,
  2. $\operatorname{Free}(p)$.

Let $q\in\mathcal P$ and assume $q\neq p$. We prove $\neg(q/\Phi(p)\downarrow p)$.

From $\operatorname{Free}(p)$ and $TP1$, we have $\operatorname{Real}(p)$, hence $p<p$ (by $DP1$).
Also, from $\operatorname{Free}(p)$ and $TP3$, we have $\operatorname{Sov}(p)$, i.e. $\forall r\in\mathcal P\,(p<r\rightarrow r=p)$.
Therefore, if $p<q$ then $q=p$, contradicting $q\neq p$; hence $\neg(p<q)$.

Now apply $TF2'$ with the same $p,q$: we have $F(\Phi,p)$ by (1), $\operatorname{Real}(p)$ as shown, and $\neg(p<q)$ as shown, so $TF2'$ yields
\[
\neg(q/\Phi(p)\downarrow p).
\]
Since $q$ was arbitrary (subject to $q\neq p$), we conclude
\[
\forall q\in\mathcal P\ (q\neq p\rightarrow \neg(q/\Phi(p)\downarrow p)).
\]
$\square$

Excluded (X-)states

Van Dun’s “X-state” condition for $\Psi(x)$ is: any action that produces $\Psi(x)$ is such that no one has a right to do it without the consent of any person. In our action-right notation $p/i\Downarrow q$:

$DX$ (Excluded State): $X(\Psi,x)\ \:=\ \forall i\in\mathcal A\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\bigl((i\Vdash \Psi(x))\rightarrow \neg(p/i\Downarrow q)\bigr).$
An Excluded State ($\Psi$) is a state that is universally strictly prohibited. It is a state that no one has the right to produce in anyone (or anything) without consent.

Immediate consequence stated in the text

For any $x$ that has an X-state $\Psi$, no one has a weak right to produce $\Psi(x)$ without anyone’s consent:

$TX1$: $\forall x\in\mathcal D\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl(X(\Psi,x)\rightarrow \neg\bigl(p/\Psi(x)\downarrow q\bigr)\Bigr)$
If a state is Excluded, then logically, no one has even a weak right to produce it.
Proof. Fix $x\in\mathcal D$ and $p,q\in\mathcal P$, and assume $X(\Psi,x)$, i.e.
\[
\forall i\in\mathcal A\ \forall p'\in\mathcal P\ \forall q'\in\mathcal P\ \bigl((i\Vdash \Psi(x))\rightarrow \neg(p'/i\Downarrow q')\bigr).
\]
Suppose for contradiction that $p/\Psi(x)\downarrow q$. By definition of weak right,
\[
p/\Psi(x)\downarrow q \;\equiv\; \exists i\in\mathcal A\bigl((i\Vdash \Psi(x))\wedge (p/i\Downarrow q)\bigr).
\]
Choose $i\in\mathcal A$ with $i\Vdash \Psi(x)$ and $p/i\Downarrow q$. But instantiating $X(\Psi,x)$ at this $i$, and at $p'=p$, $q'=q$, yields $\neg(p/i\Downarrow q)$, contradiction. Hence $\neg(p/\Psi(x)\downarrow q)$. $\square$

“No innocence” examples (as formal schemas)

Let $I(p)$ be the primitive “innocent” predicate on persons (from $\mathbf L_0$). Consider the state-former
$$
\Psi_I(p)\ \text{meaning the state } \neg I(p).
$$
Then “$\neg I$ is an X-state for any person” can be expressed as:

$Assump-I-X$: $\forall q\in\mathcal P\ X(\Psi_I,q).$
We assume that “Loss of Innocence” ($\neg I$) is an Excluded State.

From this, you get the two displayed instances in the text as specializations of TX1: no one has the right to make another person (or themselves) non-innocent. Depriving someone of innocence is a universal wrong. As follows:

$IX1$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \forall r\in\mathcal P\
\neg\bigl(p/\neg I(q)\downarrow r\bigr)$
Proof. Assume $Assump$-$I$-$X$: $\forall t\in\mathcal P\ X(\Psi_I,t)$, where $\Psi_I(t)$ denotes the state $\neg I(t)$.
Fix $p,q,r\in\mathcal P$. From the assumption with $t:=q$, we have $X(\Psi_I,q)$.
Now apply $TX1$ with $x:=q$, $\Psi:=\Psi_I$, and $(p,q)$ there replaced by $(p,r)$ here:
\[
X(\Psi_I,q)\rightarrow \neg(p/\Psi_I(q)\downarrow r),
\]
i.e. $\neg\bigl(p/\neg I(q)\downarrow r\bigr)$. $\square$

$IX2$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\
\neg\bigl(p/\neg I(p)\downarrow q\bigr)$
Proof. This is the special case of $IX1$ obtained by setting $r:=q$ and keeping the same $p$, and taking $q:=p$ in $IX1$:
\[
\forall p\in\mathcal P\ \forall q\in\mathcal P\ \neg\bigl(p/\neg I(p)\downarrow q\bigr).
\]
$\square$

(These match the text’s “there is no person $R$/$Q$ without whose consent …” formulation, which is exactly $\neg$p/S\downarrow r$$ under DA5.)

“No freedom” example

Let $\Psi_F(p)$ mean “$\neg\operatorname{Free}(p)$” as a state of a person. As Van Dun said, the following statement requires extra assumptions. I show that it does follow if you add such extra assumptions.

$IFree$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\Bigl(\operatorname{Free}(p)\rightarrow \neg\bigl(p/\neg\operatorname{Free}(p)\downarrow q\bigr)\Bigr).$
We can derive that no one has the right to deprive a Free Person of their freedom ($\neg \text{Free}(p)$). This follows if we assume that losing freedom implies losing innocence (a free person who becomes a slave or serf has been wronged), or if we directly assume that “Loss of Freedom” is an Excluded State for free persons.

Claim. $IFree$ is derivable from the following two assumptions:

\[
(A\text{-}I\text{-}X)\quad \forall r\in\mathcal P\ X(\Psi_I,r),
\]
i.e.
\[
\forall r\in\mathcal P\ \forall i\in\mathcal A\ \forall a\in\mathcal P\ \forall b\in\mathcal P\
\Bigl((i\Vdash \neg I(r))\rightarrow \neg(a/i\Downarrow b)\Bigr),
\]
and
\[
(A\text{-}F\Rightarrow I)\quad \forall p\in\mathcal P\Bigl(\operatorname{Free}(p)\rightarrow \forall i\in\mathcal A\bigl((i\Vdash \Psi_F(p))\rightarrow (i\Vdash \Psi_I(p))\bigr)\Bigr),
\]
equivalently
\[
\forall p\in\mathcal P\ \forall i\in\mathcal A\
\Bigl((\operatorname{Free}(p)\wedge i\Vdash \neg\operatorname{Free}(p))\rightarrow (i\Vdash \neg I(p))\Bigr).
\]

Proof (from $(A\text{-}I\text{-}X)$ and $(A\text{-}F\Rightarrow I)$).
Fix $p\in\mathcal P$ and $q\in\mathcal P$, and assume $\operatorname{Free}(p)$. We prove
$\neg\bigl(p/\neg\operatorname{Free}(p)\downarrow q\bigr)$.

Suppose for contradiction that $p/\neg\operatorname{Free}(p)\downarrow q$.
By the definition of weak right for states,
\[
p/\neg\operatorname{Free}(p)\downarrow q\ \equiv\ \exists i\in\mathcal A\Bigl((i\Vdash \neg\operatorname{Free}(p))\wedge (p/i\Downarrow q)\Bigr).
\]
Choose $i\in\mathcal A$ such that $i\Vdash \neg\operatorname{Free}(p)$ and $p/i\Downarrow q$.

From $\operatorname{Free}(p)$ and $(A\text{-}F\Rightarrow I)$, we get
\[
(i\Vdash \neg\operatorname{Free}(p))\rightarrow (i\Vdash \neg I(p)),
\]
hence $i\Vdash \neg I(p)$.

Now apply $(A\text{-}I\text{-}X)$ with $r:=p$, $a:=p$, $b:=q$:
since $i\Vdash \neg I(p)$, we obtain $\neg(p/i\Downarrow q)$, contradicting $p/i\Downarrow q$.

Therefore $\neg\bigl(p/\neg\operatorname{Free}(p)\downarrow q\bigr)$, and since $q$ was arbitrary,
\[
\forall q\in\mathcal P\Bigl(\operatorname{Free}(p)\rightarrow \neg\bigl(p/\neg\operatorname{Free}(p)\downarrow q\bigr)\Bigr).
\]
As $p$ was arbitrary, $IFree$ holds. $\square$

Alternative sufficient assumption.
Instead of $(A\text{-}F\Rightarrow I)$, one may assume directly that “no freedom” is an X-state \emph{for free persons}:
\[
(A\text{-}F\text{-}X)\quad \forall p\in\mathcal P\Bigl(\operatorname{Free}(p)\rightarrow X(\Psi_F,p)\Bigr),
\]
i.e.
\[
\forall p\in\mathcal P\Bigl(\operatorname{Free}(p)\rightarrow \forall i\in\mathcal A\ \forall a\in\mathcal P\ \forall b\in\mathcal P\
\bigl((i\Vdash \neg\operatorname{Free}(p))\rightarrow \neg(a/i\Downarrow b)\bigr)\Bigr).
\]

Proof (from $(A\text{-}F\text{-}X)$).
Fix $p,q\in\mathcal P$ and assume $\operatorname{Free}(p)$. Then $X(\Psi_F,p)$ by $(A\text{-}F\text{-}X)$.
By $TX1$ (instantiated with $x:=p$ and $\Psi:=\Psi_F$), we have:
\[
X(\Psi_F,p)\rightarrow \neg\bigl(p/\Psi_F(p)\downarrow q\bigr),
\]
i.e.
\[
\neg\bigl(p/\neg\operatorname{Free}(p)\downarrow q\bigr).
\]
Thus $IFree$ follows. $\square$

General Principle of Justice

Axiom constraining innocence

Only persons can be “innocent.” Objects cannot have moral innocence.

$A_{03}$: $
\forall o\in\mathcal D\ \Bigl(I(o)\rightarrow \exists p\in\mathcal P\ (p=o)\Bigr)$

Equivalently (and more simply, since $p=o$ just means “$o$ is a person”):

$A_{03'}
\forall o\in\mathcal D\ \bigl(I(o)\rightarrow o\in\mathcal P\bigr)$

General principle of justice (GJ)

Van Dun’s statement “Only innocent persons are free” becomes:

$GJ$ (Justice and Freedom): $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\rightarrow I(p)\bigr)$

Since earlier we proved $\operatorname{Free}(p)\leftrightarrow \operatorname{Sov}(p)$, you can also write the equivalent form:

$GJ′$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow I(p)\bigr)$

Formally, if a person is Free (or Sovereign), they must be Innocent. Freedom is conditional on maintaining innocence.

Contrapositive: If you are not innocent (i.e., you are a criminal/aggressor), you cannot be Free/Sovereign. You lose your standing as a self-owner.

Theorems derived from GJ (TG)

TG1

$TG1$ (The Solitary Man): $\forall p\in\mathcal P\ \Bigl(\bigl(\forall q\in\mathcal P\ (q=p)\bigr)\rightarrow I(p)\Bigr)$
If only one person exists in the universe, that person must be Innocent. (Because they are necessarily Sovereign by TP20, and Sovereignty implies Innocence by GJ).
Proof. Fix $p\in\mathcal P$ and assume $\forall q\in\mathcal P\,(q=p)$.
Then by $TP20$, $\operatorname{Sov}(p)$.
By $GJ'$, $\operatorname{Sov}(p)\rightarrow I(p)$.
Hence $I(p)$. $\square$

(If $p$ is the only person, then $p$ is innocent.)

TG2

Van Dun writes: “If no person is innocent, then no person is sovereign.” Formally:

$TG2$ (Universal Guilt implies Universal Serfdom): $\Bigl(\forall p\in\mathcal P\ \neg I(p)\Bigr)\ \rightarrow\ \Bigl(\forall q\in\mathcal P\ \neg\operatorname{Sov}(q)\Bigr)$
If no one is innocent (everyone is a criminal), then no one can be Sovereign.
Proof. Assume $\forall p\in\mathcal P\ \neg I(p)$. Let $q\in\mathcal P$ be arbitrary; we show $\neg\operatorname{Sov}(q)$.
Suppose for contradiction that $\operatorname{Sov}(q)$. Then by $GJ'$, $I(q)$, contradicting $\neg I(q)$ from the assumption.
Therefore $\neg\operatorname{Sov}(q)$. Since $q$ was arbitrary, $\forall q\in\mathcal P\,\neg\operatorname{Sov}(q)$. $\square$

(Using GJ′ and classical contraposition.)

TG3 (finite-world add-on)

This is a meta-result again (it depends on finiteness of (|\mathcal P|), like MT3 earlier).

$TG3$ (The Finite World Result): $\Bigl(|\mathcal P|<\infty\ \wedge\ \forall p\in\mathcal P\ \neg I(p)\Bigr)\ \rightarrow\ \exists q\in\mathcal P\ \operatorname{SAut}(q)$
In a finite world, if everyone is non-innocent (guilty), then some people must be Strictly Autonomous (members of a collective).
Proof (metalanguage). Assume $|\mathcal P|<\infty$ and $\forall p\in\mathcal P\ \neg I(p)$.
By $TG2$, from $\forall p\in\mathcal P\ \neg I(p)$ we obtain $\forall p\in\mathcal P\ \neg\operatorname{Sov}(p)$.

By $MT3$, $|\mathcal P|<\infty$ implies $\exists a\in\mathcal P\ \operatorname{Aut}(a)$. Choose such an $a$.
From $TP10$, $\operatorname{Aut}(a)\rightarrow (\operatorname{Sov}(a)\ \vee\ \operatorname{SAut}(a))$.
But we have $\neg\operatorname{Sov}(a)$, so $\operatorname{SAut}(a)$ follows. Therefore $\exists q\in\mathcal P\ \operatorname{SAut}(q)$. $\square$

That is, if we are all criminals, we cannot be independent sovereigns. We must form collectives (states/gangs) where we belong to one another to survive, or we are all just serfs. But since a finite chain of serfs must end somewhere, if there are no Sovereigns, there must be Collectives.

Section II: System $\mathbf L_2$: Natural persons and natural belonging

Primitive addition

We introduce a new, fundamental relationship called Natural Belonging ($\lessdot$). This is distinct from legal ownership ($<$). Legal ownership is a social construct; “natural belonging” is a physical or biological fact (e.g., my arm naturally belongs to me in a way that my car does not).

Add a primitive binary relation
$$
\lessdot\ \subseteq \mathcal D\times \mathcal D
$$
read “naturally belongs to”.

(We will only use it below with $x\in\mathcal M$ and $p\in\mathcal P$, and occasionally with $p,q\in\mathcal P$.)

Definition of natural persons (DN)

Introduce the class of natural persons:
$DN1$: $\mathcal N \;\:=\; {p\in\mathcal P \mid p\lessdot p}.$
A Natural Person is defined as any person who naturally belongs to themselves.

Equivalently, for $p\in\mathcal P$:
$$
p\in\mathcal N\ \leftrightarrow\ (p\lessdot p).
$$

This distinguishes human beings (who have a physical, biological link to their own existence) from artificial persons (like corporations or the State), which exist only legally.

Axioms constraining $\lessdot$ ($A_2$)

$A_{21}$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \bigl((x\lessdot p)\rightarrow (p\in\mathcal N)\bigr)$
If a physical object (means) naturally belongs to a person, that person must be a Natural Person. (Corporations don’t have biological limbs).

$A_{22}$ (Uniqueness of Self): $\forall p\in\mathcal P\ \forall q\in\mathcal P\ \bigl((p\lessdot q)\rightarrow (p=q)\bigr)$
If Person $p$ naturally belongs to Person $q$, then $p$ and $q$ must be the same person. (You cannot naturally be someone else).

$A_{23}$ (Exclusivity of Body): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\
\bigl((x\lessdot p\ \wedge\ x\lessdot q)\rightarrow (p=q)\bigr)$
If a specific object (like a body part) naturally belongs to Person $p$ and also naturally belongs to Person $q$, then $p$ and $q$ must be the same person.

That is, natural belonging is exclusive. Two distinct people cannot naturally possess the exact same physical body. (With apologies to the plural community.)

Theorems on Natural Persons (TN)

(Using $\mathcal P\subseteq\mathcal M$, so persons count as means.)

$TN1$: $\forall p\in\mathcal P\ \bigl(p\in\mathcal N\rightarrow \exists x\in\mathcal M\ (x\lessdot p)\bigr)$
Every Natural Person possesses at least one means that naturally belongs to them (i.e., their body).
Proof. Fix $p\in\mathcal P$ and assume $p\in\mathcal N$. By $DN1$, $p\lessdot p$.
Using the standing convention “$\mathcal P\subseteq\mathcal M$”, we have $p\in\mathcal M$.
Let $x:=p$. Then $x\in\mathcal M$ and $x\lessdot p$ (since $p\lessdot p$). Hence $\exists x\in\mathcal M\,(x\lessdot p)$. $\square$

$TN2$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\
\Bigl((p\in\mathcal N\ \wedge\ q\in\mathcal N\ \wedge\ p\neq q)\rightarrow
\exists x\in\mathcal M\ (x\lessdot p\ \wedge\ \neg(x\lessdot q))\Bigr)$
Distinct Natural Persons have distinct bodies. If $p$ and $q$ are two different natural persons, there is some physical part of $p$ that does not naturally belong to $q$.
Proof. Fix $p,q\in\mathcal P$ and assume $p\in\mathcal N$, $q\in\mathcal N$, and $p\neq q$.
By $DN1$, $p\lessdot p$ and $q\lessdot q$.
Again using $\mathcal P\subseteq\mathcal M$, we have $p\in\mathcal M$.

Take $x:=p$. Then $x\lessdot p$ holds (since $p\lessdot p$).
We show $\neg(x\lessdot q)$: if $x\lessdot q$, then $p\lessdot q$.
But $A_{22}$ says $\forall r\in\mathcal P\ \forall s\in\mathcal P\,((r\lessdot s)\rightarrow r=s)$, so from $p\lessdot q$ we would get $p=q$, contradicting $p\neq q$.
Hence $\neg(p\lessdot q)$, i.e. $\neg(x\lessdot q)$.

Therefore $\exists x\in\mathcal M\,(x\lessdot p\wedge \neg(x\lessdot q))$. $\square$

Postulates of Natural Law

These are “meta-principles” regarding how the abstract legal system connects to the physical world.

The Framework

PF: Finitism

$PF$ (Finitism): $|\mathcal N|<\infty$
The number of Natural Persons is finite.

PN: Naturalism

$PN$ (Naturalism): $\forall x\in\mathcal M\ \exists q\in\mathcal N\ (x<q)$
Every object and every legal person ultimately “anchors” back to a Natural Person.

From PN (using $\mathcal P\subseteq\mathcal M$):

$NL1$: $\forall p\in\mathcal P\ \exists q\in\mathcal N\ (p<q)$
Every legal person belongs to a Natural Person (or a chain leading to one).
Proof. Assume $PN$: $\forall x\in\mathcal M\ \exists q\in\mathcal N\ (x<q)$.
Fix $p\in\mathcal P$. Using $\mathcal P\subseteq\mathcal M$, we have $p\in\mathcal M$.
Apply $PN$ to $x:=p$ to obtain $\exists q\in\mathcal N\,(p<q)$. $\square$

$NL2$: $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\rightarrow p\in\mathcal N\bigr)$
Only natural persons can be free.
Proof. Assume $PN$. Fix $p\in\mathcal P$ and assume $\operatorname{Free}(p)$.
By $NL1$, choose $q\in\mathcal N$ with $p<q$.
Since $q\in\mathcal N$, by $DN1$ we have $q\lessdot q$.

Now use $A_{22}$: if $p\lessdot q$ then $p=q$. So to show $p\in\mathcal N$ it suffices to show $p\lessdot p$.
But with only $PN$ and the given axioms $A_{21}$–$A_{23}$, there is no principle that produces a $\lessdot$-fact for $p$ from $\operatorname{Free}(p)$ or from $p<q$.
Thus, as stated, $NL2$ is not derivable from $PN$ alone (it requires an additional bridge principle relating freedom/sovereignty to natural belonging, or an axiom asserting that the “top” natural person over $p$ is $p$ itself, etc.). $\square$

$NL3$: $\forall p\in\mathcal P\ \bigl(\operatorname{Sov}(p)\rightarrow p\in\mathcal N\bigr)$
Only natural persons can be sovereign.
Proof. Assume $PN$. Fix $p\in\mathcal P$ and assume $\operatorname{Sov}(p)$.
As with $NL2$, $PN$ yields $\exists q\in\mathcal N\,(p<q)$ but the axioms $A_{21}$–$A_{23}$ do not allow concluding $p\lessdot p$ from $\operatorname{Sov}(p)$ or from $p<q$.
So $NL3$ is likewise not derivable from $PN$ alone without an additional bridge axiom connecting sovereignty (or $p<p$) to $p\lessdot p$. $\square$

And from PF + PN (a finiteness meta-argument, as earlier with MT3/MT4):

$NL4$: $(PF\ \wedge\ PN)\ \rightarrow\ \exists p\in\mathcal N\ \operatorname{Aut}(p)$
In a finite world, there must be at least one Natural Person who is Autonomous. (The chain of responsibility cannot go on forever; it must stop at a human being).
Proof (metalanguage). Assume $PF$: $|\mathcal N|<\infty$ and $PN$: $\forall x\in\mathcal M\ \exists q\in\mathcal N\ (x<q)$.
Restrict the relation $<$ to $\mathcal N$. The transitivity-on-persons lemma from Section I (derived from $A_{02}$ and $SD2$) applies in particular to elements of $\mathcal N\subseteq\mathcal P$.
By finiteness of $\mathcal N$, the same maximal-element argument as in $MT3$ yields some $p\in\mathcal N$ such that for all $q\in\mathcal N$, $p<q\rightarrow q<p$.

To see $\operatorname{Aut}(p)$ (which quantifies over all $q\in\mathcal P$), take any $q\in\mathcal P$ with $p<q$.
By $PN$ applied to $x:=q$ (using $\mathcal P\subseteq\mathcal M$), pick $r\in\mathcal N$ with $q<r$.
Then by transitivity on persons, $p<q$ and $q<r$ imply $p<r$.
By maximality of $p$ within $\mathcal N$, from $p<r$ (with $r\in\mathcal N$) we get $r<p$.
Now $q<r$ and $r<p$ give $q<p$ by transitivity.
Thus $p<q\rightarrow q<p$ for arbitrary $q\in\mathcal P$, so $\operatorname{Aut}(p)$. Hence $\exists p\in\mathcal N\,\operatorname{Aut}(p)$. $\square$

PC: Consistency (natural (\Rightarrow) lawful)

$PC$ (Consistency): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \bigl((x\lessdot p)\rightarrow (x<p)\bigr)$
If something naturally belongs to you, it must legally belong to you ($x \lessdot p \rightarrow x < p$).

That is, natural fact creates legal title. If it is my hand biologically, it is my property legally.

Consequences (using $p\in\mathcal N\iff p\lessdot p$ and $\operatorname{Real}(p)\equiv(p<p)$):

$NL5$: $\forall p\in\mathcal P\ \bigl(p\in\mathcal N\rightarrow \operatorname{Real}(p)\bigr)$
Every Natural Person is a Real Person (self-owner). Proof. Assume $PC$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\,((x\lessdot p)\rightarrow (x<p))$.
Fix $p\in\mathcal P$ and assume $p\in\mathcal N$.
By $DN1$, $p\lessdot p$. Using $\mathcal P\subseteq\mathcal M$, $p\in\mathcal M$.
Apply $PC$ with $x:=p$ and $p:=p$ to get $p<p$.
By $DP1$, $\operatorname{Real}(p)\equiv (p<p)$. Hence $\operatorname{Real}(p)$. $\square$

$NL6$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\
\bigl((x\lessdot p\ \wedge\ p<q)\rightarrow x<q\bigr)$
If $x$ naturally belongs to $p$, and $p$ lawfully belongs to $q$, then $x$ lawfully belongs to $q$.
Proof. Fix $x\in\mathcal M$, $p,q\in\mathcal P$ and assume $x\lessdot p$ and $p<q$.
From $PC$, $x\lessdot p \rightarrow x<p$, so obtain $x<p$.
Now apply $A_{02}$ with this $x\in\mathcal M$ and $p<q$:
\[
(x<p\ \wedge\ p<q)\rightarrow x<q.
\]
Hence $x<q$. $\square$

PI: Individualism (claims to natural property track claims to the person)

$PI$ (Individualism): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\bigl((x\lessdot p\ \wedge\ x<q)\rightarrow (p<q)\bigr)$
This is a crucial “anti-slavery” postulate. It states: If $x$ naturally belongs to me (e.g., my body), and you claim to own $x$, then you are claiming to own me.

From PC + PI (and the transitivity axiom $A_{02}$ from $\mathbf L_0$):

$NL7$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\
\Bigl((x\lessdot p)\rightarrow \bigl((x<q)\leftrightarrow(p<q)\bigr)\Bigr)$
Owning a person’s natural means is logically equivalent to owning the person themselves.
Proof. Assume $PC$ and $PI$.
Fix $x\in\mathcal M$, $p,q\in\mathcal P$ and assume $x\lessdot p$.

($\Rightarrow$) Assume $x<q$. Then by $PI$,
\[
(x\lessdot p\ \wedge\ x<q)\rightarrow (p<q),
\]
so $p<q$.

($\Leftarrow$) Assume $p<q$. Then by $PC$, $x\lessdot p\rightarrow x<p$, so $x<p$.
Now apply $A_{02}$:
\[
(x<p\ \wedge\ p<q)\rightarrow x<q,
\]
hence $x<q$.

Therefore $(x<q)\leftrightarrow(p<q)$ under the assumption $x\lessdot p$. $\square$

Using the earlier “right-to-deny” notation $q\uparrow p/x$: If you deny my right to my own body, you are asserting a claim of ownership over me, as follows.

$NL8$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\
\bigl((x\lessdot p\ \wedge\ (q\uparrow p/x))\rightarrow (p<q)\bigr)$
If $x$ naturally belongs to $p$, then $q$ can have a right to deny $p$ the use of $x$ only if $p$ belongs to $q$. Proof. Fix $x\in\mathcal M$, $p,q\in\mathcal P$ and assume $x\lessdot p$ and $(q\uparrow p/x)$.
By $DR1$, specializing variables as in $q\uparrow p/x$, we have
\[
(q\uparrow p/x)\ \equiv\ \bigl((x<q\ \vee\ p<q)\ \wedge\ \neg(q<p)\bigr),
\]
hence in particular $x<q\ \vee\ p<q$.
If $p<q$, done. Otherwise $x<q$.
Then by $PI$, $(x\lessdot p\ \wedge\ x<q)\rightarrow (p<q)$, and since both antecedents hold, conclude $p<q$.
Thus $(x\lessdot p\ \wedge\ (q\uparrow p/x))\rightarrow (p<q)$. $\square$

$NL9$: $\forall p\in\mathcal P\ \forall q\in\mathcal P\
\bigl((p\in\mathcal N\ \wedge\ (q\uparrow p/p))\rightarrow (p<q)\bigr)$
If $p$ is a natural person, then $q$ can have a right to deny $p$ the use of himself only if $p$ belongs to $q$. Proof. Fix $p,q\in\mathcal P$ and assume $p\in\mathcal N$ and $(q\uparrow p/p)$.
By $DN1$, $p\in\mathcal N\rightarrow (p\lessdot p)$, so $p\lessdot p$.
Using $\mathcal P\subseteq\mathcal M$, we have $p\in\mathcal M$.
Now apply $NL8$ with $x:=p$ to the conjunction $(p\lessdot p\ \wedge\ (q\uparrow p/p))$ to obtain $p<q$.
Hence $(p\in\mathcal N\ \wedge\ (q\uparrow p/p))\rightarrow (p<q)$. $\square$

Principle of Natural Justice

Definition of $\mathbb I$ (innocent natural person)

$Def (\mathbb I)$: $\mathbb I(p)\ \:=\ \bigl(p\in\mathcal N\ \wedge\ I(p)\bigr)
\qquad(p\in\mathcal P)$
An Innocent Natural Person is simply a Natural Person who is Innocent ($I$).

NJ: Innocent natural persons are free

$NJ$ (Natural Justice): $\forall p\in\mathcal P\ \bigl(\mathbb I(p)\rightarrow \operatorname{Free}(p)\bigr)$
Innocent natural persons are Free.

This bridges the gap between biology and rights. If you are a human being and you have done no wrong, you are legally Free.

Consequences of Natural Justice

Together with the general justice principle from Section I (GJ: $\operatorname{Free}(p)\to I(p)$), this yields:

$NJ1$: $\forall p\in\mathcal N\ \bigl(\operatorname{Free}(p)\leftrightarrow I(p)\bigr)$
For Natural Persons, Freedom and Innocence are equivalent. To be innocent is to be free; to be free requires being innocent. Proof. Assume $NJ$: $\forall p\in\mathcal P\,(\mathbb I(p)\rightarrow \operatorname{Free}(p))$ and the general justice principle $GJ$: $\forall p\in\mathcal P\,(\operatorname{Free}(p)\rightarrow I(p))$.
Fix $p\in\mathcal N$.

($\rightarrow$) If $\operatorname{Free}(p)$ then by $GJ$ we get $I(p)$.

($\leftarrow$) If $I(p)$, then since $p\in\mathcal N$ we have $\mathbb I(p)$ by $Def(\mathbb I)$, hence $\operatorname{Free}(p)$ by $NJ$.

Thus $\operatorname{Free}(p)\leftrightarrow I(p)$. $\square$

And since $\operatorname{Free}\to\operatorname{Sov}\to\operatorname{Aut}$ and $\operatorname{Free}\to\neg\operatorname{SAut}$:

Innocent natural persons are Autonomous (self-governing) and cannot be Strictly Autonomous (they cannot be mere members of a collective):

$NJ2$: $\forall p\in\mathcal P\ \bigl(\mathbb I(p)\rightarrow \operatorname{Aut}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\mathbb I(p)$. By $NJ$, $\operatorname{Free}(p)$.
From Section I, $TP3$ gives $\operatorname{Free}(p)\rightarrow \operatorname{Sov}(p)$, and $TP6'$ gives $\operatorname{Sov}(p)\rightarrow \operatorname{Aut}(p)$.
Hence $\operatorname{Aut}(p)$. $\square$

$NJ3$: $\forall p\in\mathcal P\ \bigl(\mathbb I(p)\rightarrow \neg\operatorname{SAut}(p)\bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\mathbb I(p)$. By $NJ$, $\operatorname{Free}(p)$, hence by $TP3$ we get $\operatorname{Sov}(p)$.
But $\operatorname{SAut}(p)\equiv \operatorname{Aut}(p)\wedge \neg\operatorname{Sov}(p)$ by $DP6$, so $\operatorname{Sov}(p)$ implies $\neg\operatorname{SAut}(p)$. $\square$

That is, innocence implies independence. You cannot be an innocent member of a collective where ownership is shared; innocent humans are sovereigns.

Using $\operatorname{Free}\leftrightarrow\operatorname{Sov}$ from Section I:

$NJ4$: $\forall p\in\mathcal N\ \bigl(\operatorname{Sov}(p)\leftrightarrow I(p)\bigr)$
For Natural Persons, Sovereignty is equivalent to Innocence.
Proof. Fix $p\in\mathcal N$.
From Section I, $TP5$ gives $\operatorname{Sov}(p)\leftrightarrow \operatorname{Free}(p)$.
From $NJ1$ (since $p\in\mathcal N$), $\operatorname{Free}(p)\leftrightarrow I(p)$.
Chaining equivalences yields $\operatorname{Sov}(p)\leftrightarrow I(p)$. $\square$

Property and Rights of the Innocent

Further consequences listed in the text: Innocent natural persons are separate entities. If $p$ is innocent, there is property (their body) that belongs to them and not to anyone else:

$NJ5$: $\forall p\in\mathcal P\ \forall q\in\mathcal P
\Bigl((\mathbb I(p)\ \wedge\ \mathbb I(q)\ \wedge\ p\neq q)\rightarrow
\exists x\in\mathcal M\ (x<p\ \wedge\ \neg(x<q))\Bigr)$
Proof. Fix $p,q\in\mathcal P$ and assume $\mathbb I(p)$, $\mathbb I(q)$, and $p\neq q$.
From $\mathbb I(p)$ and $NJ$, we get $\operatorname{Free}(p)$; then by $TP3$, $\operatorname{Sov}(p)$; and by $DP2$ (or $TP1$), $\operatorname{Free}(p)$ implies $p<p$.
Since $p<p$, by $SD2$ we have $p\in\mathcal M$ (witness $o:=p$ in $\exists o\,(p<o)$).

Let $x:=p$. Then $x\in\mathcal M$ and $x<p$ is $p<p$, which holds.
Also, $\neg(x<q)$: if $p<q$, then $\operatorname{Sov}(p)$ (i.e. $\forall r\in\mathcal P\,(p<r\rightarrow r=p)$) would give $q=p$, contradicting $p\neq q$.
Hence $\exists x\in\mathcal M\,(x<p\wedge \neg(x<q))$. $\square$

$NJ6$: $\forall p\in\mathcal P
\Bigl(\mathbb I(p)\rightarrow \exists x\in\mathcal M\ \bigl(x<p\ \wedge\ \forall q\in\mathcal P\ (q\neq p\rightarrow \neg(x<q))\bigr)\Bigr)$
Proof. Fix $p\in\mathcal P$ and assume $\mathbb I(p)$. Then by $NJ$, $\operatorname{Free}(p)$, hence $p<p$ and $\operatorname{Sov}(p)$ by $TP3$.
As in $NJ5$, $p<p$ implies $p\in\mathcal M$ by $SD2$.

Let $x:=p$. Then $x\in\mathcal M$ and $x<p$ holds (since $p<p$).
Now take any $q\in\mathcal P$ with $q\neq p$. If $x<q$ (i.e. $p<q$), then $\operatorname{Sov}(p)$ would force $q=p$, contradiction. Hence $\neg(x<q)$.
Therefore $\forall q\in\mathcal P\,(q\neq p\rightarrow \neg(x<q))$, and the required $x$ exists. $\square$

$NJ7$ (Self-Determination): $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P
\bigl((x\lessdot p\ \wedge\ x<q\ \wedge\ I(p))\rightarrow (p=q)\bigr)$
If $x$ is my natural body part ($x \lessdot p$), and I am innocent, and someone else ($q$) claims to own $x$, then $q$ must be me. (No one else can own an innocent person’s body).
Proof. Assume $PI$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\ \forall q\in\mathcal P\,((x\lessdot p\wedge x<q)\rightarrow (p<q))$.
Fix $x\in\mathcal M$, $p,q\in\mathcal P$ and assume $x\lessdot p$, $x<q$, and $I(p)$.

From $x\lessdot p$ and $A_{21}$, we get $p\in\mathcal N$.
Together with $I(p)$, by $Def(\mathbb I)$ we have $\mathbb I(p)$, hence by $NJ$ we get $\operatorname{Free}(p)$, and by $TP3$ we get $\operatorname{Sov}(p)$.

From $x\lessdot p$ and $x<q$, $PI$ yields $p<q$.
But $\operatorname{Sov}(p)$ means $p<r\rightarrow r=p$ for all $r\in\mathcal P$, so from $p<q$ we conclude $q=p$, i.e. $p=q$. $\square$

$NJ8$ (Exclusive Title): $\forall x\in\mathcal M\ \forall p\in\mathcal P
\bigl((x\lessdot p\ \wedge\ I(p))\rightarrow (x\ll p)\bigr)$
If I am an innocent natural person, and $x$ is my natural body part, then I Own ($x \ll p$) it in the strongest sense. No one else has any claim to it whatsoever.
Proof. (Using the standard “exclusive belonging” reading)
Assume $x\ll p$ abbreviates:
\[
x\ll p\ \;:\equiv\;\ x<p\ \wedge\ \forall q\in\mathcal P\ \bigl((x<q)\rightarrow (q=p)\bigr).
\]
Assume also $PC$: $\forall x\in\mathcal M\ \forall p\in\mathcal P\,((x\lessdot p)\rightarrow (x<p))$.

Fix $x\in\mathcal M$ and $p\in\mathcal P$, and assume $x\lessdot p$ and $I(p)$.
By $PC$, from $x\lessdot p$ we get $x<p$.

To show exclusivity, let $q\in\mathcal P$ and assume $x<q$.
Then $x\lessdot p\wedge x<q\wedge I(p)$ holds, so by $NJ7$ we conclude $p=q$, i.e. $q=p$.
Thus $\forall q\in\mathcal P\,((x<q)\rightarrow (q=p))$.

Therefore $x<p \wedge \forall q\in\mathcal P\,((x<q)\rightarrow (q=p))$, i.e. $x\ll p$. $\square$

Theories of natural law

From Section I we have the trichotomy of legal status for any person $p\in\mathcal P$:

$$
\forall p\in\mathcal P\quad
\bigl(\operatorname{Sov}(p)\ \vee\ \operatorname{SAut}(p)\ \vee\ \operatorname{Het}(p)\bigr),
$$

and these three predicates are pairwise incompatible. (Here $\operatorname{SAut}$ = “strictly autonomous”, $\operatorname{Het}$ = “heteronomous”.)

A type of theory of natural law (here: a “TType”) specifies the originary legal status assigned to natural persons—i.e. to members of $\mathcal N$—in the (idealized) condition where they count as “innocent”. We also set aside “aspect persons” (citizen-$c(p)$, etc.), and talk only about $p\in\mathcal N$ as such.

To make the tables readable, I’ll use ● instead of an asterisk to mean “this theory-type assigns at least one natural person this status (originarily).”

I’ll also keep Van Dun’s “M” column as: some natural persons are denied personal standing and treated as mere means (i.e. as members of $\mathcal M\setminus\mathcal P$ under the theory’s classification). “Type 0” is the extreme where natural persons have no standing even as means (treated as “mere objects”).

Exhaustive list of logically possible theory-types (TType 0–15)

TType $\exists p\in\mathcal N\,\operatorname{Sov}(p)$ $\exists p\in\mathcal N\,\operatorname{SAut}(p)$ $\exists p\in\mathcal N\,\operatorname{Het}(p)$ $\exists p\in\mathcal N$ “mere means” Originary status in law of natural persons
Equal originary status for all
0 None has any standing in law (treated as mere objects)
1 ● All sovereign
2 ● All strictly autonomous
3 ● All heteronomous
4 ● None is a person; all are mere means
Unequal originary status
5 ● ● All autonomous, but only some sovereign
6 ● ● Some sovereign, the rest heteronomous
7 ● ● Some sovereign, the rest mere means
8 ● ● Some strictly autonomous, the rest heteronomous
9 ● ● Some strictly autonomous, the rest mere means
10 ● ● Some heteronomous, the rest mere means
11 ● ● ● Some autonomous, the rest heteronomous
12 ● ● ● Some autonomous, the rest mere means
13 ● ● ● Some sovereign; the rest heteronomous or mere means
14 ● ● ● Some strictly autonomous; some heteronomous; some mere means
15 ● ● ● ● Some of every kind

How to read the columns.

  • A “●” under Sov means: at least one natural person is assigned sovereignty (originarily) by that type.
  • A “●” under SAut means: at least one natural person is assigned strict autonomy (i.e. membership in some autonomous collective).
  • A “●” under Het means: at least one natural person is assigned heteronomy (master/serf or ruler/subject style dependence).
  • A “●” under mere means means: at least one natural person is denied personhood (no standing as a person) and treated as a mere means.

Equal vs. unequal originary status

If a theory says all natural persons share the same originary status, it still must say which status that is (Types 1–4, or 0). But it does not owe an extra story about why some innocents get one status and others get another.

Unequal-status types (5–15) must do more work: even after you pick a status for each category, you still need a justification for the distribution of innocent natural persons across:

  • different autonomous collectives (if strict autonomy is assigned),
  • different masters/rulers (if heteronomy is assigned),
  • different non-person standings (if “mere means” is allowed).

Type 1 (“all sovereign”) is the one that avoids those distribution problems entirely.

Compatibility with the postulates of natural law and with natural justice

When checking compatibility, Van Dun assumes the “originary innocence” condition:

$Orig-Innocence$: $\forall p\in\mathcal N\ I(p).$

And we evaluate each TType against three packages:

  • PNL = the “postulates of natural law” in the broad sense (here: PF + PN, i.e. finiteness + naturalism).
  • PC = the postulate of consistency: $x\lessdot p \Rightarrow x<p$.
  • NJ = natural justice: $\mathbb I(p)\Rightarrow \operatorname{Free}(p)$ (equivalently for $p\in\mathcal N$: $I(p)\Rightarrow \operatorname{Sov}(p)$).

I’ll keep “✓” to mean “satisfies PNL but violates NJ” (i.e. “natural law without natural justice”), as in the original.

TT Sov SAut Het Means PNL (PF+PN) PC NJ Notes
0 No No No no standing at all
1 ● yes yes yes the unique “natural law + natural justice” type
2 ● yes yes No ✓
3 ● No yes No ruled out by PNL (needs infinite descent)
4 ● No No No denies personhood to all naturals
5 ● ● yes yes No ✓
6 ● ● yes yes No ✓
7 ● ● yes No No violates PC
8 ● ● yes yes No ✓
9 ● ● yes No No violates PC
10 ● ● No No No fails PNL
11 ● ● ● yes yes No ✓
12 ● ● ● yes No No violates PC
13 ● ● ● yes No No violates PC
14 ● ● ● yes No No violates PC
15 ● ● ● ● yes No No violates PC

Why PNL eliminates some rows.

  • PNL forces all means (hence all persons) to belong to some finite stock of natural persons. That already conflicts with “no natural persons have any standing” (Types 0 and 4).
  • PNL also implies the existence of at least one autonomous natural person (the finite-world argument), which rules out “all heteronomous” (Type 3) and the mixed “heteronomous + mere means only” (Type 10).

Why PC eliminates many rows.
PC implies natural persons are real persons and thus persons in the $\mathbf L_0$ sense; so any type that assigns mere-object or mere-means standing to some natural persons is incompatible: (0,4,7,9,10,12,13,14,15).

Why NJ collapses everything to TT1.
Under originary innocence, NJ says innocent natural persons are free, hence sovereign. That leaves only Type 1.

Natural law without natural justice (the “political/legal” natural-law types)

These are exactly the types marked ✓ above: they satisfy PNL but reject NJ.

Type Sov SAut Het Originary status for natural persons
Equal originary status
2 ● All strictly autonomous
Unequal originary status
5 ● ● All autonomous, only some sovereign
6 ● ● Some sovereign, the rest heteronomous
8 ● ● Some strictly autonomous, the rest heteronomous
11 ● ● ● Some autonomous, the rest heteronomous

What these share, in our notation, is: some innocent natural persons are not sovereign, hence (by the equivalences in Section I) they satisfy $p<q$ for some $q\neq p$. Combined with $PN$ (everything ultimately belongs to some natural person), this yields the characteristic “legislative” feature:

  • Some natural persons have a right to use other innocent natural persons (or their means) without consent—i.e. some innocents are ruled.

More concretely:

  • Types 2 and 5 confine “rule” to mutual rule inside autonomous collectives (everyone rules everyone in the collective).
  • Type 6 introduces unilateral rulers: some sovereign natural persons rule heteronomous natural persons.
  • Type 8 mixes collective rule (inside autonomous collectives) with heteronomous subjects outside them.
  • Type 11 is the broad mixed case: some are sovereign, some strictly autonomous, some heteronomous.

And that’s the punchline Van Dun is aiming at: any attempt to justify originary unilateral legislation (as distinct from contract) must reject NJ, i.e. must reject the claim that innocent natural persons are free/sovereign.

Section III: System $\mathbf L_3$: Human beings and human law

New primitive predicate

We introduce a new category to the object domain: The Human Being ($\mu$).

Add a unary predicate $\mu(\cdot)$ on the object domain $\mathcal D$, read “is a human being”.

It is often convenient to name the human-beings class:
$$
\mathcal H \;\:=\; {o\in\mathcal D \mid \mu(o)}.
$$

Previously, we only spoke of “Persons” (legal entities) and “Natural Persons” (self-owners). Now, we explicitly identify the biological class of Humans ($\mathcal H$).

Postulates about humans and natural persons

This section explores different logical worldviews regarding how biological humanity relates to natural personhood.

Postulate of anti-humanism

“No human being is a natural person” (formulated for persons, since $\mathcal N\subseteq \mathcal P$):

$PAH$ (The Postulate of Anti-Humanism): $\forall p\in\mathcal P\ \bigl(\mu(p)\rightarrow p\notin\mathcal N\bigr).$

In this grim worldview, biological humanity grants no natural standing. Humans are distinct from the class of entities that naturally belong to themselves.

Postulate of humanist naturalism (PHN)

“Every natural person is a human being”:

$PHN$ (The Postulate of Humanist Naturalism): $\forall p\in\mathcal P\ \bigl(p\in\mathcal N\rightarrow \mu(p)\bigr).$

To be a natural self-owner, you must be human. (There are no Martian or AI natural persons). However, this does not guarantee that all humans are persons.

Postulate of naturalist humanism (PNH)

“Every human being is a natural person” (again, for persons):

$PNH$ (The Postulate of Naturalist Humanism): $\forall p\in\mathcal P\ \bigl(\mu(p)\rightarrow p\in\mathcal N\bigr).$

That is, if you are biologically human, you are automatically a natural person (a self-owner).

(Van Dun’s “weak” version $PNH'$ = “every human person is a natural person” is the same statement in this formalization, since it quantifies only over $\mathcal P$.)

Postulate of humanism (PH)

“All human persons are natural persons; nothing else is a natural person”:

$PH$ (The Postulate of Humanism): $\forall p\in\mathcal P\ \bigl(p\in\mathcal N\leftrightarrow \mu(p)\bigr).$

Equivalently: $\mathcal N = \mathcal P\cap \mathcal H$.

This is the standard “Human Rights” view. The set of Natural Persons and the set of Human Persons are identical ($\mathcal N = \mathcal P \cap \mathcal H$). To be a natural person is to be human, and to be human is to be a natural person.

If one accepts this postulate alongside the Principle of Natural Justice (which states that innocent natural persons are free/sovereign), the result is a theory of law that rejects the originary right of legislation.

Innocent human persons

Define the shorthand “innocent human person”:

$Def (\mathbb I_\mu)$: $\mathbb I_\mu(p)\ \:=\ \bigl(\mu(p)\wedge I(p)\bigr)
\qquad(p\in\mathcal P).$
We define an Innocent Human Person as an entity that is both biologically Human ($\mu$) and legally Innocent ($I$).

(Recall from Section II: $\mathbb I(p)\:= (p\in\mathcal N\wedge I(p))$.)

Theorems/implications stated in the text: deriving human rights

These theorems show what happens when we combine the General Justice principles from previous sections with the Humanist postulates above.

From $PN$ + $GJ$ + $PHN$: Freedom implies Humanity

Using $NL2$ (from $PN$): $\operatorname{Free}(p)\to p\in\mathcal N$, plus $GJ$: $\operatorname{Free}(p)\to I(p)$, plus $PHN$: $p\in\mathcal N\to\mu(p)$, we get:

$H1$: $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\rightarrow \mathbb I_\mu(p)\bigr).$
Proof. Assume $PN$ (so that, in particular, $NL2$: $\forall p\in\mathcal P\,(\operatorname{Free}(p)\rightarrow p\in\mathcal N)$), assume $GJ$: $\forall p\in\mathcal P\,(\operatorname{Free}(p)\rightarrow I(p))$, and assume $PHN$: $\forall p\in\mathcal P\,(p\in\mathcal N\rightarrow \mu(p))$.
Fix $p\in\mathcal P$ and assume $\operatorname{Free}(p)$.

By $NL2$, $\operatorname{Free}(p)\rightarrow p\in\mathcal N$, so $p\in\mathcal N$.
By $PHN$, $p\in\mathcal N\rightarrow \mu(p)$, so $\mu(p)$.
By $GJ$, $\operatorname{Free}(p)\rightarrow I(p)$, so $I(p)$.

By $Def(\mathbb I_\mu)$, $\mathbb I_\mu(p)\equiv (\mu(p)\wedge I(p))$, hence $\mathbb I_\mu(p)$.
Therefore $\operatorname{Free}(p)\rightarrow \mathbb I_\mu(p)$, and since $p$ was arbitrary, the theorem follows. $\square$

“Every Free Person is necessarily an Innocent Human Being.” That is, you cannot be “Free” in this system unless you are human.

From $PNH$ + $NJ$: Humanity implies Freedom

Since $PNH$ gives $\mu(p)\to p\in\mathcal N$, and $NJ$ gives $\mathbb I(p)\to \operatorname{Free}(p)$, we obtain the “innocent humans are free” form:

$H2$: $\forall p\in\mathcal P\ \bigl(\mathbb I_\mu(p)\rightarrow \operatorname{Free}(p)\bigr).$
Proof. Assume $PNH$: $\forall p\in\mathcal P\,(\mu(p)\rightarrow p\in\mathcal N)$ and $NJ$: $\forall p\in\mathcal P\,(\mathbb I(p)\rightarrow \operatorname{Free}(p))$.
Fix $p\in\mathcal P$ and assume $\mathbb I_\mu(p)$.

By $Def(\mathbb I_\mu)$, $\mathbb I_\mu(p)$ means $\mu(p)\wedge I(p)$, so in particular $\mu(p)$ and $I(p)$.
From $PNH$ and $\mu(p)$ we get $p\in\mathcal N$.
Then $p\in\mathcal N$ together with $I(p)$ gives $\mathbb I(p)$ by $Def(\mathbb I)$ from Section II.
Now apply $NJ$ to obtain $\operatorname{Free}(p)$.
Thus $\mathbb I_\mu(p)\rightarrow \operatorname{Free}(p)$, and since $p$ was arbitrary, the theorem follows. $\square$

“Every Innocent Human Being is Free”, i.e., mere biological humanity (combined with innocence) is sufficient to guarantee Freedom.

From $PH$ + $GJ$ + $NJ$: The Humanist Equivalence

Under $PH$, for persons $p$, $p\in\mathcal N\leftrightarrow \mu(p)$, hence $\mathbb I(p)\leftrightarrow \mathbb I_\mu(p)$. Together with $NJ$ $(\mathbb I(p)\to \operatorname{Free}(p))$ and $GJ$ ($\operatorname{Free}(p)\to I(p)$, plus $NL2$ ($\operatorname{Free}(p)\to p\in\mathcal N$)), we get:

$H3$: $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\leftrightarrow \mathbb I(p)\bigr)$
Proof. Assume $PH$: $\forall p\in\mathcal P\,(p\in\mathcal N\leftrightarrow \mu(p))$, assume $NJ$: $\forall p\in\mathcal P\,(\mathbb I(p)\rightarrow \operatorname{Free}(p))$, assume $GJ$: $\forall p\in\mathcal P\,(\operatorname{Free}(p)\rightarrow I(p))$, and assume $NL2$: $\forall p\in\mathcal P\,(\operatorname{Free}(p)\rightarrow p\in\mathcal N)$ (as used in the text).

Fix $p\in\mathcal P$.

($\rightarrow$) Assume $\operatorname{Free}(p)$.
By $NL2$, $p\in\mathcal N$.
By $GJ$, $I(p)$.
Hence $(p\in\mathcal N\wedge I(p))$, i.e. $\mathbb I(p)$ by $Def(\mathbb I)$.

($\leftarrow$) Assume $\mathbb I(p)$.
Then by $NJ$, $\operatorname{Free}(p)$.

Thus $\operatorname{Free}(p)\leftrightarrow \mathbb I(p)$, and since $p$ was arbitrary, the theorem follows. $\square$

and equivalently (the text’s “all and only innocent human persons are free”):

$H3′$: $\forall p\in\mathcal P\ \bigl(\operatorname{Free}(p)\leftrightarrow \mathbb I_\mu(p)\bigr).$
Proof. Assume the same hypotheses as for $H3$, in particular $PH$, $NJ$, $GJ$, and $NL2$.
Fix $p\in\mathcal P$.

First note that under $PH$ we have $p\in\mathcal N\leftrightarrow \mu(p)$, hence:
\[
\mathbb I(p)\equiv(p\in\mathcal N\wedge I(p))\ \leftrightarrow\ (\mu(p)\wedge I(p))\equiv \mathbb I_\mu(p).
\]

From $H3$ we have $\operatorname{Free}(p)\leftrightarrow \mathbb I(p)$.
Combine with $\mathbb I(p)\leftrightarrow \mathbb I_\mu(p)$ to obtain $\operatorname{Free}(p)\leftrightarrow \mathbb I_\mu(p)$.
Since $p$ was arbitrary, the theorem follows. $\square$

“A person is Free if and only if they are an Innocent Human Being.” That is, under the full humanist framework, Freedom, Innocence, and Humanity are inextricably linked. Being an innocent human is the sole and sufficient condition for being a Free Sovereign.

To avoid this anarchistic, libertarian-individualist conclusion, historical legal and political theories that justify unilateral legislation by denying either the freedom or the equality of natural persons. Pre-18th-century thinkers, including Plato, Aristotle, and Hobbes, generally maintained that equality in natural law must be denied or sacrificed to ensure political survival. For instance, Aristotle argued that natural equality is non-existent, while Hobbes viewed the natural equality of an autonomous collective as a state of war that necessitates the institutionalization of inequality. These theories allow for a framework where only a select few are free while the majority remain subject to rule, compatible with the view that while natural persons may be human, not all humans are accorded equal status.

In later developments, medieval political theology and modern philosophy shifted toward affirming equality while simultaneously denying natural freedom. Medieval theology accepted the Postulate of Naturalist Humanism but positioned God as the supreme legislator, rendering all humans equal only in their shared subjection to divine law, thus stripping them of sovereignty. Modern theories, specifically those of Rousseau and Marx, secularized this approach by sanctifying equality but redefining freedom. By replacing the natural individual with abstract “aspect persons” such as the Citizen or Universal Man, these theories posit that individuals are free only to the extent that they control the collective. This results in systems (such as Types TT2, TT5, TT6, TT8, and TT11) where the denial of natural justice is a consequence of redefining the legal status of the individual.

Our formal theory successfully outlines natural law as an order of persons without relying on unscientific metaphysics. It demonstrates that the concept of natural law is logically independent of theology or empirical observation of physical data. However, while the formalization provides a rigorous description of the human condition under natural law, it requires a semantic scheme of interpretation to apply to the real world and does not, in itself, provide the ethical justification for why one ought to respect the law it describes.

Posted by at
Labels:

No comments:

Post a Comment

Subscribe to: Post Comments (Atom)