Modal Tableaux

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Editorial

Draft chapter on prefixed tableaux for modal logic. Needs more examples, completeness proofs, and discussion of how one can find countermodels from unsuccessful searches for closed tableaux.

Introduction

Tableaux are certain (downward-branching) trees of signed formulas, i.e., pairs consisting of a truth value sign ( $\True$ source or $\False$ source) and a sentence

\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.

source

A tableau begins with a number of assumptions. Each further signed formula is generated by applying one of the inference rules. Some inference rules add one or more signed formulas to a tip of the tree; others add two new tips, resulting in two branches. Rules result in signed formulas where the formula is less complex than that of the signed formula to which it was applied. When a branch contains both $\sFmla{\True}{!A}$ source and $\sFmla{\False}{!A}$ source, we say the branch is closed. If every branch in a tableau is closed, the entire tableau is closed. A closed tableau constitutes a derivation that shows that the set of signed formulas which were used to begin the tableau are unsatisfiable. This can be used to define a $\Proves$ source relation: $\Gamma \Proves !A$ source iff there is some finite set $\Gamma_0 = \{!B_1, \dots, !B_n\} \subseteq \Gamma$ source such that there is a closed tableau for the assumptions

\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.

source

For modal logics, we have to both extend the notion of signed formula and add rules that cover $\Box$ source and $\Diamond$ source . In addition to a sign( $\True$ source or $\False$ source), formulas in modal tableaux also have prefixes $\sigma$ source. The prefixes are non-empty sequences of positive integers, i.e., $\sigma \in (\PosInt)^* \setminus \{\emptyseq\}$ source. When we write such prefixes without the surrounding $\tuple{\ }$ source, and separate the individual elements by $.$ source's instead of $,$ source's. If $\sigma$ source is a prefix, then $\sigma.n$ source is $\sigma \concat \tuple{n}$ source; e.g., if $\sigma = 1.2.1$ source, then $\sigma.3$ source is $1.2.1.3$ source. So for instance,

\sFmla{\True}{\Box !A \lif !A}[1.2]

source

is a prefixed signed formula (or just a prefixed formula for short).

Intuitively, the prefix names a world in a model that might satisfy the formulas on a branch of a tableau, and if $\sigma$ source names some world, then $\sigma.n$ source names a world accessible from (the world named by) $\sigma$ source.

Rules for AxK

The rules for the regular propositional connectives are the same as for regular propositional signed tableaux, just with prefixes added. In each case, the rule applied to a signed formula $\sFmla{S}{!A}[\sigma]$ source produces new formulas that are also prefixed by $\sigma$ source. This should be intuitively clear: e.g., if $!A \land !B$ source is true at (a world named by) $\sigma$ source, then $!A$ source and $!B$ source are true at $\sigma$ source (and not at any other world). We collect the propositional rules in the propositional prefixed-tableau rule table.

Propositional prefixed-tableau rule table

Propositional prefixed-tableau rule table. Propositional prefixed tableau rules. Row one, true negation: from true not A at prefix sigma, infer false A at prefix sigma. False negation: from false not A at prefix sigma, infer true A at prefix sigma. Row two, true conjunction: from true A and B at prefix sigma, stack true A and true B at that prefix. False conjunction: from false A and B at prefix sigma, branch to false A or false B at that prefix. Row three, true disjunction: from true A or B at prefix sigma, branch to true A or true B at that prefix. False disjunction: from false A or B at prefix sigma, stack false A and false B at that prefix. Row four, true conditional: from true if A then B at prefix sigma, branch to false A or true B at that prefix. False conditional: from false if A then B at prefix sigma, stack true A and false B at that prefix. End propositional rule table. End table.

\def\arraystretch{3}\begin{array}{|c|c|} \hline \AxiomC{\sFmla{\True}{\lnot !A}[\sigma]} \RightLabel{\TRule{\True}{\lnot}} \UnaryInfC{\sFmla{\False}{!A}[\sigma]} \DisplayProof & \AxiomC{\sFmla{\False}{\lnot !A}[\sigma]} \RightLabel{\TRule{\False}{\lnot}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \DisplayProof \\[1ex] \hline \AxiomC{\sFmla{\True}{!A \land !B}[\sigma]} \RightLabel{\TRule{\True}{\land}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\True}{!B}[\sigma]} \DisplayProof & \AxiomC{\sFmla{\False}{!A \land !B}[\sigma]} \RightLabel{\TRule{\False}{\land}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad \sFmla{\False}{!B}[\sigma]$} \DisplayProof \\[2ex] \hline \AxiomC{\sFmla{\True}{!A \lor !B}[\sigma]} \RightLabel{\TRule{\True}{\lor}} \UnaryInfC{$\sFmla{\True}{!A}[\sigma] \quad \mid \quad \sFmla{\True}{!B}[\sigma]$} \DisplayProof & \AxiomC{\sFmla{\False}{!A \lor !B}[\sigma]} \RightLabel{\TRule{\False}{\lor}} \UnaryInfC{\sFmla{\False}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma]} \DisplayProof \\[2ex] \hline \AxiomC{\sFmla{\True}{!A \lif !B}[\sigma]} \RightLabel{\TRule{\True}{\lif}} \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad \sFmla{\True}{!B}[\sigma]$} \DisplayProof & \AxiomC{\sFmla{\False}{!A \lif !B}[\sigma]} \RightLabel{\TRule{\False}{\lif}} \UnaryInfC{\sFmla{\True}{!A}[\sigma]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma]} \DisplayProof \\[2ex] \hline \end{array}

source

Propositional prefixed-tableau rule table
True-sign rule	False-sign rule
True-negation tableau rule From true not A at prefix sigma, infer false A at prefix sigma. Step 1. No premises. Rule: premise. true not formula A at prefix sigma Step 2. Depends on step 1. Rule: true negation rule. false formula A at prefix sigma	False-negation tableau rule From false not A at prefix sigma, infer true A at prefix sigma. Step 1. No premises. Rule: premise. false not formula A at prefix sigma Step 2. Depends on step 1. Rule: false negation rule. true formula A at prefix sigma
True-conjunction tableau rule From true A and B at prefix sigma, stack true A and true B at the same prefix. Step 1. No premises. Rule: premise. true the conjunction of formula A and formula B at prefix sigma Step 2. Depends on step 1. Rule: true conjunction rule. true formula A at prefix sigma Step 3. Depends on step 1. Rule: true conjunction rule. true formula B at prefix sigma	False-conjunction tableau rule From false A and B at prefix sigma, branch to false A or false B at the same prefix. Step 1. No premises. Rule: premise. false the conjunction of formula A and formula B at prefix sigma Step 2. Depends on step 1. Rule: false conjunction rule. false formula A at prefix sigma or false formula B at prefix sigma
True-disjunction tableau rule From true A or B at prefix sigma, branch to true A or true B at the same prefix. Step 1. No premises. Rule: premise. true the disjunction of formula A and formula B at prefix sigma Step 2. Depends on step 1. Rule: true disjunction rule. true formula A at prefix sigma or true formula B at prefix sigma	False-disjunction tableau rule From false A or B at prefix sigma, stack false A and false B at the same prefix. Step 1. No premises. Rule: premise. false the disjunction of formula A and formula B at prefix sigma Step 2. Depends on step 1. Rule: false disjunction rule. false formula A at prefix sigma Step 3. Depends on step 1. Rule: false disjunction rule. false formula B at prefix sigma
True-conditional tableau rule From true if A then B at prefix sigma, branch to false A or true B at the same prefix. Step 1. No premises. Rule: premise. true the conditional from formula A to formula B at prefix sigma Step 2. Depends on step 1. Rule: true conditional rule. false formula A at prefix sigma or true formula B at prefix sigma	False-conditional tableau rule From false if A then B at prefix sigma, stack true A and false B at the same prefix. Step 1. No premises. Rule: premise. false the conditional from formula A to formula B at prefix sigma Step 2. Depends on step 1. Rule: false conditional rule. true formula A at prefix sigma Step 3. Depends on step 1. Rule: false conditional rule. false formula B at prefix sigma

source 22

The closure condition is the same as for ordinary tableaux, although we require that not just the formulas but also the prefixes must match. So a branch is closed if it contains both

\sFmla{\True}{!A}[\sigma] \quad\text{and}\quad \sFmla{\False}{!A}[\sigma]

source

for some prefix $\sigma$ source and formula $!A$ source.

The rules for setting up assumptions is also as for ordinary tableaux, except that for assumptions we always use the prefix $1$ source. (It does not matter which prefix we use, as long as it's the same for all assumptions.) So, e.g., we say that

!B_1, \dots, !B_n \Proves !A

source

iff there is a closed tableau for the assumptions

\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1].

source

For the modal operator s $\Box$ source and $\Diamond$ source , the prefix of the conclusion of the rule applied to a formula with prefix $\sigma$ source is $\sigma.n$ source. However, which $n$ source is allowed depends on whether the sign is $\True$ source or $\False$ source.

The $\TRule{\True}{\Box}$ source rule extends a branch containing $\sFmla{\True}{\Box !A}[\sigma]$ source by $\sFmla{\True}{!A}[\sigma.n]$ source. Similarly, t he $\TRule{\False}{\Diamond}$ source rule extends a branch containing $\sFmla{\False}{\Diamond !A}[\sigma]$ source by $\sFmla{\False}{!A}[\sigma.n]$ source. They can only be applied for a prefix $\sigma.n$ source which already occurs on the branch in which it is applied. Let's call such a prefix “used” (on the branch).

The $\TRule{\False}{\Box}$ source rule extends a branch containing $\sFmla{\False}{\Box !A}[\sigma]$ source by $\sFmla{\False}{!A}[\sigma.n]$ source. Similarly, t he $\TRule{\True}{\Diamond}$ source rule extends a branch containing $\sFmla{\True}{\Diamond !A}[\sigma]$ source by $\sFmla{\True}{!A}[\sigma.n]$ source. These rules , however, can only be applied for a prefix $\sigma.n$ source which does not already occur on the branch in which it is applied. We call such prefixes “new” (to the branch).

The rules are given in the four modal K tableau rules.

Outer table for the four modal K rules

defarraystretch3deffCenter

Four modal K tableau rules

Four modal K rules. Headers: true-sign rule; false-sign rule. Row one, necessity. Premise true necessarily formula A at prefix sigma. Rule true necessity rule. Conclusion true formula A at prefix sigma dot n. Premise false necessarily formula A at prefix sigma. Rule false necessity rule. Conclusion false formula A at prefix sigma dot n. Side conditions: prefix sigma dot n; prefix sigma dot n. Row two, possibility. Premise true possibly formula A at prefix sigma. Rule true possibility rule. Conclusion true formula A at prefix sigma dot n. Premise false possibly formula A at prefix sigma. Rule false possibility rule. Conclusion false formula A at prefix sigma dot n. Side conditions: prefix sigma dot n; prefix sigma dot n. End modal K rule table.

Four modal K tableau rules
True-sign rule	False-sign rule
True-necessity used-prefix rule Proof diagram. Premise true necessarily formula A at prefix sigma. Rule true necessity rule. Conclusion true formula A at prefix sigma dot n. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[\sigma]$ source Step 2. Depends on step 1. Rule: true necessity rule. $\sFmla{\True}{!A}[\sigma.n]$ source $\sigma.n$ source	False-necessity new-prefix rule Proof diagram. Premise false necessarily formula A at prefix sigma. Rule false necessity rule. Conclusion false formula A at prefix sigma dot n. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Box !A}[\sigma]$ source Step 2. Depends on step 1. Rule: false necessity rule. $\sFmla{\False}{!A}[\sigma.n]$ source $\sigma.n$ source
True-possibility new-prefix rule Proof diagram. Premise true possibly formula A at prefix sigma. Rule true possibility rule. Conclusion true formula A at prefix sigma dot n. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Diamond !A}[\sigma]$ source Step 2. Depends on step 1. Rule: true possibility rule. $\sFmla{\True}{!A}[\sigma.n]$ source $\sigma.n$ source	False-possibility used-prefix rule Proof diagram. Premise false possibly formula A at prefix sigma. Rule false possibility rule. Conclusion false formula A at prefix sigma dot n. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[\sigma]$ source Step 2. Depends on step 1. Rule: false possibility rule. $\sFmla{\False}{!A}[\sigma.n]$ source $\sigma.n$ source

\TRule{\True}{\Box}

source

\TRule{\False}{\Box}

source

\TRule{\True}{\Diamond}

source

\TRule{\False}{\Diamond}

source

source 137

captionThe modal rules for AxK.

The requirement that the restriction that the prefix for $\TRule{\True}{\Box}$ source must be used is necessary as otherwise we would count the following as a closed tableau:

Closed necessity-versus-possibility tableau

Closed necessity-versus-possibility tableau. Node one: true necessarily formula A at prefix one. Rule: tableau assumption. Node two: false possibly formula A at prefix one. Rule: tableau assumption. Node three: true formula A at prefix one point one. Rule: true necessity rule, depending on node one. Node four: false formula A at prefix one point one. Rule: false possibility rule, depending on node two; source close marker present. Branch one is closed, closed by nodes three and four. End tableau.

Node 1. $\sFmla{\True}{\Box \formula{A}}[1]$ source Rule: tableau assumption. Parents: none.
Node 2. $\sFmla{\False}{\Diamond \formula{A}}[1]$ source Rule: tableau assumption. Parents: projected-env-003854-node-1.
Node 3. $\sFmla{\True}{\formula{A}}[1.1]$ source Rule: true necessity rule. Parents: projected-env-003854-node-2.
Node 4. $\sFmla{\False}{\formula{A}}[1.1]$ source Rule: false possibility rule. Parents: projected-env-003854-node-3. Markers: closed marker.

closed branch; nodes projected-env-003854-node-1, projected-env-003854-node-2, projected-env-003854-node-3, projected-env-003854-node-4; closure witnesses projected-env-003854-node-3, projected-env-003854-node-4.

source 211

But $\Box \formula{A} \Entails/ \Diamond \formula{A}$ source, so our proof system would be unsound. Likewise, $\Diamond \formula{A} \Entails/ \Box \formula{A}$ source, but without the restriction that the prefix for $\TRule{\False}{\Box}$ source must be new, this would be a closed tableau:

Closed possibility-versus-necessity tableau

Closed possibility-versus-necessity tableau. Node one: true possibly formula A at prefix one. Rule: tableau assumption. Node two: false necessarily formula A at prefix one. Rule: tableau assumption. Node three: true formula A at prefix one point one. Rule: true possibility rule, depending on node one. Node four: false formula A at prefix one point one. Rule: false necessity rule, depending on node two; source close marker present. Branch one is closed, closed by nodes three and four. End tableau.

Node 1. $\sFmla{\True}{\Diamond \formula{A}}[1]$ source Rule: tableau assumption. Parents: none.
Node 2. $\sFmla{\False}{\Box \formula{A}}[1]$ source Rule: tableau assumption. Parents: projected-env-003855-node-1.
Node 3. $\sFmla{\True}{\formula{A}}[1.1]$ source Rule: true possibility rule. Parents: projected-env-003855-node-2.
Node 4. $\sFmla{\False}{\formula{A}}[1.1]$ source Rule: false necessity rule. Parents: projected-env-003855-node-3. Markers: closed marker.

closed branch; nodes projected-env-003855-node-1, projected-env-003855-node-2, projected-env-003855-node-3, projected-env-003855-node-4; closure witnesses projected-env-003855-node-3, projected-env-003855-node-4.

source 262

tableau for LogK

Closed tableau for distributing necessity over conjunction

We give a closed tableau that shows $\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$ source.

Tableau for necessity and conjunction

Tableau for necessity and conjunction. Node one: false the conditional from the conjunction of necessarily formula A and necessarily formula B to necessarily the conjunction of formula A and formula B at prefix one. Rule: tableau assumption. Node two: true the conjunction of necessarily formula A and necessarily formula B at prefix one. Rule: false conditional rule, depending on node one. Node three: false necessarily the conjunction of formula A and formula B at prefix one. Rule: false conditional rule, depending on node one. Node four: true necessarily formula A at prefix one. Rule: true conjunction rule, depending on node two. Node five: true necessarily formula B at prefix one. Rule: true conjunction rule, depending on node two. Node six: false the conjunction of formula A and formula B at prefix one point one. Rule: false necessity rule, depending on node three. Node seven: false formula A at prefix one point one. Rule: false conjunction rule, depending on node six. Node eight: true formula A at prefix one point one. Rule: true necessity rule, depending on node four; source close marker present. Node nine: false formula B at prefix one point one. Rule: false conjunction rule, depending on node six. Node one zero: true formula B at prefix one point one. Rule: true necessity rule, depending on node five; source close marker present. Branch one is closed, closed by nodes seven and eight. Branch two is closed, closed by nodes nine and one zero. End tableau.

Node 1. $\sFmla{\False}{(\Box\formula{A} \land \Box\formula{B}) \lif \Box (\formula{A} \land \formula{B})}[1]$ source Rule: tableau assumption. Parents: none.
Node 2. $\sFmla{\True}{\Box\formula{A} \land \Box\formula{B}}[1]$ source Rule: false conditional rule. Parents: projected-env-003856-node-1.
Node 3. $\sFmla{\False}{\Box(\formula{A} \land \formula{B})}[1]$ source Rule: false conditional rule. Parents: projected-env-003856-node-2.
Node 4. $\sFmla{\True}{\Box\formula{A}}[1]$ source Rule: true conjunction rule. Parents: projected-env-003856-node-3.
Node 5. $\sFmla{\True}{\Box\formula{B}}[1]$ source Rule: true conjunction rule. Parents: projected-env-003856-node-4.
Node 6. $\sFmla{\False}{\formula{A} \land \formula{B}}[1.1]$ source Rule: false necessity rule. Parents: projected-env-003856-node-5.
Node 7. $\sFmla{\False}{\formula{A}}[1.1]$ source Rule: false conjunction rule. Parents: projected-env-003856-node-6.
Node 8. $\sFmla{\True}{\formula{A}}[1.1]$ source Rule: true necessity rule. Parents: projected-env-003856-node-7. Markers: closed marker.
Node 9. $\sFmla{\False}{\formula{B}}[1.1]$ source Rule: false conjunction rule. Parents: projected-env-003856-node-6.
Node 10. $\sFmla{\True}{\formula{B}}[1.1]$ source Rule: true necessity rule. Parents: projected-env-003856-node-9. Markers: closed marker.

closed branch; nodes projected-env-003856-node-1, projected-env-003856-node-2, projected-env-003856-node-3, projected-env-003856-node-4, projected-env-003856-node-5, projected-env-003856-node-6, projected-env-003856-node-7, projected-env-003856-node-8; closure witnesses projected-env-003856-node-7, projected-env-003856-node-8.
closed branch; nodes projected-env-003856-node-1, projected-env-003856-node-2, projected-env-003856-node-3, projected-env-003856-node-4, projected-env-003856-node-5, projected-env-003856-node-6, projected-env-003856-node-9, projected-env-003856-node-10; closure witnesses projected-env-003856-node-9, projected-env-003856-node-10.

source 18

Closed tableau for distributing possibility over disjunction

We give a closed tableau that shows $\Proves \Diamond(!A \lor !B) \lif (\Diamond !A \lor \Diamond !B)$ source:

Tableau for possibility and disjunction

Tableau for possibility and disjunction. Node one: false the conditional from possibly the disjunction of formula A and formula B to the disjunction of possibly formula A and possibly formula B at prefix one. Rule: tableau assumption. Node two: true possibly the disjunction of formula A and formula B at prefix one. Rule: false conditional rule, depending on node one. Node three: false the disjunction of possibly formula A and possibly formula B at prefix one. Rule: false conditional rule, depending on node one. Node four: false possibly formula A at prefix one. Rule: false disjunction rule, depending on node three. Node five: false possibly formula B at prefix one. Rule: false disjunction rule, depending on node three. Node six: true the disjunction of formula A and formula B at prefix one point one. Rule: true possibility rule, depending on node two. Node seven: true formula A at prefix one point one. Rule: true disjunction rule, depending on node six. Node eight: false formula A at prefix one point one. Rule: false possibility rule, depending on node four; source close marker present. Node nine: true formula B at prefix one point one. Rule: true disjunction rule, depending on node six. Node one zero: false formula B at prefix one point one. Rule: false possibility rule, depending on node five; source close marker present. Branch one is closed, closed by nodes seven and eight. Branch two is closed, closed by nodes nine and one zero. End tableau.

Node 1. $\sFmla{\False}{\Diamond(\formula{A} \lor \formula{B}) \lif (\Diamond \formula{A} \lor \Diamond \formula{B})}[1]$ source Rule: tableau assumption. Parents: none.
Node 2. $\sFmla{\True}{\Diamond(\formula{A} \lor \formula{B})}[1]$ source Rule: false conditional rule. Parents: projected-env-003858-node-1.
Node 3. $\sFmla{\False}{\Diamond\formula{A} \lor \Diamond\formula{B}}[1]$ source Rule: false conditional rule. Parents: projected-env-003858-node-2.
Node 4. $\sFmla{\False}{\Diamond\formula{A}}[1]$ source Rule: false disjunction rule. Parents: projected-env-003858-node-3.
Node 5. $\sFmla{\False}{\Diamond\formula{B}}[1]$ source Rule: false disjunction rule. Parents: projected-env-003858-node-4.
Node 6. $\sFmla{\True}{\formula{A} \lor \formula{B}}[1.1]$ source Rule: true possibility rule. Parents: projected-env-003858-node-5.
Node 7. $\sFmla{\True}{\formula{A}}[1.1]$ source Rule: true disjunction rule. Parents: projected-env-003858-node-6.
Node 8. $\sFmla{\False}{\formula{A}}[1.1]$ source Rule: false possibility rule. Parents: projected-env-003858-node-7. Markers: closed marker.
Node 9. $\sFmla{\True}{\formula{B}}[1.1]$ source Rule: true disjunction rule. Parents: projected-env-003858-node-6.
Node 10. $\sFmla{\False}{\formula{B}}[1.1]$ source Rule: false possibility rule. Parents: projected-env-003858-node-9. Markers: closed marker.

closed branch; nodes projected-env-003858-node-1, projected-env-003858-node-2, projected-env-003858-node-3, projected-env-003858-node-4, projected-env-003858-node-5, projected-env-003858-node-6, projected-env-003858-node-7, projected-env-003858-node-8; closure witnesses projected-env-003858-node-7, projected-env-003858-node-8.
closed branch; nodes projected-env-003858-node-1, projected-env-003858-node-2, projected-env-003858-node-3, projected-env-003858-node-4, projected-env-003858-node-5, projected-env-003858-node-6, projected-env-003858-node-9, projected-env-003858-node-10; closure witnesses projected-env-003858-node-9, projected-env-003858-node-10.

source 54

Exercise constructing four closed K tableaux

Find closed tableaux in $\Log{K}$ source for the following formulas:

$\Box \lnot p \lif \Box(p \lif q)$ source
$(\Box p \lor \Box q) \lif \Box(p \lor q)$ source
$\Diamond p \lif \Diamond(p \lor q)$ source
$\Box(p \land q) \lif \Box p$ source

Soundness for LogK

Editorial

This soundness proof reuses the soundness proof for classical propositional logic, i.e., it proves everything from scratch. That's ok if you want a self-contained soundness proof. If you already have seen soundness for ordinary tableau this will be repetitive. It's planned to make it possible to switch between self-contained version and a version building on the non-modal case.

Explain

In order to show that prefixed tableaux are sound, we have to show that if

\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1]

source

has a closed tableau then $!B_1, \dots, !B_n \Entails !A$ source. It is easier to prove the contrapositive: if for some $\mModel{M}$ source and world $w$ source, $\mSat{M}{!B_i}[w]$ source for all $i=1$ source, dots, $n$ source but $\mSat{M}{!A}[w]$ source, then no tableau can close. Such a countermodel shows that the initial assumptions of the tableau are satisfiable. The strategy of the proof is to show that whenever all the prefixed formulas on a tableau branch are satisfiable, any application of a rule results in at least one extended branch that is also satisfiable. Since closed branches are unsatisfiable, any tableau for a satisfiable set of prefixed formulas must have at least one open branch.

In order to apply this strategy in the modal case, we have to extend our definition of “satisfiable” to modal modals and prefixes. With that in hand, however, the proof is straightforward.

Interpretation of tableau prefixes in a model

Let $P$ source be some set of prefixes, i.e., $P \subseteq (\PosInt)^* \setminus \{\emptyseq\}$ source and let $\mModel{M}$ source be a model. A function $f\colon P \to W$ source is an interpretation of $P$ source in $\mModel{M}$ source if, whenever $\sigma$ source and $\sigma.n$ source are both in $P$ source, then $Rf(\sigma)f(\sigma.n)$ source.

Relative to an interpretation of prefixes $P$ source we can define:

$\mModel{M}$ source satisfies $\sFmla{\True}{!A}[\sigma]$ source iff $\mSat{M}{!A}[f(\sigma)]$ source.
$\mModel{M}$ source satisfies $\sFmla{\False}{!A}[\sigma]$ source iff $\mSat/{M}{!A}[f(\sigma)]$ source.

Satisfaction and satisfiability of a prefixed set

Let $\Gamma$ source be a set of prefixed formulas, and let $P(\Gamma)$ source be the set of prefixes that occur in it. If $f$ source is an interpretation of $P(\Gamma)$ source in $\mModel{M}$ source, we say that $\mModel{M}$ source satisfies $\Gamma$ source with respect to $f$ source, $\mSat{M}{\Gamma}[f]$ source, if $\mModel{M}$ source satisfies every prefixed formula in $\Gamma$ source with respect to $f$ source. $\Gamma$ source is satisfiable iff there is a model $\mModel{M}$ source and interpretation $f$ source of $P(\Gamma)$ source such that $\mSat{M}{\Gamma}[f]$ source.

Contradictory signed formulas are unsatisfiable

If $\Gamma$ source contains both $\sFmla{\True}{!A}[\sigma]$ source and $\sFmla{\False}{!A}[\sigma]$ source, for some formula $!A$ source and prefix $\sigma$ source, then $\Gamma$ source is unsatisfiable.

Proof

There cannot be a model $\mModel{M}$ source and interpretation $f$ source of $P(\Gamma)$ source such that both $\mSat{M}{!A}[f(\sigma)]$ source and $\mSat/{M}{!A}[f(\sigma)]$ source.

Soundness of closed tableaux

[Soundness] If $\Gamma$ source has a closed tableau, $\Gamma$ source is unsatisfiable.

Proof

We call a branch of a tableau satisfiable iff the set of signed formulas on it is satisfiable, and let's call a tableau satisfiable if it contains at least one satisfiable branch.

We show the following: Extending a satisfiable tableau by one of the rules of inference always results in a satisfiable tableau. This will prove the theorem: any closed tableau results by applying rules of inference to the tableau consisting only of assumptions from $\Gamma$ source. So if $\Gamma$ source were satisfiable, any tableau for it would be satisfiable. A closed tableau, however, is clearly not satisfiable, since all its branches are closed and closed branches are unsatisfiable.

Suppose we have a satisfiable tableau, i.e., a tableau with at least one satisfiable branch. Applying a rule of inference either adds signed formulas to a branch, or splits a branch in two. If the tableau has a satisfiable branch which is not extended by the rule application in question, it remains a satisfiable branch in the extended tableau, so the extended tableau is satisfiable. So we only have to consider the case where a rule is applied to a satisfiable branch.

Let $\Gamma$ source be the set of signed formulas on that branch, and let $\sFmla{S}{!A}[\sigma] \in \Gamma$ source be the signed formula to which the rule is applied. If the rule does not result in a split branch, we have to show that the extended branch, i.e., $\Gamma$ source together with the conclusions of the rule, is still satisfiable. If the rule results in split branch, we have to show that at least one of the two resulting branches is satisfiable. tagfalseprvDiamond First, we consider the possible inferences with only one premise.

