Timeline for Consistency in pure type systems
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 11, 2023 at 8:25 | vote | accept | Spaceka13 | ||
| Sep 11, 2023 at 8:23 | comment | added | Peter LeFanu Lumsdaine | [cont’d] In dependent type theory, these are all mutually recursive, since proofs/terms can appear inside propositions/types — so axioms/constants of the system have to be all given at the start, before the typing judgement can be defined. On the other hand, for finite theories this isn’t an issue, because you don’t need any constants/axioms baked in — you can just introduce them as variables — this is one of the powerful features of a PTS or similar systems. | |
| Sep 11, 2023 at 8:22 | comment | added | Peter LeFanu Lumsdaine | @Spaceka13: On your second comment — This is subtle and depends a bit on the type theory. Conceptually, most type theorists I know do think of theories in a “stratified” way, with parts of the syntax introduced before others, not all-at-once. But formally, the presentation of the system isn’t stratified so straightforwardly. E.g. in predicate logic, types (if any) can be presented first, then terms (generated from atomic ones), then propositions (generated from atomic predicates), then proofs (generated from axioms). [cont’d] | |
| Sep 11, 2023 at 8:14 | comment | added | Spaceka13 | Perfect, that's what I was thinking; thank you for clarifying. | |
| Sep 11, 2023 at 8:13 | comment | added | Peter LeFanu Lumsdaine | @Spaceka13: On your first comment — No, variables don’t give inconsistency, because use of variables is tracked by the context saying what variables you’re currently assuming — so you have $v \colon \bot \vdash v \colon \bot$, but you don’t have $\vdash v \colon \bot$ in the empty context — and the definition of inconsistency is proving $\bot$ in the empty context. The explicit use of contexts throughout is fundamental to how most type theories work — be careful not to disregard them! | |
| Sep 11, 2023 at 4:26 | comment | added | Spaceka13 | Second, on your second bolded point...My audience generally uses typed languages like this: first specify what the vocabulary is, along with each bit of vocabulary's grammatical category; then use that vocabulary to formulate grammatical expressions of type t which comprise a formal theory of something. It sounds like you're saying that the way this would go, in comp sci, is more `all at once': specify both the vocabulary and associated grammatical categories in a way which (implies terms of type t which?) comprises a formal theory of that same something. Is that right? | |
| Sep 11, 2023 at 4:11 | comment | added | Spaceka13 | Thank you, this is very helpful. Two follow-ups. First: the problem which motivated my first question seems to arise even if Consistency is denied. Variables also implies that there is a variable $\nu$ such that $\nu\mathbin{:}(\Pi x\mathbin{:}\ast.\ast)$ is an expression; so $(\Pi x\mathbin{:}\ast.\ast)$ is inhabited; and so once again, the standard definition of consistency is violated. Do I have that right? | |
| Sep 10, 2023 at 14:11 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |