Skip to content

Commit 418ecb0

Browse files
rzachrzach
committed
add tableaux to intuitionistic logic
1 parent 48a9272 commit 418ecb0

File tree

6 files changed

+512
-6
lines changed

6 files changed

+512
-6
lines changed

‎content/intuitionistic-logic/intuitionistic-logic.tex‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,18 +6,14 @@
66

77
\olpart{int}{Intuitionistic Logic}
88

9-
\begin{editorial}
10-
This is a brief introduction to intuitionistic logic produced by
11-
Zesen Qian and revised by RZ. It is not yet well integrated with the
12-
rest of the text and needs examples and motivations.
13-
\end{editorial}
14-
159
\olimport[introduction]{introduction}
1610

1711
\olimport[semantics]{semantics}
1812

1913
\olimport[soundness-completeness]{soundness-completeness}
2014

15+
\olimport[tableaux]{tableaux}
16+
2117
\olimport[propositions-as-types]{propositions-as-types}
2218

2319
\OLEndPartHook

‎content/intuitionistic-logic/tableaux/introduction.tex‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
% Part: intuitionistic-logic
2+
% Chapter: tableaux
3+
% Section: introduction
4+
5+
\documentclass[../../../../include/open-logic-section]{subfiles}
6+
7+
\begin{document}
8+
9+
\olfileid{int}{tab}{int}
10+
11+
\olsection{Introduction}
12+
13+
!!^{tableau}s are certain (downward-branching) trees of !!{signed
14+
formula}s, i.e., pairs consisting of a truth value sign ($\True$ or
15+
$\False$) and !!a{sentence}
16+
\[
17+
\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.
18+
\]
19+
!!^a{tableau} begins with a number of \emph{assumptions}. Each further
20+
!!{signed formula} is generated by applying one of the inference
21+
rules. Some inference rules add one or more !!{signed formula}s to a
22+
tip of the tree; others add two new tips, resulting in two branches.
23+
Rules result in !!{signed formula}s where the !!{formula} is
24+
less complex than that of the !!{signed formula} to which it was
25+
applied. When a branch contains both $\sFmla{\True}{!A}$ and
26+
$\sFmla{\False}{!A}$, we say the branch is \emph{closed}. If every
27+
branch in !!a{tableau} is closed, the entire !!{tableau} is closed. A
28+
closed !!{tableau} constitutes !!a{derivation} that shows that the set
29+
of !!{signed formula}s which were used to begin the !!{tableau} are
30+
unsatisfiable. This can be used to define a $\Proves$ relation:
31+
$\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1,
32+
\dots, !B_n\} \subseteq \Gamma$ such that there is a closed
33+
!!{tableau} for the assumptions
34+
\[
35+
\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.
36+
\]
37+
38+
For intuitionistic logic, we have to both extend the notion of
39+
!!{signed formula} and adjust the rules for the connectives. In
40+
addition to a sign($\True$ or $\False$), !!{formula}s in modal
41+
!!{tableau}s also have \emph{prefixes}~$\sigma$. The prefixes are
42+
non-empty sequences of positive integers, i.e., $\sigma \in
43+
(\PosInt)^* \setminus \{\emptyseq\}$. When we write such prefixes
44+
without the surrounding $\tuple{\ }$, and separate the individual
45+
!!{element}s by~$.$'s instead of $,$'s. If $\sigma$ is a prefix, then
46+
$\sigma.n$ is $\sigma \concat \tuple{n}$; e.g., if $\sigma = 1.2.1$,
47+
then $\sigma.3$ is $1.2.1.3$. So for instance,
48+
\[
49+
\sFmla{\True}{!A \lif (!B \lif !C)}[1.2]
50+
\]
51+
is a \emph{prefixed !!{signed formula}} (or just a \emph{prefixed
52+
!!{formula}} for short).
53+
54+
Intuitively, the prefix names a world in a model that might satisfy
55+
the !!{formula}s on a branch of !!a{tableau}, and if $\sigma$ names
56+
some world, then $\sigma.n$ names a world accessible from (the world
57+
named by)~$\sigma$.
58+
59+
In intuitionistic models, the accessibility relation is reflexive and
60+
transitive. In terms of prefixes, this means that $\sigma$ is
61+
accessible from $\sigma$ itself, and so is any prefix that
62+
extends~$\sigma$, i.e., any prefix of the form
63+
$\sigma.n_1.\cdots.n_k$. Let's introduce the notation $\sigma.*$ to
64+
indicate $\sigma$ itself and any extension of it. In other words, the
65+
prefixes $\sigma.*$ are all and only the prefixes accessible
66+
from~$\sigma$.
67+
68+
\end{document}

‎content/intuitionistic-logic/tableaux/proofs.tex‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
% Part: intuitionistic-logic
2+
% Chapter: tableaux
3+
% Section: proofs
4+
5+
\documentclass[../../../include/open-logic-section]{subfiles}
6+
7+
\begin{document}
8+
9+
\olfileid{int}{tab}{prf}
10+
11+
\olsection{\usetoken{P}{tableau} for Intuitionistic Logic}
12+
13+
\begin{ex}
14+
We give a closed tableau that shows $(!A \land !B) \lif !C \Proves
15+
!A \lif (!B \lif !C)$.
16+
\begin{oltableau}
17+
[\pFmla{\True}{(\formula{A} \land \formula{B}) \lif \formula{C}}{1},
18+
just =\TAss
19+
[\pFmla{\False}{\formula{A} \lif (\formula{B} \lif \formula{C})}{1},
20+
just =\TAss
21+
[\pFmla{\True}{\formula{A}}{1.1},
22+
just = {\TRule{\False}{\lif}[2]}
23+
[\pFmla{\False}{\formula{B} \lif \formula{C}}{1.1},
24+
just = {\TRule{\False}{\lif}[2]}
25+
[\pFmla{\True}{\formula{B}}{1.1.1},
26+
just = {\TRule{\False}{\lif}[4]}
27+
[\pFmla{\False}{\formula{C}}{1.1.1},
28+
just = {\TRule{\False}{\lif}[4]}
29+
[\pFmla{\False}{\formula{A} \land \formula{B}}{1.1.1},
30+
just = {\TRule{\True}{\lif}[1]}
31+
[\pFmla{\False}{\formula{A}}{1.1.1},
32+
just= {\TRule{\False}{\land}[4]}, close]
33+
[\pFmla{\False}{\formula{B}}{1.1.1},
34+
just= {\TRule{\False}{\land}[4]}, close]]
35+
[\pFmla{\True}{\formula{C}}{1.1.1},
36+
just = {\TRule{\True}{\lif}[1]}, close]]
37+
]
38+
]
39+
]
40+
]
41+
]
42+
]
43+
\end{oltableau}
44+
\end{ex}
45+
46+
47+
48+
\begin{prob}
49+
Find closed intuitionistic !!{tableau}s to show the following:
50+
\begin{enumerate}
51+
\item $\Proves !A \lif (!B \lif !A)$
52+
\item $\Proves \lnot(!A \land \lnot !A)$
53+
\item $!A \lif (!B \lif !C) \Proves (!A \land !B) \lif !C$
54+
\item $\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)$
55+
\end{enumerate}
56+
\end{prob}
57+
58+
\end{document}