The branch is expanded by applying $\TRule{\True}{\lnot}$ source to $\sFmla{\True}{\lnot !B}[\sigma] \in \Gamma$ source. Then the extended branch contains the signed formulas $\Gamma \cup \{\sFmla{\False}{!B}[\sigma]\}$ source. Suppose $\mSat{M}{\Gamma}[f]$ source. In particular, $\mSat{M}{\lnot !B}[f(\sigma)]$ source. Thus, $\mSat/{M}{!B}[f(\sigma)]$ source, i.e., $\mModel{M}$ source satisfies $\sFmla{\False}{!B}[\sigma]$ source with respect to $f$ source.
The branch is expanded by applying $\TRule{\False}{\lnot}$ source to $\sFmla{\False}{\lnot !B}[\sigma] \in \Gamma$ source: Exercise.
The branch is expanded by applying $\TRule{\True}{\land}$ source to $\sFmla{\True}{!B \land !C}[\sigma] \in \Gamma$ source, which results in two new signed formulas on the branch: $\sFmla{\True}{!B}[\sigma]$ source and $\sFmla{\True}{!C}[\sigma]$ source. Suppose $\mSat{M}{\Gamma}[f]$ source, in particular $\mSat{M}{!B \land !C}[f(\sigma)]$ source. Then $\mSat{M}{!B}[f(\sigma)]$ source and $\mSat{M}{!C}[f(\sigma)]$ source. This means that $\mModel{M}$ source satisfies both $\sFmla{\True}{!B}[\sigma]$ source and $\sFmla{\True}{!C}[\sigma]$ source with respect to $f$ source.
The branch is expanded by applying $\TRule{\False}{\lor}$ source to $\sFmla{\False}{!B \lor !C} \in \Gamma$ source: Exercise.
The branch is expanded by applying $\TRule{\False}{\lif}$ source to $\sFmla{\False}{!B \lif !C}[\sigma] \in \Gamma$ source: This results in two new signed formulas on the branch: $\sFmla{\True}{!B}[\sigma]$ source and $\sFmla{\False}{!C}[\sigma]$ source. Suppose $\mSat{M}{\Gamma}[f]$ source, in particular $\mSat/{M}{!B \lif !C}[f(\sigma)]$ source. Then $\mSat{M}{!B}[f(\sigma)]$ source and $\mSat/{M}{!C}[f(\sigma)]$ source. This means that $\mModel{M}, f$ source satisfies both $\sFmla{\True}{!B}[\sigma]$ source and $\sFmla{\False}{!C}[\sigma]$ source.
The branch is expanded by applying $\TRule{\True}{\Box}$ source to $\sFmla{\True}{\Box !B}[\sigma] \in \Gamma$ source: This results in a new signed formula $\sFmla{\True}{!B}[\sigma.n]$ source on the branch, for some $\sigma.n \in P(\Gamma)$ source (since $\sigma.n$ source must be used). Suppose $\mSat{M}{\Gamma}[f]$ source, in particular, $\mSat{M}{\Box !B}[f(\sigma)]$ source. Since $f$ source is an interpretation of prefixes and both $\sigma$ source, $\sigma.n \in P(\Gamma)$ source, we know that $Rf(\sigma)f(\sigma.n)$ source. Hence, $\mSat{M}{!B}[f(\sigma.n)]$ source, i.e., $\mModel{M}, f$ source satisfies $\sFmla{\True}{!B}[\sigma.n]$ source.
The branch is expanded by applying $\TRule{\False}{\Box}$ source to $\sFmla{\False}{\Box !B}[\sigma] \in \Gamma$ source: This results in a new signed formula $\sFmla{\False}{!A}[\sigma.n]$ source, where $\sigma.n$ source is a new prefix on the branch, i.e., $\sigma.n \notin P(\Gamma)$ source. Since $\Gamma$ source is satisfiable, there is a $\Struct{M}$ source and interpretation $f$ source of $P(\Gamma)$ source such that $\Sat{M}{\Gamma}[f]$ source, in particular $\mSat/{M}{\Box !B}[f(\sigma)]$ source. We have to show that $\Gamma \cup \{\sFmla{\False}{!B}[\sigma.n]\}$ source is satisfiable. To do this, we define an interpretation of $P(\Gamma) \cup \{\sigma.n\}$ source as follows:
Since $\mSat/{M}{\Box !B}[f(\sigma)]$ source, there is a $w \in W$ source such that $Rf(\sigma)w$ source and $\mSat/{M}{!B}[w]$ source. Let $f'$ source be like $f$ source, except that $f'(\sigma.n) = w$ source. Since $f'(\sigma) = f(\sigma)$ source and $Rf(\sigma)w$ source, we have $Rf'(\sigma)f'(\sigma.n)$ source, so $f'$ source is an interpretation of $P(\Gamma) \cup \{\sigma.n\}$ source. Obviously $\mSat/{M}{!B}[f'(\sigma.n)]$ source. Since $f(\sigma') = f'(\sigma')$ source for all prefixes $\sigma' \in P(\Gamma)$ source, $\mSat{M}{\Gamma}[f']$ source. So, $\mModel{M}, f'$ source satisfies $\Gamma \cup \{\sFmla{\False}{!B}[\sigma.n]\}$ source.

Now let's consider the possible inferences with two premises.

The branch is expanded by applying $\TRule{\False}{\land}$ source to $\sFmla{\False}{!B \land !C}[\sigma] \in \Gamma$ source, which results in two branches, a left one continuing through $\sFmla{\False}{!B}[\sigma]$ source and a right one through $\sFmla{\False}{!C}[\sigma]$ source. Suppose $\mSat{M}{\Gamma}[f]$ source, in particular $\mSat/{M}{!B \land !C}[f(\sigma)]$ source. Then $\mSat/{M}{!B}[f(\sigma)]$ source or $\mSat/{M}{!C}[f(\sigma)]$ source. In the former case, $\mModel{M}, f$ source satisfies $\sFmla{\False}{!B}[\sigma]$ source, i.e., the left branch is satisfiable. In the latter, $\mModel{M}, f$ source satisfies $\sFmla{\False}{!C}[\sigma]$ source, i.e., the right branch is satisfiable.
The branch is expanded by applying $\TRule{\True}{\lor}$ source to $\sFmla{\True}{!B \lor !C}[\sigma] \in \Gamma$ source: Exercise.
The branch is expanded by applying $\TRule{\True}{\lif}$ source to $\sFmla{\True}{!B \lif !C}[\sigma] \in \Gamma$ source: Exercise.

Exercise completing tableau soundness

Complete the proof of the tableau soundness theorem.

Entailment soundness corollary

If $\Gamma \Proves !A$ source then $\Gamma \Entails !A$ source.

Proof

If $\Gamma \Proves !A$ source then for some $!B_1$ source, dots, $!B_n \in \Gamma$ source, $\Delta = \{\sFmla{\False}{!A}[1], \sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1]\}$ source has a closed tableau. We want to show that $\Gamma \Entails !A$ source. Suppose not, so for some $\mModel{M}$ source and $w$ source, $\mSat{M}{!B_i}[w]$ source for $i=1$ source, dots, $n$ source, but $\mSat/{M}{!A}[w]$ source. Let $f(1) = w$ source; then $f$ source is an interpretation of $P(\Delta)$ source into $\mModel{M}$ source, and $\mModel{M}$ source satisfies $\Delta$ source with respect to $f$ source. But by the tableau soundness theorem, $\Delta$ source is unsatisfiable since it has a closed tableau, a contradiction. So we must have $\Gamma \Proves !A$ source after all.

Weak soundness corollary

If $\Proves !A$ source then $!A$ source is true in all models.

Rules for Other Accessibility Relations

In order to deal with logics determined by special accessibility relations, we consider the additional rules in the additional modal tableau rule table.

Outer table for additional modal rules

defarraystretch3deffCenter

Additional modal tableau rules

Additional modal rules. Headers: necessity form; possibility form. Row one, reflexive T. Premise true necessarily formula A at prefix sigma. Rule label T the necessity operator. Conclusion true formula A at prefix sigma. Premise false possibly formula A at prefix sigma. Rule label T the possibility operator. Conclusion false formula A at prefix sigma. Row two, serial D. Premise true necessarily formula A at prefix sigma. Rule label D the necessity operator. Conclusion true possibly formula A at prefix sigma. Premise false possibly formula A at prefix sigma. Rule label D the possibility operator. Conclusion false necessarily formula A at prefix sigma. Row three, symmetric B. Premise true necessarily formula A at prefix sigma dot n. Rule label B the necessity operator. Conclusion true formula A at prefix sigma. Premise false possibly formula A at prefix sigma dot n. Rule label B the possibility operator. Conclusion false formula A at prefix sigma. Row four, transitive four. Premise true necessarily formula A at prefix sigma. Rule label four the necessity operator. Conclusion true necessarily formula A at prefix sigma dot n. Premise false possibly formula A at prefix sigma. Rule label four the possibility operator. Conclusion false possibly formula A at prefix sigma dot n. Both prefixes are used: prefix sigma dot n; prefix sigma dot n. Row five, euclidean four r. Premise true necessarily formula A at prefix sigma dot n. Rule label four r the necessity operator. Conclusion true necessarily formula A at prefix sigma. Premise false possibly formula A at prefix sigma dot n. Rule label four r the possibility operator. Conclusion false possibly formula A at prefix sigma. End additional-rule table.

Additional modal tableau rules
Necessity form	Possibility form
Reflexive true-necessity rule Proof diagram. Premise true necessarily formula A at prefix sigma. Rule label T the necessity operator. Conclusion true formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[\sigma]$ source Step 2. Depends on step 1. Rule: T necessity rule. $\sFmla{\True}{!A}[\sigma]$ source $\Box$ source	Reflexive false-possibility rule Proof diagram. Premise false possibly formula A at prefix sigma. Rule label T the possibility operator. Conclusion false formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[\sigma]$ source Step 2. Depends on step 1. Rule: T possibility rule. $\sFmla{\False}{!A}[\sigma]$ source $\Diamond$ source
Serial true-necessity rule Proof diagram. Premise true necessarily formula A at prefix sigma. Rule label D the necessity operator. Conclusion true possibly formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[\sigma]$ source Step 2. Depends on step 1. Rule: D necessity rule. $\sFmla{\True}{\Diamond!A}[\sigma]$ source $\Box$ source	Serial false-possibility rule Proof diagram. Premise false possibly formula A at prefix sigma. Rule label D the possibility operator. Conclusion false necessarily formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[\sigma]$ source Step 2. Depends on step 1. Rule: D possibility rule. $\sFmla{\False}{\Box!A}[\sigma]$ source $\Diamond$ source
Symmetric true-necessity rule Proof diagram. Premise true necessarily formula A at prefix sigma dot n. Rule label B the necessity operator. Conclusion true formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[\sigma.n]$ source Step 2. Depends on step 1. Rule: B necessity rule. $\sFmla{\True}{!A}[\sigma]$ source $\Box$ source	Symmetric false-possibility rule Proof diagram. Premise false possibly formula A at prefix sigma dot n. Rule label B the possibility operator. Conclusion false formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[\sigma.n]$ source Step 2. Depends on step 1. Rule: B possibility rule. $\sFmla{\False}{!A}[\sigma]$ source $\Diamond$ source
Transitive true-necessity rule Proof diagram. Premise true necessarily formula A at prefix sigma. Rule label four the necessity operator. Conclusion true necessarily formula A at prefix sigma dot n. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[\sigma]$ source Step 2. Depends on step 1. Rule: four necessity rule. $\sFmla{\True}{\Box!A}[\sigma.n]$ source $\Box$ source $\sigma.n$ source	Transitive false-possibility rule Proof diagram. Premise false possibly formula A at prefix sigma. Rule label four the possibility operator. Conclusion false possibly formula A at prefix sigma dot n. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[\sigma]$ source Step 2. Depends on step 1. Rule: four possibility rule. $\sFmla{\False}{\Diamond!A}[\sigma.n]$ source $\Diamond$ source $\sigma.n$ source
Euclidean reverse true-necessity rule Proof diagram. Premise true necessarily formula A at prefix sigma dot n. Rule label four r the necessity operator. Conclusion true necessarily formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[\sigma.n]$ source Step 2. Depends on step 1. Rule: four r necessity rule. $\sFmla{\True}{\Box!A}[\sigma]$ source $\Box$ source	Euclidean reverse false-possibility rule Proof diagram. Premise false possibly formula A at prefix sigma dot n. Rule label four r the possibility operator. Conclusion false possibly formula A at prefix sigma. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[\sigma.n]$ source Step 2. Depends on step 1. Rule: four r possibility rule. $\sFmla{\False}{\Diamond!A}[\sigma]$ source $\Diamond$ source

source 21

captionMore modal rules.

Adding these rules results in systems that are sound and complete for the logics given in the modal logics, frame conditions, and rules table.

Outer logic-and-rule correspondence table

Modal logics, frame conditions, and tableau rules

Logic and tableau-rule correspondence. Headers: logic; accessibility relation R is; rules. Header formula accessibility relation R. Row one: T equals K T; reflexive; formulas logic T equals logic K T, then the necessity operator, then the possibility operator. Row two: D equals K D; serial; formulas logic D equals logic K D, then the necessity operator, then the possibility operator. Row three: K four; transitive; formulas logic K four, then the necessity operator, then the possibility operator. Row four: B equals K T B; reflexive and symmetric; formulas logic B equals logic K T B, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator. Row five: S four equals K T four; reflexive and transitive; formulas logic S four equals logic K T four, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator. Row six: S five equals K T four B; reflexive, transitive, and euclidean; formulas logic S five equals logic K T four B, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator, then the necessity operator, then the possibility operator. End correspondence table.

Modal logics, frame conditions, and tableau rules
Logic	$R$ source is followed by an ellipsis	Rules
$\Log{T} = \Log{KT}$ source	reflexive	$\Box$ source $\Diamond$ source
$\Log{D} = \Log{KD}$ source	serial	$\Box$ source $\Diamond$ source
$\Log{K4}$ source	transitive	$\Box$ source $\Diamond$ source
$\Log{B} = \Log{KTB}$ source	reflexive and symmetric	$\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source
$\Log{S4} = \Log{KT4}$ source	reflexive and transitive	$\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source
$\Log{S5} = \Log{KT4B}$ source	reflexive, transitive, and euclidean	$\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source $\Box$ source $\Diamond$ source

source 103

captionTableau rules for various modal logics.

Closed S five tableau for axiom five

We give a closed tableau that shows $\Log{S5} \Proves \Ax{5}$ source, i.e., $\Box!A \lif \Box\Diamond!A$ source.

Tableau proof of axiom five in S five

Tableau proof of axiom five in S five. Node one: false the conditional from necessarily formula A to necessarily possibly formula A at prefix one. Rule: tableau assumption. Node two: true necessarily formula A at prefix one. Rule: false conditional rule, depending on node one. Node three: false necessarily possibly formula A at prefix one. Rule: false conditional rule, depending on node one. Node four: false possibly formula A at prefix one point one. Rule: false necessity rule, depending on node three. Node five: false possibly formula A at prefix one. Rule: four r the possibility operator, depending on node four. Node six: false formula A at prefix one point one. Rule: false possibility rule, depending on node five. Node seven: true formula A at prefix one point one. Rule: true necessity rule, depending on node two; source close marker present. Branch one is closed, closed by nodes six and seven. End tableau.

Node 1. $\sFmla{\False}{\Box\formula{A} \lif \Box\Diamond \formula{A}}[1]$ source Rule: tableau assumption. Parents: none.
Node 2. $\sFmla{\True}{\Box \formula{A}}[1]$ source Rule: false conditional rule. Parents: projected-env-003883-node-1.
Node 3. $\sFmla{\False}{\Box\Diamond \formula{A}}[1]$ source Rule: false conditional rule. Parents: projected-env-003883-node-2.
Node 4. $\sFmla{\False}{\Diamond \formula{A}}[1.1]$ source Rule: false necessity rule. Parents: projected-env-003883-node-3.
Node 5. $\Diamond$ source $\sFmla{\False}{\Diamond \formula{A}}[1]$ source Rule: four r possibility rule. Parents: projected-env-003883-node-4.
Node 6. $\sFmla{\False}{\formula{A}}[1.1]$ source Rule: false possibility rule. Parents: projected-env-003883-node-5.
Node 7. $\sFmla{\True}{\formula{A}}[1.1]$ source Rule: true necessity rule. Parents: projected-env-003883-node-6. Markers: closed marker.

closed branch; nodes projected-env-003883-node-1, projected-env-003883-node-2, projected-env-003883-node-3, projected-env-003883-node-4, projected-env-003883-node-5, projected-env-003883-node-6, projected-env-003883-node-7; closure witnesses projected-env-003883-node-6, projected-env-003883-node-7.

source 163

Exercise proving six modal derivabilities

Give closed tableaux that show the following:

$\Log{KT5} \Proves \Ax{B}$ source;
$\Log{KT5} \Proves \Ax{4}$ source;
$\Log{KDB4} \Proves \Ax{T}$ source;
$\Log{KB4} \Proves \Ax{5}$ source;
$\Log{KB5} \Proves \Ax{4}$ source;
$\Log{KT} \Proves \Ax{D}$ source.

Complete the proof of the proposition on soundness of the euclidean rules

tagendprob

Soundness of the listed modal tableau systems

The tableau systems given in the modal logics, frame conditions, and rules table are sound for the respective classes of models.

Simple tableau for LogS5

LogS5 is sound and complete with respect to the class of universal models, i.e., models where every world is accessible from every world. In universal models the accessibility relation doesn't matter: “there is a world $w$ source where $\mSat{M}{!A}[w]$ source” is true if and only if there is such a $w$ source that's accessible from $u$ source. So in LogS5, we can define models as simply a set of worlds and a valuation $V$ source. This suggests that we should be able to simplify the tableau rules as well. In the general case, we take as prefixes sequences of positive integers, so that we can keep track of which such prefixes name worlds which are accessible from others: $\sigma.n$ source names a world accessible from $\sigma$ source. But in LogS5 any world is accessible from any world, so there is no need to so keep track. Instead, we can use positive integers as prefixes. The simplified rules are given in the simplified S five tableau rule table.

Outer table for simplified S five rules

defarraystretch3deffCenter

Simplified S five tableau rules

Simplified S five rules. Headers: true-sign rule; false-sign rule. Row one, necessity. Premise true necessarily formula A at prefix n. Rule true necessity rule. Conclusion true formula A at prefix m. Premise false necessarily formula A at prefix n. Rule false necessity rule. Conclusion false formula A at prefix m. Side conditions: prefix m; prefix m. Row two, possibility. Premise true possibly formula A at prefix n. Rule true possibility rule. Conclusion true formula A at prefix m. Premise false possibly formula A at prefix n. Rule false possibility rule. Conclusion false formula A at prefix m. Side conditions: prefix m; prefix m. End simplified S five rule table.

Simplified S five tableau rules
True-sign rule	False-sign rule
Simplified S five true-necessity rule Proof diagram. Premise true necessarily formula A at prefix n. Rule true necessity rule. Conclusion true formula A at prefix m. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Box !A}[n]$ source Step 2. Depends on step 1. Rule: true necessity rule. $\sFmla{\True}{!A}[m]$ source $m$ source	Simplified S five false-necessity rule Proof diagram. Premise false necessarily formula A at prefix n. Rule false necessity rule. Conclusion false formula A at prefix m. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Box !A}[n]$ source Step 2. Depends on step 1. Rule: false necessity rule. $\sFmla{\False}{!A}[m]$ source $m$ source
Simplified S five true-possibility rule Proof diagram. Premise true possibly formula A at prefix n. Rule true possibility rule. Conclusion true formula A at prefix m. Step 1. No premises. Rule: premise. $\sFmla{\True}{\Diamond !A}[n]$ source Step 2. Depends on step 1. Rule: true possibility rule. $\sFmla{\True}{!A}[m]$ source $m$ source	Simplified S five false-possibility rule Proof diagram. Premise false possibly formula A at prefix n. Rule false possibility rule. Conclusion false formula A at prefix m. Step 1. No premises. Rule: premise. $\sFmla{\False}{\Diamond !A}[n]$ source Step 2. Depends on step 1. Rule: false possibility rule. $\sFmla{\False}{!A}[m]$ source $m$ source

\TRule{\True}{\Box}

source

\TRule{\False}{\Box}

source

\TRule{\True}{\Diamond}

source

\TRule{\False}{\Diamond}

source

source 31

captionSimplified rules for LogS5.

Simplified S five tableau for axiom five

We give a simplified closed tableau that shows $\Log{S5} \Proves \Ax{5}$ source, i.e., $\Diamond!A \lif \Box\Diamond!A$ source.

Simplified S five tableau proof

Simplified S five tableau proof. Node one: false the conditional from possibly formula A to necessarily possibly formula A at prefix one. Rule: tableau assumption. Node two: true possibly formula A at prefix one. Rule: false conditional rule, depending on node one. Node three: false necessarily possibly formula A at prefix one. Rule: false conditional rule, depending on node one. Node four: false possibly formula A at prefix two. Rule: false necessity rule, depending on node three. Node five: true formula A at prefix three. Rule: true possibility rule, depending on node two. Node six: false formula A at prefix three. Rule: false possibility rule, depending on node four; source close marker present. Branch one is closed, closed by nodes five and six. End tableau.

Node 1. $\sFmla{\False}{\Diamond\formula{A} \lif \Box\Diamond \formula{A}}[1]$ source Rule: tableau assumption. Parents: none.
Node 2. $\sFmla{\True}{\Diamond \formula{A}}[1]$ source Rule: false conditional rule. Parents: projected-env-003911-node-1.
Node 3. $\sFmla{\False}{\Box\Diamond \formula{A}}[1]$ source Rule: false conditional rule. Parents: projected-env-003911-node-2.
Node 4. $\sFmla{\False}{\Diamond \formula{A}}[2]$ source Rule: false necessity rule. Parents: projected-env-003911-node-3.
Node 5. $\sFmla{\True}{\formula{A}}[3]$ source Rule: true possibility rule. Parents: projected-env-003911-node-4.
Node 6. $\sFmla{\False}{\formula{A}}[3]$ source Rule: false possibility rule. Parents: projected-env-003911-node-5. Markers: closed marker.

closed branch; nodes projected-env-003911-node-1, projected-env-003911-node-2, projected-env-003911-node-3, projected-env-003911-node-4, projected-env-003911-node-5, projected-env-003911-node-6; closure witnesses projected-env-003911-node-5, projected-env-003911-node-6.

source 68

Completeness for LogK

Explain

To show that the method of tableaux is complete, we have to show that whenever there is no closed tableau to show $\Gamma \Proves !A$ source, then $\Gamma \Entails/ !A$ source, i.e., there is a countermodel. But “there is no closed tableau” means that every way we could try to construct one has to fail to close. The trick is to see that if every such way fails to close, then a specific, systematic and exhaustive way also fails to close. And this systematic and exhaustive way would close if a closed tableau exists. The single tableau will contain, among its open branches, all the information required to define a countermodel. The countermodel given by an open branch in this tableau will contain the all the prefixes used on that branch as the worlds, and a propositional variable $p$ source is true at $\sigma$ source iff $\sFmla{\True}{p}[\sigma]$ source occurs on the branch.

Complete tableau branch

A branch in a tableau is called complete if, whenever it contains a prefixed formula $\sFmla{S}{!A}[\sigma]$ source to which a rule can be applied, it also contains

the prefixed formulas that are the corresponding conclusions of the rule, in the case of propositional stacking rules;
one of the corresponding conclusion formulas in the case of propositional branching rules;
at least one possible conclusion in the case of modal rules that require a new prefix;
the corresponding conclusion for every prefix occurring on the branch in the case of modal rules that require a used prefix.

Explain

For instance, a complete branch contains $\sFmla{\True}{!B}[\sigma]$ source and $\sFmla{\True}{!C}[\sigma]$ source whenever it contains $\sFmla{\True}{!B \land !C}$ source. If it contains $\sFmla{\True}{!B \lor !C}[\sigma]$ source it contains at least one of $\sFmla{\False}{!B}[\sigma]$ source and $\sFmla{\True}{!C}[\sigma]$ source. If it contains $\sFmla{\False}{\Box}[\sigma]$ source it also contains $\sFmla{\False}{\Box}[\sigma.n]$ source for at least one $n$ source. And whenever it contains $\sFmla{\True}{\Box}[\sigma]$ source it also contains $\sFmla{\True}{\Box}[\sigma.n]$ source for every $n$ source such that $\sigma.n$ source is used on the branch.

Existence of a complete tableau

Every finite $\Gamma$ source has a tableau in which every branch is complete.

Proof

Consider an open branch in a tableau for $\Gamma$ source. There are finitely many prefixed formulas in the branch to which a rule could be applied. In some fixed order (say, top to bottom), for each of these prefixed formulas for which the conditions (1)--(4) do not already hold, apply the rules that can be applied to it to extend the branch. In some cases this will result in branching; apply the rule at the tip of each resulting branch for all remaining prefixed formulas. Since the number of prefixed formulas is finite, and the number of used prefixes on the branch is finite, this procedure eventually results in (possibly many) branches extending the original branch. Apply the procedure to each, and repeat. But by construction, every branch is closed.

Completeness of closed tableaux

[Completeness] If $\Gamma$ source has no closed tableau, $\Gamma$ source is satisfiable.

Proof

By the proposition, $\Gamma$ source has a tableau in which every branch is complete. Since it has no closed tableau, it thas has a tableau in which at least one branch is open and complete. Let $\Delta$ source be the set of prefixed formulas on the branch, and $P(\Delta)$ source the set of prefixes occurring in it.

We define a model $\mModel{M(\Delta)} = \tuple{P(\Delta), R, V}$ source where the worlds are the prefixes occurring in $\Delta$ source, the accessibility relation is given by:

R\sigma\sigma' \quad \text{iff} \quad \sigma'=\sigma.n \quad \text{for some~$n$}

source

and

V(p) = \Setabs{\sigma}{\sFmla{\True}{p}[\sigma] \in \Delta}.

source

We show by induction on $!A$ source that if $\sFmla{\True}{!A}[\sigma] \in \Delta$ source then $\mSat{M(\Delta)}{!A}[\sigma]$ source, and if $\sFmla{\False}{!A}[\sigma] \in \Delta$ source then $\mSat/{M(\Delta)}{!A}[\sigma]$ source.

Case: $!A \ident p$ source
If $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$ source then $\sigma \in V(p)$ source (by definition of $V$ source) and so $\mSat{M(\Delta)}{\indfrm}[\sigma]$ source.
If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$ source then $\sFmla{\True}{\indfrm}[\sigma] \notin \Delta$ source, since the branch would otherwise be closed. So $\sigma \notin V(p)$ source and thus $\mSat/{M(\Delta)}{\indfrm}[\sigma]$ source.
Case: $!A \ident \lnot !B$ source
If $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$ source, then $\sFmla{\False}{!B}[\sigma] \in \Delta$ source since the branch is complete. By induction hypothesis, $\mSat/{M(\Delta)}{!B}[\sigma]$ source and thus $\mSat{M(\Delta)}{\indfrm}[\sigma]$ source.
If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$ source, then $\sFmla{\True}{!B}[\sigma] \in \Delta$ source since the branch is complete. By induction hypothesis, $\mSat{M(\Delta)}{!B}[\sigma]$ source and thus $\mSat/{M(\Delta)}{\indfrm}[\sigma]$ source.
Case: $!A \ident !B \land !C$ source
Exercise.
Case: $!A \ident !B \lor !C$ source
If $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$ source, then either $\sFmla{\True}{!B}[\sigma] \in \Delta$ source or $\sFmla{\True}{!C}[\sigma] \in \Delta$ source since the branch is complete. By induction hypothesis, either $\mSat{M(\Delta)}{!B}[\sigma]$ source or $\mSat{M(\Delta)}{!C}[\sigma]$ source. Thus $\mSat{M(\Delta)}{\indfrm}[\sigma]$ source.
If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$ source, then both $\sFmla{\False}{!B}[\sigma] \in \Delta$ source and $\sFmla{\False}{!C}[\sigma] \in \Delta$ source since the branch is complete. By induction hypothesis, both $\mSat/{M(\Delta)}{!B}[\sigma]$ source and $\mSat/{M(\Delta)}{!B}[\sigma]$ source. Thus $\mSat/{M(\Delta)}{\indfrm}[\sigma]$ source.
Case: $!A \ident !B \lif !C$ source
Exercise.
Case: $!A \ident \Box !B$ source
If $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$ source, then, since the branch is complete, $\sFmla{\True}{!B}[\sigma.n] \in \Delta$ source for every $\sigma.n$ source used on the branch, i.e., for every $\sigma' \in P(\Delta)$ source such that $R\sigma\sigma'$ source. By induction hypothesis, $\mSat{M(\Delta)}{!B}[\sigma']$ source for every $\sigma'$ source such that $R\sigma\sigma'$ source. Therefore, $\mSat{M(\Delta)}{\indfrm}[\sigma]$ source.
If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$ source, then for some $\sigma.n$ source, $\sFmla{\False}{!B}[\sigma.n] \in \Delta$ source since the branch is complete. By induction hypothesis, $\mSat/{M(\Delta)}{!B}[\sigma.n]$ source. Since $R\sigma(\sigma.n)$ source, there is a $\sigma'$ source such that $\mSat/{M(\Delta)}{!B}[\sigma']$ source. Thus $\mSat/{M(\Delta)}{\indfrm}[\sigma]$ source.
Case: $!A \ident \Diamond !B$ source
Exercise.

