Intuitionistic Tableaux

Reading preferences

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

Editorial

Draft chapter on prefixed tableaux for intuitionistic 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 intuitionistic logic, we have to both extend the notion of signed formula and adjust the rules for the connectives. 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}{!A \lif (!B \lif !C)}[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.

In intuitionistic models, the accessibility relation is reflexive and transitive. In terms of prefixes, this means that $\sigma$ source is accessible from $\sigma$ source itself, and so is any prefix that extends $\sigma$ source, i.e., any prefix of the form $\sigma.n_1.\cdots.n_k$ source. Let's introduce the notation $\sigma.*$ source to indicate $\sigma$ source itself and any extension of it. In other words, the prefixes $\sigma.*$ source are all and only the prefixes accessible from $\sigma$ source.

Rules for Intuitionistic Logic

The rules for the connectives $\land$ source and $\lor$ source 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 rules for $\land$ source and $\lor$ source in the prefixed conjunction and disjunction rule table.

Prefixed conjunction and disjunction rule table

Four prefixed propositional tableau rules, read across each source row. Row one left, signed true A and B at sigma yields signed true A and then signed true B at sigma. Row one right, signed false A and B at sigma branches to signed false A or signed false B at sigma. Row two left, signed true A or B at sigma branches to signed true A or signed true B at sigma. Row two right, signed false A or B at sigma yields signed false A and then signed false B at sigma. End of rule table. Caption connective labels, in source order: conjunction, then disjunction. End of table.

\def\arraystretch{3}\begin{array}{|c|c|} \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 \end{array}

source

\land

source

\lor

source

Prefixed conjunction and disjunction rule table
signed-true rule	signed-false rule
Signed true conjunction rule Signed-true conjunction rule. From signed true A and B at sigma, continue the same branch with signed true A at sigma and signed true B at sigma. Step 1. No premises. Rule: source premise. premise: signed true A and B at sigma Step 2. Depends on step 1. Rule: signed-true conjunction. first same-branch conclusion: signed true A at sigma Step 3. Depends on step 1. Rule: signed-true conjunction. second same-branch conclusion: signed true B at sigma	Signed false conjunction rule Signed-false conjunction rule. From signed false A and B at sigma, split into a left branch containing signed false A at sigma and a right branch containing signed false B at sigma. Step 1. No premises. Rule: source premise. premise: signed false A and B at sigma Step 2. Depends on step 1. Rule: signed-false conjunction. left branch: signed false A at sigma Step 3. Depends on step 1. Rule: signed-false conjunction. right branch: signed false B at sigma
Signed true disjunction rule Signed-true disjunction rule. From signed true A or B at sigma, split into a left branch containing signed true A at sigma and a right branch containing signed true B at sigma. Step 1. No premises. Rule: source premise. premise: signed true A or B at sigma Step 2. Depends on step 1. Rule: signed-true disjunction. left branch: signed true A at sigma Step 3. Depends on step 1. Rule: signed-true disjunction. right branch: signed true B at sigma	Signed false disjunction rule Signed-false disjunction rule. From signed false A or B at sigma, continue the same branch with signed false A at sigma and signed false B at sigma. Step 1. No premises. Rule: source premise. premise: signed false A or B at sigma Step 2. Depends on step 1. Rule: signed-false disjunction. first same-branch conclusion: signed false A at sigma Step 3. Depends on step 1. Rule: signed-false disjunction. second same-branch conclusion: signed false B at sigma

source 22

The closure condition is similar to that for ordinary tableaux, although we require that not just the formulas, but also that the prefixes must match. In fact, we can be somewhat more liberal: Since in intuitionistic models, formulas, once true, remain true, it is impossible that $!A$ source is true at $\sigma$ source but false at any accessible prefix $\sigma.{*}$ source. 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. Note that if the signs are reversed, i.e., if it contains

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

source

the branch is closed only if $*$ source is the empty sequence.

In addition, a branch is closed if it contains $\sFmla{\True}{\bot}[\sigma]$ 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 conditional $\lif$ source, the rules differ from the classical and modal cases. The $\TRule{\lif}{\True}$ source rule extends a branch containing $\sFmla{\True}{!A \lif !B}[\sigma]$ source by $\sFmla{\True}{!A}[\sigma.{*}]$ source and $\sFmla{\False}{!B}[\sigma.{*}]$ source on two different branches. It can only be applied for a prefix $\sigma.{*}$ source which already occurs on the branch in which it is applied. Let's call such a prefix “used” (on the branch). (Since $\sigma.{*}$ source includes $\sigma$ source itself, the rule can always be applied by adding the prefixed signed formulas $\sFmla{\True}{!A}[\sigma]$ source and $\sFmla{\False}{!B}[\sigma]$ source on separate branches.)

The $\TRule{\lif}{\False}$ source rule extends a branch containing $\sFmla{\False}{!A \lif !B}[\sigma]$ source by both $\sFmla{\True}{!A}[\sigma.n]$ source and $\sFmla{\False}{!B}[\sigma.n]$ source on the same branch, with $\sigma.n$ source a prefix new to the branch.

The rules for $\lnot$ source are defined analogously (using the definition of $\lnot !A$ source as $!A \lif \lfalse$ source).

The rules are given in the prefixed negation and conditional rule table.

Prefixed negation and conditional rule table

Four prefixed tableau rules, read across each source row. Row one left, signed true not A at sigma yields signed false A at used accessible prefix sigma dot star. Row one right, signed false not A at sigma yields signed true A at a new prefix sigma dot n. Row two left, signed true if A then B at sigma branches to signed false A or signed true B at a used accessible prefix sigma dot star. Row two right, signed false if A then B at sigma yields signed true A and then signed false B at a new prefix sigma dot n. End of rule table. Caption connective labels, in source order: negation, then conditional. End of 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.n]} \DisplayProof \\[1ex] \text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\ \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.n]} \noLine \UnaryInfC{\sFmla{\False}{!B}[\sigma.n]} \DisplayProof \\[1ex] \text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\ \hline \end{array}

source

\lnot

source

\lif

source

Prefixed negation and conditional rule table
signed-true rule	signed-false rule
Signed true negation rule Signed-true negation rule. From signed true not A at sigma, add signed false A at an already used accessible prefix sigma dot star. Step 1. No premises. Rule: source premise. premise: signed true not A at sigma Step 2. Depends on step 1. Rule: signed-true negation. conclusion: signed false A at a used accessible prefix sigma dot star	Signed false negation rule Signed-false negation rule. From signed false not A at sigma, add signed true A at a new prefix sigma dot n. Step 1. No premises. Rule: source premise. premise: signed false not A at sigma Step 2. Depends on step 1. Rule: signed-false negation. conclusion: signed true A at a new prefix sigma dot n
Signed true conditional rule Signed-true conditional rule. From signed true if A then B at sigma, split at an already used accessible prefix sigma dot star: left signed false A, right signed true B. Step 1. No premises. Rule: source premise. premise: signed true if A then B at sigma Step 2. Depends on step 1. Rule: signed-true conditional. left branch: signed false A at a used accessible prefix sigma dot star Step 3. Depends on step 1. Rule: signed-true conditional. right branch: signed true B at a used accessible prefix sigma dot star	Signed false conditional rule Signed-false conditional rule. From signed false if A then B at sigma, continue the same branch at a new prefix sigma dot n with signed true A and signed false B. Step 1. No premises. Rule: source premise. premise: signed false if A then B at sigma Step 2. Depends on step 1. Rule: signed-false conditional. first same-branch conclusion: signed true A at a new prefix sigma dot n Step 3. Depends on step 1. Rule: signed-false conditional. second same-branch conclusion: signed false B at the same new prefix sigma dot n

source 110

tableau for Intuitionistic Logic

Example closed intuitionistic tableau

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

Closed tableau for conditional currying

