Historical/temporal necessities/possibilities, and a logical theory of them in branching time

TL;DR

This paper introduces a logical framework for understanding six notions of necessity and possibility related to time flow, based on branching time models and agent-specific ontic rules, with formal axiomatic foundations.

Contribution

It defines and formalizes six temporal notions of necessity and possibility within a branching time logic, incorporating agent rules and providing soundness and completeness proofs.

Findings

Six notions of necessity and possibility are characterized in branching time.

A logical system with six operators is developed and axiomatized.

The axiomatic system is proven sound and complete.

Abstract

In this paper, we do three kinds of work. First, we recognize four notions of necessity and two notions of possibility related to time flow, namely strong/weak historical/temporal necessities, as well as historical/temporal possibilities, which are motivated more from a linguistic perspective than from a philosophical one. Strong/weak historical necessities and historical possibility typically concern the possible futures of the present world, and strong/weak temporal necessities and temporal possibility concern possible timelines of alternatives of the present world. Second, we provide our approach to the six notions and present a logical theory of them in branching time. Our approach to the six notions is as follows. The agent has a system of ontic rules that determine expected timelines. She treats some ontic rules as undefeatable, determining accepted timelines. The domains of strong/weak historical necessities, respectively, consist of accepted and expected timelines passing through the present moment, and historical possibility is the dual of strong historical necessity. The domains of strong/weak temporal necessities, respectively, consist of accepted and expected timelines, and temporal possibility is the dual of strong temporal necessity. The logical theory has six operators: a last-moment operator, a next-moment operator, and four operators for the four notions of necessity. Formulas' evaluation contexts consist of a tree-like model representing a time flow, a context representing the agent's system of ontic rules, a timeline, and an instant. Third, we offer an axiomatic system for the logical theory and show its soundness and completeness.