Since $\Gamma \subseteq \Delta$ source, $\mSat{M(\Delta)}{\Gamma}$ source.

Exercise completing tableau completeness

Complete the proof of the tableau completeness theorem.

Entailment completeness corollary

If $\Gamma \Entails !A$ source then $\Gamma \Proves !A$ source.

Weak completeness corollary

If $!A$ source is true in all models, then $\Proves !A$ source.

Countermodels from tableau

Explain

The proof of the completeness theorem doesn't just show that if $\Entails !A$ source then $\Proves !A$ source, it also gives us a method for constructing countermodels to $!A$ source if $\Entails/ A$ source. In the case of $\Log{K}$ source, this method constitutes a decision procedure. For suppose $\Entails/ !A$ source. Then the proof of the proposition that every finite Gamma has a complete tableau gives a method for constructing a complete tableau. The method in fact always terminates. The propositional rules for $\Log{K}$ source only add prefixed formulas of lower complexity, i.e., each propositional rule need only be applied once on a branch for any signed formula $\sFmla{S}{!A}[\sigma]$ source. New prefixes are only generated by the $\TRule{\False}{\Box}$ source and $\TRule{\True}{\Diamond}$ source rules , and also only have to be applied once (and produce a single new prefix). $\TRule{\True}{\Box}$ source and $\TRule{\False}{\Diamond}$ source have to be applied potentially multiple times, but only once per prefix, and only finitely many new prefixes are generated. So the construction either results in a closed branch or a complete branch after finitely many stages.

Once a tableau with an open complete branch is constructed, the proof of the tableau completeness theorem gives us an explict model that satisfies the original set of prefixed formulas. So not only is it the case that if $\Gamma \Entails !A$ source, then a closed tableau exists and $\Gamma \Proves !A$ source, if we look for the closed tableau in the right way and end up with a “complete” tableau, we'll not only know that $\Gamma \Entails/ !A$ source but actually be able to construct a countermodel.

Countermodel construction for failed box distribution

We know that $\Proves/ \Box(p \lor q) \lif (\Box p \lor \Box q)$ source. The construction of a tableau begins with:

Initial unfinished countermodel tableau

Initial unfinished countermodel tableau. Node one: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one. Rule: tableau assumption; source checkmark present. Node two: true necessarily the disjunction of p and q at prefix one. Rule: false conditional rule, depending on node one. Node three: false the disjunction of necessarily p and necessarily q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node four: false necessarily p at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node five: false necessarily q at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node six: false p at prefix one point one. Rule: false necessity rule, depending on node four; source checkmark present. Node seven: false q at prefix one point two. Rule: false necessity rule, depending on node five; source checkmark present. Branch one is unfinished. End tableau.

Node 1. $\sFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[1]$ source Rule: tableau assumption. Parents: none. Markers: checked.
Node 2. $\sFmla{\True}{\Box(p \lor q)}[1]$ source Rule: false conditional rule. Parents: projected-env-003926-node-1.
Node 3. $\sFmla{\False}{\Box p \lor \Box q}[1]$ source Rule: false conditional rule. Parents: projected-env-003926-node-2. Markers: checked.
Node 4. $\sFmla{\False}{\Box p}[1]$ source Rule: false disjunction rule. Parents: projected-env-003926-node-3. Markers: checked.
Node 5. $\sFmla{\False}{\Box q}[1]$ source Rule: false disjunction rule. Parents: projected-env-003926-node-4. Markers: checked.
Node 6. $\sFmla{\False}{p}[1.1]$ source Rule: false necessity rule. Parents: projected-env-003926-node-5. Markers: checked.
Node 7. $\sFmla{\False}{q}[1.2]$ source Rule: false necessity rule. Parents: projected-env-003926-node-6. Markers: checked.

unfinished branch; nodes projected-env-003926-node-1, projected-env-003926-node-2, projected-env-003926-node-3, projected-env-003926-node-4, projected-env-003926-node-5, projected-env-003926-node-6, projected-env-003926-node-7; closure witnesses none.

source 50

The tableau is of course not finished yet. In the next step, we consider the only line without a checkmark: the prefixed formula $\sFmla{\True}{\Box(p \lor q)}[1]$ source on line $2$ source. The construction of the closed tableau says to apply the $\TRule{\True}{\Box}$ source rule for every prefix used on the branch, i.e., for both $1.1$ source and $1.2$ source:

Second unfinished countermodel tableau

Second unfinished countermodel tableau. Node one: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one. Rule: tableau assumption; source checkmark present. Node two: true necessarily the disjunction of p and q at prefix one. Rule: false conditional rule, depending on node one. Node three: false the disjunction of necessarily p and necessarily q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node four: false necessarily p at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node five: false necessarily q at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node six: false p at prefix one point one. Rule: false necessity rule, depending on node four; source checkmark present. Node seven: false q at prefix one point two. Rule: false necessity rule, depending on node five; source checkmark present. Node eight: true the disjunction of p and q at prefix one point one. Rule: true necessity rule, depending on node two. Node nine: true the disjunction of p and q at prefix one point two. Rule: true necessity rule, depending on node two. Branch one is unfinished. End tableau.

Node 1. $\sFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[1]$ source Rule: tableau assumption. Parents: none. Markers: checked.
Node 2. $\sFmla{\True}{\Box(p \lor q)}[1]$ source Rule: false conditional rule. Parents: projected-env-003927-node-1.
Node 3. $\sFmla{\False}{\Box p \lor \Box q}[1]$ source Rule: false conditional rule. Parents: projected-env-003927-node-2. Markers: checked.
Node 4. $\sFmla{\False}{\Box p}[1]$ source Rule: false disjunction rule. Parents: projected-env-003927-node-3. Markers: checked.
Node 5. $\sFmla{\False}{\Box q}[1]$ source Rule: false disjunction rule. Parents: projected-env-003927-node-4. Markers: checked.
Node 6. $\sFmla{\False}{p}[1.1]$ source Rule: false necessity rule. Parents: projected-env-003927-node-5. Markers: checked.
Node 7. $\sFmla{\False}{q}[1.2]$ source Rule: false necessity rule. Parents: projected-env-003927-node-6. Markers: checked.
Node 8. $\sFmla{\True}{p \lor q}[1.1]$ source Rule: true necessity rule. Parents: projected-env-003927-node-7.
Node 9. $\sFmla{\True}{p \lor q}[1.2]$ source Rule: true necessity rule. Parents: projected-env-003927-node-8.

unfinished branch; nodes projected-env-003927-node-1, projected-env-003927-node-2, projected-env-003927-node-3, projected-env-003927-node-4, projected-env-003927-node-5, projected-env-003927-node-6, projected-env-003927-node-7, projected-env-003927-node-8, projected-env-003927-node-9; closure witnesses none.

source 78

Now lines 2, 8, and 9, don't have checkmarks. But no new prefix has been added, so we apply $\TRule{\True}{\lor}$ source to lines 8 and 9, on all resulting branches (as long as they don't close):

Complete countermodel tableau

Complete countermodel tableau. Node one: false the conditional from necessarily the disjunction of p and q to the disjunction of necessarily p and necessarily q at prefix one. Rule: tableau assumption; source checkmark present. Node two: true necessarily the disjunction of p and q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node three: false the disjunction of necessarily p and necessarily q at prefix one. Rule: false conditional rule, depending on node one; source checkmark present. Node four: false necessarily p at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node five: false necessarily q at prefix one. Rule: false disjunction rule, depending on node three; source checkmark present. Node six: false p at prefix one point one. Rule: false necessity rule, depending on node four; source checkmark present. Node seven: false q at prefix one point two. Rule: false necessity rule, depending on node five; source checkmark present. Node eight: true the disjunction of p and q at prefix one point one. Rule: true necessity rule, depending on node two; source checkmark present. Node nine: true the disjunction of p and q at prefix one point two. Rule: true necessity rule, depending on node two; source checkmark present. Node one zero: true p at prefix one point one. Rule: true disjunction rule, depending on node eight; source checkmark present; source close marker present. Node one one: true q at prefix one point one. Rule: true disjunction rule, depending on node eight; source checkmark present. Node one two: true p at prefix one point two. Rule: true disjunction rule, depending on node nine; source checkmark present. Node one three: true q at prefix one point two. Rule: true disjunction rule, depending on node nine; source checkmark present; source close marker present. Branch one is closed, closed by nodes six and one zero. Branch two is open and complete. Branch three is closed, closed by nodes seven and one three. End tableau.

