Cut Elimination for a Logic with Generic Judgments and Induction
| dc.creator | Tiu, Alwen | |
| dc.date | 2008-01-20 | |
| dc.date.accessioned | 2026-07-07T08:55:34Z | |
| dc.date.available | 2026-07-07T08:55:34Z | |
| dc.description | This paper presents a cut-elimination proof for the logic $LG^ω$, which is an extension of a proof system for encoding generic judgments, the logic $\FOLDNb$ of Miller and Tiu, with an induction principle. The logic $LG^ω$, just as $\FOLDNb$, features extensions of first-order intuitionistic logic with fixed points and a ``generic quantifier'', $\nabla$, which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend $\FOLDNb$ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on $\nabla$, in particular by adding the axiom $B \equiv \nabla x. B$, where $x$ is not free in $B$. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. This paper contains the technical proofs for the results stated in \cite{tiu07entcs}; readers are encouraged to consult \cite{tiu07entcs} for motivations and examples for $LG^ω.$ | |
| dc.identifier | https://arxiv.org/abs/0801.3065 | |
| dc.identifier | http://arxiv.org/abs/0801.3065 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/146310 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1 | |
| dc.title | Cut Elimination for a Logic with Generic Judgments and Induction | |
| dc.type | text |