Tag Info

Alright I'll give a crack at it: In general for a given type system $T$, the following is true: If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a logic. The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and ...

The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL. Taking $\iota$ as the base type of numbers ans $\omicron$ as the base type of propositions, you can add the constants $$ \forall_\tau:(\tau\rightarrow \omicron)\...

Here is an answer to a variant of @cody's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @cody's sense, if we allow the introduction of additional axioms and $\beta$-reduction rules. Thus strictly speaking the system is not an LPTS; it is merely something much like one. Consider the calculus of constructions (...

I suspect someone is going to come along with a deep category-theoretic reason for the connection, but in the meantime, here is my insight. Both logic and programming with functions are built around the notion of hypotheticals. The proposition $A \to B$ says "If I had an $A$, I could prove $B$." A function of type $A \to B$ says "If I had a ...

Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the HoTT book. This provides an equivalence along which we can swap $\Sigma$ and $\Pi$ types. Assuming $A : U$, $B : A \to U$ and $C : \prod_{a : A} B\,a \to U$, we have an equivalence: $$ac : \Big(\prod_{a : A}\sum_{b : B\,a}\,C\,a\,b\...

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type is held abstract, it works a lot like 'false' in that there is no introduction rule for it. With respect to the paper you linked (I'm by no means an expert on ...

Actually, the motivation for introducing dependent types goes in the opposite direction! Curry had noticed that there was a direct correspondence between typed terms in the $SK$ calculus and proofs in (minimal implicational) propositional logic, but there was no programing language known to correspond in such a way to predicate logic. Indeed, introducing $\...

I'll answer the opposite question which is: can Curry-Howard prove a theorem for your program, which has nothing to do with the type? The answer is yes, depending on the meaning of "nothing to do". I'll leave the Curry-Howard aspect aside somewhat, but it underlies a lot of this approach. The key idea is Wadlers' Theorems for Free! building on ideas ...

Someone wanted a deep category-theoretic insight? A Heyting algebra is a cartesian-closed category.

Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): Olivier Laurent, Étude de la polarisation en logique (2002). A good explanation of what is going on from a categorical perspective is given in Melliès and Tabareau, Resource modalities in tensor logic (2010). A ...

As other commenters have mentioned what you are actually asking for is a language for planar string diagrams, aka monoidal categories. But let me address your question purely from the point of view of quantum computation. Clearly in any reasonable system you would want to have an introduction rule for the tensor product -- your proposed weakening rule is ...

If you remove all those rules and add something like If $A \vdash B$ and $A' \vdash B'$ then $A, A' \vdash B, B'$ you get a logic essentially for monoidal categories (it's basically string diagrams in a sequent form). As a concrete example, you can imagine that the propositions are endo-functors and $,$ is composition.

For me, what is going on is reasonably standard: You have $c$ with free variables $(x_i : \tau_i)_i$, and you replace it with $c[t_i/x_i]$ with the $(t_i)_i$ at types $(\tau_i)_i$; this is a standard cut/substitution. The replacement is done along a variable $k$ that is defined somewhere and used elsewhere; this sort of "action at a distance" is ...

You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has "coexponentials." Unfortunately you can't combine "coimplication" and "implication" constructively. You need to weaken something somewhere ...