Node 1. $\sFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[1]$ source Rule: tableau assumption. Parents: none. Markers: checked.
Node 2. $\sFmla{\True}{\Box(p \lor q)}[1]$ source Rule: false conditional rule. Parents: projected-env-003928-node-1. Markers: checked.
Node 3. $\sFmla{\False}{\Box p \lor \Box q}[1]$ source Rule: false conditional rule. Parents: projected-env-003928-node-2. Markers: checked.
Node 4. $\sFmla{\False}{\Box p}[1]$ source Rule: false disjunction rule. Parents: projected-env-003928-node-3. Markers: checked.
Node 5. $\sFmla{\False}{\Box q}[1]$ source Rule: false disjunction rule. Parents: projected-env-003928-node-4. Markers: checked.
Node 6. $\sFmla{\False}{p}[1.1]$ source Rule: false necessity rule. Parents: projected-env-003928-node-5. Markers: checked.
Node 7. $\sFmla{\False}{q}[1.2]$ source Rule: false necessity rule. Parents: projected-env-003928-node-6. Markers: checked.
Node 8. $\sFmla{\True}{p \lor q}[1.1]$ source Rule: true necessity rule. Parents: projected-env-003928-node-7. Markers: checked.
Node 9. $\sFmla{\True}{p \lor q}[1.2]$ source Rule: true necessity rule. Parents: projected-env-003928-node-8. Markers: checked.
Node 10. $\sFmla{\True}{p}[1.1]$ source Rule: true disjunction rule. Parents: projected-env-003928-node-9. Markers: checked, closed marker.
Node 11. $\sFmla{\True}{q}[1.1]$ source Rule: true disjunction rule. Parents: projected-env-003928-node-9. Markers: checked.
Node 12. $\sFmla{\True}{p}[1.2]$ source Rule: true disjunction rule. Parents: projected-env-003928-node-11. Markers: checked.
Node 13. $\sFmla{\True}{q}[1.2]$ source Rule: true disjunction rule. Parents: projected-env-003928-node-11. Markers: checked, closed marker.

closed branch; nodes projected-env-003928-node-1, projected-env-003928-node-2, projected-env-003928-node-3, projected-env-003928-node-4, projected-env-003928-node-5, projected-env-003928-node-6, projected-env-003928-node-7, projected-env-003928-node-8, projected-env-003928-node-9, projected-env-003928-node-10; closure witnesses projected-env-003928-node-6, projected-env-003928-node-10.
open branch; nodes projected-env-003928-node-1, projected-env-003928-node-2, projected-env-003928-node-3, projected-env-003928-node-4, projected-env-003928-node-5, projected-env-003928-node-6, projected-env-003928-node-7, projected-env-003928-node-8, projected-env-003928-node-9, projected-env-003928-node-11, projected-env-003928-node-12; closure witnesses none.
closed branch; nodes projected-env-003928-node-1, projected-env-003928-node-2, projected-env-003928-node-3, projected-env-003928-node-4, projected-env-003928-node-5, projected-env-003928-node-6, projected-env-003928-node-7, projected-env-003928-node-8, projected-env-003928-node-9, projected-env-003928-node-11, projected-env-003928-node-13; closure witnesses projected-env-003928-node-7, projected-env-003928-node-13.

source 110

There is one remaining open branch, and it is complete. From it we define the model with worlds $W = \{1, 1.1, 1.2\}$ source (the only prefixes appearing on the open branch), the accessibility relation $R = \{\tuple{1, 1.1}, \tuple{1, 1.2}\}$ source, and the assignment $V(p) = \{1.2\}$ source (because line 11 contains $\sFmla{\True}{p}[1.2]$ source) and $V(q) = \{1.1\}$ source (because line 10 contains $\sFmla{\True}{q}[1.1]$ source). The model is pictured in the three-world countermodel figure, and you can verify that it is a countermodel to $\Box(p \lor q) \lif (\Box p \lor \Box q)$ source.

Figure containing the three-world countermodel

The figure contains the source graph with three worlds, six printed p-and-q valuations, and two directed accessibility edges.

Source transcription

Three-world countermodel graph

Three-world countermodel graph. Node one is prefix one, with printed valuations p is false and q is false. Node two is prefix one point one, with printed valuations p is false and q is true. Node three is prefix one point two, with printed valuations p is true and q is false. Directed accessibility edges, in printed order: from world one to world one point one; then from world one to world one point two. No loop or further edge is printed. End graph.

Nodes

Node 1: world one $\mFalse{p}$ source $\mFalse{q}$ source $1$ source
Node 2: world one point one $\mFalse{p}$ source $\mTrue{q}$ source $1.1$ source
Node 3: world one point two $\mTrue{p}$ source $\mFalse{q}$ source $1.2$ source

Edges

Edge 1: w1 to w2; accessibility relation R.
Edge 2: w1 to w3; accessibility relation R.

source 160

captionA countermodel to $\Box(p \lor q) \lif (\Box p \lor \Box q)$ source.

Source disclosures

TR055-SAR-001: Source caveat. The contrapositive paragraph says A is true at w, while its preceding entailment claim and the next sentence describe a countermodel. The printed positive satisfaction statement is retained. source
TR055-SAR-002: Source caveat. The false-necessity case first calls its new conclusion false A at sigma dot n, then immediately constructs and proves satisfiable the set with false B there. Both source occurrences remain unchanged. source
TR055-SAR-003: Source caveat. The soundness-corollary proof ends by repeating derivability, although the contradiction was introduced to establish semantic entailment. The printed conclusion remains discoverable. source
TR055-SAR-011: Source caveat. The euclidean necessity proof places dot n outside the closing parenthesis of f of sigma. Speech preserves that source placement rather than silently changing it to f of sigma dot n. source
TR055-SAR-012: Source caveat. The four-r possibility case says its new signed formula is true necessarily B, while the case begins and ends with false possibility B. The true-necessity source formula is retained. source
TR055-SAR-004: Source caveat. The complete-branch example for a true disjunction prints false B as its first alternative and true C as its second. Those signs are retained exactly. source
TR055-SAR-005: Source caveat. The modal completeness examples print signed necessity or possibility operators without a formula operand. Speech explicitly identifies the missing printed operand rather than supplying A or B. source
TR055-SAR-006: Source caveat. The construction proposition claims every branch is complete, but its proof's final sentence says every branch is closed. The sentence is preserved as written. source
TR055-SAR-007: Source caveat. The duplicated source wording 'thas has' is preserved in prose and noted; no mathematical content is inferred from it. source
TR055-SAR-008: Source caveat. The false-conjunction induction case repeats false B in its second semantic alternative where the signed premises just named false B or false C. The repeated B remains unchanged. source
TR055-SAR-009: Source caveat. The false-disjunction induction case repeats false B in its second conjunct where the signed premises just named false B and false C. The repeated B remains unchanged. source
TR055-SAR-010: Source caveat. The false-conditional induction case prints true B and false B as its semantic pair, though the signed premises are true B and false C. The second B remains unchanged. source
TR055-SAR-013: Source caveat. The first countermodel-method sentence omits the usual formula-marker exclamation before A. Speech explicitly reports the source expression without supplying the missing marker. source

Reading preferences

Source file content/normal-modal-logic/tableaux/tableaux.tex

Editorial

Source file content/normal-modal-logic/tableaux/introduction.tex

Introduction

Source file content/normal-modal-logic/tableaux/rules-for-K.tex

Rules for AxK

Propositional prefixed-tableau rule table

True-negation tableau rule

False-negation tableau rule

True-conjunction tableau rule

False-conjunction tableau rule

True-disjunction tableau rule

False-disjunction tableau rule

True-conditional tableau rule

False-conditional tableau rule

Outer table for the four modal K rules

Four modal K tableau rules

True-necessity used-prefix rule

False-necessity new-prefix rule

True-possibility new-prefix rule

False-possibility used-prefix rule

Closed necessity-versus-possibility tableau

Closed possibility-versus-necessity tableau

Source file content/normal-modal-logic/tableaux/proofs-in-K.tex

tableau for LogK

Closed tableau for distributing necessity over conjunction

Tableau for necessity and conjunction

Closed tableau for distributing possibility over disjunction

Tableau for possibility and disjunction

Exercise constructing four closed K tableaux

Source file content/normal-modal-logic/tableaux/soundness.tex

Soundness for LogK

Editorial

Explain

Interpretation of tableau prefixes in a model

Satisfaction and satisfiability of a prefixed set

Contradictory signed formulas are unsatisfiable

Proof

Soundness of closed tableaux

Proof

Exercise completing tableau soundness

Entailment soundness corollary

Proof

Weak soundness corollary

Source file content/normal-modal-logic/tableaux/more-rules.tex

Rules for Other Accessibility Relations

Outer table for additional modal rules

Additional modal tableau rules

Reflexive true-necessity rule

Reflexive false-possibility rule

Serial true-necessity rule

Serial false-possibility rule

Symmetric true-necessity rule

Symmetric false-possibility rule

Transitive true-necessity rule

Transitive false-possibility rule

Euclidean reverse true-necessity rule

Euclidean reverse false-possibility rule

Outer logic-and-rule correspondence table

Modal logics, frame conditions, and tableau rules

Closed S five tableau for axiom five

Tableau proof of axiom five in S five

Exercise proving six modal derivabilities

Source file content/normal-modal-logic/tableaux/more-soundness.tex

Soundness for Additional Rules

Soundness of the reflexive rules

Proof

Tagenumerate

Exercise completing reflexive-rule soundness

Soundness of the serial rules

Proof

Tagenumerate

Exercise completing serial-rule soundness

Soundness of the symmetric rules

Proof

Tagenumerate

Exercise completing symmetric-rule soundness

Soundness of the transitive rules

Proof