8

I posted this to TYPES, but its probably worth copying here as well: In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F: However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging. There may be another explanation in ...


6

If every term in system T terminates, then $t\overline{n}\leadsto\overline{m}$ for every numeral $n$, and it is easy to show that a normal form $\overline{m}$ in the empty context is a numeral as well (and cannot be more complex!). In addition, it is easy to show, if the term $t\overline{n}$ is normalizing, that computing the normal form $\overline{m}$ can ...


4

The fact that a system is complete for proving valid formulas without the cut rule doesn't mean you can derive the cut rule from other rules. In fact it is not difficult to construct counter-examples. Consider $\Rightarrow A \rightarrow B$ and $\Rightarrow A$. From these assumptions it would follow that $\Rightarrow B$. But you cannot derive it without ...


2

Showing that from two cut-free derivations $\Gamma \vdash A$ and $\Gamma, A \vdash C$ you can produce a cut-free derivation of $\Gamma \vdash C$ is called cut admissibility. Admissibility of cut is actually equivalent to showing that cut can be eliminated. If you have cut-elimination, you just cut the two derivations together and then eliminate the cut. On ...


Only top voted, non community-wiki answers of a minimum length are eligible