blob: efd9ff3d593ca8b9d65567986f6208423d9b40a3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
\import{set.tex}
\import{nat.tex}
\begin{datatype}\label{propform}
%! infixr 0
Define $\propform$ inductively as follows.
\begin{enumerate}
\item $\propbot \in \propform$.
\item $\propvar{n} \in \propform$ for $n \in \naturals$.
\item $(p \propto q) \in \propform$ for $p \in \propform$ and $q \in \propform$.
\end{enumerate}
\end{datatype}
\begin{abbreviation}\label{propnot}
$\propnot{p} = (p \propto \propbot)$.
\end{abbreviation}
\begin{proposition}\label{propform_bot_intro}
$\propbot \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propbot_intro}.
\end{proof}
\begin{proposition}\label{propform_var_intro}
Suppose $n \in \naturals$.
Then $\propvar{n} \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propvar_intro}.
\end{proof}
\begin{proposition}\label{propform_imp_intro}
Suppose $p \in \propform$ and $q \in \propform$.
Then $(p \propto q) \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propto_intro}.
\end{proof}
\begin{proposition}\label{propnot_intro}
Suppose $p \in \propform$.
Then $\propnot{p} \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_propbot_intro,propform_propto_intro}.
\end{proof}
\begin{proposition}\label{propform_induction_sanity}
For every $x \in \propform$ we have $x \in \propform$.
\end{proposition}
\begin{proof}
Follows by \cref{propform_induct,propform_propbot_intro,propform_propvar_intro,propform_propto_intro}.
\end{proof}
% Predicate-level inductive derivability remains pending support for
% inductively defined predicates.
%\begin{inductive}\label{propcalc}
% \begin{enumerate}
% \item (Detachment) If $\deducible{p}$ and $\deducible{p\propto q}$, then $\deducible{q}$.
% \item (Implosion) $\deducible{p\propto q\propto p}$.
% \item (Chain) $\deducible{(p\propto q\propto r)\propto(p\propto q)\propto(p\propto r)}$.
% \item (Negation) $\propnot{\propnot{p}} \propto p$.
% \end{enumerate}
%\end{inductive}
%
%\begin{lemma}\label{weaken}
% Suppose $\deducible{q}$.
% Then $\deducible{p\propto q}$.
%\end{lemma}
|
