1: \documentclass[envcountsame,orivec]{llncs}

2: \usepackage{proof}

3: \usepackage{amssymb}

4: \usepackage{fullpage}

5: \usepackage{graphics} %needed for the NEW quantifier

6: 

7: \newcommand{\NEW}{\reflectbox{\ensuremath{\mathsf{N}}}}

8: %\newcommand{\NEW}{{\ensuremath{\mathsf{N}}}}

9: \newcommand\New[1]{\NEW #1.}

10: 

11: \bibliographystyle{abbrv}

12: %\bibliographystyle{splncs}

13: 

14: \def\relbar{\mathrel{\smash-}}

15: \def\joinrelm{\mathrel{\mkern-3mu}}

16: \def\tailpiece{\kern 1pt\vrule height 1ex width 0.3ex depth -.3ex}

17: \def\seqsym{\mathrel{\tailpiece\joinrelm\relbar}}

18: \newcommand{\Seq}[2]{#1\seqsym #2}

19: \newcommand{\NSeq}[3]{#1 ; #2 \seqsym #3}

20: \newcommand{\TSeq}[3]{#1 \vdash #2 : #3}

21: \newcommand{\GSeq}[4]{#1;#2;#3 \seqsym #4}

22: \newcommand{\botL}{\bot{\cal L}}

23: \newcommand{\cL}{\hbox{\sl c}{\cal L}}

24: \newcommand{\defeq}{\stackrel{{\scriptstyle\triangle}}{=}}

25: \newcommand{\defL}{\hbox{\sl def}{\cal L}}

26: \newcommand{\defR}{\hbox{\sl def\/}{\cal R}}

27: \newcommand{\defmu}{\stackrel{\mu}{=}}

28: \newcommand{\eqL}{{\rm eq}{\cal L}}

29: \newcommand{\eqR}{{\rm eq}{\cal R}}

30: \newcommand{\existsL}{\exists{\cal L}}

31: \newcommand{\existsR}{\exists{\cal R}}

32: \newcommand{\forallL}{\forall{\cal L}}

33: \newcommand{\forallR}{\forall{\cal R}}

34: \newcommand{\landL}{\land{\cal L}}

35: \newcommand{\landR}{\land{\cal R}}

36: \newcommand{\lorL}{\lor{\cal L}}

37: \newcommand{\lorR}{\lor{\cal R}}

38: \newcommand{\nablaL}{\nabla{\cal L}}

39: \newcommand{\nablaR}{\nabla{\cal R}}

40: \newcommand{\oimp}{\supset}

41: \newcommand{\oimpL}{\oimp{\cal L}}

42: \newcommand{\oimpR}{\oimp{\cal R}}

43: \newcommand{\piL}{\pi_{\cal L}}

44: \newcommand{\piR}{\pi_{\cal R}}

45: \newcommand{\topR}{\top{\cal R}}

46: \newcommand{\wL}{\hbox{\sl w}{\cal L}}

47: \newcommand{\perm}[1]{Perm(#1)}

48: \newcommand{\const}[1]{{\cal C}(#1)}

49: 

50: \newcommand{\FOL   }{FO\lambda}

51: \newcommand{\Nset}{{\rm I} \! {\rm N}}

52: \newcommand{\FOLDN }{\FOL^{\Delta\Nset}}

53: \newcommand{\LGN}{LG^\omega}

54: \newcommand{\LG}{LG}

55: 

56: \newcommand{\interpi}[3]{seq_{#1} ~ #2 ~ #3}

57: \newcommand{\interp}[2]{seq ~ #1 ~ #2}

58: \newcommand{\oforall}{\bigwedge}

59: \newcommand{\oatm}[1]{\langle #1 \rangle}

60: \newcommand{\oand}{\mathbin{\&}}

61: \newcommand{\oexists}{\bigvee}

62: \newcommand{\otrue}{tt}

63: 

64: \newcommand{\FOLNb }{\FOL^{\nabla}}

65: \newcommand{\FOLDNb}{FO\lambda^{\Delta\nabla}}

66: \newcommand{\trans}[1]{[\![ #1 ]\!]}

67: 

68: \newlength{\infwidthi}

69: \newlength{\infwidthii}

70: \newcommand{\init}{id}

71: \newcommand{\mc}{mc}

72: \newcommand{\natL}{nat{\cal L}}

73: \newcommand{\natR}{nat{\cal R}}

74: 

75: 

76: \pagestyle{plain}

77: 

78: \begin{document}

79: 

80: \title{Cut Elimination for a Logic with Generic Judgments and Induction}

81: \author{Alwen Tiu}

82: \institute{Computer Sciences Laboratory\\ 

83: The Australian National University}

84: 

85: \maketitle

86: 

87: \begin{abstract}

88: This paper presents a cut-elimination proof for the logic $LG^\omega$, 

89: which is an extension of a proof system for encoding generic judgments,

90: the logic $\FOLDNb$ of Miller and Tiu, with an induction principle.

91: The logic $LG^\omega$, just as $\FOLDNb$, features extensions of first-order

92: intuitionistic logic with fixed points and a ``generic quantifier'', $\nabla$, 

93: which is used to reason about the dynamics of bindings in object systems encoded 

94: in the logic. A previous attempt to extend $\FOLDNb$ with an 

95: induction principle has been unsuccessful in modeling some

96: behaviours of bindings in inductive specifications. 

97: It turns out that this problem can be solved by relaxing 

98: some restrictions on $\nabla$, 

99: in particular by adding the axiom $B \equiv \nabla x. B$, where

100: $x$ is not free in $B$. We show that by adopting the

101: equivariance principle, the presentation of the extended logic

102: can be much simplified. 

103: This paper contains the technical proofs for the 

104: results stated in \cite{tiu07entcs}; readers are encouraged to consult \cite{tiu07entcs} for

105: motivations and examples for $LG^\omega.$

106: \end{abstract}

107: 

108: \section{Introduction}

109: 

110: This work aims at providing a framework for reasoning about

111: specifications of deductive systems using {\em higher-order

112: abstract syntax}~\cite{pfenning88pldi}. 

113: Higher-order abstract syntax is a declarative approach to encoding syntax

114: with bindings using Church's simply typed $\lambda$-calculus. 

115: The main idea is to support the notions of $\alpha$-equivalence 

116: and substitutions in the object syntax by operations

117: in $\lambda$-calculus, in particular $\alpha$-conversion and

118: $\beta$-reduction. There are at least two approaches to

119: higher-order abstract syntax. The {\em functional programming} approach

120: encodes the object syntax as a data type, where the binding constructs

121: in the object language are mapped to functions in the functional language.

122: In this approach, terms in the object language become values of

123: their corresponding types in the  functional language. 

124: The {\em proof search} approach encodes object syntax as 

125: expressions in a logic whose terms are simply typed, 

126: and functions that act on the object terms are defined 

127: via relations, i.e., logic programs. 

128: There is a subtle difference between

129: this approach and the former; 

130: in the proof search approach,

131: the simple types are inhabited by well-formed expressions, instead

132: of values as in the functional approach (i.e., the abstraction type

133: is inhabited by functions). 

134: The proof search approach is often referred to 

135: as {\em $\lambda$-tree syntax}~\cite{miller99surveys}, to distinguish 

136: it from the functional approach. This paper concerns the $\lambda$-tree syntax

137: approach.

138: 

139: Specifications which use $\lambda$-tree syntax are often

140: formalized using hypothetical and generic judgments

141: in intuitionistic logic. It is enough to restrict to

142: the fragment of first-order intuitionistic logic whose only

143: formulas are those of hereditary Harrop formulas, which we will

144: refer to as the $HH$ logic. 

145: Consider for instance the problem of 

146: defining the data type for untyped $\lambda$-terms. 

147: One first introduces the following constants:

148: $$

149: app : tm \to tm \to tm

150: \qquad

151: abs : (tm \to tm) \to tm

152: $$

153: where the type $tm$ denotes the syntactic category of $\lambda$-terms

154: and $app$ and $abs$ encode application and abstraction, respectively.

155: The property of being a $\lambda$-term is then defined via 

156: the following theory:

157: $$

158: \oforall M\oforall N(lam~M \land lam~N \Rightarrow lam~(app~M~N)) ~\oand~

159: $$

160: $$

161: \oforall M ( (\oforall x. lam~x \Rightarrow lam~(M\,x)) \Rightarrow 

162: lam~(abs~M))

163: $$

164: where $\oforall$ is the universal quantifier and $\Rightarrow$ is

165: implication. 

166: %A term $M$ is a $\lambda$-term if and only if $(lam~M)$ is provable

167: %given the above theory.

168: 

169: Reasoning about object systems encoded in $HH$ is reduced to reasoning

170: about the structure of proofs in $HH$. McDowell and Miller

171: formalize this kind of reasoning in the logic $\FOLDN$~\cite{mcdowell00tcs}, 

172: which is an extension of first-order intuitionistic logic with fixed points

173: and natural numbers induction. This is done by 

174: encoding the sequent calculus of $HH$ inside $\FOLDN$ and prove

175: properties about it. We refer to $HH$ as object logic and 

176: $\FOLDN$ as meta logic.

177: McDowell and Miller considered different styles of encodings and concluded 

178: that explicit representations of hypotheses and, more importantly,

179: eigenvariables of the object logic are required in order to capture some

180: statements about object logic provability in the meta 

181: logic~\cite{mcdowell02tocl}. 

182: One typical example involves the use of hypothetical and generic reasoning

183: as follows: Suppose that the following formula is provable in $HH$.

184: $$

185: \oforall x. p\,x\,s \Rightarrow \oforall y. p\,y\,t \Rightarrow p\,x\,t.

186: $$

187: By inspection on the inference rules of $HH$, one observes 

188: that this is only possible if $s$ and $t$ are syntactically equal.

189: This observation comes from the fact that the right introduction

190: rule for universal quantifier, 

191: reading the rule bottom-up, introduces new constants, 

192: or eigenvariables.

193: The quantified variables $x$ and $y$ will be replaced by

194: distinct eigenvariables and hence the only matching hypothesis

195: for $p\,x\,t$ would be $p\,x\,s$, and therefore $s$ and $t$

196: has to be equal.  

197: Let $\vdash_{HH} F$ denote the provability of the formula $F$ in $HH$.

198: Then in the meta logic, we would want to be able to prove the statement:

199: $$

200: \forall s\forall t. (\vdash_{HH} \oforall x. p\,x\,s \Rightarrow \oforall y. p\,y\,t \Rightarrow p\,x\,t) \oimp s = t.

201: $$

202: The question is then how we would intrepret the object logic eigenvariables

203: in the meta logic. It is demonstrated in ~\cite{mcdowell02tocl} 

204: that the existing quantifiers in $\FOLDN$ cannot be used to capture 

205: the behaviours

206: of object logic eigenvariables directly. McDowell and Miller then 

207: resort to a non-logical encoding technique (in the sense that no

208: logical connectives are used) which has some similar flavor to the use

209: of deBruijn indices. The use of this encoding technique, however, 

210: has a consequence that substitutions in the object logic has to be 

211: formalized explicitly. 

212: 

213: Motivated by the above mentioned limitation of $\FOLDN$,

214: Miller and Tiu later introduce a new quantifier $\nabla$ to $\FOLDN$

215: which allows one to move the binders from the object logic

216: to the meta logic. A generic judgment in the object logic,

217: for instance $\vdash_{HH} \oforall x.G\,x$ is reflected

218: in the meta logic as $\nabla x.\vdash_{HH} G\,x.$

219: This meta logic, called $\FOLDNb$~\cite{miller05tocl}, 

220: allows one to perform case

221: analyses on the provability of the object logic. 

222: Tiu later extended $\FOLDNb$ with induction and co-induction

223: rules, resulting in the logic Linc~\cite{tiu04phd}. 

224: However, some inductive properties about the object logic

225: are not provable in Linc. For example, the fact that 

226: $\vdash_{HH} \oforall x.G\,x$ implies

227: $\forall t. \vdash_{HH} G\,t$ (that is, the extensional

228: property of universal quantification) is not provable

229: in Linc. As it is shown in \cite{tiu04phd}, this is partly 

230: caused by the fact that $B \equiv \nabla x.B$, where 

231: $x$ is not free in $B$, is not provable in Linc or $\FOLDNb$. 

232: In this paper we present the logic $\LGN$, which is an

233: extension of $\FOLDNb$ with natural number induction and

234: with the axiom schemes:

235: \begin{equation}

236: \label{eq1}

237: \nabla x\nabla y.B \, x\,y \oimp \nabla y\nabla x.B\,x\,y

238: \quad \hbox{ and } \quad 

239: B \equiv \nabla x.B

240: \end{equation}

241: where $x$ is not free in $B$ in the second scheme.

242: We show that inductive properties of $\lambda$-tree syntax 

243: specifications can be stated directly and in a purely logical

244: fashion, and proved in $\LGN.$

245: 

246: 

247: \paragraph{Relation to nominal logic}

248: In formulating the proof system for $\LGN$, it turns out that

249: we can simplify the presentation a lot if we adopt the idea of

250: {\em equivariant predicates} from nominal logic~\cite{pitts03ic}.

251: That is, provability of a predicate is invariant under

252: permutations of {\em names}. This is technically done by

253: introducing a countably infinite set of name constants

254: into the logic, and change the identity rule of the logic

255: to allow equivalence under permutations of name constants:

256: $$

257: \infer[id]

258: {\Seq {\Gamma, B}{B'} }

259: {\pi.B = \pi'.B'}

260: $$

261: where $\pi$ and $\pi'$ are permutations on names.

262: $\LGN$ is in fact very close to nominal logic, when we consider

263: only the behaviours of logical connectives. In particular,

264: the quantifier $\nabla$ in $\LGN$ shares the same properties,

265: in relation to other connectives of the logic, 

266: with the $\NEW$ quantifier in nominal logic. However, there are

267: two important differences in our approach.

268: First, we do not attempt to redefine $\alpha$-conversion and

269: substitutions in $\LGN$ in terms of permutations (or {\em swapping})

270: and the notion of {\em freshness} as in nominal logic.

271: Name swapping and freshness constraints are not part of the syntax

272: of $\LGN.$ These notions are present only in the meta theory of

273: the logic. 

274: In $\LGN$, for example, variables are always considered

275: to have empty support, that is, $\pi.x = x$ for every permutation $\pi$.

276: This is because we restrict substitutions to the ``closed'' ones,

277: in the sense that no name constants can appear in the substitutions.

278: A restricted form of open substitutions can be recovered indirectly 

279: at the meta theory of $\LGN$. 

280: The fact that variables have empty support 

281: allows one to work with permutation free formulas and terms. 

282: So in $\LGN$, we can prove that $p~x~a \oimp p~x~b$, where $a$ and

283: $b$ are names, without using explicit axioms of permutations

284: and freshness. In nominal logic, one would prove this by

285: using the swapping axiom $p~x ~ a \oimp p~((a~b).x)~((a~b).b)$, 

286: where $(a~b)$ denotes a swapping of $a$ and $b$,

287: and then show that $(a~b).x = x$. The latter might not be valid

288: if $x$ is substituted by $a$, for example. 

289: The validity of this formula in nominal logic 

290: would therefore depend on the assumption on the support of $x$.

291: 

292: The second difference between $\LGN$ and nominal logic is that 

293: $\LGN$ allows closed terms (again, in the sense that no name 

294: constants appear in them) of type

295: name, while in nominal logic, allowing such terms would

296: lead to an inconsistent theory in nominal logic~\cite{pitts03ic}.

297: As an example, the type $tm$ in the encoding of $\lambda$-terms

298: mentioned previously can be treated as a nominal type in $\LGN$.

299: This has an important consequence that we do not need to 

300: redefine the notion of substitutions for the encoded $\lambda$-terms.

301: For example, we can define the (lazy) evaluation relation on 

302: untyped $\lambda$-terms as the theory:

303: $$

304: \begin{array}{c}

305: eval ~ (abs ~ M) ~ (abs ~ M) \equiv \top \\

306: eval ~ (app~M~N) ~ V \equiv eval ~ M ~ (abs~P) \land eval ~ (P~N) ~ V

307: \end{array}

308: $$

309: without having to explicitly define substitutions on terms of type $tm$ 

310: inside $\LGN.$ Substitutions in the object language in this case 

311: is modelled by $\beta$-reduction in the meta-language of $\LGN.$

312: 

313: \paragraph{Outline of the paper} 

314: Section~\ref{sec:lgn} introduces the logic $\LG$,

315: which is an extension of first order intuitionistic logic with a notion of name permutation 

316: and the $\nabla$-quantifier. $\LG$ serves as the core logic for a more expressive 

317: logic, $\LGN$, which is obtained by adding rules for fixed points, equality and induction to $\LG.$

318: Section~\ref{sec:drv} examines several properties of derivations, in particular,

319: those that concern preservation of provability under several operations on

320: sequents, e.g., substitutions. 

321: Section~\ref{sec:reduct} defines the cut reduction, used in the cut-elimination proof.

322: The cut elimination proof itself is an adaptation of the cut-elimination proof

323: of $\FOLDN$ by McDowell and Miller~\cite{mcdowell00tcs}, which makes use of the reducibility

324: technique. Section~\ref{sec:norm} defines the normalizability and the reducibility

325: relations which are crucial to the cut elimination proof in Section~\ref{sec:cut-elim}.

326: Finally, in Section~\ref{sec:corr}, we show that the proof system $\LG$ is actually

327: equivalent to $\FOLDNb$ (without fixed points and equality) with non-logical rules

328: corresponding to the axioms given in (\ref{eq1}) above.

329: 

330: This paper contains the technical proofs for the 

331: results stated in \cite{tiu07entcs}; readers are encouraged to consult \cite{tiu07entcs} for

332: motivations and examples for $LG^\omega.$

333: 

334: 

335: \section{A logic for generic judgments}

336: \label{sec:lgn}

337: 

338: \newcommand{\swap}[2]{(#1 ~ #2)}

339: 

340: We first define the core fragment of the logic $\LGN$

341: which does not have fixed point rules or induction.

342: The starting point is the logic $\FOLNb$ introduced in ~\cite{miller05tocl}.

343: $\FOLNb$ is an extension of a subset of Church's 

344: Simple Theory of Types in which 

345: formulas are given the type $o$. The core fragment of $\LGN$,

346: which we refer to as $\LG$, shares the same set of connectives

347: as $\FOLNb$, namely, $\bot$, $\top$, $\land$, $\lor$,

348: $\oimp$, $\forall_\tau$, $\exists_\tau$ and $\nabla_\tau.$

349: The type $\tau$ in the quantifiers is restricted to that

350: which does not contain the type $o.$ Hence the logic is

351: essentially first-order. We abbreviate $(B \oimp C)

352: \land (C \oimp B)$ as $B \equiv C.$

353: 

354: The sequents of $\FOLDNb$ are expressions of the form

355: $$

356: \NSeq{\Sigma}{\sigma_1\triangleright B_1, \ldots, \sigma_n \triangleright B_n}

357: {\sigma_0 \triangleright B_0}

358: $$

359: where $\Sigma$ is a signature, i.e., a set of eigenvariables 

360: scoped over the sequent

361: and $\sigma_i$ is a local signature, i.e., 

362: list of variables locally scoped over $B_i$. The introduction rules

363: for $\nabla$, reading the rules bottom-up, introduce new local

364: variables to the local signatures, just as the right introduction rule

365: of $\forall$ introduces new eigenvariables to the signature.

366: The expression $\sigma_i \triangleright B_i$ is called a local judgment,

367: and is identified up to renaming of variables in $\sigma_i$. 

368: This enforces a limited notion of equivariance: 

369: for example $\Seq{a\triangleright p a}

370: {b \triangleright p b}$ is provable, since both local judgments

371: are equivalent up to renaming of local signatures. 

372: However, the judgments 

373: $(a,c)\triangleright p\, a$ and $b \triangleright p\, b$ are considered

374: distinct judgments, and so are $(a,b) \triangleright q\,a\,b$

375: and $(b,a)\triangleright q\,a\,b$. These restrictions are relaxed in $\LG.$

376: 

377: The sequent presentation of $\LG$ can be simplified,

378: that is, without using the local signatures, if we employ

379: the equivariance principle. 

380: For this purpose, we introduce a distinguished set of base types, 

381: called {\em nominal types}, which is denoted with ${\cal N}$. 

382: Nominal types are ranged over by $\iota$.

383: We restrict the $\nabla$ quantifier to nominal types. 

384: For each nominal type $\iota \in {\cal N}$,

385: we assume an infinite number of constants of that type.

386: These constants are called {\em nominal constants}.

387: We denote the family of nominal constants

388: by ${\cal C}_{\cal N}.$ 

389: The role of the nominal constants is to enforce the notion

390: of equivariance: provability of formulas

391: is invariant under permutations of nominal constans. 

392: Depending on the application, we might also assume a set of 

393: non-nominal constants, which is denoted by ${\cal K}.$

394: 

395: We assume the usual notion of capture-avoiding substitutions.

396: Substitutions are ranged over by $\theta$ and $\rho$. 

397: Application of substitutions is written in a postfix notation,

398: e.g., $t\theta$ is an application of $\theta$ to the term $t$.

399: Given two substitutions $\theta$ and $\theta'$, 

400: we denote their composition by $\theta \circ \theta'$

401: which is defined as $t(\theta \circ \theta') = (t\theta)\theta'.$

402: A {\em signature} is a set of variables. 

403: A substitution $\theta$ respects a given signature $\Sigma$

404: if there exists a set of typed variables $\Sigma'$

405: such that for every $x : \tau$ in the domain of $\theta$,

406: it holds that

407: $

408: \TSeq{{\cal K} \cup \Sigma' }

409: {\theta(x)}{\tau}.

410: $

411: We denote by $\Sigma\theta$ the minimal set of variables 

412: satisfying the above condition. 

413: We assume that variables, free or bound, are of a different

414: syntactic category from constants. 

415: 

416: 

417: \begin{definition}

418: A permutation on ${\cal C}_{\cal N}$ is a bijection

419: from ${\cal C}_{\cal N}$ to ${\cal C}_{\cal N}$.

420: The permutations on ${\cal C}_{\cal N}$ are ranged over by $\pi$.

421: Application of a permutation $\pi$ to a nominal constant $a$

422: is denoted with $\pi(a)$. We shall be concerned only with

423: permutations which respect types, i.e., 

424: for every $a:\iota$,  $\pi(a) : \iota.$

425: Further, we shall also restrict to permutations which

426: are finite, that is, the set

427: $\{ a \mid \pi(a) \not = a \}$ is finite. 

428: Application of a permutation to an arbitrary term

429: (or formula), written $\pi.t$, is defined as follows:

430: $$

431: \begin{array}{ccc}

432: \pi.a  =  \pi(a), \hbox{ if $a \in {\cal C}_{\cal N}.$ } & 

433: \pi.c  =  c, \quad \hbox{if } c \not \in {\cal C}_{\cal N}. &

434: \pi.x  =  x  \\

435: \pi.(M~N)  =  (\pi.M) ~ (\pi.N) & \quad

436: \pi.(\lambda x.M)  =  \lambda x. (\pi.M) & 

437: \end{array}

438: $$

439: A permutation involving only two nominal constants

440: is called {\em swapping}. We use $(a~b)$, where

441: $a$ and $b$ are constants of the same type, to denote

442: the swapping $\{ a \mapsto b, b \mapsto a\}.$

443: \end{definition}

444: 

445: The {\em support} of a term (or formula) $t$, written $supp(t)$, is the set of

446: nominal constants appearing in it. 

447: It is clear from the above definition that if $supp(t)$ is

448: empty, then $\pi.t = t$ for all $\pi$.

449: The definition of $\Sigma$-substitution implies that

450: for every $\theta$ and for every $x \in dom(\theta)$, 

451: $\theta(x)$ has empty support.

452: Therefore $\Sigma$-substitutions and permutations commute, 

453: that is, $(\pi.t)\theta = \pi.(t\theta).$

454: 

455: A sequent in $\LGN$ is an expression of the form

456: $

457: \NSeq \Sigma \Gamma C

458: $

459: where $\Sigma$ is a signature. The free variables

460: of $\Gamma$ and $C$ are among the variables in $\Sigma$.

461: The inference rules for the core fragment of $\LGN$, i.e.,

462: the logic $\LG$, is given in Figure~\ref{fig:LG}.

463: In the rules, the typing judgment

464: $

465: \TSeq{\Sigma, {\cal K}, {\cal C}_{\cal N}}

466: {t}{\tau}

467: $

468: denotes the typability of $t : \tau$, given the typing

469: context $\Sigma \cup {\cal K} \cup {\cal C}_{\cal N}$

470: in Church's simple type system.

471: 

472: In the $\nablaL$ and $\nablaR$ rules, $a$ denotes

473: a nominal constant.

474: In the $\existsL$ and $\forallR$ rules, we use 

475: {\em raising} \cite{miller92jsc} 

476: to encode the dependency of the quantified variable

477: on the support of $B$, since we do not allow

478: $\Sigma$-substitutions to mention any nominal constants. 

479: In the rules, the variable $h$ has its type raised

480: in the following way: suppose $\vec c$

481: is the list $c_1:\iota_1,\dots,c_n:\iota_n$ and

482: the quantified variable $x$ is of type $\tau$. Then

483: the variable $h$ is of type:

484: $\iota_1 \to \iota_2 \to \dots \to \iota_n \to \tau.$ 

485: This raising technique is similar to that of $\FOLDNb,$

486: and is used to encode explicitly the minimal 

487: support of the quantified variable. 

488: Its use prevents one from mixing the scopes of $\forall$ (dually, $\exists$)

489: and $\nabla$. That is, it prevents the formula 

490: $\forall x \nabla y. p\,x\,y \equiv \nabla y\forall x. p\,x\,y$,

491: and its dual, to be proved.

492: 

493: Looking at the introduction rules for $\forall$ and $\exists$,

494: one might notice the asymmetry between the

495: left and the right introduction rules. 

496: The left rule for $\forall$ allows instantiations with terms

497: containing any nominal constants 

498: while the raised variable in the right introduction rule of $\forall$

499: takes into account only those which are in the support of the quantified

500: formula.

501: However, we will see that we can extend the dependency of the 

502: raised variable to an arbitrary number of fresh nominal constants

503: not in the support without affecting the provability of the sequent

504: (see Lemma~\ref{lm:supp1} and Lemma~\ref{lm:supp2}). 

505: 

506: 

507: \begin{figure}

508: {\small

509: $$

510: \infer[id_\pi]

511: {\NSeq \Sigma {\Gamma,B} {B'}}

512: {\pi.B = \pi'.B'}

513: \qquad

514: \infer[\mc]

515: {\NSeq{\Sigma}{\Delta_1,\ldots, \Delta_n,\Gamma}{C}}

516: {\NSeq{\Sigma}{\Delta_1}{B_1} & \cdots & \NSeq{\Sigma}{\Delta_n}{B_n}

517: & \NSeq{\Sigma}{B_1,\dots,B_n,\Gamma}{C}}

518: \qquad

519: \infer[\cL]

520: {\NSeq \Sigma {\Gamma, B} C}

521: {\NSeq \Sigma{\Gamma, B, B} C}

522: $$

523: $$

524: \infer[\botL]

525: {\NSeq \Sigma {\Gamma, \bot} {C}}

526: {}

527: \qquad

528: \infer[\topR]

529: {\NSeq \Sigma \Gamma \top}

530: {}

531: $$

532: $$

533: \infer[\landL, i \in \{1,2\}]

534: {\NSeq{\Sigma}{\Gamma, B_1 \land B_2}{C}}

535: {\NSeq{\Sigma}{\Gamma, B_i}{C}}

536: \qquad

537: \infer[\landR]

538: {\NSeq{\Sigma}{\Gamma}{B \land C}} 

539: {\NSeq \Sigma  \Gamma B & \NSeq \Sigma \Gamma C}

540: $$

541: $$

542: \infer[\lorL]

543: {\NSeq \Sigma  {\Gamma, B \lor D} C}

544: {\NSeq \Sigma  {\Gamma, B} C 

545: & \NSeq \Sigma  {\Gamma, D} C}

546: \qquad

547: \infer[\lorR, i \in \{1,2\}]

548: {\NSeq \Sigma  \Gamma {B_1 \lor B_2}}

549: {\NSeq \Sigma  \Gamma {B_i}}

550: $$

551: $$

552: \infer[\oimpL]

553: {\NSeq \Sigma  {\Gamma, B \oimp D} C }

554: {\NSeq \Sigma  \Gamma B & \NSeq \Sigma  {\Gamma, D} C}

555: \qquad

556: \infer[\oimpR]

557: {\NSeq \Sigma  \Gamma {B \oimp C}}

558: {\NSeq \Sigma {\Gamma, B} C}

559: $$

560: $$

561: \infer[\forallL]

562: {\NSeq \Sigma  {\Gamma, \forall_\tau x. B} C}

563: {\TSeq {\Sigma, {\cal K}, {\cal C}_{\cal N}} t \tau & \NSeq \Sigma {\Gamma, B[t/x]} C}

564: \qquad

565: \infer[\forallR, h \not \in \Sigma, supp(B) = \{\vec c\}]

566: {\NSeq \Sigma  \Gamma {\forall x.B}}

567: {\NSeq {\Sigma,h} \Gamma {B[h\, \vec c/x]} }

568: $$

569: $$

570: \infer[\nablaL, a \not \in supp(B)]

571: {\NSeq \Sigma {\Gamma, \nabla x.B} C}

572: {\NSeq \Sigma {\Gamma, B[a/x]} C}

573: \qquad

574: \infer[\nablaR, a \not \in supp(B)]

575: {\NSeq \Sigma \Gamma {\nabla x.B}}

576: {\NSeq \Sigma \Gamma {B[a/x]}}

577: $$

578: $$

579: \infer[\existsL, h \not \in \Sigma, supp(B) = \{\vec c\}]

580: {\NSeq \Sigma  {\Gamma, \exists x.B} C}

581: {\NSeq {\Sigma, h}  {\Gamma, B[h\,\vec c/x]} C}

582: \qquad

583: \infer[\existsR]

584: {\NSeq \Sigma  \Gamma {\exists_\tau x.B}}

585: {\TSeq {\Sigma,{\cal K},{\cal C}_{\cal N}} t \tau & \NSeq \Sigma \Gamma {B[t/x]}}

586: $$

587: }

588: \caption{The inference rules of $\LG$}

589: \label{fig:LG}

590: \end{figure}

591: 

592: 

593: We now extend the logic $\LG$ with a proof theoretic notion

594: of equality and fixed points, following on works by

595: Hallnas and Schroeder-Heister~\cite{hallnas91jlc,schroeder-heister92nlip}, 

596: Girard~\cite{girard92mail} and McDowell and Miller~\cite{mcdowell00tcs}.

597: The equality rules are as follows:

598: $$

599: \infer[\eqL]

600: {\NSeq \Sigma {\Gamma, s = t} C}

601: {

602: \{\NSeq {\Sigma\theta}  {\Gamma\theta} {C\theta}

603: ~ \mid ~ (\lambda \vec c.t)\theta =_{\beta\eta} (\lambda \vec c.s)\theta  \}

604: }

605: \qquad

606: \infer[\eqR]

607: {\NSeq \Sigma \Gamma {t = t}}

608: {}

609: $$

610: where $supp(s = t) = \{\vec c\}$ in the $\eqL$ rule.

611: In the $\eqL$ rule, the substitution $\theta$ is a {\em unifier} of

612: $\lambda \vec c.s$ and $\lambda \vec c.t$.

613: We specify the premise of the rule as a set to mean that every element

614: of the set is a premise. Since the terms $s$ and $t$ can be

615: arbitrary higher-order terms, in general the set of their unifiers 

616: can be infinite. However, in some restricted cases, 

617: e.g., when $\lambda \vec c.s$ and $\lambda \vec c.t$ are 

618: {\em higher-order pattern} terms~\cite{miller91jlc,nipkow93lics},

619: if both terms are unifiable, then there exists a most general unifier.

620: The applications we are considering are those which satisfy the 

621: higher-order pattern restrictions.

622: 

623: 

624: \begin{definition}

625: To each atomic formula, we associate a fixed point equation,

626: or a {\em definition clause}, following the terminology of

627: $\FOLDNb$. A definition clause is written

628: $

629: \forall \vec x. p\,\vec x \defeq B

630: $

631: where the free variables of $B$ are among $\vec x.$

632: The predicate $p\,\vec x$ is called the {\em head}

633: of the definition clause, and $B$ is called the {\em body}.

634: A {\em definition} is a set of definition clauses. 

635: We often omit the outer quantifiers when referring to

636: a definition clause.

637: \end{definition}

638: 

639: The introduction rules for defined atoms are as follows:

640: $$

641: \infer[\defL, p\,\vec x \defeq B]

642: {\NSeq \Sigma {\Gamma, p\, \vec t} C}

643: {\NSeq \Sigma {\Gamma, B[\vec t/\vec x]} C}

644: \qquad

645: \infer[\defR, p\,\vec x \defeq B]

646: {\NSeq \Sigma  \Gamma {p\, \vec t}}

647: {\NSeq \Sigma  \Gamma {B[\vec t/\vec x]}}

648: $$

649: 

650: In order to prove the cut-elimination theorem and

651: the consistency of $\LGN$, we allow only definition clauses 

652: which satisfy an {\em equivariance preserving} condition and 

653: a certain positivity condition, so as to guarantee the

654: existence of fixed points. 

655: 

656: \newcommand{\level}[1]{lvl(#1)}

657: \begin{definition}

658: \label{def:level}

659: We associate with each predicate symbol $p$ a natural number,

660: the {\em level} of $p$. 

661: Given a formula $B$, its {\em level} $\level{B}$ is defined as follows:

662: \begin{enumerate}

663: \item $\level{p \, \bar{t}} = \level{p}$

664: \item $\level{\bot} = \level{\top} = 0$

665: \item $\level{B \land C} = \level{B \lor C} = \max(\level{B},\level{C})$

666: \item $\level{B \oimp C} = \max(\level{B}+1,\level{C})$

667: \item $\level{\forall x.B} = \level{\nabla x.B} = \level{\exists x.B}

668:        = \level{B}$. 

669: \end{enumerate}

670: A definition clause $p\,\vec x \defeq B$ is stratified if

671: $\level{B} \leq \level{p}$ and

672: $B$ has no free occurrences of nominal constants.

673: We consider only definition clauses which are stratified.

674: \end{definition}

675: An example that violates the first restriction in 

676: Definition~\ref{def:level} is the definition $p \defeq p \oimp \bot.$

677: In~\cite{schroeder-heister92nlip}, Schroeder-Heister shows that admitting this

678: definition in a logic with contraction leads to

679: inconsistency. To see why we need the second restriction

680: on name constants, consider the definition $q\, x \defeq (x = a),$

681: where $a$ is a nominal constant. Let $b$ be a

682: nominal constant different from $a$. 

683: Using this definition, we would be able to derive $\bot$:

684: $$

685: \infer[cut]

686: {\Seq{}{\bot}}

687: {

688:    \infer[\defR]

689:    {\Seq{}{q\,a}}

690:    {

691:       \infer[\eqR]

692:       {\Seq{}{a = a}}

693:       {}

694:    }

695: &

696:    \infer[cut]

697:    {\Seq{q\,a}{\bot}}

698:    {

699:      \infer[id_\pi]

700:      {\Seq{q\,a}{q\,b}}

701:      {}

702:    &

703:      \infer[\defL]

704:      {\Seq{q\,b}{\bot}}

705:      {

706:        \infer[\eqL]

707:        {\Seq{b = a}{\bot}}

708:        {}

709:      }

710:    }

711: }

712: $$

713: 

714: In examples and applications, we

715: often express definition clauses with patterns in the heads. 

716: Let us consider, for example, a definition clause for lists. 

717: We first introduce a type $lst$ to denote lists of elements of type $\alpha$, 

718: and the constants

719: $$

720: nil : lst \qquad :: ~ : \alpha \to lst \to lst

721: $$

722: which denote the empty list and a constructor to build a list

723: from an element of type $\alpha$ and another list. The latter

724: will be written in the infix notation.   

725: The definition clause for {\em lists} is as follows.

726: $$

727: list~L \defeq L = nil \lor \exists_\alpha A\exists_{lst} L'. 

728:      L = (A::L') \land list~L'.

729: $$

730: Using patterns, the above definition of lists can

731: be rewritten as

732: $$

733: list~nil \defeq \top.\qquad \quad

734: list~(A :: L) \defeq list~L.

735: $$

736: 

737: We shall often work directly with this patterned notation for definition clauses.

738: For this purpose, we introduce the notion of {\em patterned definitions}.

739: A {\em patterned definition clause} is written

740: $\forall \vec x. H \defeq B$ where the free variables of $H$  and $B$ are among

741: $\vec x.$ The stratification of definitions in Definition~\ref{def:level}

742: applies to patterned definitions as well. 

743: Since the patterned definition clauses are not allowed to have

744: free occurrences of nominal constants, in matching the heads of the

745: clauses with an atomic formula in a sequent, we need to raise the variables of

746: the clauses to account for nominal constants that are in the support

747: of the introduced formula.

748: Given a patterned definition clause 

749: $

750: \forall x_1 \dots \forall x_n. H \defeq B

751: $

752: its raised clause with respect to the list of

753: constants $c_1:\iota_1 \dots c_n:\iota_n$

754: is

755: $$

756: \forall h_1 \dots \forall h_n. H[h_1~\vec c/x_1, \ldots, h_n~\vec c/x_n] 

757: \defeq B[h_1~\vec c/x_1, \ldots, h_n~\vec c/x_n].

758: $$

759: The introduction rules for patterned definitions are

760: $$

761: \infer[\defL]

762: {\NSeq{\Sigma}{A, \Gamma}{C}}

763: {\{\NSeq{\Sigma\theta}{B\theta, \Gamma\theta}{C\theta}\}_\theta}

764: \qquad

765: \infer[\defR]

766: {\NSeq{\Sigma}{\Gamma}{A}}

767: {\NSeq{\Sigma}{\Gamma}{B\theta}}

768: $$

769: In the $\defL$ rule, $B$ is the body of the raised patterned clause

770: $\forall x_1 \dots \forall x_n. H \defeq B$ and

771: $(\lambda \vec c.H)\theta = (\lambda \vec c.A)\theta$ where $\{\vec c\}$ is

772: the support of $A.$ 

773: In the $\defR$ rule, we match $A$ with the head of the clause,

774: i.e., $\lambda \vec c.A = (\lambda \vec c.H)\theta.$

775: These patterned rules can be derived using the non-patterned

776: definition rules and the equality rules, as shown in~\cite{tiu04phd},

777: 

778: 

779: \paragraph{Natural number induction.}

780: We introduce a type $nt$ to denote natural numbers,

781: with the usual constants $z : nt$ (zero) and $s : nt \to nt$ (the

782: successor function), and a special predicate $nat : nt \to nt \to o.$

783: The rules for natural number induction are the same as

784: those in $\FOLDN$~\cite{mcdowell00tcs}, which are the introduction rules

785: for the predicate $nat$.

786: $$

787: \infer[nat{\cal L}]

788: {\NSeq{\Sigma}{\Gamma, nat\,I}{C}}

789: {\Seq{}{D\,z} & \NSeq{j}{D\,j}{D\,(s\,j)} 

790: & \NSeq{\Sigma}{\Gamma, D\,I}{C}}

791: $$

792: 

793: $$

794: \infer[nat{\cal R}]

795: {\NSeq{\Sigma}{\Gamma}{nat~z}}

796: {}

797: \qquad

798: \infer[nat{\cal R}]

799: {\NSeq{\Sigma}  \Gamma {nat\,(s\,I)}}

800: {\NSeq{\Sigma}  \Gamma {nat\,I}}

801: $$

802: 

803: The logic $\LG$ extended with the equality, definitions and

804: induction rules is referred to as $\LGN.$

805: 

806: 

807: \section{Properties of derivations}

808: \label{sec:drv}

809: 

810: In this section we examine several properties of the $\nabla$-quantifier and 

811: derivations in $\LGN$ that are useful in the cut elimination proof. 

812: These properties concern the transformation of derivations, in particular,

813: they state that provability is preserved under $\Sigma$-substitutions, permutations

814: and a restricted form of name substitutions.

815: 

816: We first look at the properties of the $\nabla$ quantifier

817: in relation to other connectives. 

818: The proof of the following proposition is straightforward by

819: inspection on the rules of $\LG.$

820: 

821: \begin{proposition}

822: The following formulas are provable in $\LG$:

823: \begin{enumerate}

824: \item $\nabla x.(B x \land C x) \equiv \nabla x.B x \land \nabla x. C x.$

825: \item $\nabla x.(B x \oimp C x) \equiv \nabla x.B x \oimp \nabla x. C x.$

826: \item $\nabla x.(B x \lor C x) \equiv \nabla x.B x \lor \nabla x.C x.$

827: \item $\nabla x. B \equiv B$, provided that $x$ is not free in $B$.

828: \item $\nabla x\nabla y.B x y \equiv \nabla y\nabla x.Bxy.$

829: \item $\forall x.B x \oimp \nabla x.B x.$

830: \item $\nabla x.B x \oimp \exists x.B x.$ 

831: \end{enumerate}

832: \end{proposition}

833: The formulas (1) -- (3) are provable in $\FOLNb$. The proposition

834: is true also in nominal logic with $\nabla$ replaced by $\NEW.$

835: 

836: 

837: \begin{definition}

838: \label{def:ht}

839: Given a derivation $\Pi$ with premise derivations 

840: $\{\Pi_i\}_{i \in {\cal I}}$ where ${\cal I}$ is some

841: index set, the measure $ht(\Pi)$, the {\em height} of $\Pi$, 

842: is defined as the least upper bound of

843: $

844: \{ht(\Pi_i) + 1\}_{i \in {\cal I}}.

845: $

846: \end{definition}

847: 

848: We now define some transformations of derivations:

849: weakening of hypotheses, substitutions on derivations,

850: permutations and restricted name substitutions.

851: In the following definitions we omit the signatures

852: in the sequents if it is clear from context which

853: signatures we refer to.

854: We denote with $id$ the identity function on ${\cal C}_{\cal N}$.

855: 

856: \begin{definition}

857: \label{def:weak}

858: {\em Weakening of hypotheses.}

859: Let $\Pi$ be a derivation of $\NSeq{\Sigma}{\Gamma}{C}.$

860: Let $\Delta$ be a multiset of formulas whose free variables

861: are among $\Sigma$. We define the derivation $w(\Delta,\Pi)$

862: of $\NSeq{\Sigma}{\Gamma, \Delta}{C}$ as follows:

863: \begin{enumerate}

864: \item If $\Pi$ ends with $\eqL$

865: $$

866: \infer[\eqL]

867: {\NSeq{\Sigma}{s = t, \Gamma'}{C}}

868: {\left\{

869: \raisebox{-1.5ex}{\deduce{\NSeq{\Sigma\theta}{\Gamma'\theta}{C\theta}}{\Pi_\theta}}

870: \right\}_\theta

871: }

872: $$

873: then $w(\Delta, \Pi)$ is 

874: $$

875: \infer[\eqL]

876: {\NSeq{\Sigma}{s = t, \Gamma', \Delta}{C}}

877: {

878: \left\{

879: \raisebox{-1.5ex}{\deduce{\NSeq{\Sigma\theta}{\Gamma'\theta, \Delta\theta}{C\theta}}

880: {w(\Delta\theta,\Pi_\theta)}}

881: \right\}_\theta

882: }

883: $$

884: \item If $\Pi$ ends with $\natL$

885: $$

886: \infer[\natL]

887: {\Seq{nat~I, \Gamma'}{C}}

888: {\deduce{\Seq{}{D~z }}{\Pi_1}

889: & \deduce{\Seq{D~i}{D~(s~i)}}{\Pi_2}

890: & \deduce{\Seq{D~I, \Gamma'}{C}}{\Pi_3}}

891: $$

892: then $w(\Delta, \Pi)$ is

893: $$

894: \infer[\natL]

895: {\Seq{nat~I, \Gamma', \Delta}{C}}

896: {\deduce{\Seq{}{D~z }}{\Pi_1}

897: & \deduce{\Seq{D~i}{D~(s~i)}}{\Pi_2}

898: & \deduce{\Seq{D~I, \Gamma', \Delta}{C}}{w(\Delta,\Pi_3)}}

899: $$

900: \item If $\Pi$ ends with the $mc$ rule

901: $$

902: \infer[mc]

903: {\Seq{\Delta_1,\ldots,\Delta_n, \Gamma'}{C}}

904: {

905: \deduce{\Seq{\Delta_1}{B_1}}{\Pi_1}

906: & \ldots &

907: \deduce{\Seq{\Delta_n}{B_n}}{\Pi_n}

908: & 

909: \deduce{\Seq{B_1,\dots,B_n,\Gamma'}{C}}{\Pi'}

910: }

911: $$

912: then $w(\Delta,\Pi)$ is

913: $$

914: \infer[mc]

915: {\Seq{\Delta_1,\ldots,\Delta_n, \Gamma', \Delta}{C}}

916: {

917: \deduce{\Seq{\Delta_1}{B_1}}{\Pi_1}

918: & \ldots &

919: \deduce{\Seq{\Delta_n}{B_n}}{\Pi_n}

920: & 

921: \deduce{\Seq{B_1,\dots,B_n,\Gamma', \Delta}{C}}{w(\Delta,\Pi')}

922: }

923: $$

924: \item If $\Pi$ ends with any other rule and has premise derivations

925: $\Pi_1,\dots,\Pi_n$ then $w(\Delta,\Pi)$ ends with the same

926: rule with premise derivations $w(\Delta,\Pi_n),$ $\dots,$ $w(\Delta,\Pi_n).$

927: \end{enumerate}

928: \end{definition}

929: 

930: \begin{definition}

931: \label{def:subst}

932: {\em Substitutions on derivations.}

933: If $\Pi$ is a derivation of $\NSeq{\Sigma}{\Gamma}{C}$ and $\theta$

934: is a $\Sigma$-substitution, then we define the derivation $\Pi\theta$ 

935: of $\NSeq{\Sigma\theta}{\Gamma\theta}{C\theta}$ as follows:

936: \begin{enumerate}

937: \item Suppose $\Pi$ ends with $\eqL$:

938: $$

939: \infer[\eqL]

940: {\NSeq{\Sigma}{s = t, \Gamma'}{C}}

941: {\left\{

942: \raisebox{-1.5ex}{\deduce{\NSeq{\Sigma\rho}{\Gamma'\rho}{C\rho}}{\Pi_\rho}}

943: \right\}_\rho

944: }

945: $$

946: where each $\rho$ is a unifier of $\lambda \vec c.s$

947: and $\lambda \vec c.t$. Observe that if $\rho'$ is a unifier

948: of $(\lambda \vec c.s)\theta$ and $(\lambda \vec c.t)\theta$, 

949: then $\theta\circ \rho'$ is a unifier of  $\lambda \vec c.s$

950: and $\lambda \vec c.t$. Thus $\Pi\theta$ is the derivation:

951: $$

952: \infer[\eqL]

953: {\NSeq{\Sigma}{s\theta = t\theta, \Delta\theta}{C\theta}}

954: {

955: \left\{ 

956: \raisebox{-1.5ex}{\deduce{\NSeq{\Sigma\theta\rho'}{\Delta\theta\rho}{C\theta\rho}}

957: {\Pi_{\theta\circ \rho'}}}

958: \right\}_{\rho'}

959: }

960: $$

961: \item Suppose $\Pi$ ends with $\forallR$:

962: $$

963: \infer[\forallR]

964: {\NSeq{\Sigma}{\Gamma}{\forall x.B}}

965: {\deduce{\NSeq{\Sigma}{\Gamma}{B[h\,\vec c/x]}}{\Pi_1}}

966: \enspace ,

967: $$

968: where $\{\vec c\} = supp(\forall x.B).$

969: Let $\{\vec d\}$ be the support of $(\forall x.B) \theta$,

970: which might be smaller than $\{ \vec c\}.$

971: Let $\rho$ be the substitution $[\lambda \vec c.h' \vec d/h]$

972: where $h'$ is a new variable not already in $\Sigma$ and 

973: not among the free variables in $\theta.$ 

974: We can assume without loss of generality that 

975: $x$ is not free in $\theta$, hence 

976: $((B[h\,\vec c/x])\rho) \theta = (B[h'\,\vec d/x])\theta = (B\theta)[h'\,\vec d/x].$

977: Then $\Pi\theta$ is

978: $$

979: \infer[\forallR]

980: {\NSeq{\Sigma\theta}{\Gamma\theta}{(\forall x.B)\theta}}

981: {\deduce{\NSeq{\Sigma\theta, h'}{\Gamma\theta}{(B\theta)[h'\,\vec d/x]}}{\Pi_1(\rho \circ \theta)}}

982: $$

983: \item Suppose $\Pi$ ends with $\existsL$: this case is dual to the previous one.

984: \item If $\Pi$ ends with any other rule and has premise derivations

985: $\Pi_1,\dots,\Pi_n$, then $\Pi\theta$ ends with the same rule and has

986: premise derivations $\Pi_1\theta$,$\dots,$ $\Pi_n\theta.$

987: \end{enumerate}

988: \end{definition}

989: 

990: \begin{definition}

991: \label{def:perm}

992: Let $\Pi$ be a proof of $\NSeq \Sigma {B_1, \ldots, B_n} {B_0}$

993: and let $\vec \pi = \pi_0,\dots,\pi_n$ be a list of permutations. We define

994: a derivation $\langle\vec \pi\rangle.\Pi$ of 

995: $\NSeq{\Sigma}{\pi_1.B_1, \ldots, \pi_n.B_n}{\pi_0.B_0}$

996: as follows:

997: \begin{enumerate}

998: \item Suppose that $\Pi$ ends with $id_\pi$

999: $$

1000: \infer[id_\pi]

1001: {\NSeq \Sigma {B_1, \ldots, B_n}{B_0}}

1002: {\pi.B_j = \pi'.B_0}

1003: \enspace .

1004: $$

1005: Obverse that $\pi.\pi_j^{-1}.\pi_j.B = \pi'.\pi_0^{-1}.\pi_0.B'.$

1006: Hence $\langle\vec \pi\rangle.\Pi$ ends with the same rule.

1007: 

1008: \item Suppose $\Pi$ ends with $mc$:

1009: $$

1010: \infer[mc]

1011: {\Seq{B_1,\ldots,B_n}{B_0}}

1012: {

1013: \deduce{\Seq{\Delta_1}{D_1}}{\Pi_1}

1014: &

1015: \ldots

1016: &

1017: \deduce{\Seq{\Delta_m}{D_m}}{\Pi_m}

1018: &

1019: \deduce{\Seq{D_1,\ldots,D_m,\Delta_{m+1}}{B_0}}{\Pi'}

1020: }

1021: $$

1022: where $\Delta_1, \ldots, \Delta_{m+1}$ are partitions of

1023: $B_1,\dots,B_n.$ Suppose that for each $i \in \{1,\dots,m+1\}$, 

1024: $\Delta_i = B_{i1},\dots,B_{ik_i}$ for some index $k_i.$

1025: Let $\vec \pi(i)$, for $i \in \{1,\dots,m\}$, 

1026: be the permutations $id,\pi_{i1},\dots,\pi_{ik_i}.$

1027: Let $\vec \pi(m+1)$ be the permutations

1028: $$\pi_0, \underbrace{id,\dots,id}_m,\pi_{(m+1)1},\ldots \pi_{(m+1)k_{m+1}}$$

1029: 

1030: We denote with $\Delta_i'$ the list

1031: $$

1032: \pi_{i1}.B_{ij}, \ldots, \pi_{ik_i}.B_{ik_i}.

1033: $$

1034: Then $\langle \vec \pi \rangle.\Pi$ is the derivation

1035: $$

1036: \infer[mc]

1037: {\Seq{\pi_1.B_1,\ldots,\pi_n.B_n}{\pi_0.B_0}}

1038: {

1039: \deduce{\Seq{\Delta_1'}{D_1}}{\langle \vec \pi(1)\rangle.\Pi_1}

1040: &

1041: \ldots

1042: &

1043: \deduce{\Seq{\Delta_m'}{D_m}}{\langle \vec \pi(m)\rangle.\Pi_m}

1044: &

1045: \deduce{\Seq{D_1,\ldots,D_m,\Delta_{m+1}'}{\pi_0.B_0}}{\langle \vec \pi(m+1)\rangle.\Pi'}

1046: }

1047: $$

1048: 

1049: \item Suppose $\Pi$ ends with $\nablaR$:

1050: $$

1051: \infer[\nablaR]

1052: {\NSeq{\Sigma}{B_1,\ldots,B_n}{\nabla_\iota x.B}}

1053: {\deduce{\NSeq{\Sigma}{B_1,\ldots,B_n}{B[a/x]}}{\Pi_1}}

1054: $$

1055: where $a : \iota \not \in supp(B).$ 

1056: Let $d : \iota$ be a nominal constant such that 

1057: $d \not \in supp(B)$ and $\pi_0(d) = d$. Such a constant

1058: exists since $supp(B)$ is finite and $\pi_0$ is a finite

1059: permutation. Thus $\pi_0.(a~d).B_0[a/x] = \pi_0.B_0[d/x].$

1060: Then $\langle\vec \pi\rangle.\Pi$ is the derivation:

1061: $$

1062: \infer[\nablaR]

1063: {\NSeq{\Sigma}{\pi_1.B_1, \ldots, \pi_n.B_n}{\pi_0.(\nabla x.B)}}

1064: {\deduce{\NSeq{\Sigma}{\pi_1.B_1, \ldots, \pi_n.B_n}{\pi_0.B[d/x]}}

1065: {\langle\pi_0.(a~d), \dots,\pi_n\rangle.\Pi_1}}

1066: $$

1067: \item Suppose $\Pi$ ends with $\nablaL$: this case is analogous to previous one.

1068: 

1069: \item Suppose $\Pi$ ends with $\cL$:

1070: $$

1071: \infer[\cL]

1072: {\Seq{B_1,\ldots,B_j,\ldots,B_n}{B_0}}

1073: {

1074: \deduce{

1075: \Seq{B_1,\ldots,B_j,B_j\ldots,B_n}{B_0}

1076: }

1077: {

1078: \Pi'

1079: }

1080: }

1081: $$

1082: then $\langle\vec \pi\rangle.\Pi$ is

1083: $$

1084: \infer[\cL]

1085: {\Seq{\pi_1.B_1,\ldots,\pi_{j}.B_j,\ldots,\pi_n.B_n}{\pi_0.B_0}}

1086: {

1087: \deduce{

1088: \Seq{\pi_1.B_1,\ldots,\pi_{j}.B_j,\pi_j.B_j\ldots,\pi_n.B_n}{\pi_0.B_0}

1089: }

1090: {

1091: \langle \pi_1,\ldots,\pi_j,\pi_j,\ldots,\pi_n\rangle.\Pi'

1092: }

1093: }

1094: $$

1095: \item If $\Pi$ ends with any other rule and has premise derivations 

1096: $\Pi_1, \dots, \Pi_m$, then $\langle \vec \pi \rangle.\Pi$ ends with

1097: the same rule and has premise derivations

1098: $\langle \vec \pi \rangle.\Pi_1,$ $\dots,$ $\langle \vec \pi \rangle.\Pi_m.$

1099: 

1100: \end{enumerate}

1101: \end{definition}

1102: 

1103: \begin{definition}

1104: \label{def:res}

1105: Let $\Pi$ be a proof of $\NSeq{\Sigma,x:\iota}{B_1, \ldots, B_n}{B_0}$

1106: and let $\vec a = a_0, \dots, a_n$ be a list of nominal constants

1107: such that $a_i\not \in supp(B_i).$

1108: We define a derivation $r(x,\langle \vec a\rangle, \Pi)$

1109: of 

1110: $\NSeq{\Sigma}{B_1[a_1/x], \ldots, B_n[a_n/x]}{B_0[a_0/x]},$

1111: as follows:

1112: \begin{enumerate}

1113: \item Suppose $\Pi$ is

1114: $$

1115: \infer[id_\pi]

1116: {\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B_0}}

1117: {\pi.B_j = \pi'.B_0}

1118: \enspace .

1119: $$

1120: Let $d : \iota$ be a nominal constant which is not in

1121: the support of $B_j$ and $B_0$, and $\pi(d) = d$

1122: and $\pi'(d) = d$. 

1123: Then $r(x,\vec a,\Pi)$ is 

1124: $$

1125: \infer[id_\pi]

1126: {\NSeq{\Sigma}{B_1[a_1/x], \ldots, B_n[a_n/x]}{B_0[a_0/x]}}

1127: {\pi.(a_j~d).B_1[a_1/x] = \pi'.(a_0~d).B_0[a_0/x]}

1128: $$

1129: 

1130: \item Suppose $\Pi$ ends with $mc$:

1131: $$

1132: \infer[mc]

1133: {\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B_0}}

1134: {

1135: \deduce{\NSeq{\Sigma,x}{\Delta_1}{D_1}}{\Pi_1}

1136: &

1137: \ldots

1138: &

1139: \deduce{\NSeq{\Sigma,x}{\Delta_m}{D_m}}{\Pi_m}

1140: &

1141: \deduce{\NSeq{\Sigma,x}{D_1,\ldots,D_m,\Delta_{m+1}}{B_0}}{\Pi'}

1142: }

1143: $$

1144: where $\Delta_1, \ldots, \Delta_{m+1}$ is a partition of

1145: $B_1,\dots,B_n.$ Suppose that for each $i \in \{1,\dots,m+1\}$, 

1146: $\Delta_i = B_{i1},\dots,B_{ik_i}$ for some index $k_i.$

1147: Let $\vec d = d_1,\dots,d_m$ be a list of nominal constants

1148: such that $d_i \not \in supp(D_i).$

1149: Let $f(i)$, for $i \in \{1,\dots,m\}$ be the list

1150: $d_i,a_{i1},\dots,a_{ik_i}$

1151: and let $f(m+1)$ be the list

1152: $$a_0,\vec d,a_{(m+1)1},\dots,a_{(m+1)k_{(m+1)}}.$$

1153: Let $\Delta_i'$ be the list 

1154: $$

1155: B_{i1}[a_{i1}/x],\ldots,B_{ik_i}[a_{ik_i}/x]

1156: $$

1157: and let $\Gamma$ be the list

1158: $$

1159: D_{1}[d_1/x],\ldots,D_{m}[d_m/x], \Delta_{m+1}'.

1160: $$

1161: Then $r(x,\vec a, \Pi)$ is the derivation

1162: $$

1163: \infer[mc]

1164: {\NSeq{\Sigma}{B_1[a_1/x],\ldots,B_n[a_n/x]}{B_0[a_0/x]}}

1165: {

1166: \deduce{\NSeq{\Sigma}{\Delta_1'}{D_1[d_1/x]}}{r(x,f(1),\Pi_1)}

1167: &

1168: \ldots

1169: &

1170: \deduce{\NSeq{\Sigma}{\Delta_m'}{D_m[a_m/x]}}{r(x,f(m),\Pi_m)}

1171: &

1172: \deduce{\NSeq{\Sigma}{\Gamma}{B_0[a_0/x]}}{r(x,f(m+1),\Pi')}

1173: }

1174: $$

1175: \item Suppose $\Pi$ is

1176: $$

1177: \infer[\nablaR]

1178: {\NSeq{\Sigma,x}{B_1, \ldots, B_n}{\nabla y.B}}

1179: {\deduce{\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B[c/y]}}{\Pi_1}}

1180: \enspace .

1181: $$

1182: If $a_0 \not = c$ then $r(x,\vec a, \Pi)$ is

1183: $$

1184: \infer[\nablaR]

1185: {\NSeq{\Sigma,x}{B_1, \ldots, B_n}{\nabla y.B}}

1186: {\deduce{\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B[c/y]}}{r(x,\vec a, \Pi_1)}}

1187: \enspace .

1188: $$

1189: If $a_0 = c$, then we swap $c$ with a fresh constant.

1190: Let $d : \iota$ be a nominal constant not in the support of $B[c/y]$.

1191: We apply the swapping $(c~d)$ to the conclusion of the 

1192: end sequent of $\Pi_1$ according to the construction

1193: in Definition~\ref{def:perm} to get a proof $\Pi_2$

1194: of $\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B_0[d/y]}.$ 

1195: The derivation $r(x,\vec a,\Pi)$ is constructed

1196: as follows:

1197: $$

1198: \infer[\nablaR]

1199: {\NSeq{\Sigma}{B_1[a_1/x],\ldots,B_n[a_n/x]}{\nabla y.B[a_0/x]}}

1200: {\deduce{\NSeq{\Sigma}{B_1[a_1/x],\ldots,B_n[a_n/x]}{B[a_0/x, d/y]}}{r(x,\vec a,\Pi_2)}}

1201: $$

1202: 

1203: \item If $\Pi$ ends with $\nablaL$ apply the same construction as in the

1204: previous case.

1205: 

1206: \item Suppose $\Pi$ ends with $\forallR$

1207: $$

1208: \infer[\forallR]

1209: {\NSeq{\Sigma,x}{B_1,\ldots,B_n}{\forall y.B}}

1210: {\deduce{\NSeq{\Sigma,x,h}{B_1,\ldots,B_n}{B[h\,\vec c/y]}}{\Pi_1}}

1211: \enspace .

1212: $$

1213: Let $\theta = [\lambda \vec c.h'\,\vec c x/h]$

1214: where $h'$ is a variable not in $\Sigma.$

1215: Apply the construction in Definition~\ref{def:subst}

1216: to get the proof $\Pi\theta$ of 

1217: $$

1218: \NSeq{\Sigma,x,h'}{B_1,\ldots,B_n}{B[h'\,\vec a x/y]}

1219: $$

1220: Then $r(x,\vec a, \Pi)$ is 

1221: $$

1222: \infer[\forallR]

1223: {\NSeq{\Sigma}{B_1[a_1/x],\ldots,B_n[a_n/x]}{\forall y.B[a_0/x]}}

1224: {\deduce{\NSeq{\Sigma,h'}{B_1[a_1/x],\ldots,B_n[a_n/x]}

1225:   {B[a_0/x, (h'\,\vec c a_0)/y]}}{r(x,\vec a, \Pi\theta)}

1226: }

1227: \enspace .

1228: $$

1229: \item If $\Pi$ ends with $\existsL$, apply the same construction as in

1230: the previous case.

1231: 

1232: \item Suppose $\Pi$ ends with $\existsR$:

1233: $$

1234: \infer[\existsR]

1235: {\NSeq{\Sigma,x}{B_1,\ldots,B_n}{\exists y.B}}

1236: {\deduce{\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B[t/y]}}{\Pi_1}}

1237: \enspace .

1238: $$

1239: If $a_0\not \in supp(B[t/y])$ then $r(x,\vec a, \Pi)$ is

1240: $$

1241: \infer[\existsR]

1242: {\NSeq{\Sigma}{B_1[a_1/x], \ldots, B_n[a_n/x]}{\exists y.B[a_0/x]}}

1243: {\deduce{\NSeq{\Sigma}{B_1[a_1/x], \ldots, B_n[a_n/x]}{B[a_0/x,t/y]}}{r(x,\vec a,\Pi_1)}}

1244: \enspace .

1245: $$

1246: If $a_0 \in supp(B[t/y]$, we exchange it with a fresh constant. 

1247: Let $d$ be a nominal constant distinct from $a_0$ and not in the

1248: support of $B[t/y].$ Then $((a_0~d).B[t/y])[a_0/x] = B[(a_0~d).t/y,a_0/x].$

1249: We first apply the construction in Definition~\ref{def:perm}

1250: to $\Pi_1$ to get a derivation $\Pi_2$ of 

1251: $\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B[(a_0~d).t/y, a_0/x]}.$

1252: The derivation $r(x,\vec a, \Pi)$ is thus

1253: $$

1254: \infer[\existsR]

1255: {\NSeq{\Sigma}{B_1[a_1/x],\ldots,B[a_n/x]}{\exists y.B[a_0/x]}}

1256: {\deduce{\NSeq{\Sigma}{B_1[a_1/x], \ldots, B_n[a_n/x]}{B[(a_0~d).t/y, a_0/x]}}{r(x,\vec a,\Pi_2)}}

1257: \enspace .

1258: $$

1259: 

1260: 

1261: \item Suppose $\Pi$ ends with $\eqL$:

1262: $$

1263: \infer[\eqL]

1264: {\NSeq{\Sigma,x}{s = t, B_2, \ldots, B_n}{B_0}}

1265: {

1266: \left\{

1267: \raisebox{-1.5ex}

1268: {\deduce{\NSeq{(\Sigma,x)\theta}{B_2\theta,\ldots,B_n\theta}{B_0\theta}}{\Pi_\theta}}

1269: \right\}_\theta

1270: }

1271: $$

1272: where each $\theta$ is a unifier of $(\lambda \vec c.s, \lambda \vec c.t)$ and 

1273: $\{ \vec c \} = supp(s = t).$

1274: We need to show that for each unifier of 

1275: $(\lambda a_1\lambda \vec c.s[a_1/x], \lambda a_1\lambda \vec c.t[a_1/x])$ 

1276: there is a corresponding unifier for $\lambda \vec c.s$ and $\lambda \vec c.t.$ 

1277: We can assume without loss of generality

1278: that $x$ is not in the domain of $\rho$.

1279: 

1280: We first show the case where $x$ is not free in $\rho$. It is clear that

1281: in this case $\rho$ is a unifier of $\lambda \vec c.s$ and $\lambda \vec c.t$. 

1282: Therefore we apply the procedure recursively

1283: to the premise derivation $\Pi_\rho$, to get the derivation

1284: $r(x,\vec a,\Pi_\rho)$

1285: of 

1286: $$

1287: \NSeq{\Sigma\rho}{(B_2[a_2/x])\rho, \ldots, (B_n[a_n/x])\rho}{(B_0[a_0/x])\rho}.

1288: $$

1289: In the other case, where $x$ is free in the range of $\rho$, 

1290: we show that it can be reduced to the previous case.

1291: First we define a substitution $\rho'$ to be the substitution $\rho$  where $x$

1292: is replaced by a new variable $u$ which is not free in $\rho$.

1293: Clearly $\rho'$ is also a unifier of 

1294: $\lambda a_1\lambda \vec c.s[a_1/x]$ and $\lambda a_1\lambda \vec c.t[a_1/x].$

1295: Moreover, it is more general than $\rho$, since $\rho = [x/u] \circ \rho'.$

1296: Therefore we can apply the construction in the previous case

1297: to get a derivation $r(x,\vec a,\Pi_{\rho'})$ and apply the substitution $[x/u]$ to 

1298: to this derivation, using the procedure in Definition~\ref{def:subst}, 

1299: to get a derivation of 

1300: $$

1301: \NSeq{\Sigma\rho}{(B_2[a_2/x])\rho, \ldots, (B_n[a_n/x])\rho}{(B_0[a_0/x])\rho.}

1302: $$

1303: The derivation $r(x,\vec a,\Pi)$ is then constructed as follows

1304: $$

1305: \infer[\eqL]

1306: {\NSeq{\Sigma}{s[a_1/x] = t[a_1/x], \ldots, B_n[a_n/x]}{B_0[a_0/x]}}

1307: {

1308: \left\{

1309: \raisebox{-1.5ex}{

1310: \deduce{\NSeq{\Sigma\rho}{(B_2[a_2/x])\rho, \ldots, (B_n[a_n/x])\rho}{(B_0[a_0/x])\rho}}

1311:   {\Pi_\rho'}

1312: }

1313: \right\}_{\rho}

1314: }

1315: $$

1316: where each $\Pi_{\rho}'$ is constructed as explained above.

1317: 

1318: \item If $\Pi$ ends with $\cL$:

1319: $$

1320: \infer[\cL]

1321: {\Seq{B_1,\ldots,B_j, \ldots, B_n}{B_0}}

1322: {

1323: \deduce{

1324: \Seq{B_1,\ldots,B_j, B_j, \ldots, B_n}{B_0}

1325: }

1326: {\Pi'}

1327: }

1328: $$

1329: then $r(x, \vec a, \Pi)$ is

1330: $$

1331: \infer[\cL]

1332: {\Seq{B_1[a_1/x],\ldots,B_j[a_j/x], \ldots, B_n[a_n/x]}{B_0[a_0/x]}}

1333: {

1334: \deduce{

1335: \Seq{B_1[a_1/x],\ldots,B_j[a_j/x], B_j[a_j/x], \ldots, B_n[a_n/x]}{B_0[a_0/x]}

1336: }

1337: {r(x, (a_0,\dots,a_j,a_j,\dots,a_n), \Pi')}

1338: }

1339: $$

1340: 

1341: 

1342: \item If $\Pi$ ends with any other rule and has premise derivations $\Pi_1$,$\dots$, $\Pi_n$,

1343: then $r(x,\vec a,\Pi)$ ends with the same rule and has premise derivations

1344: $r(x,\vec a,\Pi_1)$, $\dots$, $r(x,\vec a,\Pi_n).$

1345: 

1346: \end{enumerate}

1347: \end{definition}

1348: 

1349: 

1350: \begin{lemma}

1351: \label{lm:weak drv}

1352: For any derivation $\Pi$ of $\NSeq{\Sigma}{\Gamma}{C}$ and any

1353: multiset of $\Sigma$-formulas $\Delta$, $w(\Delta,\Pi)$ is

1354: a derivation of $\NSeq{\Sigma}{\Gamma,\Delta}{C}$

1355: and $ht(w(\Delta,\Pi)) \leq ht(\Pi).$

1356: \end{lemma}

1357: 

1358: \begin{lemma}

1359: \label{lm:subst drv}

1360: For any derivation $\Pi$ of $\NSeq{\Sigma}{\Gamma}{C}$

1361: and any $\Sigma$-substitution $\theta$, $\Pi\theta$ is

1362: a derivation of $\NSeq{\Sigma\theta}{\Gamma\theta}{C\theta}$

1363: and $ht(\Pi\theta) \leq ht(\Pi).$

1364: \end{lemma}

1365: 

1366: \begin{lemma}

1367: \label{lm:perm drv}

1368: For any derivation $\Pi$ of $\Seq{B_1,\ldots,B_n}{B_0}$

1369: and permutations $\vec \pi = \pi_0,\dots,\pi_n$,

1370: $\langle \vec \pi \rangle.\Pi$ is a derivation of

1371: $\Seq{\pi_1.B_1,\ldots,\pi_n.B_n}{\pi_0.B_0}$

1372: and $ht(\langle \vec \pi\rangle.\Pi) \leq ht(\Pi).$

1373: \end{lemma}

1374: 

1375: \begin{lemma}

1376: \label{lm:res drv}

1377: For any derivation $\Pi$ of $\NSeq{\Sigma,x}{B_1,\ldots,B_n}{B_0}$

1378: and any list of nominal constants $\vec a = a_0,\dots,a_n$ such that

1379: $a_i \not \in supp(B_i),$  $r(x,\vec a,\Pi)$ is a derivation

1380: of $\NSeq{\Sigma}{B_1[a_1/x],\ldots,B_n[a_n/x]}{B_0[a_0/x]}$

1381: and $ht(r(x,\vec a,\Pi)) \leq ht(\Pi).$

1382: \end{lemma}

1383: 

1384: \begin{lemma}

1385: \label{lm:subst}{\em Substitutions.} 

1386: Let $\Pi$ be a proof of $\NSeq{\Sigma}{\Gamma}{C}$

1387: and let $\theta$ be a $\Sigma$-substitution.

1388: Then there exists a proof $\Pi'$ of

1389: $\NSeq{\Sigma\theta}{\Gamma\theta}{C\theta}$ such

1390: that $ht(\Pi') \leq ht(\Pi).$

1391: \end{lemma}

1392: \begin{proof}

1393: Follows immediately from Lemma~\ref{lm:subst drv}.

1394: \qed

1395: \end{proof}

1396: 

1397: \begin{lemma}

1398: \label{lm:perm} {\em Permutations.}

1399: Let $\Pi$ be a proof of $\NSeq \Sigma {B_1, \ldots, B_n} {B_0}.$

1400: Then there exists a proof $\Pi'$ of 

1401: $\NSeq{\Sigma}{\pi_1.B_1, \ldots, \pi_n.B_n}{\pi_0.B_0}$

1402: such that $ht(\Pi') \leq ht(\Pi).$

1403: \end{lemma}

1404: \begin{proof}

1405: Follows immediately from Lemma~\ref{lm:perm drv}.

1406: \qed

1407: \end{proof}

1408: 

1409: \begin{lemma}

1410: \label{lm:res}{\em Restricted name substitutions.}

1411: Let $\Pi$ be a proof of 

1412: $$\NSeq{\Sigma,x:\iota}{B_1, \ldots, B_n}{B_0}.$$

1413: Then there exists a proof of $\Pi'$ of

1414: $\NSeq{\Sigma}{B_1[a_1/x], \ldots, B_n[a_n/x]}{B_0[a_0/x]},$

1415: where $a_i \not \in supp(B_i)$ for each $i \in \{0,\dots,n\},$

1416: such that $ht(\Pi') \leq ht(\Pi).$

1417: \end{lemma}

1418: \begin{proof}

1419: Follows immediately from Lemma~\ref{lm:res drv}.

1420: \qed

1421: \end{proof}

1422: 

1423: The next two lemmas are crucial to the cut-elimination proof: they allow

1424: one to reintroduce the symmetry between $\forallL$ and $\forallR$,

1425: and dually, between $\existsL$ and $\existsR$ rules.

1426: 

1427: \begin{lemma}

1428: \label{lm:supp1}{\em Support extension.}

1429: Let $\Pi$ be a proof of $\NSeq{\Sigma,h}{\Gamma}{B[h~\vec{a}/x]}$

1430: where $\{\vec a\} = supp(B)$, 

1431: $h \not \in \Sigma$ and $h$ is not free in $\Gamma$ and $B$. 

1432: Let $\vec{c}$ be a list of nominal constants not in the support

1433: of $B$. Then there exists a proof $\Pi'$ of

1434: $\NSeq{\Sigma, h'}{\Gamma}{B[h'~\vec{a}\vec{c}/x]}$ where

1435: $h' \not \in \Sigma.$

1436: \end{lemma}

1437: \begin{proof}

1438: Suppose $\vec c$ is the list of constants 

1439: $c_1 : \iota_1,\ldots,c_n : \iota_n$. 

1440: Let $\vec y = y_1 : \iota_1,\ldots, y_n:\iota_n$

1441: be a list of distinct variables not appearing in $\Sigma \cup \{h, h'\}$. 

1442: We first apply the substitution $[\lambda \vec a.h'\,\vec c \vec x/h]$

1443: to the sequent $\NSeq{\Sigma,h}{\Gamma}{B[h\vec a/x]}.$

1444: By Lemma~\ref{lm:subst}, there is a proof $\Pi_1$ of

1445: $$

1446: \NSeq{\Sigma, h', \vec y}{\Gamma}{B[h'\,\vec a \vec y/x]}

1447: $$

1448: The derivation $\Pi'$ is then obtained by repeatedly applying 

1449: Lemma~\ref{lm:res} to $\Pi_1$ to change $\vec y$ into

1450: $\vec c$.

1451: \qed

1452: \end{proof}

1453: 

1454: 

1455: \begin{lemma}

1456: \label{lm:supp2}{\em Support extension.}

1457: Let $\Pi$ be a proof of $\NSeq{\Sigma,h}{B[h~\vec{a}/x], \Gamma}{C}$

1458: where $\{\vec a\} = supp(B)$, 

1459: $h \not \in \Sigma$ and $h$ is not free in $\Gamma$, $B$ and $C$. 

1460: Let $\vec{c}$ be a list of nominal constants not in the support

1461: of $B$. Then there exists a proof $\Pi'$ of

1462: $\NSeq{\Sigma, h'}{B[h'~\vec{a}\vec{c}/x], \Gamma}{C}$ where

1463: $h' \not \in \Sigma.$

1464: \end{lemma}

1465: \begin{proof}

1466: Use the same construction as in the proof of Lemma~\ref{lm:supp1}.

1467: \qed

1468: \end{proof}

1469: 

1470: 

1471: 

1472: \section{Cut reduction}

1473: \label{sec:reduct}

1474: 

1475: We define a {\em reduction} relation between derivations, following closely

1476: the reduction relation in ~\cite{mcdowell00tcs}.

1477: For simplicity of presentation, we shall omit the signatures in the sequents

1478: in the following reduction of cuts when the signatures are not changed 

1479: by the reduction or when it is clear from context

1480: which signatures should be assigned to the sequents.

1481: The redex is always a derivation $\Xi$ ending with the multicut rule

1482: \begin{displaymath}

1483: \infer[\mc]{\NSeq{\Sigma}{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1484:         {\deduce{\NSeq{\Sigma}{\Delta_1}{B_1}}

1485:                 {\Pi_1}

1486:         & \cdots

1487:         & \deduce{\NSeq{\Sigma}{\Delta_n}{B_n}}

1488:                 {\Pi_n}

1489:         & \deduce{\NSeq{\Sigma}{B_1,\ldots,B_n,\Gamma}{C}}

1490:                 {\Pi}}

1491: \enspace .

1492: \end{displaymath}

1493: We refer to the formulas $B_1,\dots,B_n$ produced by the

1494: $\mc$ as {\em cut formulas}.

1495: 

1496: If $n=0$, $\Xi$ reduces to the premise derivation $\Pi$.

1497: 

1498: For $n > 0$ we specify the reduction relation based on the last rule

1499: of the premise derivations.

1500: If the rightmost premise derivation $\Pi$ ends with a left rule acting

1501: on a cut formula $B_i$, then the last rule of $\Pi_i$ and the last

1502: rule of $\Pi$ together determine the reduction rules that apply.

1503: We classify these rules according to the following criteria: we call

1504: the rule an {\em essential} case when $\Pi_i$ ends with a right rule;

1505: if it ends with a left rule, it is a {\em left-commutative} case;

1506: if $\Pi_i$ ends with the $\init$ rule, then we have an {\em axiom}

1507: case; a {\em multicut} case arises when it ends with the $\mc$ rule.

1508: When $\Pi$ does not end with a left rule acting on a cut formula, then

1509: its last rule is alone sufficient to determine the reduction rules

1510: that apply.

1511: If $\Pi$ ends in a rule acting on a formula other than a cut

1512: formula, then we call this a {\em right-commutative} case.

1513: A {\em structural} case results when $\Pi$ ends with a contraction or weakening on

1514: a cut formula.

1515: If $\Pi$ ends with the $\init$ rule, this is also an axiom case;

1516: similarly a multicut case arises if $\Pi$ ends in the $\mc$ rule.

1517: 

1518: For simplicity of presentation, we always show $i = 1$. 

1519: 

1520: 

1521: \noindent{\em \underline{Essential cases:}}

1522: 

1523: \noindent $\landR/\landL$: If $\Pi_1$ and $\Pi$ are

1524: \begin{displaymath}

1525: \infer[\landR]{\Seq{\Delta_1}{B_1' \land B_1''}}

1526:         {\deduce{\Seq{\Delta_1}{B_1'}}

1527:                 {\Pi_1'}

1528:         & \deduce{\Seq{\Delta_1}{B_1''}}

1529:                 {\Pi_1''}}

1530: \qquad\qquad\qquad

1531: \infer[\landL]{\Seq{B_1' \land B_1'',B_2,\ldots,B_n,\Gamma}{C}}

1532:         {\deduce{\Seq{B_1',B_2,\ldots,B_n,\Gamma}{C}}

1533:                 {\Pi'}}

1534: \enspace ,

1535: \end{displaymath}

1536: then $\Xi$ reduces to

1537: \begin{displaymath}

1538: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1539:         {\deduce{\Seq{\Delta_1}{B_1'}}

1540:                 {\Pi_1'}

1541:         & \deduce{\Seq{\Delta_2}{B_2}}

1542:                 {\Pi_2}

1543:         & \cdots

1544:         & \deduce{\Seq{\Delta_n}{B_n}}

1545:                 {\Pi_n}

1546:         & \deduce{\Seq{B_1',B_2,\ldots,B_n,\Gamma}{C}}

1547:                 {\Pi'}}

1548: \enspace .

1549: \end{displaymath}

1550: The case for the other $\landL$ rule is symmetric.

1551: 

1552: \vskip12pt

1553: 

1554: \noindent $\lorR/\lorL$: If $\Pi_1$ and $\Pi$ are

1555: \begin{displaymath}

1556: \infer[\lorR]{\Seq{\Delta_1}{B_1' \lor B_1''}}

1557:         {\deduce{\Seq{\Delta_1}{B_1'}}

1558:                 {\Pi_1'}}

1559: \qquad\qquad\!\!\!

1560: \infer[\lorL]{\Seq{B_1' \lor B_1'',B_2,\ldots,B_n,\Gamma}{C}}

1561:         {\deduce{\Seq{B_1',B_2,\ldots,B_n,\Gamma}{C}}

1562:                 {\Pi'}

1563:         & \deduce{\Seq{B_1'',B_2,\ldots,B_n,\Gamma}{C}}

1564:                 {\Pi''}}

1565: \enspace ,

1566: \end{displaymath}

1567: then $\Xi$ reduces to

1568: \begin{displaymath}

1569: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1570:         {\deduce{\Seq{\Delta_1}{B_1'}}

1571:                 {\Pi_1'}

1572:         & \deduce{\Seq{\Delta_2}{B_2}}

1573:                 {\Pi_2}

1574:         & \cdots

1575:         & \deduce{\Seq{\Delta_n}{B_n}}

1576:                 {\Pi_n}

1577:         & \deduce{\Seq{B_1',B_2,\ldots,B_n,\Gamma}{C}}

1578:                 {\Pi'}}

1579: \enspace .

1580: \end{displaymath}

1581: The case for the other $\lorR$ rule is symmetric.

1582: 

1583: \vskip12pt

1584: 

1585: \noindent $\oimpR/\oimpL$: Suppose $\Pi_1$ and $\Pi$ are

1586: \begin{displaymath}

1587: \infer[\oimpR]{\Seq{\Delta_1}{B_1' \oimp B_1''}}

1588:         {\deduce{\Seq{B_1',\Delta_1}{B_1''}}

1589:                 {\Pi_1'}}

1590: \qquad\qquad\!\!

1591: \infer[\oimpL]{\Seq{B_1' \oimp B_1'',B_2,\ldots,B_n,\Gamma}{C}}

1592:         {\deduce{\Seq{B_2,\ldots,B_n,\Gamma}{B_1'}}

1593:                 {\Pi'}

1594:         & \deduce{\Seq{B_1'',B_2,\ldots,B_n,\Gamma}{C}}

1595:                 {\Pi''}}

1596: \enspace .

1597: \end{displaymath}

1598: Let $\Xi_1$ be

1599: \begin{displaymath}

1600: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{B_1''}}

1601:         {\infer[\mc]{\Seq{\Delta_2,\ldots,\Delta_n,\Gamma}{B_1'}}

1602:                 {\left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_i}{B_i}}

1603:                         {\Pi_i}}\right\}_{i \in \{2..n\}}

1604:                 & \raisebox{-2.5ex}{\deduce{\Seq{B_2,\ldots,B_n,\Gamma}{B_1'}}

1605:                         {\Pi'}}}

1606:         & \deduce{\Seq{B_1',\Delta_1}{B_1''}}

1607:                 {\Pi_1'}}

1608: \enspace .

1609: \end{displaymath}

1610: Then $\Xi$ reduces to

1611: \settowidth{\infwidthi}

1612:         {$\Seq{\Delta_1,\ldots,\Delta_n,\Gamma,\Delta_2,\ldots,\Delta_n,\Gamma}{C}$}

1613: \begin{displaymath}

1614: \infer{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1615:         {\infer[\cL]{\makebox[\infwidthi]{}}

1616:                 {\infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma,

1617:                                         \Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1618:                         {\raisebox{-2.5ex}{\deduce{\Seq{\ldots}{B_1''}}

1619:                                 {\Xi_1}}

1620:                         & \left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_i}{B_i}}

1621:                                 {\Pi_i}}\right\}_{i \in \{2..n\}}

1622:                         & \raisebox{-2.5ex}{\deduce{\Seq{B_1'',\{B_i\}_{i \in \{2..n\}},\Gamma}{C}}

1623:                                 {\Pi''}}}}}

1624: \enspace .

1625: \end{displaymath}

1626: We use the double horizontal lines to indicate that the relevant

1627: inference rule (in this case, $\cL$) may need to be applied zero or

1628: more times.

1629: 

1630: \vskip12pt

1631: 

1632: \noindent $\forallR/\forallL$: Suppose $\Pi_1$ and $\Pi$ are

1633: \begin{displaymath}

1634: \infer[\forallR]

1635: {\NSeq{\Sigma}{\Delta_1}{\forall x.B_1'}}

1636: {\deduce{\NSeq{\Sigma, h}{\Delta_1}{B_1'[(h\,\vec{c})/x]}}

1637:                 {\Pi_1'}}

1638: \qquad\qquad\qquad

1639: \infer[\forallL]

1640: {\NSeq{\Sigma}{\forall x.B_1',B_2,\ldots,B_n,\Gamma}{C}}

1641: {\deduce{\NSeq{\Sigma}{B_1'[t/x],B_2,\ldots,B_n,\Gamma}{C}}

1642:                 {\Pi'}}

1643: \enspace ,

1644: \end{displaymath}

1645: where $\{\vec c\} = supp(B_1').$

1646: Let $\{\vec d\} = supp(B_1'[t/x]) \setminus supp(B_1').$

1647: Apply Lemma~\ref{lm:supp1} to get a derivation

1648: $\Pi_1''$ of $\NSeq{\Sigma,h'}{\Delta_1}{B_1'[(h\,\vec c\vec d)/x]}.$

1649: The derivation $\Xi$ reduces to

1650: 

1651: \begin{displaymath}

1652: \infer[\mc]

1653: {\NSeq{\Sigma}{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1654: {\raisebox{-2.5ex}

1655:    {\deduce{\NSeq{\Sigma}{\Delta_1}{B_1'[t/x]}}

1656:            {\Pi_1''[\lambda\vec{c}\vec d.t/h']}}

1657:   & \left\{\raisebox{-1.5ex}

1658:            {\deduce{\NSeq{\Sigma}{\Delta_i}{B_i}}

1659:                    {\Pi_i}}\right\}_{i \in \{2..n\}}

1660:   & \raisebox{-2.5ex}{\deduce{\Seq{\ldots}{C}}

1661:                 {\Pi'}}}

1662: \enspace .

1663: \end{displaymath}

1664: 

1665: \vskip12pt

1666: 

1667: \noindent $\existsR/\existsL$:

1668: Suppose $\Pi_1$ and $\Pi$ are

1669: \begin{displaymath}

1670: \infer[\existsR]

1671: {\NSeq{\Sigma}{\Delta_1}{\exists x.B_1'}}

1672:         {\deduce{\NSeq{\Sigma}{\Delta_1}{B_1'[t/x]}}

1673:                 {\Pi_1'}}

1674: \qquad\qquad\qquad

1675: \infer[\existsL]

1676: {\NSeq{\Sigma}{\exists x.B_1',B_2,\ldots, B_n,\Gamma}{C}}

1677: {\deduce{\NSeq{\Sigma,h}{B_1'[(h\,\vec{c})/x],B_2,\ldots,B_n,

1678:             \Gamma}{C}}

1679:                 {\Pi'}}

1680: \enspace ,

1681: \end{displaymath}

1682: where $\{\vec c\} = supp(B_1').$

1683: Let $\{\vec d\} = supp(B_1'[t/x])\setminus supp(B_1').$

1684: Apply Lemma~\ref{lm:supp2} to $\Pi'$ to get a derivation $\Pi''$

1685: of $\NSeq{\Sigma,h'}{\Delta_1}{B_1'[(h'\,\vec c\vec d)/x]}.$

1686: Then $\Xi$ reduces to

1687: \begin{displaymath}

1688: \infer[\mc]{\NSeq{\Sigma}{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1689:   {\deduce{\NSeq{\Sigma}{\Delta_1}{B_1'[t/x]}}{\Pi_1'}

1690:   & \ldots

1691:   & \deduce{\NSeq{\Sigma}{B_1'[t/x], B_2,\dots,\Gamma}{C}}

1692:               {\Pi''[\lambda \vec{c}\vec d.t/h']}

1693:         }

1694: \enspace .

1695: \end{displaymath}

1696: 

1697: \vskip12pt

1698: 

1699: \noindent $\nablaR/\nablaL$: Suppose $\Pi_1$ and $\Pi$ are

1700: \begin{displaymath}

1701: \infer[\nablaR]

1702: {\Seq{\Delta_1}{\nabla x.B_1'}}

1703:      {\deduce{\Seq{\Delta_1}{B_1'[a/x]}}

1704:            {\Pi_1'}}

1705: \qquad\qquad\qquad

1706: \infer[\nablaL]{\Seq{\nabla x.B_1',\ldots,

1707:        B_n,\Gamma}{C}}

1708:   {\deduce{\Seq{B_1'[b/x],\ldots,B_n,

1709:             \Gamma}{C}}

1710:                 {\Pi'}}

1711: \enspace .

1712: \end{displaymath}

1713: Apply the construction in Definition~\ref{def:perm}

1714: to to $\Pi_1'$ to swap $a$ with $b$ to get a derivation $\Pi_1''$

1715: of $\Seq{\Delta_1}{B_1'[b/x]}.$

1716: $\Xi$ reduces to

1717: \begin{displaymath}

1718: \infer[\mc]

1719: {\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1720: {

1721:    \deduce{\Seq{\Delta_1}{B_1'[b/x]}}{\Pi_1''}

1722:     & \ldots

1723:         & 

1724:     \deduce{\Seq{B_1'[b/x], \dots,B_n, \Gamma}{C}}

1725:            {\Pi'}

1726: }

1727: \enspace .

1728: \end{displaymath}

1729: 

1730: \vskip12pt

1731: 

1732: \noindent $\natR/\natL:$

1733: Suppose $\Pi_1$ is

1734: $

1735: \infer[\natR]

1736: {\Seq {\Delta_1} {nat~z}}

1737: {}

1738: $

1739: and $\Pi$ is

1740: $$

1741: \infer[\natL]

1742: {\Seq{nat~z, B_2, \ldots, B_n, \Gamma}{C}}

1743: {

1744: \deduce{\Seq{}{D~z}}{\Pi'} &

1745: \deduce{\Seq{D~j}{D~(s\,j)}}{\Pi''} &

1746: \deduce{\Seq{D~z, B_2, \ldots, B_n, \Gamma}{C}}{\Pi'''}

1747: }

1748: \enspace .

1749: $$

1750: Then $\Xi$ reduces to

1751: \begin{displaymath}

1752:    \infer[\mc]

1753:    {\Seq{\Delta_1,\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1754:    {\raisebox{-1.5ex}{\deduce{\Seq {\Delta_1}{D~z}}{w(\Delta_1,\Pi')}} &

1755:     \left\{\raisebox{-1.5ex}

1756:       {\deduce{\Seq {\Delta_i}{B_i}}{\Pi_i}}

1757:     \right\}_{i\in\{2\dots n\}} &

1758:     \raisebox{-1.5ex}{\deduce{\Seq{D~z,  B_2, \ldots, B_n, \Gamma}{C}}{\Pi'''}}

1759:    }

1760: \end{displaymath}

1761: 

1762: 

1763: \vskip12pt

1764: 

1765: \noindent $\natR/\natL:$

1766: Suppose $\Pi_1$ is

1767: $$

1768: \infer[\natR]

1769: {\Seq{\Delta_1}{nat~(s\,I)}}

1770: {\deduce{\Seq{\Delta}{nat\,I}}{\Pi_1'}}

1771: $$

1772: and $\Pi$ is

1773: $$

1774: \infer[\natL]

1775: {\Seq{nat~(s\,I), B_2, \ldots, B_n, \Gamma} C}

1776: {

1777: \deduce{\Seq{}{D\,z}}{\Pi'} &

1778: \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''} &

1779: \deduce{\Seq{D\,(s\,I), B_2, \ldots, B_n, \Gamma}{C}}{\Pi'''}

1780: }

1781: $$

1782: Let $\Xi_1$ be

1783: $$

1784: \infer[mc.]

1785: {\Seq{\Delta_1}{D~I}}

1786: {

1787: \deduce{\Seq{\Delta_1}{nat\,I}}{\Pi_1'}

1788: &

1789: \infer[\natL]

1790: {\Seq{nat\,I}{D\,I}}

1791: {

1792: \deduce{\Seq{}{D\,z}}{\Pi'}

1793: &

1794: \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''}

1795: &

1796: \infer[id_\pi]{\Seq{D\,I}{D\,I}}{}

1797: }

1798: }

1799: $$

1800: Suppose $\{\vec c \} = supp(I).$

1801: We apply the procedures in Definition~\ref{def:subst}

1802: and Definition~\ref{def:res} to $\Pi''$ to obtain

1803: the derivation $\Pi^\bullet$ of

1804: $$

1805: \NSeq{h}{D\,(h\,\vec c)}{D\,(s\,(h\,\vec c))}.

1806: $$

1807: Let $\Xi_2$ be

1808: $$

1809: \infer[mc.]

1810: {\Seq{\Delta_1}{D\,(s\,I)}}

1811: {

1812: \deduce{\Seq{\Delta_1}{D\,I}}{\Xi_1}

1813: &

1814: \deduce{\Seq{D\,I}{D\,(s\,I)}}{\Pi^{\bullet}[\lambda \vec c.I/h]}

1815: }

1816: $$

1817: Then $\Xi$ reduces to

1818: $$

1819: \infer[mc.]

1820: {\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1821: {

1822: \deduce{\Seq{\Delta_1}{D\,(s\,I)}}{\Xi_2}

1823: &

1824: \deduce{\Seq{\Delta_2}{B_2}}{\Pi_2}

1825: &

1826: \ldots

1827: &

1828: \deduce{\Seq{\Delta_n}{B_n}}{\Pi_n}

1829: &

1830: \deduce{\Seq{D\,(s\,I), B_2,\dots,B_n,\Gamma}{C}}{\Pi'''}

1831: }

1832: $$

1833: 

1834: \vskip12pt

1835: 

1836: \noindent $\eqL/\eqR:$

1837: If $\Pi_1$ and $\Pi$ are

1838: $$

1839: \infer[\eqR]

1840: {\NSeq{\Sigma}{\Delta_1}{t=t}}

1841: {}

1842: \qquad

1843: \infer[\eqL]

1844: {\NSeq{\Sigma}{t=t, \Gamma}{C}}

1845: {

1846: \left\{

1847: \raisebox{-1.5ex}

1848: {\deduce{\NSeq{\Sigma\theta}{\Gamma\theta}{C\theta}}{\Pi_\theta}}

1849: \right\}_\theta

1850: }

1851: $$

1852: then $\Xi$ reduces to 

1853: $$

1854: \infer[mc]

1855: {\NSeq{\Sigma}{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

1856: {

1857: \deduce{\NSeq{\Sigma}{\Delta_2}{B_2}}{\Pi_2}

1858: &

1859: \ldots

1860: &

1861: \deduce{\NSeq{\Sigma}{\Delta_n}{B_n}}{\Pi_n}

1862: &

1863: \deduce{\NSeq{\Sigma}{\Delta_1,B_2,\ldots,B_n,\Gamma}{C}}{w(\Delta_1,\Pi_\epsilon)}

1864: }

1865: $$

1866: where $\epsilon$ is the empty substitution.

1867: 

1868: \noindent $\defR/\defL$:

1869: Suppose $\Pi_1$ and $\Pi$ are

1870: $$

1871: \infer[\defR]

1872: {\Seq{\Delta_1}{p\,\bar{t}}}

1873:   {\deduce{\Seq{\Delta_1}{B[\vec{t}/\vec x]}}{\Pi_1'}}

1874: \qquad \qquad

1875: \infer[\defL]{\Seq{p\,\vec{t},B_2,\dots,\Gamma}{C}}

1876:   {

1877:    \deduce

1878:       {\Seq{B[\vec{t}/\vec x],B_2, \dots,\Gamma}{C}}

1879:       {\Pi'}

1880:   }  

1881: \enspace .  

1882: $$

1883: Then $\Xi$ reduces to

1884: $$

1885: \infer[\mc]

1886: {\Seq{\Delta_1,\dots,\Delta_n,\Gamma}{C}}

1887: {

1888: \deduce{\Seq{\Delta_1}{B[\vec{t}/\vec x]}}

1889:    {\Pi_1'}

1890: &

1891: \deduce{\Seq{\Delta_2}{B_2}}{\Pi_2}

1892: &

1893: \ldots

1894: &

1895: \deduce{\Seq{\Delta_n}{B_n}}{\Pi_n}

1896: &

1897: \deduce{\Seq{B[\vec t/\vec x], \dots, \Gamma}{C}}{\Pi'}   

1898: }

1899: \enspace .

1900: $$

1901: 

1902: \vskip12pt

1903: 

1904: \newcommand{\bulletL}{\bullet{\cal L}}

1905: \newcommand{\circL}{\circ{\cal L}}

1906: 

1907: \noindent{\em \underline{Left-commutative cases:}}

1908: 

1909: \vskip12pt

1910: 

1911: \noindent $\bulletL/\circL$:

1912: Suppose $\Pi$ ends with a left rule other than $\cL$

1913: acting on $B_1$ and $\Pi_1$ is

1914: \begin{displaymath}

1915: \infer[\bulletL]

1916: {\Seq{\Delta_1}{B_1}}

1917: {\left\{

1918:   \raisebox{-1.5ex}

1919:   {\deduce{\Seq{\Delta_1^i}{B_1}

1920:   }

1921:   {\Pi_1^i}}

1922: \right\}

1923: }

1924: \enspace ,

1925: \end{displaymath}

1926: where $\bulletL$ is any left rule except $\oimpL$, $\eqL$, or

1927: $\natL$. 

1928: Then $\Xi$ reduces to

1929: \settowidth{\infwidthi}

1930: {$\left\{\raisebox{-3.5ex}

1931:   {\infer[\mc]{\Seq{\Delta_1^i,\Delta_2,\ldots,\Delta_n,\Gamma}

1932:     {C}}

1933:   {\raisebox{-2.5ex}{\deduce{\Seq{\Delta_1^i}{B_1}}

1934:        {\Pi_1^i}}

1935:   & \left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_j}{B_j}}

1936:                         {\Pi_j}}\right\}_{j \in \{2..n\}}

1937:                 & \raisebox{-2.5ex}{\deduce{\Seq{B_1,\ldots,B_n,\Gamma}{C}}

1938:                         {\Pi}}}}\right\}$}

1939: \settowidth{\infwidthii}{\mc}

1940: \begin{displaymath}

1941: \infer[\bulletL]

1942: {\Seq{\Delta_1,\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1943: {\deduce{\makebox[\infwidthi]{}}

1944:   {\left\{\raisebox{-3.5ex}

1945:       {\infer[\mc]

1946:           {\Seq{\Delta_1^i,\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1947:           {\raisebox{-2.5ex}{

1948:              \deduce{\Seq{\Delta_1^i}{B_1}}

1949:                     {\Pi_1^i}}

1950:          & \left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_j}{B_j}}

1951:                  {\Pi_j}}\right\}_{j \in \{2..n\}}

1952:          & \raisebox{-2.5ex}{\deduce{\Seq{B_1,\ldots,B_n,\Gamma}{C}}

1953:                  {\Pi}}}}\right\}\makebox[\infwidthii]{}}}

1954: \enspace .

1955: \end{displaymath}

1956: 

1957: \vskip12pt

1958: \noindent $\oimpL/\circL$:

1959: Suppose $\Pi$ ends with a left rule other than $\cL$ acting

1960: on $B_1$ and $\Pi_1$ is

1961: \begin{displaymath}

1962: \infer[\oimpL]

1963: {\Seq{D_1' \oimp D_1'',\Delta_1'}{B_1}}

1964: {\deduce{\Seq{\Delta_1'}{D_1'}}

1965:                 {\Pi_1'}

1966:         & \deduce{\Seq{D_1'',\Delta_1'}{B_1}}

1967:                 {\Pi_1''}}

1968: \enspace .

1969: \end{displaymath}

1970: Let $\Xi_1$ be

1971: \begin{displaymath}

1972: \infer[\mc]

1973: {\Seq{D_1'',\Delta_1',\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1974:         {\deduce{\Seq{D_1'',\Delta_1'}{B_1}}

1975:                 {\Pi_1''}

1976:         & \deduce{\Seq{\Delta_2}{B_2}}

1977:                 {\Pi_2}

1978:         & \cdots

1979:         & \deduce{\Seq{\Delta_n}{B_n}}

1980:                 {\Pi_n}

1981:         & \deduce{\Seq{B_1,\ldots,B_n,\Gamma}{C}}

1982:                 {\Pi}}

1983: \enspace .

1984: \end{displaymath}

1985: Then $\Xi$ reduces to

1986: \begin{displaymath}

1987: \infer[\oimpL]

1988: {\Seq{D_1' \oimp D_1'',\Delta_1',\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1989: {

1990:  \deduce{\Seq{\Delta_1',\Delta_2,\ldots,\Delta_n,\Gamma}{D_1'}}

1991:   {w(\Delta_2\cup \dots \cup \Delta_n\cup \Gamma, \Pi_1')}

1992:   & 

1993: \deduce{\Seq{D_1'',\Delta_1',\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

1994:                 {\Xi_1}

1995: }

1996: \enspace .

1997: \end{displaymath}

1998: 

1999: \vskip12pt

2000: 

2001: \noindent $\natL/\circL:$

2002: Suppose $\Pi$ ends with a left rule other than $\cL$ acting on $B_1$

2003: and $\Pi_1$ is

2004: $$

2005: \infer[\natL]

2006: {\Seq{nat\,I, \Delta_1'}{B_1}}

2007: {\deduce{\Seq{}{D_1\,z}}{\Pi_1^1}

2008: & \deduce{\Seq{D_1\,j}{D_1(s\,j)}}{\Pi_1^2} 

2009: & \deduce{\Seq{D_1 I, \Delta_1'}{B_1}}{\Pi_1^3}

2010: }

2011: $$

2012: Let $\Xi_1$ be

2013: $$

2014: \infer[mc]

2015: {\Seq{D_1 I, \Delta_1', \Delta_2, \ldots, \Delta_n, \Gamma}{C}}

2016: {

2017: \deduce{\Seq{D_1 I, \Delta_1'}{B_1}}{\Pi_1^3}

2018: &

2019: \deduce{\Seq{\Delta_2}{B_2}}{\Pi_2}

2020: &

2021: \ldots

2022: &

2023: \deduce{\Seq{\Delta_n}{B_n}}{\Pi_n}

2024: &

2025: \deduce{\Seq{B_1,\ldots,B_n}{C}}{\Pi}

2026: }

2027: $$

2028: Then $\Xi$ reduces to

2029: $$

2030: \infer[\natL]

2031: {\Seq{nat\,I, \Delta_1', \Delta_2, \ldots,\Delta_n,\Gamma}{C}}

2032: {

2033: \deduce{\Seq{}{D_1 z}}{\Pi_1^1}

2034: &

2035: \deduce{\Seq{D_1 j}{D_1 (s\,j)}}{\Pi_1^2}

2036: &

2037: \deduce{\Seq{D_1 I, \Delta_1', \Delta_2,\ldots,\Delta_2,\Gamma}{C}}{\Xi_1}

2038: }

2039: $$

2040: 

2041: \vskip12pt

2042: 

2043: \noindent $\eqL/\circL:$

2044: If $\Pi$ ends with a left rule other than $\cL$ acting

2045: on $B_1$ and $\Pi_1$ is

2046: $$

2047: \infer[\eqL]

2048: {\Seq{s=t, \Delta_1'}{B_1}}

2049: {

2050: \left\{

2051: \raisebox{-1.5ex}

2052: {\deduce{\Seq{\Delta_1'\theta}{B_1\theta}}{\Pi^\theta}}

2053: \right\}_\theta

2054: }

2055: $$

2056: then $\Xi$ reduces to

2057: $$

2058: \infer[\eqL]

2059: {

2060: \Seq{\qquad \qquad \qquad \quad

2061: s=t,\Delta_1',\Delta_2,\ldots,\Delta_n,\Gamma}{C

2062: \qquad \qquad \qquad \qquad \qquad \qquad}

2063: }

2064: {

2065: \left\{

2066: \raisebox{-1.5ex}

2067: {

2068: \infer[mc]

2069: {\Seq{\Delta_1'\theta, \Delta_2\theta,\ldots, \Delta_n\theta,

2070: \Gamma\theta}{C\theta}}

2071: {

2072: \deduce{\Seq{\Delta_1'\theta}{B_1\theta}}{\Pi^\theta}

2073: &

2074: \deduce{\Seq{\Delta_2\theta}{B_2\theta}}{\Pi_2\theta}

2075: &

2076: \ldots

2077: &

2078: \deduce{\Seq{\Delta_n\theta}{B_n\theta}}{\Pi_n\theta}

2079: &

2080: \deduce{\Seq{B_1\theta,\ldots,B_n\theta,\Gamma\theta}{C\theta}}{\Pi\theta}

2081: }

2082: }

2083: \right\}_\theta

2084: }

2085: $$

2086: 

2087: \vskip12pt

2088: 

2089: \noindent{\em \underline{Right-commutative cases:}}

2090: 

2091: \vskip12pt

2092: 

2093: \noindent $-/\circL$:

2094: Suppose $\Pi$ is

2095: \begin{displaymath}

2096: \infer[\circL]

2097: {\Seq{B_1,\ldots,B_n,\Gamma}{C}}

2098: {\left\{\raisebox{-1.5ex}

2099: {\deduce{\Seq{B_1,\ldots,B_n,\Gamma^i}{C}}

2100:  {\Pi^i}}\right\}}

2101: \enspace ,

2102: \end{displaymath}

2103: where $\circL$ is any left rule other than $\oimpL$, $\eqL$,

2104: or $\natL$ (but including $\cL$) acting on a formula other

2105: than $B_1, \ldots, B_n$. 

2106: The derivation $\Xi$ reduces to

2107: \settowidth{\infwidthi}

2108:         {$\left\{\raisebox{-2.45ex}{

2109:           \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma^i}{C}}

2110:                 {\deduce{\Seq{\Delta_1}{B_1}}

2111:                         {\Pi_1'}

2112:                 & \cdots

2113:                 & \deduce{\Seq{\Delta_n}{B_n}}

2114:                         {\Pi_n'}

2115:                 & \deduce{\Seq{B_1,\ldots,B_n,\Gamma^i}{C}}

2116:                         {\Pi^i}}}\right\}$}

2117: \settowidth{\infwidthii}{\mc}

2118: \begin{displaymath}

2119: \infer[\circL]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

2120:         {\deduce{\makebox[\infwidthi]{}}

2121:             {\left\{\raisebox{-2.45ex}{

2122:              \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma^i}{C}}              

2123:              {\deduce{\Seq{\Delta_1}{B_1}}

2124:                         {\Pi_1}

2125:                 & \cdots

2126:                 & \deduce{\Seq{\Delta_n}{B_n}}

2127:                         {\Pi_n}

2128:                 & \deduce{\Seq{B_1,\ldots,B_n,\Gamma^i}{C}}

2129:                         {\Pi^i}}}\right\}\makebox[\infwidthii]{}}}

2130: \enspace ,

2131: \end{displaymath}

2132: 

2133: \noindent $-/\oimpL$:

2134: Suppose $\Pi$ is

2135: \begin{displaymath}

2136: \infer[\oimpL]{\Seq{B_1,\ldots,B_n, D' \oimp D'',\Gamma'}{C}}

2137:         {\deduce{\Seq{B_1,\ldots,B_n,\Gamma'}{D'}}

2138:                 {\Pi'}

2139:         & \deduce{\Seq{B_1,\ldots,B_n,D'',\Gamma'}{C}}

2140:                 {\Pi''}}

2141: \enspace .

2142: \end{displaymath}

2143: Let $\Xi_1$ be

2144: \begin{displaymath}

2145: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma'}{D'}}

2146:         {\deduce{\Seq{\Delta_1}{B_1}}

2147:                 {\Pi_1}

2148:         & \cdots

2149:         & \deduce{\Seq{\Delta_n}{B_n}}

2150:                 {\Pi_n}

2151:         & \deduce{\Seq{B_1,\ldots,B_n,\Gamma'}{D'}}

2152:                 {\Pi'}}

2153: \end{displaymath}

2154: and $\Xi_2$ be

2155: \begin{displaymath}

2156: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,D'',\Gamma'}{C}}

2157:         {\deduce{\Seq{\Delta_1}{B_1}}

2158:                 {\Pi_1}

2159:         & \cdots

2160:         & \deduce{\Seq{\Delta_n}{B_n}}

2161:                 {\Pi_n}

2162:         & \deduce{\Seq{B_1,\ldots,B_n,D'',\Gamma'}{C}}

2163:                 {\Pi''}}

2164: \enspace .

2165: \end{displaymath}

2166: Then $\Xi$ reduces to

2167: \begin{displaymath}

2168: \infer[\oimpL]{\Seq{\Delta_1,\ldots,\Delta_n,D' \oimp D'',\Gamma'}{C}}

2169:         {\deduce{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma'}{D'}}

2170:                 {\Xi_1}

2171:         & \deduce{\Seq{\Delta_1,\ldots,\Delta_n,D'',\Gamma'}{C}}

2172:                 {\Xi_2}}

2173: \enspace .

2174: \end{displaymath}

2175: 

2176: \vskip12pt

2177: 

2178: \noindent $-/\natL:$

2179: Suppose $\Pi$ is

2180: $$

2181: \infer[\natL]

2182: {\Seq{B_1,\ldots,B_n, nat\,I, \Gamma'}{C}}

2183: {

2184: \deduce{\Seq{}{D\,z}}{\Pi'}

2185: &

2186: \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''}

2187: &

2188: \deduce{\Seq{B_1,\ldots,B_n,D\,I,\Gamma'}{C}}{\Pi'''}

2189: }

2190: $$

2191: Let $\Xi_1$ be 

2192: $$

2193: \infer[mc,]

2194: {\Seq{\Delta_1,\ldots,\Delta_n,D\,I,\Gamma'}{C}}

2195: {

2196: \deduce{\Seq{\Delta_1}{B_1}}{\Pi_1}

2197: &

2198: \ldots

2199: &

2200: \deduce{\Seq{\Delta_n}{B_n}}{\Pi_n}

2201: &

2202: \deduce{\Seq{B_1,\ldots,B_n,D\,I, \Gamma'}{C}}{\Pi'''}

2203: }

2204: $$

2205: then $\Xi$ reduces to

2206: $$

2207: \infer[\natL]

2208: {\Seq{\Delta_1,\ldots,\Delta_n,nat\,I,\Gamma'}{C}}

2209: {

2210: \deduce{\Seq{}{D\,z}}{\Pi'}

2211: &

2212: \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''}

2213: &

2214: \deduce{\Seq{\Delta_1,\ldots,\Delta_n,D\,I,\Gamma'}{C}}{\Xi_1}

2215: }

2216: $$

2217: 

2218: \vskip12pt

2219: 

2220: \noindent $-/\eqL$:

2221: If $\Pi$ is

2222: \begin{displaymath}

2223: \infer[\eqL]{\Seq{B_1,\ldots,B_n,{s=t},

2224:                  \Gamma'}{C}}

2225:         {\left\{\raisebox{-1.5ex}

2226:                 {\deduce{\Seq{B_1\rho,\ldots,

2227:                                  B_n\rho,\Gamma'\rho}

2228:                                 {C\rho}}

2229:                 {\Pi^{\rho}}}\right\}}

2230: \enspace ,

2231: \end{displaymath}

2232: then $\Xi$ reduces to

2233: \settowidth{\infwidthi}

2234:         {$\left\{\raisebox{-3.5ex}{\infer[\mc]

2235:                         {\Seq{\Delta_1\rho,\ldots,

2236:                                  \Delta_n\rho,D\sigma,\Gamma'\rho}

2237:                                 {C\rho}}

2238:                 {\left\{\raisebox{-1.5ex}

2239:                         {\deduce{\Seq{\Delta_i\rho}{B_i\rho}}

2240:                                 {\Pi_i\rho}}

2241:                  \right\}_{i \in \{1..n\}}

2242:                 & \raisebox{-2.5ex}

2243:                         {\deduce{\Seq{\{B_i\rho\}_{i\in\{1..n\}},

2244:                                          D\sigma,\Gamma'\rho}

2245:                                         {C\rho}}

2246:                                 {\Pi^{\rho,\sigma,D}}}}}

2247:         \right\}$}

2248: \settowidth{\infwidthii}{\mc}

2249: \begin{displaymath}

2250: \infer[\eqL]

2251: {\Seq{\Delta_1,\ldots,\Delta_n,s=t,\Gamma'}{C}}

2252:      {\deduce{\makebox[\infwidthi]{}}

2253:      {\left\{\raisebox{-3.5ex}{\infer[\mc]

2254:             {\Seq{\Delta_1\rho,\ldots,

2255:                   \Delta_n\rho,\Gamma'\rho}

2256:                                         {C\rho}}

2257:        {\left\{\raisebox{-1.5ex}

2258:           {\deduce{\Seq{\Delta_i\rho}{B_i\rho}}

2259:                                 {\Pi_i\rho}}

2260:                  \right\}_{i \in \{1..n\}}

2261:                 & \raisebox{-2.5ex}

2262:                         {\deduce{\Seq{B_i\rho, \ldots,

2263:                                  \Gamma'\rho}

2264:                                 {C\rho}}

2265:                         {\Pi^{\rho}}}}}

2266:         \right\}\makebox[\infwidthii]{}}}

2267: \enspace .

2268: \end{displaymath}

2269: 

2270: \newcommand{\circR}{\circ{\cal R}}

2271: 

2272: \vskip12pt

2273: 

2274: \noindent $-/\circR$:

2275: If $\Pi$ is

2276: \begin{displaymath}

2277: \infer[\circR]

2278: {\Seq{B_1,\ldots,B_n,\Gamma}{C}}

2279:   {\left\{\raisebox{-1.5ex}{

2280:       \deduce{\Seq{B_1,\ldots,B_n,\Gamma^i}{C^i}}

2281:                 {\Pi^i}}\right\}}

2282: \enspace ,

2283: \end{displaymath}

2284: where $\circR$ is any right rule,

2285: then $\Xi$ reduces to

2286: \settowidth{\infwidthi}

2287:         {$\left\{\raisebox{-2.45ex}{

2288:           \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma^i}{C^i}}

2289:                 {\deduce{\Seq{\Delta_1}{B_1}}

2290:                         {\Pi_1}

2291:                 & \cdots

2292:                 & \deduce{\Seq{\Delta_n}{B_n}}

2293:                         {\Pi_n}

2294:                 & \deduce{\Seq{B_1,\ldots,B_n,\Gamma^i}{C^i}}

2295:                         {\Pi^i}}}\right\}$}

2296: \settowidth{\infwidthii}{\mc}

2297: \begin{displaymath}

2298: \infer[\circR]

2299: {\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

2300:      {\deduce{\makebox[\infwidthi]{}}

2301:             {\left\{\raisebox{-2.45ex}{

2302:             \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma^i}{C^i}}

2303:                 {\deduce{

2304:                    \Seq{\Delta_1}{B_1}}

2305:                         {\Pi_1}

2306:                 & \cdots

2307:                 & \deduce{\Seq{\Delta_n}{B_n}}

2308:                         {\Pi_n'}

2309:                 & \deduce{\Seq{B_1,\ldots,B_n,\Gamma^i}{C^i}}

2310:                         {\Pi^i}}}\right\}\makebox[\infwidthii]{}}}

2311: \enspace .

2312: \end{displaymath}

2313: 

2314: \vskip12pt

2315: 

2316: \noindent{\em \underline{Multicut cases:}}

2317: 

2318: \vskip12pt

2319: 

2320: \noindent $\mc/\circL$:

2321: If $\Pi$ ends with a left rule other than $\cL$ acting on $B_1$ and

2322: $\Pi_1$ ends with a multicut and reduces to $\Pi_1'$,

2323: then $\Xi$ reduces to

2324: \begin{displaymath}

2325: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}

2326:         {\deduce{\Seq{\Delta_1}{B_1}}

2327:                 {\Pi_1'}

2328:         & \deduce{\Seq{\Delta_2}{B_2}}

2329:                 {\Pi_2}

2330:         & \cdots

2331:         & \deduce{\Seq{\Delta_n}{B_n}}

2332:                 {\Pi_n}

2333:         & \deduce{\Seq{B_1,\ldots,B_n,\Gamma}{C}}

2334:                 {\Pi}}

2335: \enspace .

2336: \end{displaymath}

2337: 

2338: \noindent $-/\mc$:

2339: Suppose $\Pi$ is

2340: \begin{displaymath}

2341: \infer[\mc]{\Seq{B_1,\ldots,B_n,\Gamma^1,\ldots,\Gamma^m,\Gamma'}{C}}

2342:         {\left\{\raisebox{-1.5ex}{\deduce{\Seq{\{B_i\}_{i \in I^j},\Gamma^j}{D^j}}

2343:                 {\Pi^j}}\right\}_{j \in \{1..m\}}

2344:         & \raisebox{-2.5ex}{\deduce{\Seq{\{D^j\}_{j \in \{1..m\}},\{B_i\}_{i \in I'},\Gamma'}{C}}

2345:                 {\Pi'}}}

2346: \enspace ,

2347: \end{displaymath}

2348: where $I^1,\ldots,I^m,I'$ partition the formulas

2349: $\{B_i\}_{i \in \{1..n\}}$ among the premise derivations

2350: $\Pi_1$, \ldots, $\Pi_m$,$\Pi'$.

2351: For $1 \leq j \leq m$ let $\Xi^j$ be

2352: \begin{displaymath}

2353: \infer[\mc]{\Seq{\{\Delta_i\}_{i \in I^j},\Gamma^j}{D^j}}

2354:         {\left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_i}{B_i}}

2355:                         {\Pi_i}}\right\}_{i \in I^j}

2356:         & \raisebox{-2.5ex}{\deduce{\Seq{\{B_i\}_{i \in I^j},\Gamma^j}{D^j}}

2357:                 {\Pi^j}}}

2358: \enspace .

2359: \end{displaymath}

2360: Then $\Xi$ reduces to

2361: \begin{displaymath}

2362: \infer[\mc]{\Seq{\Delta_1,\ldots,\Delta_n,\Gamma^1,\ldots\Gamma^m,\Gamma'}{C}}

2363:         {\left\{\raisebox{-1.5ex}{\deduce{\Seq{\ldots}{D^j}}

2364:                         {\Xi^j}}\right\}_{j \in \{1..m\}}

2365:         & \left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_i}{B_i}}

2366:                         {\Pi_i}}\right\}_{i \in I'}

2367:         & \raisebox{-2.5ex}{\deduce{\Seq{\ldots}{C}}

2368:                 {\Pi'}}}

2369: \enspace .

2370: \end{displaymath}

2371: 

2372: \vskip12pt

2373: 

2374: \noindent{\em \underline{Structural case:}}

2375: 

2376: \vskip12pt

2377: 

2378: \noindent $-/\cL$:

2379: If $\Pi$ is

2380: \begin{displaymath}

2381: \infer[\cL]{\Seq{B_1,B_2,\ldots,B_n,\Gamma}{C}}

2382:         {\deduce{\Seq{B_1,B_1,B_2,\ldots,B_n,\Gamma}{C}}

2383:                 {\Pi'}}

2384: \enspace ,

2385: \end{displaymath}

2386: then $\Xi$ reduces to

2387: \settowidth{\infwidthi}

2388:         {$\Seq{\Delta_1,\Delta_1,\Delta_2,\ldots,\Delta_n,\Delta_n,\Gamma}{C}$}

2389: \begin{displaymath}

2390: \infer{\Seq{\Delta_1,\Delta_2,\ldots,\Delta_n,\Gamma}{C}}

2391:         {\infer[\cL]{\makebox[\infwidthi]{}}

2392:                 {\infer[\mc]{\Seq{\Delta_1,\Delta_1,\Delta_2,\ldots,\Delta_n,\Delta_n,\Gamma}{C}}

2393:                         {\raisebox{-2.5ex}{\deduce{\Seq{\Delta_1}{B_1}}

2394:                                 {\Pi_1}}

2395:                         & \left\{\raisebox{-1.5ex}{\deduce{\Seq{\Delta_i}{B_i}}

2396:                                         {\Pi_i}}\right\}_{i \in \{1..n\}}

2397:                         & \raisebox{-2.5ex}{\deduce{\Seq{B_1,B_1,B_2,\ldots,B_n,\Gamma}{C}}

2398:                                 {\Pi'}}}}}

2399: \enspace .

2400: \end{displaymath}

2401: 

2402: 

2403: \vskip12pt

2404: 

2405: \noindent{\em \underline{Axiom cases:}}

2406: 

2407: \vskip12pt

2408: 

2409: \noindent $id_\pi/\circL$:

2410: Suppose $\Pi$ ends with either $\natL$ or $\eqL$ on $B_1$ and 

2411: $\Pi_1$ ends with the $id_\pi$ rule:

2412: $$

2413: \infer[id_\pi]

2414: {\Seq{\Delta_1',B}{B_1}}

2415: {\pi_1.B = \pi_2.B_1}

2416: $$

2417: Then it is the case that $B = \pi_1^{-1}.\pi_2.B_1.$

2418: Apply the construction in Definition~\ref{def:perm}

2419: to $\Pi$ to get a derivation $\Pi'$ of

2420: $\Seq{B, B_2,\ldots,B_n,\Gamma}{C}.$

2421: The derivation $\Xi$ reduces to

2422: \begin{displaymath}

2423: \infer[\mc]{\Seq{B, \Delta_1', \Delta_2,\ldots,\Delta_n,\Gamma}{C}}

2424:         {\deduce{\Seq{\Delta_2}{B_2}}

2425:                 {\Pi_2}

2426:         & \cdots

2427:         & \deduce{\Seq{\Delta_n}{B_n}}

2428:                 {\Pi_n}

2429:         & \deduce{\Seq{B,\Delta_1', B_2,\ldots,B_n,\Gamma}{C}}

2430:                 {w(\Delta_1',\Pi')}}          

2431: \enspace .

2432: \end{displaymath}

2433: 

2434: \vskip12pt

2435: 

2436: \noindent $-/id_\pi$:

2437: If $\Pi$ ends with the $id_\pi$ rule with a matching

2438: formula in $\Gamma$, i.e., there exists $C' \in \Gamma$

2439: such that $\pi.C' = \pi'.C$ for some permutations

2440: $\pi$ and $\pi'$, then 

2441: then $\Xi$ reduces to

2442: $$

2443: \infer[id_\pi]

2444: {\Seq{\Delta_1,\ldots,\Delta_n,\Gamma}{C}}{}

2445: $$

2446: If $\Pi$ ends with the $id_\pi$ rule but $C$ does not

2447: match any formula in $\Gamma$, then $C$ must match one

2448: of the cut formulas, say $B_1$, i.e.,

2449: there exists permutations $\pi_1$ and $\pi_2$ such

2450: that $\pi_1.B_1 = \pi_2.C$. That is, $C = \pi_2^{-1}.\pi_1.B_1.$

2451: In this case, we first apply the permutation 

2452: $\pi_2^{-1}.\pi_1$ to $\Pi_1$ according to the construction

2453: in Definition~\ref{def:perm} to get a derivation

2454: $\Pi_1'$ of $\Seq{\Delta_1}{\pi_2^{-1}.\pi_1.B_1}$. 

2455: $\Xi$ then reduces to  

2456: $w(\Delta_2\cup \ldots \cup \Delta_n \cup \Gamma, \Pi_1').$

2457: \qed

2458: 

2459: 

2460: An inspection of the rules of the logic and this definition will

2461: reveal that every derivation ending with a multicut has a

2462: reduct.

2463: Because we use a multiset as the left side of the sequent, there may

2464: be ambiguity as to whether a formula occurring on the left side of the

2465: rightmost premise to a multicut rule is in fact a cut formula, and if

2466: so, which of the left premises corresponds to it.

2467: As a result, several of the reduction rules may apply, and so a

2468: derivation may have multiple reducts.

2469: 

2470: 

2471: \newcommand{\Ascr}{{\cal A}}

2472: \newcommand{\Bscr}{{\cal B}}

2473: \newcommand{\Cscr}{{\cal C}}

2474: \newcommand{\Dscr}{{\cal D}}

2475: \newcommand{\Escr}{{\cal E}}

2476: \newcommand{\Fscr}{{\cal F}}

2477: \newcommand{\Gscr}{{\cal G}}

2478: \newcommand{\Hscr}{{\cal H}}

2479: \newcommand{\ul}[1]{\underline{#1}}

2480: \newcommand{\Tscr}{{\cal T}}

2481: 

2482: \section{Normalizability and reducibility}

2483: \label{sec:norm}

2484: 

2485: We now define two properties of derivations:  normalizability and

2486: reducibility.

2487: Each of these properties implies that the derivation can be reduced to

2488: a cut-free derivation of the same end-sequent.

2489: In the following, substitutions mean $\Sigma$-substitutions for

2490: some signature $\Sigma.$

2491: The definitions are similar to those by McDowell and 

2492: Miller~\cite{mcdowell00tcs}. 

2493: However, since the cut reduction in our case involves 

2494: several transformations of derivations, other than substitutions

2495: and weakening, we need to build this transformations

2496: into the definitions of normalizability and reducibility.

2497: 

2498: \begin{definition}

2499: A {\em height-preserving} (HP) transformation ${\cal T}$

2500: is a finite sequence of transformations ${\cal F}_1, \ldots , {\cal F}_n$

2501: where each ${\cal F}_i$ is one of the transformations

2502: described in Definition~\ref{def:weak}, Definition~\ref{def:subst},

2503: Definition~\ref{def:perm} and Definition~\ref{def:res}.

2504: The number $n$ is the {\em order} of ${\cal T}$.

2505: The application of ${\cal T}$ to $\Pi$ is defined as follows:

2506: $$

2507: \begin{array}{ll}

2508: {\cal T}_0(\Pi) = \Pi\\

2509: {\cal T}_{i+1}(\Pi) = {\cal F}_{i+1}({\cal T}_i(\Pi))\\

2510: {\cal T}(\Pi) = {\cal T}_n(\Pi)

2511: \end{array}

2512: $$

2513: \end{definition}

2514: Note that a height-preserving transformation may not be defined for all derivations, and that

2515: it may be the identity transformation (i.e., it does nothing).

2516: Height-preserving transformations are ranged over by $\Tscr, \Fscr, \Gscr$

2517: and $\Hscr.$

2518: 

2519: 

2520: \begin{lemma}

2521: \label{lm:height}

2522: Let ${\cal T}$ be a height-preserving transformation.

2523: For any derivation $\Pi$, if ${\cal T}(\Pi)$ is defined,

2524: then $ht({\cal T}(\Pi)) \leq ht(\Pi).$

2525: \end{lemma}

2526: 

2527: \begin{definition}

2528: \label{def:norm}

2529: We define the set of {\em normalizable} derivations to be the smallest

2530: set that satisfies the following conditions:

2531: \begin{enumerate}

2532: \item

2533: If a derivation $\Pi$ ends with a multicut, then it is normalizable

2534: if for every height-preserving transformation ${\cal T}$ such that ${\cal T}(\Pi)$ is defined,

2535: there is a normalizable reduct of ${\cal T}(\Pi)$.

2536: 

2537: \item

2538: If a derivation ends with any rule other than a multicut,

2539: then it is normalizable if the premise derivations are normalizable.

2540: \end{enumerate}

2541: These clauses assert that a given derivation is normalizable

2542: provided certain (perhaps infinitely many) other derivations are

2543: normalizable.

2544: If we call these other derivations the predecessors of the given

2545: derivation, then a derivation is normalizable if and only if the tree

2546: of the derivation and its successive predecessors is well-founded.

2547: In this case, the well-founded tree is called the {\em normalization} of

2548: the derivation.

2549: \end{definition}

2550: The set of normalizable derivations is not empty; the cut-free

2551: proofs, for instance, are normalizable.

2552: 

2553: Since a normalization is well-founded, it has an associated induction

2554: principle:  for any property $P$ of derivations, if for every

2555: derivation $\Pi$ in the normalization, $P$ holds for every predecessor

2556: of $\Pi$ implies that $P$ holds for $\Pi$, then $P$ holds for every

2557: derivation in the normalization.

2558: 

2559: \begin{lemma}

2560: \label{lm:norm-cut-free}

2561: If there is a normalizable derivation of a sequent, then there is a

2562: cut-free derivation of the sequent.

2563: \end{lemma}

2564: \begin{proof} 

2565: Let $\Pi$ be a normalizable derivation of the sequent

2566: $\Seq{\Gamma}{B}$.

2567: We show by induction on the normalization of $\Pi$ that there is a

2568: cut-free derivation of $\Seq{\Gamma}{B}$.

2569: \begin{enumerate}

2570: \item

2571: If $\Pi$ ends with a multicut, then any of its reducts is one of its

2572: predecessors  and so is normalizable.

2573: One of its reduct, via the empty transformation, is also 

2574: a derivation of $\Seq{\Gamma}{B}$, so by the

2575: induction hypothesis this sequent has a cut-free derivation.

2576: 

2577: \item

2578: Suppose $\Pi$ ends with a rule other than multicut.

2579: Since we are given that $\Pi$ is normalizable, by definition the

2580: premise derivations are normalizable.

2581: These premise derivations are the predecessors of $\Pi$, so by the

2582: induction hypothesis there are cut-free derivations of the premises.

2583: Thus there is a cut-free derivation of $\Seq{\Gamma}{B}$.

2584: \end{enumerate}

2585: \qed

2586: \end{proof}

2587: 

2588: The next four lemmas are also proved by induction on the

2589: normalization of derivations.

2590: 

2591: 

2592: \begin{lemma}

2593: \label{lm:norm subst}

2594: If $\Pi$ is a normalizable derivation, then for any substitution

2595: $\theta$ such that $\Pi\theta$ is defined,  

2596: $\Pi\theta$ is normalizable.

2597: \end{lemma}

2598: 

2599: \begin{lemma}

2600: \label{lm:norm weak}

2601: If $\Pi$ is normalizable, then for any multiset of formulas $\Delta$,

2602: if $w(\Delta,\Pi)$ is defined, then $w(\Delta,\Pi)$ is normalizable.

2603: \end{lemma}

2604: 

2605: \begin{lemma}

2606: \label{lm:norm perm}

2607: If $\Pi$ is normalizable, then for any permutations $\vec \pi$

2608: such that $\langle \vec \pi \rangle.\Pi$ is defined,

2609: $\langle \vec \pi \rangle.\Pi$ is normalizable.

2610: \end{lemma}

2611: 

2612: \begin{lemma}

2613: \label{lm:norm res}

2614: If $\Pi$ is normalizable, then for any nominal constants $\vec a$

2615: such that $r(x,\vec a,\Pi)$ is defined, 

2616: $r(x,\vec a,\Pi)$ is normalizable.

2617: \end{lemma}

2618: 

2619: \begin{lemma}

2620: \label{lm:norm hpt}

2621: If $\Pi$ is normalizable, then for any height-preserving transformation

2622: ${\cal T}$ such that ${\cal T}(\Pi)$ is defined,

2623: ${\cal T}(\Pi)$ is normalizable.

2624: \end{lemma}

2625: 

2626: \begin{definition}

2627: \label{def:level drv}

2628: The level of a sequent $\Seq \Gamma C$ is the level of $C$.

2629: The level of a derivation $\Pi$ is the level of its root sequent.

2630: \end{definition}

2631: 

2632: The definition of reducibility for derivations 

2633: is done by induction on the level of derivations:

2634: in defining the reducibility of level-$i$ derivations,

2635: we assume that the reducibility of derivations

2636: of level $j$, for all $j < i$ is already defined.

2637: In the following definition,

2638: when we apply a transformation ${\cal T}$ to

2639: a derivation $\Pi$ of $\Seq{B_1,\dots,B_n}{B_0},$

2640: we use the notation ${\cal T}(B_i)$ to denote 

2641: the formula in the root sequent of ${\cal T}(\Pi)$ 

2642: that results from applying the transformation to $B_i$.

2643: 

2644: \begin{definition}

2645: \label{def:reducibility}

2646: {\em Reducibility.}

2647: For any $i$, we define the set of {\em reducible}

2648: $i$-level derivations to be the smallest

2649: set of $i$-level derivations that satisfies

2650: the following conditions:

2651: \begin{enumerate}

2652: \item If a derivation $\Pi$ ends with a multicut then it is reducible

2653: if for every height-preserving transformation ${\cal T}$ such

2654: that ${\cal T}(\Pi)$ is defined,

2655: there is a reducible reduct of ${\cal T}(\Pi).$

2656: \item Suppose the derivation ends with the implication right rule

2657: $$

2658: \infer[\oimpR]

2659: {\Seq{\Gamma}{B\oimp C}}

2660: {\deduce{\Seq{B,\Gamma}{C}}{\Pi}}

2661: $$

2662: Then the derivation is reducible if $\Pi$ is reducible and

2663: for every height-preserving transformation ${\cal T}$ such that

2664: ${\cal T}(\Pi)$ is defined, multiset of formulas $\Delta$ and

2665: reducible derivation $\Pi'$ of $\Seq{\Delta}{B'}$, where $B' = {\cal T}(B)$,

2666: the derivation

2667: $$

2668: \infer[mc]

2669: {\Seq{\Delta, \Gamma'}{C'}}

2670: {\deduce{\Seq \Delta {B'}}{\Pi'}

2671: & \deduce{\Seq{B',\Gamma'}{C'}}{{\cal T}(\Pi)}

2672: }

2673: $$

2674: is reducible.

2675: \item If the derivation ends with the implication left rule or the $nat$ rule,

2676: then it is reducible if the right premise derivation is reducible and the

2677: other premise derivations are normalizable.

2678: \item If the derivation ends with any other rule, then it is reducible if

2679: the premise derivations are reducible.

2680: \end{enumerate}

2681: These clauses assert that a given derivation is reducible 

2682: provided certain other derivations 

2683: are reducible. If we call these other derivations the 

2684: predecessors of the given derivation, then a derivation 

2685: is reducible only if the tree of the derivation and its 

2686: successive predecessors is well founded. 

2687: In this case, the well founded tree is called the {\em reduction}

2688: of the derivation.

2689: \end{definition}

2690: 

2691: 

2692: \begin{lemma}

2693: \label{lm:reducible implies norm}

2694: If a derivation is reducible, then it is normalizable.

2695: \end{lemma}

2696: \begin{proof} By induction on the reduction of the derivation. 

2697: \qed

2698: \end{proof}

2699: 

2700: \begin{lemma}

2701: \label{lm:reducible hpt}

2702: If a derivation $\Pi$ is reducible, then for

2703: any height-preserving ${\cal T}$ such

2704: that ${\cal T}(\Pi)$ is defined, ${\cal T}(\Pi)$

2705: is reducible.

2706: \end{lemma}

2707: \begin{proof}

2708: By induction on the reduction of $\Pi$ and

2709: Lemma~\ref{lm:norm hpt}.

2710: \end{proof}

2711: 

2712: \section{Cut elimination}

2713: \label{sec:cut-elim}

2714: 

2715: 

2716: In the following, when we mention ${\cal T}(\Pi)$ we assume

2717: implicitly that it is defined. 

2718: We shall also use the notation $\underline{B}_{\cal T}$

2719: to denote ${\cal T}(B)$, that is the application of

2720: the transformation to the formula $B.$ Similarly, the multiset ${\cal T}(\Delta)$

2721: will be written $\underline{\Delta}_{\cal T}.$

2722: We drop the subscript ${\cal T}$ if it is clear from context

2723: which transformation we refer to.

2724: 

2725: \begin{lemma}

2726: \label{lm:reducibility}

2727: For any derivation $\Pi$ of $\NSeq{\Sigma}{B_1,\ldots,B_n,\Gamma}{C}$

2728: and reducible derivations $\Pi_1, \ldots, \Pi_n$

2729: of $\NSeq{\Sigma}{\Delta_1}{C_1}, \ldots, \NSeq{\Sigma}{\Delta_n}{C_n},$

2730: where $n \geq 0$, 

2731: and for any transformations $\Tscr_1, \ldots, \Tscr_n, \Tscr$

2732: such that $\Tscr_i(\Pi_i)$ is defined and 

2733: $\Tscr_i(C_i) = \Tscr(B_i)$, 

2734: the derivation $\Xi$

2735: $$

2736: \infer[\mc]

2737: {\NSeq{\Sigma'}{\ul{\Delta_1}_{\Tscr_1},\ldots,

2738: \ul{\Delta_n}_{\Tscr_n},\ul{\Gamma}_{\Tscr}}{\ul{C}_{\Tscr}}}

2739: {

2740: \deduce{\NSeq{\Sigma'}{\ul{\Delta_1}_{\Tscr_1}}{\ul{B_1}_{\Tscr}}}{\Tscr_1(\Pi_1)} &

2741: \ldots &

2742: \deduce{\NSeq{\Sigma'}{\ul{\Delta_n}_{\Tscr_n}}{\ul{B_n}_{\Tscr}}}{\Tscr_n(\Pi_n)} &

2743: \deduce{\NSeq{\Sigma'}{\ul{B_1}_{\Tscr},\ldots,\ul{B_n}_{\Tscr}, \ul{\Gamma}_{\Tscr}}

2744: {\ul{C}_{\Tscr}}}{\Tscr(\Pi)}

2745: }

2746: $$

2747: is reducible.

2748: \end{lemma}

2749: \begin{proof}

2750: The proof is by induction on $ht(\Pi)$ with subordinate induction

2751: on $n$ and on the reductions of $\Pi_1,\ldots,\Pi_n.$

2752: Since the proof does not depend on the order of the inductions

2753: on reductions, when we need to distinguish of one the $\Pi_i$'s

2754: we shall refer to it as $\Pi_1$ without loss of generality.

2755: 

2756: We need to show that for every $\Tscr'$, the derivation

2757: every reduct of $\Tscr'(\Xi)$ is reducible.

2758: If $n=0$ then $\Tscr'(\Xi)$ reduces to $\Tscr'(\Tscr(\Pi)).$

2759: Since reducibility is preserved by height-preserving

2760: transformation, it suffices to consider the case where

2761: $\Tscr$ and $\Tscr'$ are the identity transformation, that is,

2762: we need only to show that $\Pi$ is reducible.

2763: This is proved by case analysis on the last rule of

2764: $\Pi.$

2765: For each case, the results follow from the outer induction 

2766: hypothesis and Definition~\ref{def:reducibility}. 

2767: The case with $\oimpR$ requires that height-preserving

2768: transformations do not increase the height of the derivations

2769: (see Lemma~\ref{lm:height}).

2770: In the cases for $\oimpL$ and $\natL$ we need the

2771: additional information that reducibility implies

2772: normalizability (see Lemma~\ref{lm:reducible implies norm}).

2773: 

2774: For $n > 0$, we analyze all possible reductions that apply to $\Tscr'(\Xi)$ 

2775: and show that every reduct of ${\cal T}'(\Xi)$ is reducible. 

2776: We suppose that $\Tscr'(\Xi)$ is of the following form:

2777: $$

2778: \infer[mc]

2779: {\Seq{\ul{\Delta_1}_{\Fscr_1}, \ldots, \ul{\Delta_n}_{\Fscr_n},

2780: \ul{\Gamma}_{\Fscr}}{\ul{C}_{\Fscr}}}

2781: {

2782: \deduce{\Seq{\ul{\Delta_1}_{\Fscr_1}}{\ul{C_1}_{\Fscr_1}}}{\Fscr_1(\Pi_1)}

2783: &

2784: \ldots

2785: &

2786: \deduce{\Seq{\ul{\Delta_n}_{\Fscr_n}}{\ul{C_n}_{\Fscr_n}}}{\Fscr_n(\Pi_n)}

2787: &

2788: \deduce{\Seq{\ul{B_1}_{\Fscr},\ul{B_n}_{\Fscr}, \ul{\Gamma}_{\Fscr}}

2789: {\ul{C}_{\Fscr}}}{\Fscr(\Pi)}

2790: }

2791: $$

2792: where $\ul{B_i}_{\Fscr} = \ul{C_i}_{\Fscr_i}.$

2793: In several cases below, we often omit the subscripts $\Fscr$ or $\Fscr_i$

2794: when it is clear from context which transformations we refer to.

2795: We also often switch between $\ul{B_i}_{\Fscr}$ and $\ul{C_i}_{\Fscr_i}$

2796: to make the inference figures more readable.

2797:  

2798: Most cases follow immediately from the inductive

2799: hypothesis and Definition~\ref{def:reducibility} and 

2800: Lemma~\ref{lm:reducible implies norm}, Lemma~\ref{lm:reducible hpt} and 

2801: Lemma~\ref{lm:height}. We show here the interesting cases. 

2802: 

2803: \vskip12pt

2804: \noindent $\oimpR/\oimpL$: Suppose $\Pi_1$ and $\Pi$ are

2805: $$

2806: \infer[\oimpR]

2807: {\Seq{\Delta_1}{B_1'\oimp B_1''}}

2808: {

2809: \deduce{\Seq{\Delta_1,B_1'}{B_1''}}{\Pi_1'}

2810: }

2811: \qquad \qquad

2812: \infer[\oimpL]

2813: {\Seq{B_1'\oimp B_1'',B_2,\dots, B_n,\Gamma}{C}}

2814: {

2815: \deduce{\Seq{B_2,\dots,\Gamma}{B_1'}}{\Pi'}

2816: &

2817: \deduce{\Seq{B_1'',B_2,\dots,\Gamma}{C}}{\Pi''}

2818: }

2819: \enspace .

2820: $$

2821: Let $\Xi_1$ be the derivation

2822: $$

2823: \infer[\mc]

2824: {\Seq{\underline{\Delta_2},\dots,\underline{\Delta_n},\underline{\Gamma}}{\underline{B_1'}}}

2825: {

2826: \deduce{\Seq{\underline {\Delta_2}}{\underline{B_2}}}{\Fscr_2(\Pi_2)}

2827: &

2828: \ldots

2829: &

2830: \deduce{\Seq{\underline{\Delta_n}}{\underline{B_n}}}{\Fscr_n(\Pi_n)}

2831: &

2832: \deduce{\Seq{\underline{B_2},\dots,\underline{B_n}, \underline \Gamma}{\underline{B_1'}}}

2833:              {\Fscr_n(\Pi')}

2834: }

2835: $$

2836: Then $\Xi_1$ is reducible by induction hypothesis 

2837: since $\Fscr$ and $\Fscr_i$ preserve

2838: reducibility (Lemma~\ref{lm:reducible hpt}) and do not increase

2839: the height of derivations (Lemma~\ref{lm:height}). Since we are given that

2840: $\Pi_1$ is reducible, by Definition~\ref{def:reducibility}, the derivation

2841: $\Xi_2$

2842: $$

2843: \infer[\mc]

2844: {\Seq{\ul{\Delta_1}, \ldots, \ul{\Delta_n}, \ul \Gamma}{\ul {B_1''}}}

2845: {

2846: \deduce{\Seq{\ul{\Delta_2}, \ldots, \ul{\Delta_n}, \ul\Gamma}

2847:   {\ul {B_1'}}}{\Xi_1}

2848: &

2849: \deduce{\Seq{\ul{B_1'}, \ul {\Delta_1}}{\ul {B_1''}}}{\Fscr_1(\Pi_1')}

2850: }

2851: $$

2852: is reducible as well.

2853: Therefore, the reduct of $\Tscr'(\Xi)$

2854: \settowidth{\infwidthi}

2855:         {$\Seq{\underline{\Delta_1},\ldots,\underline{\Delta_n},

2856: \underline{\Gamma},\underline{\Delta_2},\ldots,\underline{\Delta_n},\underline \Gamma}{\underline C}$}

2857: \begin{displaymath}

2858: \infer{\Seq{\underline{\Delta_1},\ldots,\underline{\Delta_n},\underline{\Gamma}}{\underline C}}

2859:         {\infer[\cL]{\makebox[\infwidthi]{}}

2860:                 {\infer[\mc]{\Seq{\ul{\Delta_1},\ldots,\ul{\Delta_n}, \ul\Gamma,

2861:                                         \ul{\Delta_2},\ldots,\ul{\Delta_n},\ul{\Gamma}}{\ul C}}

2862:                         {\raisebox{-2.5ex}{\deduce{\Seq{\ldots}{\ul{B_1''}}}

2863:                                 {\Xi_2}}

2864:                         & \left\{\raisebox{-1.5ex}{\deduce{\Seq{\ul{\Delta_i}}{\ul{B_i}}}

2865:                                 {\Fscr_i(\Pi_i)}}\right\}_{i \in \{2..n\}}

2866:                         & \raisebox{-2.5ex}{

2867:      \deduce{\Seq{\ul{B_1''},\{\ul{B_i}\}_{i \in \{2..n\}},\ul \Gamma}{\ul C}}

2868:                                 {\Fscr(\Pi'')}}}}}

2869: \enspace .

2870: \end{displaymath}

2871: is reducible by the outer induction hypothesis and Definition~\ref{def:reducibility}.

2872: 

2873: \vskip12pt

2874: \noindent $\forallR/\forallL:$

2875: Suppose $\Pi_1$ and $\Pi$ are

2876: $$

2877: \infer[\forallR]

2878: {\NSeq{\Sigma}{\Delta_1}{\forall x.B}}

2879: {\deduce{\NSeq {\Sigma, h} {\Delta_1} {B[h\,\vec c/x]}}{\Pi_1'}}

2880: \qquad

2881: \infer[\forallL]

2882: {\NSeq{\Sigma}{\forall x.B, B_2, \ldots, B_n,\Gamma}{C}}

2883: {

2884: \deduce{\NSeq{\Sigma}{B[t/x], B_2,\ldots, B_n,\Gamma}{C}}{\Pi'}

2885: }

2886: $$

2887: Applying the transformation $\Fscr_1$ to $\Pi_1$ (and similarly,

2888: $\Fscr$ to $\Pi$) might require several transformation be done

2889: on the premise of the derivation, e.g., to avoid clashes of 

2890: nominal constants, etc., so let us suppose that $\Fscr_1(\Pi_1)$

2891: and $\Fscr(\Pi)$ are of the following shapes:

2892: $$

2893: \infer[\forallR]

2894: {\NSeq{\Sigma'}{\ul{\Delta_1}}{\forall x.D}}

2895: {\deduce{\NSeq {\Sigma', h} {\Delta_1} {D[h'\,\vec d/x]}}{\Gscr_1(\Pi_1')}}

2896: \qquad

2897: \infer[\forallL]

2898: {\NSeq{\Sigma'}{\forall x.D, \ul{B_2}, \ldots, \ul{B_n}, \ul{\Gamma}}{\ul{C}}}

2899: {

2900: \deduce{\NSeq{\Sigma'}{D[s/x], \ul{B_2},\ldots, \ul{B_n}, \ul{\Gamma}}{\ul C}}

2901: {\Gscr(\Pi')}

2902: }

2903: $$

2904: where $\forall x.D = \ul{\forall x.B}$ and $D[s/x] = \ul{B[t/x]}.$

2905: If the support of $D[s/x]$ is larger than $\{ \vec d \}$,

2906: then the reduction rule for $\forallR/\forallL$ requires further

2907: transformations be applied to $\Gscr_1(\Pi_1')$, i.e.,

2908: as is described in Lemma~\ref{lm:supp1}.

2909: So let us suppose that this transformation is applied, resulting

2910: in a derivation 

2911: $$

2912: \deduce{\NSeq{\Sigma',f}{\ul{\Delta_1}}{D[f\vec e/x]}}{\Gscr_1'(\Pi_1')}

2913: \enspace .

2914: $$

2915: Then $\Tscr'(\Xi)$ reduces to

2916: $$

2917: \infer[mc]

2918: {\NSeq{\Sigma'}{\ul{\Delta_1},\ldots,\ul{\Delta_n}, \ul \Gamma}{\ul C}}

2919: {\deduce{\NSeq{\Sigma'}{\ul {\Delta_1}}{D[s/x]}}

2920:  {\Gscr_1'(\Pi_1')[\lambda \vec e.s/f]}

2921: &

2922: \deduce{\Seq{\ul{\Delta_2}}{\ul{B_2}}}{\Fscr_2(\Pi_2)}

2923: &

2924: \ldots

2925: &

2926: \deduce{\Seq{\ul{\Delta_2}}{\ul{B_2}}}{\Fscr_n(\Pi_n)}

2927: &

2928: \deduce{\NSeq{\Sigma'}{D[s/x], \ldots, \ul{\Gamma}}{\ul C}}{\Gscr(\Pi')}

2929: }

2930: $$

2931: which is reducible by the outer induction hypothesis.

2932: 

2933: 

2934: \vskip12pt

2935: 

2936: \noindent $\natR/ \natL:$

2937: Suppose $\Pi_1$ and $\Pi$ are 

2938: $$

2939: \infer[\natR]

2940: {\Seq{\Delta_1}{nat\,M}}

2941: {\deduce{\Seq{\Delta_1}{nat\,M}}{\Pi_1'}}

2942: \qquad

2943: \infer[\natL]

2944: {\Seq{nat\,(s\,I), B_2, \ldots, B_n,\Gamma}{C}}

2945: {\deduce{\Seq{}{D\,z}}{\Pi'}

2946: & \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''}

2947: & \deduce{\Seq{D\,(s\,M),B_2,\ldots,B_n,\Gamma}{C}}{\Pi'''}

2948: }

2949: $$

2950: then $\Fscr_1(\Pi_1)$ and $\Fscr(\Pi)$ are

2951: $$

2952: \infer[\natR]

2953: {\Seq{\ul{\Delta_1}}{nat\,I}}

2954: {\deduce{\Seq{\ul{\Delta_1}}{nat\,I}}{\Fscr_1(\Pi_1')}}

2955: \qquad

2956: \infer[\natL]

2957: {\Seq{nat\,(s\,I), \ul{B_2}, \ldots, \ul{B_n},\ul{\Gamma}}{\ul{C}}}

2958: {\deduce{\Seq{}{D\,z}}{\Pi'}

2959: & \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''}

2960: & \deduce{\Seq{D\,(s\,I),\ul{B_2},\ldots,\ul{B_n},\ul \Gamma}{\ul C}}{\Fscr(\Pi''')}

2961: }

2962: $$

2963: Note that the derivations $\Pi'$ and $\Pi''$ are not affected

2964: by the transformation $\Fscr$ since $D$ is a closed term

2965: with no occurrences of nominal constants and $j$ in

2966: $\Pi''$ is a new eigenvariable.

2967: Let $\Xi_1$ be the derivation

2968: $$

2969: \infer[mc]

2970: {\Seq{\ul{\Delta_1}}{D\,I}}

2971: {

2972: \deduce{\Seq{\ul {\Delta_1}}{nat\,I}}{\Fscr_1(\Pi_1')}

2973: & 

2974: \infer[\natL]

2975: {\Seq{nat\,I}{D\,I}}

2976: {

2977: \deduce{\Seq{}{D\,z}}{\Pi'} &

2978: \deduce{\Seq{D\,j}{D\,(s\,j)}}{\Pi''}

2979: &

2980: \infer[id_\pi]

2981: {\Seq{D\,I}{D\,I}}

2982: {}

2983: }

2984: }

2985: \enspace .

2986: $$

2987: Since the height of the right premise is no larger than $ht(\Pi)$,

2988: and $\Pi_1'$ is a predecessor of $\Pi_1$, 

2989: $\Xi_1$ is reducible by induction on the reduction of $\Pi_1.$

2990: Let $\{\vec c\}$ be the support of $I.$

2991: We construct the derivation $\Pi^\bullet$ of

2992: $\NSeq{h}{D\,(h\,\vec c)}{D\,(s\,(h\,\vec c))}$

2993: from $\Pi''$ using the procedures described in Definition~\ref{def:subst}

2994: and Definition~\ref{def:res}. 

2995: Let $\Xi_2$ be

2996: $$

2997: \infer[\mc .]

2998: {\Seq{\ul{\Delta_1}}{D\,(s\, I)}}

2999: {

3000: \deduce{\Seq{\ul{\Delta_1}}{D\,I}}{\Xi_1}

3001: &

3002: \deduce{\Seq{D\,I}{D\,(s\,I)}}{\Pi^{\bullet}[\lambda \vec c.I/h]}

3003: }

3004: $$

3005: Since $ht(\Pi^{\bullet} [ \lambda \vec c.I/h ]) \leq ht( \Pi'')$,

3006: by the outer induction hypothesis, $\Xi_2$ is also reducible.

3007: Therefore the reduct of $\Tscr'(\Xi)$

3008: $$

3009: \infer[mc]

3010: {\Seq{\ul{\Delta_1}, \ldots, \ul{\Delta_2},\ul \Gamma}{\ul C}}

3011: {

3012: \deduce{\Seq{\ul {\Delta_1}}{D\,(s\,I)}}{\Xi_2}

3013: &

3014: \deduce{\Seq{\ul {\Delta_2}}{\ul{B_2}}}{\Fscr_2(\Pi_2)}

3015: &

3016: \ldots

3017: &

3018: \deduce{\Seq{\ul {\Delta_n}}{\ul{B_n} } }{\Fscr_n(\Pi_n)}

3019: &

3020: \deduce{\Seq{D\,(s\,I), \ul{B_2}, \ldots, \ul \Gamma}{\ul C}}{\Fscr(\Pi''')}

3021: }

3022: $$

3023: is reducible by the outer induction hypothesis.

3024: 

3025: \vskip12pt

3026: 

3027: \noindent $\eqL/\circL:$

3028: Suppose $\Pi_1$ is 

3029: $$

3030: \infer[\eqL]

3031: {\Seq{s = t, \Delta_1}{B_1}}

3032: {

3033: \left\{

3034: \raisebox{-1.5ex}{\deduce{\Seq{\Delta_1\theta}{B_1\theta}}{\Pi^\theta}}

3035: \right\}_\theta

3036: }

3037: $$

3038: then $\Fscr_1(\Pi_1)$ is 

3039: $$

3040: \qquad

3041: \infer[\eqL]

3042: {\Seq{\ul s = \ul t, \ul{\Delta_1}}{\ul{B_1}}}

3043: {

3044: \left\{

3045: \raisebox{-1.5ex}{\deduce{\Seq{\ul{\Delta_1}\theta}{\ul{B_1}\theta}}{\Pi^{\bullet\rho}}}

3046: \right\}_\rho

3047: }

3048: $$

3049: where each $\Pi^{\bullet\rho}$ is obtained from some $\Pi^\theta$ by

3050: the transformations described in Definition~\ref{def:weak},

3051: Definition~\ref{def:subst}, Definition~\ref{def:perm}

3052: and Definition~\ref{def:res}. 

3053: We denote with $f(\rho)$ the substitution $\theta$ such that 

3054: $\Pi^{\bullet\rho}$ is constructed out of $\Pi^\theta.$

3055: Thus we can write each $\Pi^{\bullet\rho}$

3056: as the derivation $\Fscr_\rho(\Pi^{f(\rho)})$ for some

3057: transformation $\Fscr_\rho.$

3058: The reduct of $\Tscr'(\Xi)$ 

3059: $$

3060: \infer[\eqL]

3061: {

3062: \Seq{\qquad \qquad \qquad \quad

3063: \ul s= \ul t,\ul{\Delta_1'},\ul{\Delta_2},\ldots,\ul{\Delta_n},\ul \Gamma}{\ul C

3064: \qquad \qquad \qquad \qquad \qquad \qquad \qquad\qquad}

3065: }

3066: {

3067: \left\{

3068: \raisebox{-1.5ex}

3069: {

3070: \infer[mc]

3071: {\Seq{\ul{\Delta_1'}\rho, \ul{\Delta_2}\rho,\ldots, \ul{\Delta_n}\rho,

3072: \ul \Gamma\rho}{\ul C \rho}}

3073: {

3074: \deduce{\Seq{\ul{\Delta_1'}\rho}{\ul{B_1}\rho}}{\Fscr_\rho(\Pi^{f(\rho)})}

3075: &

3076: \deduce{\Seq{\ul{\Delta_2}\rho}{\ul{B_2}\rho}}{\Fscr_2(\Pi_2)\rho}

3077: &

3078: \ldots

3079: &

3080: \deduce{\Seq{\ul{\Delta_n}\rho}{\ul{B_n}\rho}}{\Fscr_n(\Pi_n)\rho}

3081: &

3082: \deduce{\Seq{\ul{B_1}\rho,\ldots,\ul{B_n}\rho,\ul{\Gamma}\rho}{\ul C\rho}}{\Fscr(\Pi)\rho}

3083: }

3084: }

3085: \right\}_\rho

3086: }

3087: $$

3088: Each premise derivation of the above derivation is reducible by

3089: the induction hypothesis on the reduction of $\Pi_1$, since each

3090: $\Pi^{f(\rho)}$ is a predecessor of $\Pi_1.$

3091: The reduct of $\Tscr'(\Xi)$ is therefore reducible by 

3092: Definition~\ref{def:reducibility}.

3093: 

3094: \vskip12pt

3095: 

3096: \noindent $-/\oimpR:$

3097: Suppose $\Pi$ is 

3098: $$

3099: \infer[\oimpR]

3100: {\Seq{B_1, \ldots, B_n, \Gamma}{ {C_1 \oimp C_2}}}

3101: {

3102: \deduce{\Seq{B_1, \ldots, B_n, \Gamma, C_1 }{C_2}}{\Fscr(\Pi')}

3103: }

3104: $$

3105: then $\Fscr_1(\Pi)$

3106: $$

3107: \infer[\oimpR]

3108: {\Seq{\ul{B_1}, \ldots, \ul{B_n}, \ul \Gamma}{\ul {C_1 \oimp C_2}}}

3109: {

3110: \deduce{\Seq{\ul{B_1}, \ldots, \ul{B_n}, \ul \Gamma, \ul{C_1} }{\ul{C_2}}}{\Fscr(\Pi')}

3111: }

3112: $$

3113: Let $\Xi_1$ be

3114: $$

3115: \infer[]

3116: {\Seq{\ul{\Delta_1}, \ldots, \ul{\Delta_n}, \ul{C_1}}{\ul{C_2}}}

3117: {

3118: \deduce{\Seq{\ul{\Delta_1}}{\ul{B_1}}}{\Fscr_1(\Pi_1)}

3119: &

3120: \ldots

3121: &

3122: \deduce{\Seq{\ul{\Delta_n}}{\ul{B_n}}}{\Fscr_n(\Pi_n)}

3123: &

3124: \deduce{\Seq{\ul{B_1},\ldots,\ul{B_1},\ul{\Gamma}, \ul{C_1}}{\ul{C_2}}}{\Fscr(\Pi')}

3125: }

3126: $$

3127: which is reducible by the outer induction hypothesis.

3128: Let $\Xi_2$ be the derivation

3129: $$

3130: \infer[\oimpR]

3131: {\Seq{\ul{\Delta_1}, \ldots, \ul{\Delta_n}, \ul{\Gamma}}

3132: {\ul{C_1\oimp C_2}}}

3133: {

3134: \deduce{\Seq{\ul{\Delta_1}, \ldots, \ul{\Delta_n}, \ul \Gamma, \ul {C_1}}{\ul{C_2}}}{\Xi_1}

3135: }

3136: \enspace ,

3137: $$

3138: which is the reduct of $\Tscr'(\Xi).$

3139: To show that $\Xi_2$ is reducible, we need to show

3140: that for any $\Tscr''$, and for any derivation $\Pi''$ of $\Seq{\Delta}{D},$

3141: where $D = \Tscr''(\ul{C_1})$, the derivation $\Xi_3$

3142: $$

3143: \infer[mc]

3144: {\Seq{\Delta, \ul{\Delta_1}_{\Gscr_1}, \ldots, \ul{\Delta_n}_{\Gscr_n}, \ul{\Gamma}_{\Gscr}}

3145: {\ul{C_2}_{\Gscr}}}

3146: {

3147: \deduce{\Seq{\Delta}{D}}{\Pi''}

3148: &

3149: \deduce{\Seq{D, \ul{\Delta_1}_{\Gscr_1}, \ldots, \ul{\Delta_n}_{\Gscr_n},

3150:       \ul{\Gamma}_{\Gscr}}{\ul{C_2}_{\Gscr}} }{\Tscr''(\Xi_2)}

3151: }

3152: $$

3153: is reducible. Here the transformations $\Gscr_i$ and $\Gscr$ are

3154: transformations associated with the premise derivations 

3155: in $\Tscr''(\Xi_2).$ $\Xi_3$ is reducible if for any transformation

3156: $\Hscr$, every reduct of the derivation $\Hscr(\Xi_3)$ is reducible.

3157: The reduct of $\Hscr(\Xi_3)$ in this case is:

3158: $$

3159: \infer[\mc]

3160: {\Seq{\ul{\Delta}, \ul{\Delta_1}, \ldots, \ul{\Delta_n}, \ul{\Gamma}}{\ul{C_2}}}

3161: {

3162: \deduce{\Seq{\ul{\Delta}}{\ul D}}{\Hscr'(\Pi'')}

3163: &

3164: \deduce{\Seq{\ul {\Delta_1}}{\ul {B_1}}}{\Hscr_1(\Pi_1)}

3165: &

3166: \ldots

3167: &

3168: \deduce{\Seq{\ul {\Delta_n}}{\ul{B_n}}}{\Hscr_n(\Pi_n)}

3169: &

3170: \deduce{\Seq{\ul D, \ul{B_1}, \ldots, \ul{B_n}, \ul{\Gamma}}{\ul{C_2}}}{\Hscr''(\Pi')}

3171: }

3172: $$

3173: where $\Hscr_1,\ldots,\Hscr_n$ and $\Hscr''$ are transformations applied

3174: to the premises of $\Hscr(\Tscr''(\Xi_2))$ and

3175: $\Hscr'$ is the transformation applied to the left premise of

3176: $\Hscr(\Xi_3).$ This derivation is reducible by the outer induction hypothesis.

3177: \qed

3178: \end{proof}

3179: 

3180: \begin{corollary}

3181: \label{cor:reducibility}

3182: Every derivation is reducible.

3183: \end{corollary}

3184: \begin{proof}

3185: This result follows immediately from Lemma~\ref{lm:reducibility}

3186: with $n = 0.$ 

3187: \qed

3188: \end{proof}

3189: 

3190: 

3191: 

3192: \begin{theorem}

3193: \label{thm:cut elim}

3194: The cut rule is admissible in $\LGN$.

3195: \end{theorem}

3196: \begin{proof}

3197: Follows immediately from Corollary~\ref{cor:reducibility},

3198: Lemma~\ref{lm:reducible implies norm} and Lemma~\ref{lm:norm-cut-free}.\qed

3199: \end{proof}

3200: 

3201: \begin{corollary}

3202: The logic $\LGN$ is consistent, i.e., it is not the case

3203: that both $A$ and $A \oimp \bot$

3204: are provable.

3205: \end{corollary}

3206: 

3207: 

3208: \section{Correspondence between $\LG$ and $\FOLNb$}

3209: \label{sec:corr}

3210: 

3211: \newcommand{\Judg}[2]{#1 \triangleright #2}

3212: 

3213: 

3214: \begin{figure}

3215: {\small

3216: $$

3217: \infer[id]

3218:       {\NSeq{\Sigma}{\Judg{\sigma}{B},\Gamma}{\Judg{\sigma}{B}}}{}

3219: \qquad 

3220: \infer[cut]

3221:         {\NSeq{\Sigma}{\Delta,\Gamma}{\Cscr}}

3222:         {\NSeq{\Sigma}{\Delta}{\Bscr} \qquad

3223:          \NSeq{\Sigma}{\Bscr,\Gamma}{\Cscr}}

3224: $$

3225: $$

3226: \infer[\landL]

3227:       {\NSeq

3228:         {\Sigma}

3229:         {\Judg{\sigma}{B \land C},\Gamma}

3230:         {\Dscr}

3231:       }

3232:       {\NSeq

3233:         {\Sigma}

3234:         {\Judg{\sigma}{B}, \Judg{\sigma}{C}, \Gamma}

3235:         {\Dscr}

3236:       }

3237: \qquad

3238: \infer[\landR]

3239:       {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B \land C}}}

3240:       {

3241:         \NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B} }

3242:         \qquad 

3243:         \NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{C}}

3244:       }

3245: $$

3246: $$

3247: \infer[\lorL]

3248:       {\NSeq{\Sigma}

3249:         {\Judg{\sigma}{B \lor C},\Gamma}{\Dscr}}

3250:       {\NSeq{\Sigma}{\Judg{\sigma}{B},\Gamma}{\Dscr}

3251:         \qquad

3252:         \NSeq{\Sigma}{\Judg{\sigma}{C},\Gamma}{\Dscr}

3253:       }

3254: \qquad

3255: \infer[\lorR]

3256:       {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B \lor C}}}

3257:       {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B}}}

3258: $$

3259: $$

3260: \infer[\botL]

3261:       {\NSeq{\Sigma}{\Judg{\sigma}{\bot},\Gamma}{\Bscr}}

3262:       {}

3263: \qquad 

3264: \infer[\lorR]{\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B \lor C}}}

3265:         {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{C}}}

3266: $$

3267: $$

3268: \infer[\oimpL]{\NSeq{\Sigma}{\Judg{\sigma}{B \oimp C},\Gamma}{\Dscr}}

3269:         {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B}}

3270:         \qquad \NSeq{\Sigma}{\Judg{\sigma}{C},\Gamma}{\Dscr}}

3271: \qquad 

3272: \infer[\oimpR]{\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B \oimp C}}}

3273:         {\NSeq{\Sigma}{\Judg{\sigma}{B},\Gamma}{\Judg{\sigma}{C}}}

3274: $$

3275: $$

3276: \infer[\forallL]

3277:       {\NSeq

3278:         {\Sigma}

3279:         {\Judg{\sigma}{\forall_\gamma x.B},\Gamma}

3280:         {\Cscr}

3281:       }

3282:       {

3283:         \TSeq{\Sigma, \sigma}{t}{\gamma}

3284:         \qquad

3285:         \NSeq

3286:         {\Sigma}

3287:         {\Judg{\sigma}{B[t/x]},\Gamma}{\Cscr}

3288:       }

3289: \qquad

3290: \infer[\forallR]

3291:       {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{\forall x.B}}}

3292:       {\NSeq{\Sigma, h}{\Gamma}

3293:         {\Judg{\sigma}{B[(h~\sigma)/x]}}}

3294: $$

3295: $$

3296: \infer[\existsL]{\NSeq{\Sigma}{\Judg{\sigma}{\exists x.B},\Gamma}{\Cscr}}

3297:         {\NSeq{\Sigma, h}{\Judg{\sigma}{B[(h~\sigma)/x]},\Gamma}{\Cscr}}

3298: \qquad 

3299: \infer[\existsR]

3300:       {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{\exists_\gamma x.B}}}

3301:       {

3302:         \TSeq{\Sigma, \sigma}{t}{\gamma} \qquad

3303:         \NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{B[t/x]}}}

3304: $$

3305: $$

3306: \infer[\nablaL]

3307: {\NSeq{\Sigma}{\Judg{\sigma}{\nabla x\ B},\Gamma}{\Cscr}}

3308: {

3309: \NSeq{\Sigma}{\Judg{(\sigma,y)}{B[y/x]}, \Gamma }{\Cscr}

3310: }

3311: \qquad

3312: \infer[\nablaR]

3313: {\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{\nabla x\ B}}}

3314: {

3315: \NSeq{\Sigma}{\Gamma}{\Judg{(\sigma,y)}{B[y/x]}}

3316: }

3317: $$

3318: $$

3319: \infer[\cL]{\NSeq{\Sigma}{\Bscr,\Gamma}{\Cscr}}

3320:         {\NSeq{\Sigma}{\Bscr,\Bscr,\Gamma}{\Cscr}}

3321: \qquad

3322: \infer[\wL]

3323:       {\NSeq{\Sigma}{\Bscr, \Gamma}{\Cscr}}

3324:       {\NSeq{\Sigma}{\Gamma}{\Cscr}}

3325: \qquad

3326: \infer[\topR]{\NSeq{\Sigma}{\Gamma}{\Judg{\sigma}{\top}}}{}

3327: $$

3328: }

3329: \caption{The core inference rules of $\FOLNb$.}

3330: \label{fig:folnb}

3331: \end{figure}

3332: \newcommand{\alphaL}{\alpha_{\cal R}}

3333: \newcommand{\alphaR}{\alpha_{\cal L}}

3334: 

3335: 

3336: We now show that the formulation of $\LG$ is equivalent 

3337: to $\FOLNb$ extended with the axiom schemes of name permutations

3338: and weakening:

3339: \begin{equation}

3340: \nabla x\nabla y.B \, x\,y \oimp \nabla y\nabla x.B\,x\,y

3341: \quad \hbox{ and } \quad 

3342: B \equiv \nabla x.B

3343: \end{equation}

3344: where $x$ is not free in $B$ in the second scheme.

3345: 

3346: 

3347: Sequents in $\FOLNb$ are expressions of the form

3348: $$

3349: \NSeq{\Sigma}{\Judg{\sigma_1}{B_1},\ldots, \Judg{\sigma_n}{B_n}}{\Judg{\sigma_0}{B_0}}.

3350: $$

3351: $\Sigma$ is the {\em signature} of the sequent, $\sigma_i$ is

3352: a list of variables locally scoped over $B_i$, and is referred to as {\em local signature}.

3353: The expression $\Judg{\sigma_i}{B_i}$ is called a {\em local judgment},

3354: or {\em judgment} for short.

3355: In~\cite{miller05tocl}, local judgments are considered equal modulo renaming

3356: of their local signatures, e.g., $(a,b) \triangleright P\,a\,b$ is

3357: equal to $(c,d)\triangleright P\,c\,d.$

3358: Local judgments are ranged over by scripted capital letters, e.g.,

3359: $\Bscr$, $\Dscr$, etc.

3360: For the purpose of proving the correspondence with $\LG$, however,

3361: we will make this renaming step explicit, by including the rules:

3362: $$

3363: \infer[\alphaL, \lambda \vec x.B \equiv_\alpha \lambda \vec y.B']

3364: {\Seq{\Judg{\vec x}{B}, \Gamma}{\Cscr}}

3365: {\Seq{\Judg{\vec y}{B'}, \Gamma}{\Cscr}}

3366: \qquad

3367: \infer[\alphaR,  \lambda \vec x.B \equiv_\alpha \lambda \vec y.B']

3368: {\Seq{\Gamma}{\Judg{\vec x}{B}}}

3369: {\Seq{\Gamma}{\Judg{\vec y}{B'}}}

3370: $$

3371: The inference rules of $\FOLNb$ are given in Figure~\ref{fig:folnb}.

3372: 

3373: \newcommand{\pL}{p{\cal L}}

3374: \newcommand{\pR}{p{\cal R}}

3375: \newcommand{\ssL}{ss{\cal L}}

3376: \newcommand{\ssR}{ss{\cal R}}

3377: \newcommand{\wsL}{ws{\cal L}}

3378: \newcommand{\wsR}{ws{\cal R}}

3379: 

3380: We now consider the correspondence between $\LG$ with $\FOLNb$

3381: extended with the following axiom schemes:

3382: \begin{equation}

3383: \label{eq:axiom1}

3384: \nabla x \nabla y.B\,x\,y \equiv \nabla y \nabla x.B\,x\,y.

3385: \end{equation}

3386: \begin{equation}

3387: \label{eq:axiom2}

3388: B \equiv \nabla x.B, \hbox{provided that $x$ is not free in $B$.}

3389: \end{equation}

3390: We can equivalently state these two axioms as the following inference

3391: rules:

3392: $$

3393: \infer[\pL]

3394: {\Seq{\Judg{(\vec x,a,b,\vec y)}{B}, \Gamma}{\Cscr}}

3395: {\Seq{\Judg{(\vec x,b,a,\vec y)}{B}, \Gamma}{\Cscr}}

3396: \qquad

3397: \infer[\pL]

3398: {\Seq{\Gamma}{\Judg{(\vec x,a,b,\vec y)}{B}}}

3399: {\Seq{\Gamma}{\Judg{(\vec x,b,a,\vec y)}{B}}}

3400: $$

3401: $$

3402: \infer[\ssL, a \not \in \{\vec x, \vec y\}]

3403: {\Seq{\Judg{(\vec x\vec y)}{B}, \Gamma}{\Cscr}}

3404: {\Seq{\Judg{(\vec x,a,\vec y)}{B}, \Gamma}{\Cscr}}

3405: \qquad

3406: \infer[\ssR,  a \not \in \{\vec x, \vec y\}]

3407: {\Seq \Gamma {\Judg{(\vec x\vec y)}{B}}}

3408: {\Seq \Gamma {\Judg{(\vec x,a,\vec y)}{B}} }

3409: $$

3410: $$

3411: \infer[\wsL, a \not \in supp(B)]

3412: {\Seq{\Judg{(\vec x,a,\vec y)}{B}, \Gamma}{\Cscr}}

3413: {\Seq{\Judg{(\vec x\vec y)}{B}, \Gamma}{\Cscr}}

3414: \qquad

3415: \infer[\ssR,  a \not \in supp(B)]

3416: {\Seq \Gamma {\Judg{(\vec x,a,\vec y)}{B}}}

3417: {\Seq \Gamma {\Judg{(\vec x\vec y)}{B}} }

3418: $$

3419: Implicit in the above rules is the assumption that

3420: variables in local signatures are considered as

3421: special constants, much like the nominal constants

3422: in $\LG$. The support of $B$, within a local

3423: signature $\sigma$, is defined similarly

3424: as it is in $\LG$: it is the set

3425: $\{ a \in \sigma \mid \hbox{$a$ occurs in $B.$} \}.$

3426: 

3427: \newcommand{\FOLNbp}{FO\lambda^{\nabla+}}

3428: 

3429: The logical system with the inference rules in Figure~\ref{fig:folnb} together

3430: with $\alphaL$, $\alphaR$, $\pL$, $\pR$,

3431: $\ssL$, $\ssR$, $\wsL$ and $\wsR$ is referred to as $\FOLNbp$.

3432: In relating $\LG$ and $\FOLNbp$, we map the local signatures

3433: to nominal constants, and vice versa.

3434: In the following, given a formula $B$, we assume a particular

3435: enumeration of the nominal constants appearing in $B$

3436: based the left-to-right order of their appearance in $B$.

3437: \begin{lemma}

3438: \label{lm:lg to folnb}

3439: If the sequent $\NSeq{\Sigma}{B_1,\ldots,B_n}{B_0}$

3440: is provable in $\LG$ then the sequent

3441: $$

3442: \NSeq{\Sigma}{\Judg{\vec c_1}{B_1}, \Judg{\vec c_n}{B_n}}{\Judg{\vec c_0}{B_0}}

3443: $$

3444: where $\vec c_i$  is an enumeration of $supp(B_i),$

3445: is provable in $\FOLNbp.$

3446: \end{lemma}

3447: \begin{proof}

3448: Suppose that $\Pi$ is 

3449: a proof of $\NSeq{\Sigma}{B_1,\ldots,B_n}{B_0}.$

3450: We construct a proof $\Pi'$ of

3451: $$

3452: \NSeq{\Sigma}{\Judg{\vec c_1}{B_1}, \Judg{\vec c_n}{B_n}}{\Judg{\vec c_0}{B_0}}

3453: $$

3454: by induction on $ht(\Pi).$

3455: We consider some interesting cases here:

3456: \begin{itemize}

3457: \item Suppose $\Pi$ ends with  $id_\pi:$

3458: $$

3459: \infer[id_\pi]

3460: {\Seq{\Gamma', B_i}{B_0}}

3461: {\pi.B_i = \pi'.B_0}

3462: $$

3463: The permutations $\pi$ and $\pi'$ can be imitated by a series of renaming

3464: ($\alphaL$ and $\alphaR$ rules). 

3465: The derivation $\Pi'$ is therefore constructed by applying a series of 

3466: $\alpha_R$, $\alpha_L$, followed by the $id$ rule.

3467: 

3468: \item Suppose $\Pi$ ends with $\oimpR:$ in this case we suppose that

3469: $B_0 = C \oimp D.$

3470: $$

3471: \infer[\oimpR]

3472: {\Seq{B_1,\ldots,B_n}{C \oimp D}}

3473: {\deduce{\Seq{B_1,\ldots,B_n, C}{D}}{\Pi_1}}

3474: $$

3475: By induction hypothesis we have a derivation $\Pi_2$

3476: of

3477: $$

3478: \Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n}, \Judg{\vec a}{C}}

3479: {\Judg{\vec b}{D}}

3480: $$

3481: We first have to weaken the signatures $\vec a$ and $\vec d$ to

3482: $\vec c_0$ before applying the introduction rule for $\oimp$.

3483: That is, $\Pi'$ is the derivation

3484: \settowidth{\infwidthi}

3485: {$\Seq{\Judg{\vec c_1}{B_1,\ldots, \Judg{\vec c_n}{B_n}}, \Judg{\vec c_0}{C}}

3486:     {\Judg{\vec c_0}{D}}$}

3487: $$

3488: \infer[\oimpR]

3489: {\Seq{\Judg{\vec c_1}{B_1,\ldots, \Judg{\vec c_n}{B_n}}}{\Judg{\vec c_0}{C \oimp D}}}

3490: {

3491: \infer[*]

3492: {

3493: \Seq{\Judg{\vec c_1}{B_1,\ldots, \Judg{\vec c_n}{B_n}}, \Judg{\vec c_0}{C}}

3494:     {\Judg{\vec c_0}{D}}

3495: }

3496: {

3497:   \infer[]

3498:    {\makebox[\infwidthi]{}}

3499:    {

3500:         \deduce{\Seq{\Judg{\vec c_1}{B_1,\ldots, \Judg{\vec c_n}{B_n}}, \Judg{\vec a}{C}}

3501:                {\Judg{\vec b}{D}}  }{\Pi_2}

3502:    }

3503: }

3504: }

3505: $$

3506: Here the star `*' denotes a series of applications of $\wsL$,

3507: $\wsR$, $\pL$ and $\pR.$

3508: 

3509: \item Suppose $\Pi$ is

3510: $$

3511: \infer[\existsR]

3512: {\Seq{B_1,\ldots,B_n}{\exists x.C}}

3513: {\deduce{\Seq{B_1,\ldots,B_n}{C[t/x]}}{\Pi_1}}

3514: $$

3515: It is possible that $t$ contains new constants that are not in the

3516: support of $C.$ Suppose $\vec d$ is an enumeration of 

3517: the support of $C[t/x]$. 

3518: The derivation $\Pi'$ is constructed as follows

3519: $$

3520: \infer[*]

3521: {\Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n} }

3522: {\Judg{\vec c_0}{\exists x.C}}}

3523: {

3524: \infer[]

3525: {\makebox[\infwidthi]{}}

3526: {

3527: \infer[\existsR]

3528: { 

3529: \Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n} }

3530: {\Judg{\vec d}{\exists x.C}}

3531: }

3532: {

3533: \deduce{ 

3534: \Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n} }

3535: {\Judg{\vec d}{C[t/x]}}

3536: }{\Pi_2}

3537: }

3538: }

3539: }

3540: $$

3541: where $\Pi_2$ is obtained from induction hypothesis applied

3542: to $\Pi_1$, and the rule `*' denotes a series of

3543: applications of $\ssR$ (for introducing new constants) 

3544: and $\pR$ (for rearranging the order of the local signature).

3545: 

3546: \item For other cases, the construction of $\Pi'$ follows the same 

3547: pattern as in the previous cases, i.e., 

3548: by induction hypothesis, followed by some rearranging, extension,

3549: or weakening of local signatures.

3550: \end{itemize}

3551: \qed

3552: \end{proof}

3553: 

3554: \begin{lemma}

3555: \label{lm:folnb to lg}

3556: If the sequent 

3557: $$

3558: \NSeq{\Sigma}{\Judg{\vec c_1}{B_1}, \Judg{\vec c_n}{B_n}}{\Judg{\vec c_0}{B_0}}

3559: $$

3560: is provable in $\FOLNbp$ then the sequent

3561: $\NSeq{\Sigma}{B_1,\ldots,B_n}{B_0}$

3562: is provable in $\LG$

3563: \end{lemma}

3564: \begin{proof}

3565: Suppose $\Pi$ is a derivation of 

3566: $$

3567: \Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n} } {\Judg{\vec c_0}{B_0}}

3568: $$

3569: We construct a derivation $\Pi'$ of 

3570: $\Seq{B_1,\ldots,B_n}{B_0}$ by induction on $ht(\Pi)$.

3571: We show here the interesting cases; the other cases follow

3572: immediately from induction hypothesis:

3573: \begin{itemize}

3574: \item If $\Pi$ ends with $id$, $\topR$, or $\botL$ then $\Pi'$ ends with

3575: the same rule.

3576: \item Suppose $\Pi$ is

3577: $$

3578: \infer[\alphaR]

3579: {\Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n}}{\Judg{\vec c_0}{B_0}}}

3580: {

3581: \deduce{\Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n} }{\Judg{\vec d}{B}}}

3582: {\Pi_1}

3583: }

3584: $$

3585: By induction hypothesis, there is a derivation $\Pi_2$

3586: of

3587: $\Seq{{B_1}, \ldots, {B_n} }{{B}}.$

3588: To get $\Pi'$ apply the procedure in Definition~\ref{def:perm}

3589: to $\Pi_2$ to rename $B$ to $B_0$.

3590: 

3591: \item Suppose $\Pi$ is

3592: $$

3593: \infer[\forallR]

3594: {\Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n}}{\Judg{\vec c_0}{\forall x.C}}}

3595: {

3596: \deduce{ 

3597: \Seq{\Judg{\vec c_1}{B_1}, \ldots, \Judg{\vec c_n}{B_n}}{\Judg{\vec c_0}{C[(h\,\vec c_0)/x]}}

3598: }{\Pi_1}

3599: }

3600: $$

3601: By induction hypothesis, there is a derivation $\Pi_2$

3602: of 

3603: $\Seq{{B_1}, \ldots, {B_n}}{{C[(h\,\vec c_0)/x]}}.$

3604: Suppose $\{ \vec d \} = supp(C).$ Then $\Pi'$ is

3605: $$

3606: \infer[\forallR]

3607: {\Seq{B_1,\ldots,B_n}{\forall x.C}}

3608: {

3609: \deduce{\Seq{B_1,\ldots,B_n}{C[h'\,\vec d/x]}}{\Pi_2[\lambda \vec c_0.h'\,\vec d/h]}

3610: }

3611: $$

3612: 

3613: \item If $\Pi$ ends with $\existsL$, apply the same construction as in the

3614: previous case.

3615: \end{itemize}

3616: \qed

3617: \end{proof}

3618: 

3619: 

3620: \begin{theorem}

3621: \label{thm:lg equal folnb}

3622: Let $F$ be a formula which contains no occurrences of 

3623: nominal constants. Then $F$ is provable in $\FOLNb$ extended with

3624: the axiom schemes $B \equiv \nabla x.B$ and 

3625: $\nabla x\nabla y. B\,x\,y \oimp \nabla y\nabla x.B\,x\,y$

3626: if and only if 

3627: $F$ is provable in $\LG.$

3628: \end{theorem}

3629: 

3630: 

3631: \begin{thebibliography}{10}

3632: 

3633: \bibitem{girard92mail}

3634: J.-Y. Girard.

3635: \newblock A fixpoint theorem in linear logic.

3636: \newblock Email to the linear@cs.stanford.edu mailing list, February 1992.

3637: 

3638: \bibitem{hallnas91jlc}

3639: L.~Halln{\"{a}}s and P.~Schroeder-Heister.

3640: \newblock A proof-theoretic approach to logic programming. {II}. {Programs} as

3641:   definitions.

3642: \newblock {\em Journal of Logic and Computation}, 1(5):635--660, October 1991.

3643: 

3644: \bibitem{mcdowell00tcs}

3645: R.~McDowell and D.~Miller.

3646: \newblock Cut-elimination for a logic with definitions and induction.

3647: \newblock {\em Theoretical Computer Science}, 232:91--119, 2000.

3648: 

3649: \bibitem{mcdowell02tocl}

3650: R.~McDowell and D.~Miller.

3651: \newblock Reasoning with higher-order abstract syntax in a logical framework.

3652: \newblock {\em ACM Transactions on Computational Logic}, 3(1):80--136, January

3653:   2002.

3654: 

3655: \bibitem{miller91jlc}

3656: D.~Miller.

3657: \newblock A logic programming language with lambda-abstraction, function

3658:   variables, and simple unification.

3659: \newblock {\em Journal of Logic and Computation}, 1(4):497--536, 1991.

3660: 

3661: \bibitem{miller92jsc}

3662: D.~Miller.

3663: \newblock Unification under a mixed prefix.

3664: \newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.

3665: 

3666: \bibitem{miller99surveys}

3667: D.~Miller and C.~Palamidessi.

3668: \newblock Foundational aspects of syntax.

3669: \newblock In P.~Degano, R.~Gorrieri, A.~Marchetti-Spaccamela, and P.~Wegner,

3670:   editors, {\em ACM Computing Surveys Symposium on Theoretical Computer

3671:   Science: A Perspective}, volume~31. ACM, September 1999.

3672: 

3673: \bibitem{miller05tocl}

3674: D.~Miller and A.~Tiu.

3675: \newblock A proof theory for generic judgments.

3676: \newblock {\em ACM Trans.\ on Computational Logic}, 6(4):749--783, Oct. 2005.

3677: 

3678: \bibitem{nipkow93lics}

3679: T.~Nipkow.

3680: \newblock Functional unification of higher-order patterns.

3681: \newblock In M.~Vardi, editor, {\em Proc.\ 8th {IEEE} Symposium on Logic in

3682:   Computer Science ({LICS} 1993)}, pages 64--74. IEEE, June 1993.

3683: 

3684: \bibitem{pfenning88pldi}

3685: F.~Pfenning and C.~Elliott.

3686: \newblock Higher-order abstract syntax.

3687: \newblock In {\em Proceedings of the {ACM}-{SIGPLAN} Conference on Programming

3688:   Language Design and Implementation}, pages 199--208. ACM Press, June 1988.

3689: 

3690: \bibitem{pitts03ic}

3691: A.~M. Pitts.

3692: \newblock Nominal logic, a first order theory of names and binding.

3693: \newblock {\em Information and Computation}, 186(2):165--193, 2003.

3694: 

3695: \bibitem{schroeder-heister92nlip}

3696: P.~Schroeder-Heister.

3697: \newblock Cut-elimination in logics with definitional reflection.

3698: \newblock In D.~Pearce and H.~Wansing, editors, {\em Nonclassical Logics and

3699:   Information Processing}, volume 619 of {\em LNCS}, pages 146--171. Springer,

3700:   1992.

3701: 

3702: \bibitem{tiu04phd}

3703: A.~Tiu.

3704: \newblock {\em A Logical Framework for Reasoning about Logical Specifications}.

3705: \newblock PhD thesis, Pennsylvania State University, May 2004.

3706: 

3707: \bibitem{tiu07entcs}

3708: A.~Tiu.

3709: \newblock A logic for reasoning about generic judgments.

3710: \newblock {\em Electr. Notes Theor. Comput. Sci.}, 174(5):3--18, 2007.

3711: 

3712: \end{thebibliography}

3713: 

3714: 

3715: \end{document}

3716: 

3717: