1: \subsection{The properties of $\lii$}
2:
3: We now proceed with a standard sequence of lemmas for $\lii$.
4:
5: \begin{lemma}[Canonical Forms]
6: Suppose $M$ is a value and $\proves M : \vartheta$. Then:
7: \begin{enumerate}[$\bullet$]
8: \item $\vartheta = t \ini t_A(\ov{u})$ iff $M = \pl{axRep}(t, \ov{u}, N)$ and $\p N : \phi_A(t, \ov{u})$.
9: \item $\vartheta = \phi \lor \psi$ iff ($M = \INL(N)$ and $\p N : \phi$) or ($M =
10: \INR(N)$ and $\p N : \psi$).
11: \item $\vartheta = \phi \land \psi$ iff $M = <N, O>$, $\p N : \phi$ and $\p
12: O : \psi$.
13: \item $\vartheta = \phi \to \psi$ iff $M = \lambda x : \phi.\ N$ and $x :
14: \phi \p N : \psi$.
15: \item $\vartheta = \forall a.\ \phi$ iff $M = \lambda a.\ N$ and $\p N :
16: \phi$.
17: \item $\vartheta = \exists a.\ \phi$ iff $M = [t, N]$ and $\p N : \phi[a:=t]$.
18: \item $\vartheta = \bot$ never happens.
19: \end{enumerate}
20: \end{lemma}
21: \begin{proof}
22: Immediate from the typing rules and the definition of values.
23: \end{proof}
24:
25: \begin{lemma}[Weakening]
26: If $\gp M : \phi$ and $FV(\psi) \cup \{ x \}$ are fresh to the proof tree $\gp M : \phi$, then $\g, x : \psi \p M : \phi$.
27: \end{lemma}
28: \begin{proof}
29: Straightforward induction on $\gp M : \phi$.
30: \end{proof}
31:
32: There are two substitution lemmas, one for the propositional part, the other
33: for the first-order part of the calculus. Since the rules and terms of $\lii$
34: corresponding to \izfio\ axioms do not interact with substitutions in a
35: significant way, the proofs are routine.
36:
37: \begin{lemma}\label{lamsl}
38: If $\Gamma, x : \phi \proves M : \psi$ and $\Gamma \proves N : \phi$, then
39: $\Gamma \proves M[x:=N] : \psi$.
40: \end{lemma}
41: \proof %\begin{proof}
42: By induction on $\g, x : \phi \p M : \psi$. We show two interesting cases.
43: \begin{enumerate}[$\bullet$]
44: \item $\psi = \psi_1 \to \psi_2$, $M = \lambda y : \psi_1.\ O$. Using $\alpha$-conversion
45: we can choose $y$ to be new, so that $y \notin FV(\g, x) \cup FV(N)$. The
46: proof tree must end with:
47: \[
48: \infer{\g, x : \phi \p \lambda y : \psi_1.\ O : \psi_1 \to \psi_2}{\g, x :
49: \phi, y : \psi_1 \p O : \psi_2}
50: \]
51: By the inductive hypothesis, $\g, y : \psi_1 \p O[x:=N] : \psi_2$, so $\g \p \lambda y : \psi_1.\ O[x:=N] : \psi_1
52: \to \psi_2$. By the choice of $y$, $\gp (\lambda y : \psi_1.\ O)[x:=N] :
53: \psi_1 \to \psi_2$.
54: \item $\psi = \psi_2, M = \LET\ [a, y : \psi_1] := M_1\ \IN\ M_2$. The proof tree ends with:
55: \[
56: \infer{\g, x : \phi \p \LET\ [a, y : \psi_1] := M_1\ \IN\
57: M_2 : \psi_2}{\g, x : \phi \p M_1 : \exists a.\ \psi_1 & \g, x : \phi, y : \psi_1 \p M_2
58: : \psi_2}
59: \]
60: Choose $a$ and $y$ to be fresh. By the inductive hypothesis, $\gp M_1[x:=N] : \exists a.\ \psi_1$ and $\g, y
61: : \psi_1 \p M_2[x:=N] : \psi_2$. Thus $\gp \LET\ [a, y : \psi_1] :=
62: M_1[x:=N]\ \IN\ M_2[x:=N] : \psi_2$. By $a$ and $y$ fresh, $\gp (\LET\ [a, y : \psi_1] :=
63: M_1\ \IN\ M_2)[x:=N] : \psi_2$ which is what we want.\qed
64: \end{enumerate}
65: %\end{proof}
66:
67: \begin{lemma}\label{logsl}
68: If $\gp M : \phi$, then $\Gamma[a:=t] \proves M[a:=t] : \phi[a:=t]$.
69: \end{lemma}
70: \proof %\begin{proof}
71: By induction on $\gp M : \phi$. Most of the rules do not interact with
72: first-order substitution, so we will show the proof just for two of them which
73: do.
74: \begin{enumerate}[$\bullet$]
75: \item $\phi = \forall b.\ \phi_1$, $M = \lambda b.\ M_1$. The proof tree ends with:
76: \[
77: \infer[b \notin FV_F(\g)]{\gp \lambda b.\ M_1 : \forall b.\ \phi_1}{\g \proves M_1 : \phi_1}
78: \]
79: Without loss of generality we can assume that $b \notin FV(t) \cup \{ a \}$. By the inductive hypothesis, $\Gamma[a:=t] \proves M_1[a:=t] :
80: \phi_1[a:=t]$. Therefore $\g[a:=t] \p \lambda b.\ M_1[a:=t] : \forall
81: b.\ \phi_1[a:=t]$ and by the choice of $b$, $\g[a:=t] \p (\lambda b.\ M_1)[a:=t] \p (\forall b.\ \phi_1)[a:=t]$.
82: \item $\phi = \phi_1[b:=u]$, $M = M_1\ u$ for some term $u$. The proof tree ends with:
83: \[
84: \infer{\gp M_1\ u : \phi_1[b:=u]}{\gp M_1 : \forall b.\ \phi_1}
85: \]
86: Choosing $b$ to be fresh, by the inductive hypothesis we get $\g[a:=t] \p
87: M_1[a:=t] : \forall b.\ (\phi_1[a:=t])$, so $\g[a:=t] \p M_1[a:=t]\ u[a:=t] :
88: \phi_1[a:=t][b:=u[a:=t]]$. By Lemma \ref{formsubst} and $b \notin FV(t)$, we
89: get $\g[a:=t] \p (M_1\ u)[a:=t] : \phi_1[b:=u][a:=t]$.\qed
90: \end{enumerate}
91: %\end{proof}
92:
93: With the lemmas at hand, Progress and Preservation follow easily:
94:
95: \begin{lemma}[Subject Reduction, Preservation]
96: If $\gp M : \phi$ and $M \to N$, then $\gp N : \phi$.
97: \end{lemma}
98: \begin{proof}
99: By induction on the definition of $M \to N$. We show several cases. Case $M
100: \to N$ of:
101: \begin{enumerate}[$\bullet$]
102: \item $(\lambda x : \phi_1.\ M_1)\ M_2 \to M_1[x:=M_2]$. The proof tree $\gp M
103: : \phi$ must end with:
104: \[
105: \infer{\gp (\lambda x : \phi_1.\ M_1)\ M_2 : \phi}
106: {
107: \infer
108: {
109: \gp \lambda x : \phi_1.\ M_1 : \phi_1 \to \phi
110: }
111: {
112: \g, x : \phi_1 \p M_1 : \phi
113: }
114: &
115: \gp M_2 : \phi_1
116: }
117: \]
118: By Lemma \ref{lamsl}, $\gp M_1[x:=M_2] : \phi_1$.
119: \item $\LET\ [a, x : \phi_1] := [t, M_1]\ \IN\ M_2 \to M_2[a:=t][x:=M_1]$. The
120: proof tree $\gp M : \phi$ must end with:
121: \[
122: \infer
123: {\gp \LET\ [a, x : \phi_1] := [t, M_1]\ \IN\ M_2 : \phi}
124: {
125: \infer{\gp [t, M_1] : \exists a.\ \phi_1}
126: {\gp M_1 : \phi_1[a:=t]}
127: &
128: \g, x : \phi_1 \proves M_2 : \phi
129: }
130: \]
131: Choose $a$ to be fresh. Thus $M_1[a:=t] = M_1$ and $\g[a:=t] = \g$. By the side-condition of the last
132: typing rule, $a \notin FV(\phi)$, so $\phi[a:=t] = \phi$. By Lemma
133: \ref{logsl} we get $\g[a:=t], x : \phi_1[a:=t] \p M_2[a:=t] : \phi[a:=t]$,
134: so also $\g, x : \phi_1[a:=t] \p M_2[a:=t] : \phi$. By Lemma \ref{lamsl}, we
135: get $\gp M_2[a:=t][x:=M_1] : \phi$.
136: \item $\pl{axProp}(t, \ov{u}, \pl{axRep}(t, \ov{u}, M_1)) \to M_1$.
137: The proof tree must end with:
138: \[
139: \infer{\gp \pl{axProp}(t, \ov{u}, \pl{axRep}(t, \ov{u}, M_1)) : \phi_A(t, \ov{u})}
140: {
141: \infer{\gp \pl{axRep}(t, \ov{u}, M_1)) : t \ini t_A(\ov{u})}{\gp M_1 :
142: \phi_A(t, \ov{u})}
143: }
144: \]
145: The claim follows immediately.
146: \item $\IND_{\psi(a, \ov{f})}(M_1, \ov{t}) \to \lambda c.\ M_1\ c\
147: (\lambda b. \lambda x : b \ini c.\ \IND_{\psi(a, \ov{b})}(M_1, \ov{t})\ b)$. The proof tree must end with:
148: \[
149: \infer{\gp \IND_{\psi(a, \ov{f})}(M_1, \ov{t}) : \forall a.\ \psi(a,
150: \ov{t})}{\gp M_1 : \forall c.\ (\forall b.\ b \ini c \to \psi(b, \ov{t})) \to \psi(c, \ov{t})}
151: \]
152: We choose $b, c, x$ to be fresh. By applying $\alpha$-conversion we can also obtain a proof
153: tree of $\gp M_1 : \forall e.\ (\forall d.\ d \ini e \to \psi(d, \ov{t}))
154: \to \psi(e, \ov{t})$, where $\{ d, e \} \cap \{ b, c \} = \emptyset$. Then
155: by Weakening we get $\g, x : b \ini c \p M_1 : \forall e.\ (\forall d.\ d
156: \ini e \to \psi(d, \ov{t})) \to \psi(e, \ov{t})$, so also $\g, x : b \ini c \p \IND_{\psi(a, \ov{b})}(M_1, \ov{t})
157: : \forall a.\ \psi(a, \ov{t})$. Let the proof tree $T$ be defined as:
158: \[
159: \infer{\gp \lambda b. \lambda x : b \ini c.\ \IND_{\psi(a,
160: \ov{b})}(M_1, \ov{t})\ b : \forall b.\ b \ini c \to \psi(b,
161: \ov{t})}
162: {
163: \infer{\gp \lambda x : b \ini c.\ \IND_{\psi(a,
164: \ov{b})}(M_1, \ov{t})\ b : b \ini c \to \psi(b,
165: \ov{t})}
166: {
167: \infer{\g, x : b \ini c \p \IND_{\psi(a, \ov{b})}(M_1,
168: \ov{t})\ b : \psi(b, \ov{t})}
169: {
170: \g, x : b \ini c \p \IND_{\psi(a, \ov{b})}(M_1, \ov{t})
171: : \forall a.\ \psi(a, \ov{t})
172: }
173: }
174: }
175: \]
176: Then the following proof tree shows the claim:
177: \[
178: \infer{\gp \lambda c.\ M_1\ c\ (\lambda b. \lambda x : b \ini c.\ \IND_{\psi(a,
179: \ov{b})}(M_1, \ov{t})\ b) : \forall c.\ \psi(c, \ov{t})}
180: {
181: \infer
182: {
183: \gp M_1\ c\ (\lambda b. \lambda x : b \ini c.\ \IND_{\psi(a,
184: \ov{b})}(M_1, \ov{t})\ b) : \psi(c, \ov{t})
185: }
186: {
187: \infer{\gp M_1\ c : (\forall b.\ b \ini c \to \psi(b, \ov{t})) \to \psi(c, \ov{t})}
188: {
189: \gp M_1 : \forall c.\ (\forall b.\ b \ini c \to \psi(b, \ov{t})) \to
190: \psi(c, \ov{t})
191: }
192: &
193: T
194: }
195: }
196: \]
197: \end{enumerate}
198: \end{proof}
199: \begin{lemma}[Progress]
200: If $\ \proves M : \phi$, then either $M$ is a value or there is $N$ such that $M \to N$.
201: \end{lemma}
202: \proof %\begin{proof}
203: Straightforward induction on the length of $M$. The proof proceeds by case analysis of $M$. We show several cases:
204: \begin{enumerate}[$\bullet$]
205: \item It is easy to see that the case $M = x$ cannot happen.
206: \item If $M = \lambda x : \phi.\ N$, then $M$ is a value.
207: \item If $M = N\ O$, then for some $\psi$, the proof must end with:
208: \[
209: \infer{\p N\ O : \phi}{\p N : \psi \to \phi & \p O : \psi}
210: \]
211: By the inductive hypothesis, either $N$ is a value or there is $N'$ such
212: that $N \to N'$. In the former case, by Canonical Forms for some $P$ we have $N = \lambda x :
213: \psi.\ P$, so $N\ O \to P[x:=O]$. In the latter case, $N\ O \to N'\ O$.
214: \item If $M = \pl{axRep}(t, \ov{u}, M)$, then $M$ is a value.
215: \item If $M = \pl{axProp}(t, \ov{u}, O)$, then we have the following proof tree:
216: \[
217: \infer{\p \pl{axProp}(t, \ov{u}, O) : \phi_A(t, \ov{u})}
218: {
219: \p O : t \ini t_A(\ov{u})
220: }
221: \]
222: By the inductive hypothesis, either $O$ is a value or there is $O_1$ such
223: that $O \to O_1$. In the former case, by Canonical Forms, $O = \pl{axRep}(t,
224: \ov{u}, P)$ and $M \to P$. In the latter, by the evaluation rules $\pl{axProp}(t,
225: \ov{u}, O) \to \pl{axProp}(t, \ov{u}, O_1)$.
226: \item The cases corresponding to the equality and membership axioms work in the same way.
227: \item The $\pl{ind}$ terms always reduce.\qed
228: \end{enumerate}
229: %\end{proof}
230:
231: \begin{corollary}\label{corlz}
232: If $\ \p M : \phi$ and $M \downarrow v$, then $\p v : \phi$ and $v$ is a value.
233: \end{corollary}
234:
235: \begin{corollary}\label{corbot}
236: If $\p M : \bot$, then $M$ does not normalize.
237: \end{corollary}
238: \begin{proof}
239: If $M$ normalized, then by Corollary \ref{corlz} we would have a value of
240: type $\bot$, which by Canonical Forms is impossible.
241: \end{proof}
242:
243: Finally, we state the formal correspondence between $\lii$ and \izfio:
244:
245: \begin{lemma}[Curry-Howard isomorphism]
246: If $\gp O : \phi$ then \izfio $ + rg(\g) \p \phi$, where $rg(\g) = \{
247: \phi\ |\ (x, \phi) \in \g \}$. If \izfio $+ \g \p \phi$, then there exists a term $M$ such that $\og \p M :
248: \phi$, where $\og = \{ (x_\phi, \phi)\ |\ \phi \in \g \}$.
249: \end{lemma}
250: \begin{proof}
251: Both parts follow by easy induction on the proof. The first part is
252: straightforward, to get the claim simply erase the lambda terms from the
253: proof tree. For the second part, we show terms and trees corresponding to \izfio\ axioms:
254: \begin{enumerate}[$\bullet$]
255: \item Let $\phi$ be one of the \izfio\ axioms apart from $\in$-Induction.
256: Then $\phi = \forall \ov{a}.\ \forall c.\ c \ini t_A(\ov{a}) \iffl \phi_A(c,
257: \ov{a})$ for the axiom (A) (incorporating axioms (IN) and (EQ) in this case
258: in the obvious way). Recall that $\phi_1 \iffl \phi_2$ is an
259: abbreviation for $(\phi_1 \to \phi_2) \land (\phi_2 \to \phi_1)$. Let $T$
260: be the following proof tree:
261: \[
262: \infer{\gp \lambda x : \phi_A(c, \ov{a}).\ \pl{axRep}(c, \ov{a}, x) : \phi_A(c, \ov{a}) \to c \ini t_A(\ov{a})}
263: {
264: \infer{\g, x : \phi_A(c, \ov{a}) \p \pl{axRep}(c, \ov{a}, x) : c \ini t_A(\ov{a})}
265: {
266: \g, x : \phi_A(c, \ov{a}) \p x : \phi_A(c, \ov{a})
267: }
268: }
269: \]
270: Let $M_1 = \lambda x : c \ini t_A(\ov{a}).\ \pl{axProp}(c, \ov{a}, x)$ and
271: let $M_2 = \lambda x : \phi_A(c, \ov{a}).\ \pl{axRep}(c, \ov{a}, x)$.
272: Then the following proof tree shows the claim:
273: \[
274: \infer{\gp \lambda \ov{a} \lambda c.\ <M_1,M_2>
275: : \forall
276: \ov{a}.\ \forall c.\ c \ini t_A(\ov{a}) \iffl \phi_A(c, \ov{a})}
277: {
278: \infer
279: {\gp <M_1, M_2> : c \ini t_A(\ov{a}) \iffl \phi_A(c, \ov{a})}
280: {
281: \infer
282: {
283: \gp M_1 : c \ini t_A(\ov{a}) \to \phi_A(c, \ov{a})
284: }
285: {
286: \infer{\g, x : c \ini t_A(\ov{a}) \p \pl{axProp}(c, \ov{a}, x) : \phi_A(c, \ov{a})}
287: {
288: \g, x : c \ini t_A(\ov{a}) \p x : c \ini t_A(\ov{a})
289: }
290: }
291: &
292: \qquad
293: T
294: }
295: }
296: \]
297: \item Let $\phi$ be the $\in$-induction axiom. Let
298: \[
299: M = \lambda \ov{f} \lambda x : (\forall a.
300: (\forall b.\ b \ini a \to \psi(b, \ov{f})) \to \psi(a, \ov{f})).\ \IND(x, \ov{f}).
301: \]
302: The following proof tree shows the claim:
303: \[
304: \infer{\gp M : \forall \ov{f}. (\forall a. (\forall b.\ b \ini a \to
305: \psi(b, \ov{f})) \to \psi(a, \ov{f})) \to \forall a.\ \psi(a, \ov{f})}
306: {
307: \infer{\g, x : \forall a. (\forall b.\ b \ini a \to \phi(b, \ov{f})) \to
308: \psi(a, \ov{f}) \p \IND_{\psi(a, \ov{f})}(x, \ov{f}) : \forall a.\ \psi(a, \ov{f})}
309: {
310: \g, x : \forall a. (\forall b.\ b \ini a \to \psi(b, \ov{f})) \to
311: \psi(a, \ov{f}) \p x : \forall a. (\forall b.\ b \ini a \to \psi(b, \ov{f})) \to
312: \psi(a, \ov{f})
313: }
314: }
315: \]
316: \end{enumerate}
317: \end{proof}
318:
319: Note that all proofs in this section are constructive and quite weak from
320: the proof-theoretic point of view --- Heyting Arithmetic should be
321: sufficient to formalize the arguments. However, by the Curry-Howard isomorphism
322: and Corollary \ref{corbot}, normalization of $\lii$ entails consistency of \izfio,
323: which easily interprets Heyting Arithmetic. Therefore a normalization
324: proof must utilize much stronger means, which we introduce in the following
325: section.
326: