Abstract

Psychotherapy lacks agreed formal foundations. Competing theoretical schools produce measurable clinical outcomes without consensus on the formal structure of psychological change, and without such foundations the discipline cannot adjudicate between theoretical claims at any level deeper than empirical outcome comparison, distinguish genuine structural change from symptomatic management, or explain why approaches with incompatible ontological commitments sometimes yield equivalent results. Modal logic is proposed here as providing those foundations in the model-theoretic sense articulated by Suppes (1967): not as a reducing theory that would dissolve the clinical level into formal axioms, but as a specification of the abstract structures that psychotherapy’s theoretical dimension instantiates, sufficient for internal coherence and systematic development without entailing completeness or uniqueness. The modal system governing practical psychological modality is derived on substantive grounds, establishing that the system is KD, with seriality holding globally and reflexivity, transitivity, symmetry, and the Euclidean property each failing globally while admissible locally. Local reflexivity is grounded in a formally defined atomic proposition s recording whether a configuration is self-sustaining through its operative mechanism, which unifies the otherwise heterogeneous cases of therapeutically consolidated and pathologically entrenched configurations under a single formal criterion. Two formal models are developed, of agoraphobic constriction under cognitive-behavioural exposure treatment and of obsessional neurosis under psychoanalytic working-through, with four propositions stated and proved, including results on formal inaccessibility of therapeutic goals from initial configurations and on minimum path lengths that formally ground the structural necessity of graduated intermediate work. A formal adequacy class for KD-frames of practical psychological modality is explicitly defined. Therapeutic transitions are characterised as link-addition operations in the graph-transformer framework of van Benthem (2011), with precondition structures enforcing the non-transitivity of the accessibility relation at the level of programme executability. The structural parallel with deontic KD is shown to be substantively informative without transferring the known paradoxes of deontic logic, which are artifacts of the normative rather than the descriptive practical interpretation.