Reasoning about Unreliable Actions

TL;DR

This paper develops a logical framework for reasoning about unreliable actions, integrating semantics, sequent calculus, and fibrations to handle partial equations and action outcomes.

Contribution

It introduces a strongly typed logic with a novel semantics based on fibrations, and proves cut elimination for reasoning about actions with unreliable outcomes.

Findings

Sequent calculus with cut elimination for the logic

Semantics based on fibrations over partial cartesian categories

Conditions for the existence of lax comma objects

Abstract

We analyse the philosopher Davidson's semantics of actions, using a strongly typed logic with contexts given by sets of partial equations between the outcomes of actions. This provides a perspicuous and elegant treatment of reasoning about action, analogous to Reiter's work on artificial intelligence. We define a sequent calculus for this logic, prove cut elimination, and give a semantics based on fibrations over partial cartesian categories: we give a structure theory for such fibrations. The existence of lax comma objects is necessary for the proof of cut elimination, and we give conditions on the domain fibration of a partial cartesian category for such comma objects to exist.