2022 Developer Survey is open! Take survey.
32 votes
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 ...
user avatar
  • 26.4k
26 votes
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 ...
user avatar
24 votes
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 ...
user avatar
21 votes
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 $|$, $+$...
user avatar
20 votes
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 ...
user avatar
  • 26.4k
20 votes
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 ...
user avatar
  • 26.4k
18 votes
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 ...
user avatar
  • 12.3k
17 votes
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 ...
user avatar
  • 1,999
17 votes
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 ...
user avatar
15 votes

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 ...
user avatar
  • 13.1k
15 votes
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 ...
user avatar
14 votes
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 ...
user avatar
14 votes
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 ...
user avatar
  • 13.1k
14 votes

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 ...
user avatar
  • 8,133
13 votes
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 ...
user avatar
13 votes
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 ...
user avatar
  • 13.1k
13 votes
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....
user avatar
13 votes
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 ...
user avatar
  • 13.1k
13 votes
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 ...
user avatar
12 votes
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$-...
user avatar
  • 26.4k
12 votes
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 ...
user avatar
12 votes

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, ...
user avatar
12 votes
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 ...
user avatar
12 votes

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 ...
user avatar
  • 26.4k
11 votes
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 ...
user avatar
11 votes
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 ...
user avatar
11 votes

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 ...
user avatar
  • 26.4k
11 votes
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 ...
user avatar
11 votes

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 ...
user avatar
  • 1,882
11 votes
Accepted

Simply typed lambda calculus and higher order logic

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 ...
user avatar
  • 13.1k

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