Agentive logic, also called the logic of action or logic of agency, is a branch of philosophical logic and logic in computer science that studies formal representations of agents, their actions, and their abilities. In its narrower sense, an agentive logic is a formal system whose primitive operators express that an agent does something, can do something, or sees to it that something is the case. These logics generalize modal logic by adding modalities indexed to agents and actions, allowing precise reasoning about what agents can achieve, how their choices interact, and what they bring about.
The field has roots in medieval philosophy and modern logic, and it has become central to areas such as artificial intelligence, program verification, and the semantics of natural language. Agentive logics provide a rigorous framework for modeling intelligent agents, planning systems, and multi-agent interactions, making them essential for both theoretical and applied work in computing.
Terminology and scope
The adjective "agentive" derives from the Latin agens ("one who acts") and originally referred to the grammatical agent of a verb. In logical contexts, it designates operators or predicates whose primary argument position is an agent rather than a proposition alone, for example \(A_i\varphi\) ("agent \(i\) does \(\varphi\)") or \(C_i\varphi\) ("agent \(i\) can bring about \(\varphi\)").
In contemporary literature, agentive logic is sometimes used narrowly for formal reconstructions of St. Anselm's modal account of facere ("to do"). More broadly, the term is used interchangeably with logic of action or logic of agency to cover a family of modal and dynamic logics designed to capture the structure of action and choice. This broader usage encompasses systems developed in philosophy, linguistics, and computer science, all sharing a focus on agents as explicit elements of logical form.
Historical background
Medieval and early modern roots
Medieval logicians already explored analogies between modalities of action and alethic modalities such as possibility and necessity, particularly in discussions of obligation and power. An influential early agentive analysis is due to St. Anselm (11th century), who treated "doing \(\varphi\)" as a kind of modal operator on propositions, anticipating later modal logics of agency. Modern reconstructions of Anselm's theory show that the resulting agentive logic can be modeled with neighborhood semantics and satisfies a recognizable square of opposition.
Modern logic of action
Modern study of the logic of action began in the mid-20th century, parallel to developments in deontic logic and tense logic. Early systems were proposed by Georg Henrik von Wright, Stig Kanger, and others, often motivated by questions about norms and responsibility. From the 1960s onward, two largely independent but eventually converging traditions emerged: a branching-time tradition culminating in STIT logics, emphasizing agents' choices among possible futures, and dynamic logics of programs and actions, developed within computer science to reason about program execution.
In the 1990s and 2000s, action logics were further developed in connection with knowledge representation, planning, and multi-agent systems in AI, and with dynamic and update semantics in linguistics. These developments integrated insights from philosophy, theoretical computer science, and AI, creating a rich interdisciplinary field.
Core ideas
Despite their diversity, most agentive logics share several general themes. Agents are treated as explicit indices of modal operators, as in \([i\ {\sf does}]\varphi\) or \(C_i\varphi\). Actions are represented either implicitly, via changes between possible worlds along an accessibility relation, or explicitly, as terms denoting primitive and composite actions. Choice and ability are captured by modalities describing what an agent can ensure, usually relative to assumptions about the environment and other agents.
Formal properties such as closure under composition, interaction between different agents, and connections to obligation (what an agent ought to do) and knowledge (what an agent knows how to do) are investigated. These core ideas provide a common framework for comparing different systems and for applying them to practical problems.
STIT logics
STIT ("sees to it that") logics, originating in work by Nuel Belnap and collaborators, treat agency in a branching-time framework. A STIT model consists of a partially ordered set of moments with a tree-like structure, sets of histories (maximal branches through the tree), and for each agent at each moment, a partition of the histories through that moment representing the choices available to the agent.
Intuitively, an agent's action at a moment determines which equivalence class (choice cell) of histories becomes actual; a formula \([i\ {\sf stit}:\varphi]\) is true at a history-moment pair if \(\varphi\) holds on all histories in the choice cell corresponding to the agent's current action. Different STIT operators have been distinguished, notably the Chellas STIT operator, often written \([i\ {\sf cstit}:\varphi]\), and the deliberative STIT operator, which adds the condition that the agent's choice makes a difference to the truth of \(\varphi\). These operators allow precise reasoning about individual and joint agency, including cases where agents act together or where one agent's action precludes another's.
STIT logics have been applied to deontic reasoning, game theory, and the analysis of responsibility and causation. They provide a robust framework for modeling choice and ability in dynamic environments, and they have influenced work on multi-agent systems in AI.
Dynamic logics of action
Dynamic logics, developed in computer science from the 1970s onward, represent actions as programs with modalities \([\alpha]\varphi\) and \(\langle\alpha\rangle\varphi\), meaning roughly that after every (respectively, some) execution(s) of action \(\alpha\), \(\varphi\) holds. These logics were originally designed for program verification, allowing reasoning about the effects of program execution on states.
In agentive contexts, dynamic logics are used to model actions explicitly as terms, with composition, choice, and iteration operators. This allows representation of complex action structures, such as sequences of actions, conditional actions, and repeated actions. Dynamic logics of action have been applied to planning, robotics, and the semantics of natural language, where they capture the meaning of action sentences and imperatives.
Applications in artificial intelligence
Agentive logics underpin formalisms for reasoning about actions, planning, and intelligent agents in artificial intelligence. They provide a formal basis for representing an agent's knowledge, abilities, and goals, and for reasoning about how actions change the world. In planning, agentive logics help specify preconditions and effects of actions, and they support reasoning about alternative plans and their outcomes.
In multi-agent systems, agentive logics model interactions between agents, including cooperation, competition, and communication. They are used to specify protocols, verify properties of distributed systems, and analyze strategic behavior. The development of large language models and other machine learning systems has also drawn on agentive concepts, as researchers seek to build agents that can reason about their own actions and those of others.
Relationship to other logics
Agentive logics are closely related to modal logics, deontic logics, and temporal logics. They extend modal logic by adding agent-indexed modalities, and they often incorporate temporal operators to represent change over time. Deontic logics, which reason about obligation and permission, can be combined with agentive logics to express what an agent ought to do or is permitted to do. Temporal logics, such as linear temporal logic and computation tree logic, provide a basis for reasoning about sequences of actions and branching futures.
The connections between agentive logics and knowledge are also important. Epistemic logics, which reason about what agents know, can be integrated with agentive logics to express what an agent knows how to do or knows that it can achieve. This integration is crucial for applications in AI, where agents must reason about their own knowledge and abilities.
See also
- Modal logic
- Deontic logic
- Temporal logic
- Multi-agent system