Closed tableau. Assumption one: signed true, if both A and B then C, at prefix one. Assumption two: signed false, if A then if B then C, at prefix one. By the signed-false conditional rule on node two: signed true A at prefix one dot one, then signed false, if B then C, at prefix one dot one. By the signed-false conditional rule on node four: signed true B at prefix one dot one dot one, then signed false C at prefix one dot one dot one. The signed-true conditional rule on node one splits from node six. One continuation is signed false, A and B, at prefix one dot one dot one, which branches by the signed-false conjunction rule on node four to signed false A at prefix one dot one dot one, closing against node three, or signed false B at prefix one dot one dot one, closing against node five. The other continuation is signed true C at prefix one dot one dot one, closing against node six. All three branches are closed. End of tableau.

Node 1. $\pFmla{\True}{(\formula{A} \land \formula{B}) \lif \formula{C}}{1}$ source Rule: assumption. Parents: none.
Node 2. $\pFmla{\False}{\formula{A} \lif (\formula{B} \lif \formula{C})}{1}$ source Rule: assumption. Parents: tab-n1.
Node 3. $\pFmla{\True}{\formula{A}}{1.1}$ source Rule: signed-false conditional from node two. Parents: tab-n2.
Node 4. $\pFmla{\False}{\formula{B} \lif \formula{C}}{1.1}$ source Rule: signed-false conditional from node two. Parents: tab-n3.
Node 5. $\pFmla{\True}{\formula{B}}{1.1.1}$ source Rule: signed-false conditional from node four. Parents: tab-n4.
Node 6. $\pFmla{\False}{\formula{C}}{1.1.1}$ source Rule: signed-false conditional from node four. Parents: tab-n5.
Node 7. $\pFmla{\False}{\formula{A} \land \formula{B}}{1.1.1}$ source Rule: signed-true conditional from node one, false-antecedent branch. Parents: tab-n6.
Node 8. $\pFmla{\False}{\formula{A}}{1.1.1}$ source Rule: signed-false conjunction from node seven, left branch. Parents: tab-n7.
Node 9. $\pFmla{\False}{\formula{B}}{1.1.1}$ source Rule: signed-false conjunction from node seven, right branch. Parents: tab-n7.
Node 10. $\pFmla{\True}{\formula{C}}{1.1.1}$ source Rule: signed-true conditional from node one, true-consequent branch. Parents: tab-n6.

closed branch; nodes tab-n1, tab-n2, tab-n3, tab-n4, tab-n5, tab-n6, tab-n7, tab-n8; closure witnesses tab-n3, tab-n8.
closed branch; nodes tab-n1, tab-n2, tab-n3, tab-n4, tab-n5, tab-n6, tab-n7, tab-n9; closure witnesses tab-n5, tab-n9.
closed branch; nodes tab-n1, tab-n2, tab-n3, tab-n4, tab-n5, tab-n6, tab-n10; closure witnesses tab-n6, tab-n10.

source 16

Exercise constructing four intuitionistic tableaux

Find closed intuitionistic tableaux to show the following:

$\Proves !A \lif (!B \lif !A)$ source
$\Proves \lnot(!A \land \lnot !A)$ source
$!A \lif (!B \lif !C) \Proves (!A \land !B) \lif !C$ source
$\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)$ source

Soundness for Intuitionistic tableau

Explain

In order to show that intuitionistic 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 relational and prefixes. With that in hand, however, the proof is straightforward.

Definition of an interpretation of prefixes

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.

Note that since $R$ source is reflexive and transitive and $\sigma.{*}$ source denotes, $\sigma$ source, $\sigma.n_1$ source, $\sigma.n_1.n_2$ source, dots, we also have that $Rf(\sigma)f(\sigma.{*})$ source.

Definition of satisfiable prefixed formulas

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.

Closure configurations 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, or it contains $\sFmla{\True}{\lfalse}[\sigma]$ source, then $\Gamma$ source is unsatisfiable.

Proof

Since always $\mSat/{M}{\lfalse}[f(\sigma)]$ source, a $\Gamma$ source that contains $\sFmla{\True}{\lfalse}$ source is unsatisfiable.

