Self-Formation and the Boundary of Free Will

Abstract

History-sensitive identity and autonomous action need not contradict functional determinism, while genuinely branching freedom does.

Theorem 1.1 (A total future is functional exactly when it does not branch).

$$\forall History\in \mathrm{Type},future\in History\to \mathrm{Set}\left(History\right),\left(\forall h\in History,\mathrm{Nonempty}\left(future\left(h\right)\right)\right)\Rightarrow \left(\mathrm{FunctionalFuture}\left(future\right)\iff \left(\neg \mathrm{BranchingFree}\left(future\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Agency/SelfFormationFreeWillBoundary.total_future_functional_iff_not_branching (✓ std3). ∎

Source. Repository-derived.

Commentary.

A total future relation assigns at least one successor to every history. If it is generated by a transition function, each successor set is a singleton and no genuine branch exists.

Conversely, totality selects a successor at each history. Absence of branching makes every other successor equal to the selected one, so the whole relation is the singleton graph of a function. Thus libertarian freedom understood as multiple real futures is incompatible with functional determinism in this model.

Theorem 1.2 (Self and agency are reductive exactly when no obstruction remains).

$$\forall History\in \mathrm{Type},Present\in \mathrm{Type},Identity\in \mathrm{Type},Action\in \mathrm{Type},Voluntariness\in \mathrm{Type},inhabited\in \mathrm{Nonempty}\left(History\right),present\in History\to Present,identity\in History\to Identity,action\in History\to Action,voluntariness\in History\to Voluntariness,future\in History\to \mathrm{Set}\left(History\right),\left(\forall h\in History,\mathrm{Nonempty}\left(future\left(h\right)\right)\right)\Rightarrow \left(\mathrm{ReductiveSelfAgency}\left(present,identity,action,voluntariness,future\right)\iff \left(\neg \mathrm{SelfAgencyObstruction}\left(present,identity,action,voluntariness,future\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Agency/SelfFormationFreeWillBoundary.reductive_self_agency_iff_no_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The reductive account has three clauses: identity factors through the current presentation, voluntariness factors through the observed action, and the future relation factors through one transition function.

Its exact obstruction is the disjunction of three witnesses: two histories look the same now but have different identities; two histories produce the same action but differ in voluntariness; or one history has two distinct possible futures. The theorem proves that the reductive account holds exactly when none occurs.

The first obstruction formalizes a history-constituted self: current presentation alone does not recover identity. It does not assert that any biological or phenomenological self satisfies the model.

Theorem 1.3 (History-sensitive self and deterministic autonomy coexist).

$$\exists present\in Bool\to Unit,identity\in Bool\to Bool,process\in Bool\to \left(Bool\to \mathrm{Set}\left(Bool\right)\right),step\in Bool\to Bool,\mathrm{MoralLuckWitness}\left(present,identity\right)\wedge \left(\left(\neg \mathrm{ControlPrinciple}\left(present,identity\right)\right)\wedge \left(\mathrm{AutonomousFree}\left(process\right)\wedge \left(\forall external\in Bool,history\in Bool,process\left(external,history\right)=\left\{step\left(history\right)\right\}\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Agency/SelfFormationFreeWillBoundary.history_sensitive_self_and_deterministic_autonomy_coexist (✓ std3). ∎

Source. Repository-derived.

Commentary.

A concrete Boolean history model has a constant current presentation but identity equal to the full history. Hence two histories can look identical now while retaining different identities, and identity cannot be reduced to current presentation.

Its transition process ignores the external input, so it is autonomous, yet each history has exactly its identity successor, so it is also functionally deterministic. This is a consistency witness for a compatibilist notion of freedom, not evidence that human action is in fact deterministic or free.

References

• Truth anchor: D5/S3/ConceptDynamics/Agency/SelfFormationFreeWillBoundary.history_sensitive_self_and_deterministic_autonomy_coexist
• Truth anchor: D5/S3/ConceptDynamics/Agency/SelfFormationFreeWillBoundary.reductive_self_agency_iff_no_obstruction
• Truth anchor: D5/S3/ConceptDynamics/Agency/SelfFormationFreeWillBoundary.total_future_functional_iff_not_branching
• Dependency: D5/S0/Rewriting/Quotients/AnswerabilityCriterion
• Dependency: D5/S3/ConceptDynamics/Fibers/BranchingFreedomNeedsRelation
• Dependency: D5/S3/ConceptDynamics/MoralLuck/MoralLuckDescent