Activity for Dan Doel
| Type | On... | Excerpt | Status | Date |
|---|---|---|---|---|
| Edit | Post #290954 | Initial revision | — | 9 months ago |
| Answer | — |
A: What is a “first-order substructural logic that has a cut-free sequent calculus”? The structural rules of sequent calculus are: - Weakening: $$\dfrac{Γ ⊢ C}{Γ, A ⊢ C}$$ - Contraction: $$\dfrac{Γ, A, A ⊢ C}{Γ, A ⊢ C}$$ - Exchange: $$\dfrac{Γ, A, B ⊢ C}{Γ, B, A ⊢ C}$$ Substructural logics omit at least one of these rules. As for cut elimination, part of the point is t... (more) |
— | 9 months ago |
| Edit | Post #288487 | Initial revision | — | over 1 year ago |
| Answer | — |
A: Considering the "type" $\Pi x:A.\Pi y:B(x).Type$ $\newcommand{\Type}{\mathsf{Type}}$ $\newcommand{\El}{\mathsf{El}}$ $\newcommand{\U}{\mathsf{U}}$ $\newcommand{\T}{\mathsf{T}}$ You would not add a supertype to $\Type$, because $\Type$ is not part of the object theory. It is the meta-theoretic object that classifies (all) the types of your obj... (more) |
— | over 1 year ago |