There also cannot be a model $\mModel{M}$ source and interpretation $f$ source of $P(\Gamma)$ source such that both If $\mSat{M}{!A}[f(\sigma)]$ source, then by the earlier proposition that intuitionistic truth persists along accessibility, since $Rf(\sigma)(\sigma.{*})$ source, $\mSat{M}{!A}[f(\sigma)]$ source. So we cannot have both $\mSat{M}{!A}[f(\sigma)]$ source and $\mSat/{M}{!A}[f(\sigma.{*})]$ source.

Soundness theorem for intuitionistic 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.

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}[w]$ source for any $w$ source such that $Rf(\sigma)w$ source, and that includes $f(\sigma.{*})$ source. So, $\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.n]$ source and $\sFmla{\False}{!C}[\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 $\mModel{M}$ source and interpretation $f$ source of $P(\Gamma)$ source such that $\mSat{M}{\Gamma}[f]$ source, in particular $\mSat/{M}{!B \lif !C}[f(\sigma)]$ source. We have to show that $\Gamma \cup \{\sFmla{\False}{!B \lif !C}[\sigma.n]\}$ source is satisfiable. To do this, we define an interpretation of $P(\Gamma) \cup \{\sigma.n\}$ source as follows:
Since $\mSat/{M}{!B \lif !C}[f(\sigma)]$ source, there is a $w \in W$ source such that $Rf(\sigma)w$ source such that $\mSat{M}{!B}[w]$ source and $\mSat/{M}{!C}[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 and $\mSat/{M}{!C}[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 \lif !C}[\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 the tableau soundness proof

Complete the proof of the intuitionistic tableau soundness theorem.

Soundness corollary for provability and entailment

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 intuitionistic 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.

Source disclosures

TR062-SAR-005: Source diagram caveat. Both false-conjunction steps are labelled as coming from node four in the printed tableau. Node four is a conditional; the conjunction being expanded is at node seven. The continuous reading retains the printed label, while the structural dependency links identify node seven. source
TR062-SAR-001: Source proof caveat. The stated contrapositive calls this a countermodel, so its last satisfaction sign should be negative, but the source prints that A is satisfied. The original formula is retained. source
TR062-SAR-002: Source proof caveat. Monotonicity should carry A from f of sigma to f of sigma dot star, but the source repeats f of sigma in the consequent. The original formula is retained. source
TR062-SAR-003: Source proof caveat. The false-conditional tableau rule adds signed true B and signed false C at the new prefix, while the proof twice names instead a signed-false conditional at that prefix. The printed target set is retained. source
TR062-SAR-004: Source proof caveat. This proof begins by assuming Gamma does not entail A and derives a contradiction, so its final conclusion should be that Gamma entails A; the source instead repeats Gamma proves A. The original sentence is retained. source

Reading preferences

Source file content/intuitionistic-logic/tableaux/tableaux.tex

Editorial

Source file content/intuitionistic-logic/tableaux/introduction.tex

Introduction

Source file content/intuitionistic-logic/tableaux/rules.tex

Rules for Intuitionistic Logic

Prefixed conjunction and disjunction rule table

Signed true conjunction rule

Signed false conjunction rule

Signed true disjunction rule

Signed false disjunction rule

Prefixed negation and conditional rule table

Signed true negation rule

Signed false negation rule

Signed true conditional rule

Signed false conditional rule

Source file content/intuitionistic-logic/tableaux/proofs.tex

tableau for Intuitionistic Logic

Example closed intuitionistic tableau

Closed tableau for conditional currying

Exercise constructing four intuitionistic tableaux

Source file content/intuitionistic-logic/tableaux/soundness.tex

Soundness for Intuitionistic tableau

Explain

Definition of an interpretation of prefixes

Definition of satisfiable prefixed formulas

Closure configurations are unsatisfiable

Proof

Soundness theorem for intuitionistic tableaux

Proof

Exercise completing the tableau soundness proof

Soundness corollary for provability and entailment

Proof

Weak soundness corollary

Source disclosures