Syntax & semantics
Before going any further, let us first get the syntax and semantics out of the way. We use the standard syntax and Kripke semantics, so readers familiar with these can skip this section. This section is only used for later reference. The notation is based on the book Epistemic Logic for AI and Computer Science (van der Hoek and Ch. Meyer)
Propositional variables are p, q, ... ∈ Pr. Agent names are i, j, ... ∈ Ag. Formulas φ, ψ, ... are then given by the grammar
As usual the semantics is given by Kripke models. A Kripke model M=⟨S,R,V⟩ is a triple of states, accessibility relations (one for each agent) and a valuation function. The semantics of a formula in a particular modal and world, written as M,s ⊨ φ is defined as
We say that a formula is valid (notatation: ⊨ φ), when M,s ⊨ φ for all models M and all worlds s in that model.
Tableau proofs
Given any formula φ we would like to be able to show that either φ is true in all models, or that there is a model in which φ does not hold. In other words, whether ⊨φ or ⊭φ. This is impossible using just the semantics from the previous paragraph; instead we need a proof system. The proof system will give rules for the relation ⊢ φ. By showing that the system is sound and complete we know that ⊨ φ ⇔ ⊢ φ. And hence for all valid formulas there is a derivation in the system while for invalid formulas there is none. Because there is only a small number of rules we can exhaustively search for a proof starting from the conclusion (the formula we wish to proof).
As the abbreviation suggests MOLTAP is based on semantic tableaux. In the usual presentation of tablau reasoning to prove/disprove a formula φ you assume ¬φ, and write down all the consequences of that. If you reach a contradiction ¬φ can not be true, so φ must be true. If no contradiction is reached then ¬φ can be true, and hence φ is not always true.
In this paper we take a slightly different approach, which is closer to normal proof systems. In particular, we use a sequent calculus (also called a Gentzen system). See for instance the book Basic Proof Theory for an introduction (Troelstra and Schwichtenberg). A big advantage of sequent calculi is that the whole context of assumptions is always carried around. This means that all proof steps can be local, there are no references to other parts of the proof.
Usually sequents are written ‘two sided’, φ1,φ2 ⊢ ψ1,ψ2, which stands for (φ1 ∧ φ2) → (ψ2 ∨ ψ2). Following Burchardt et al we use signed formulas instead (Burchardt et al). This means we will write {φ1-,φ2-,ψ1+,ψ2+} for the equivalent formula ¬φ1 ∨ ¬φ2 ∨ ψ2 ∨ ψ2.
Definition A signed formula is either φ+ or φ-.
- + stands for a positive occurrence, a goal. Proving φ+ is equivalent to just proving φ.
- -, on the other hand, stands for a negative occurrence, an assumption. To proof φ- it must be shown that φ does not hold. The reason for calling this an “assumption” is explained below.
The semantics of signed formulas is therefore simple. We extend the ⊨ relation slightly:
Definition: A sequent is a finite set of these signed formulas. Semantically a sequent is a disjunction; it is true if one of the formulas in the set is true.
We will use Greek capital letters Γ,Δ,Ε for sequents. When there is no ambiguity we drop the braces around sequents, and we write Γ,φ± for Γ∪{φ±}.
The terminology of goal and assumption for positive and negative formulas comes from the implication operator. The formula φ → ψ can be read as “If φ then ψ” or “Assuming φ it holds that ψ”. Because a sequent is a disjunction the above formula could be written as {¬φ, ψ}. Or using signed formulas as {φ-, ψ+}.
The search for a proof always begins with a single goal, φ+. This goal forms a sequent, or in different terminology the contents of a tableau. Later on more things will be added to the sequent. For example if φ=ψ∨χ then the sequent can be extended to {ψ∨χ+, ψ+, χ+}.