‎content/intuitionistic-logic/tableaux/rules.tex‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
% Part: intuitionistic-logic
2+
% Chapter: tableaux
3+
% Section: rules
4+
5+
\documentclass[../../../include/open-logic-section]{subfiles}
6+
7+
\begin{document}
8+
9+
\olfileid{int}{tab}{rul}
10+
11+
\olsection{Rules for Intuitionistic Logic}
12+
13+
The rules for the connectives $\land$ and $\lor$ are the same as for
14+
regular propositional signed !!{tableau}s, just with prefixes added.
15+
In each case, the rule applied to a signed !!{formula}
16+
$\sFmla{S}{!A}[\sigma]$ produces new !!{formula}s that are also
17+
prefixed by~$\sigma$. This should be intuitively clear: e.g., if $!A
18+
\land !B$ is true at (a world named by)~$\sigma$, then $!A$ and $!B$
19+
are true at~$\sigma$ (and not at any other world). We collect the
20+
rules for $\land$ and $\lor$ in \olref{tab:prop-rules}.
21+
22+
\begin{table}
23+
\[\def\arraystretch{3}\begin{array}{|c|c|}
24+
\hline
25+
\AxiomC{\sFmla{\True}{!A \land !B}[\sigma]}
26+
\RightLabel{\TRule{\True}{\land}}
27+
\UnaryInfC{\sFmla{\True}{!A}[\sigma]}
28+
\noLine
29+
\UnaryInfC{\sFmla{\True}{!B}[\sigma]}
30+
\DisplayProof
31+
&
32+
\AxiomC{\sFmla{\False}{!A \land !B}[\sigma]}
33+
\RightLabel{\TRule{\False}{\land}}
34+
\UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad
35+
\sFmla{\False}{!B}[\sigma]$}
36+
\DisplayProof
37+
\\[2ex]
38+
\hline
39+
\AxiomC{\sFmla{\True}{!A \lor !B}[\sigma]}
40+
\RightLabel{\TRule{\True}{\lor}}
41+
\UnaryInfC{$\sFmla{\True}{!A}[\sigma] \quad \mid \quad
42+
\sFmla{\True}{!B}[\sigma]$}
43+
\DisplayProof
44+
&
45+
\AxiomC{\sFmla{\False}{!A \lor !B}[\sigma]}
46+
\RightLabel{\TRule{\False}{\lor}}
47+
\UnaryInfC{\sFmla{\False}{!A}[\sigma]}
48+
\noLine
49+
\UnaryInfC{\sFmla{\False}{!B}[\sigma]}
50+
\DisplayProof
51+
\\[2ex]
52+
\hline
53+
\end{array}\]
54+
\caption{Prefixed !!{tableau} rules for $\land$ and $\lor$}
55+
\ollabel{tab:prop-rules}
56+
\end{table}
57+
58+
The closure condition is similar to that for ordinary !!{tableau}s,
59+
although we require that not just the !!{formula}s, but also that the
60+
prefixes must match. In fact, we can be somewhat more liberal: Since
61+
in intuitionistic models, !!{formula}s, once true, remain true, it is
62+
impossible that $!A$ is true at~$\sigma$ but false at any accessible
63+
prefix~$\sigma.{*}$. So a branch is closed if it contains both
64+
\[
65+
\sFmla{\True}{!A}[\sigma] \quad\text{and}\quad \sFmla{\False}{!A}[\sigma.{*}]
66+
\]
67+
for some prefix $\sigma$ and !!{formula}~$!A$. Note that if the signs
68+
are reversed, i.e., if it contains
69+
\[
70+
\sFmla{\False}{!A}[\sigma] \quad\text{and}\quad \sFmla{\True}{!A}[\sigma.{*}]
71+
\]
72+
the branch is closed only if $*$ is the empty sequence.
73+
74+
In addition, a branch is closed if it contains~$\sFmla{\True}{\bot}[\sigma]$.
75+
76+
The rules for setting up assumptions is also as for ordinary
77+
!!{tableau}s, except that for assumptions we always use the
78+
prefix~$1$. (It does not matter which prefix we use, as long as it's
79+
the same for all assumptions.) So, e.g., we say that
80+
\[
81+
!B_1, \dots, !B_n \Proves !A
82+
\]
83+
iff there is a closed tableau for the assumptions
84+
\[
85+
\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1],
86+
\sFmla{\False}{!A}[1].
87+
\]
88+
89+
For the conditional~$\lif$, the rules differ from the classical and
90+
modal cases. The $\TRule{\lif}{\True}$ rule extends a branch
91+
containing $\sFmla{\True}{!A \lif !B}[\sigma]$ by
92+
$\sFmla{\True}{!A}[\sigma.{*}]$ and $\sFmla{\False}{!B}[\sigma.{*}]$ on two
93+
different branches. It can only be applied for a prefix~$\sigma.{*}$
94+
which \emph{already} occurs on the branch in which it is applied.
95+
Let's call such a prefix ``used'' (on the branch). (Since $\sigma.{*}$
96+
includes $\sigma$ itself, the rule can always be applied by adding the
97+
prefixed signed formulas $\sFmla{\True}{!A}[\sigma]$ and
98+
$\sFmla{\False}{!B}[\sigma]$ on separate branches.)
99+
100+
The $\TRule{\lif}{\False}$ rule extends a branch containing
101+
$\sFmla{\False}{!A \lif !B}[\sigma]$ by both
102+
$\sFmla{\True}{!A}[\sigma.n]$ and $\sFmla{\False}{!B}[\sigma.n]$ on
103+
the same branch, with $\sigma.n$ a prefix new to the branch.
104+
105+
The rules for $\lnot$ are defined analogously (using the definition of
106+
$\lnot !A$ as $!A \lif \lfalse$).
107+
108+
The rules are given in \olref{tab:rules-lif-lnot}.
109+
110+
\begin{table}
111+
\[\def\arraystretch{3}\begin{array}{|c|c|}
112+
\hline
113+
\AxiomC{\sFmla{\True}{\lnot !A}[\sigma]}
114+
\RightLabel{\TRule{\True}{\lnot}}
115+
\UnaryInfC{$\sFmla{\False}{!A}[\sigma.{*}]$}
116+
\DisplayProof
117+
&
118+
\AxiomC{\sFmla{\False}{\lnot !A}[\sigma]}
119+
\RightLabel{\TRule{\False}{\lnot}}
120+
\UnaryInfC{\sFmla{\True}{!A}[\sigma.n]}
121+
\DisplayProof
122+
\\[1ex]
123+
\text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\
124+
\hline
125+
\AxiomC{\sFmla{\True}{!A \lif !B}[\sigma]}
126+
\RightLabel{\TRule{\True}{\lif}}
127+
\UnaryInfC{$\sFmla{\False}{!A}[\sigma.{*}] \quad \mid \quad
128+
\sFmla{\True}{!B}[\sigma.{*}]$}
129+
\DisplayProof
130+
&
131+
\AxiomC{\sFmla{\False}{!A \lif !B}[\sigma]}
132+
\RightLabel{\TRule{\False}{\lif}}
133+
\UnaryInfC{\sFmla{\True}{!A}[\sigma.n]}
134+
\noLine
135+
\UnaryInfC{\sFmla{\False}{!B}[\sigma.n]}
136+
\DisplayProof
137+
\\[1ex]
138+
\text{$\sigma.{*}$ is used} & \text{$\sigma.n$ is new}\\
139+
\hline
140+
\end{array}\]
141+
\caption{Prefixed !!{tableau} rules for $\lnot$ and $\lif$}
142+
\ollabel{tab:rules-lif-lnot}
143+
\end{table}
144+
145+
\end{document}

0 commit comments

Comments
 (0)