In this thesis, "Proof Theory of Semi-Substructural Logics", we introduce a class of weak logics and investigate their proof theory.

In classical logic, we are interested in the relationship between formulae as statements of truth. Given a set of true statements, we want to know which statements can be concluded from the set. Truths are freely available, they can be used as many times as needed, or not at all. In intuitionistic logic, truth requires evidence, but the reusability of true statements remains.

In substructural logics, e.g., linear logic, however, formulae function as resources rather than truths. An example is a vending machine: if a can of coke costs one euro, then providing one euro gets you exactly one can of coke, not two. If you insert two euros, you expect either two cokes, or one coke and one euro in change. The logic requires a perfect balance: the resources used must match the products received.

This thesis introduces and investigates logics where consequence is yet more restricted, which we call semi-substructural logics. These logics are for reasoning about resources for which not only the amount matters, but also the order of resources, and handling of the queue of resources can be very regulated. Typically, resources can be processed only at a special position at the front of the queue. In this case, the key substructural law of associativity only holds in one direction, as "semi-associativity", (A and B) and C can be turned into A and (B and C), but not vice versa.

The thesis “Proof Theory of Semi-Substructural Logics” is published in the Digital Collection of TalTech Library.

Supervisors: 

• Prof. Tarmo Uustalu (TalTech);
• co-supervisor: Prof. Niccolo Veltri (TalTech).

Opponents: 

• Prof. Pierre-Louis Curien, National Centre for Scientific Research (CNRS) and Université Paris Cité, France;
• Prof. Peter Dybjer, Chalmers University of Technology, Sweden.

Follow public defence in Zoom

Meeting ID: 955 5238 4468
Passcode: 769494