2022 Developer Survey is open! Take survey.

# Tag Info

Accepted

### Homotopy type theory and Gödel's incompleteness theorems

HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were ...
• 26.4k
Accepted

### What was the original intent for the creation of Lambda calculus?

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory. The basic idea was to add a constant $\Xi$ to ...
Accepted

### Why was there a need for Martin-Löf to create intuitionistic type theory?

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from ...
• 10.3k
Accepted

### Decidability of diophantine equations over {=, +, gcd}

($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$...
• 14.7k
Accepted

### Types which correspond to sets of cardinality of continuum

You must be careful here. You are using set-theoretic concepts (cardinal, continuum) outside set theory. There is potential for confusion. Your question can be understood in several ways. Maybe you ...
• 26.4k
Accepted

### Why do constructivists not seem to care too much about call/cc

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive ...
• 26.4k
Accepted

### Do past time LTL and future time LTL have the same expressiveness?

The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when ...
• 12.3k
Accepted

### Why was Schönfinkel's work on eliminating "bound variables" in logic so crucial?

TL;DR. The metamathematics of binding are subtle: they seem trivial but aren't — whether you deal with (higher-order) logics or 𝜆-calculus. They're so subtle that binding representations form an open ...
• 1,999
Accepted

### Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)

The two words do not refer to the same thing. Hilbert's Entscheidungsproblem was the question whether there is an algorithm that decides the universal truth of first-order logical sentences, which was ...
• 4,501

### Are there any annotated formal verification systems for pure functional programming languages?

You might want to check out Liquid Haskell, which allow working with type refinements rather than dependent types. Type refinements can be seen as a restricted logical language that allow you to ...
• 13.1k
Accepted

### Scott's stochastic lambda calculi

One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is ...
• 674
Accepted

### Can we distinguish strictly syntactic and semantic methods in programming language?

No, you cannot strictly distinguish syntactic from semantic methods, but the distinction still ends up making sense. Structural operational semantics is not denotational, because it is not a ...
• 31.6k
Accepted

### Logical Reations for an Impredicative System in a Predicative MetaTheory

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent ...
• 13.1k

### Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's. Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's ...
• 8,133
Accepted

### Are there any annotated formal verification systems for pure functional programming languages?

Honda and Yoshida's A Compositional Program Logic for Polymorphic Higher-Order Functions (probably) pioneered Hoare logics for purely functional languages. This work is based on Hennessy-Milner ...
• 10.3k
Accepted

### Ramification of An Impredicative Type Theory

I'm going to elaborate my comments into an answer. The origins of predicative type theory are almost as old as type theory itself, since one of Russel's motivations was to ban "circular" definitions ...
• 13.1k
Accepted

### Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent....
• 4,783
Accepted

### Is there a good notion of non-termination and halting proofs in type theory?

Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing ...
• 13.1k
Accepted

### What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

Note that formulas using $\land$ and $\lor$ gates (and possibly the constants $0$ and $1$) are known as monotone. The complexity of monotone formula equivalence depends on how complex formulas are ...
• 14.7k
Accepted

### What is a term of the type $\bot\rightarrow A$?

There are several ways of writing such a term, depending on how we write the proof terms for the elimination rule for $\bot$, which is $$\frac{\quad\bot\quad}{A}$$ The corresponding rule in $\lambda$-...
• 26.4k
Accepted

### Logical framework vs type theory

Summary. A logical framework is a meta-language for the formalisation of deductive systems, where deductions become syntactic objects. Of course what counts as a meta-language is quite vague, and it ...
• 10.3k

### What is the difference between unification and anti-unification?

The following category theory inspired analysis (adapted from Plotkin's A Note on Inductive Generalization) explains a sense in which unification and anti-unification are dual concepts. As notation, ...
• 4,289
Accepted

### Does the first order theory of a finite structure have bounded quantifier rank?

The theory of any finite structure is model complete. In fact, it is easy to see that any formula is equivalent to an existential formula with one quantifier per each element of the structure, after ...
• 14.7k

### Why/when do we ever need transfinite loop variants?

You are correct when you observe that for any particular terminating loop $L$ we may simply define the invariant "we're getting one step closer to termination". But proving that this is indeed a valid ...
• 26.4k
Accepted

### Example of where violation of strict positivity condition in inductive types leads to inconsistency

It is actually possible to relax strict positivity and remain consistent. For instance, it suffices to only have a positivity condition. That is, we can accept type definitions like  T \triangleq ...
• 31.6k
Accepted

### "Correctness" of type theory

Type theories have multiple uses, and with each kind of usage comes a different notion of correctness. They two key uses are As a foundation of mathematics. In this context correctness means ...
• 10.3k

### What is logic programming and does it really add anything new to the logic?

I will just write what Frank Pfenning taught me (all mistakes go on my account). A traditional formal system in logic, such as natural deduction, is descriptive in the sense that it tells us what ...
• 26.4k
Accepted

### Can factorial be encoded in the Kappa-calculus with fixed point operator?

The bare $\kappa$-calculus does not permit defining factorial, even when extended with a fixed point operator. However, this answer deserves some unpacking. The fixed point operator you give is not ...
• 31.6k

### Are there any annotated formal verification systems for pure functional programming languages?

See also Yann Régis-Gianas PhD thesis work with François Pottier: A Hoare Logic for Call-by-Value Functional Programs (MPC'08). This work was extended to cover the usual ML side-effects by Johannes ...
• 1,882