40

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$. It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{...


30

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 perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort). But does incompleteness "...


26

Firstly, I want to address the comments to the question, where it was suggested that "false" expresses $P = PSPACE$ because the statement is false. While this might be a good joke, it is actually very much harmful to think this way. When we ask how to express a certain sentence in a certain formal system, we are not talking about truth values. If we were, ...


26

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 the untyped lambda calculus (or combinatory logic) and interpret $XZ$ as expressing "$Z$ satisfies the predicate $X$" and $\Xi XY$ as expressing "$X\subseteq Y$". ...


24

As Steven notes, the canonical example is $\mathsf{IP} = \mathsf{PSPACE}$. This collapse does not relativize, in the sense that there is an oracle $A$, subject to which $\mathsf{IP}^A \ne \mathsf{PSPACE}^A$. The intuition why the known proof of this result avoids the relativization barrier is that it uses arithmetization (Yonatan alluded to this in a comment)...


24

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 propositional to first-order logic. The key contribution of Martin-Löf's is a novel analysis of equality. There are two main ways of giving Curry-Howard style ...


23

I am not aware of a paper concerned with the comparison between symbolic execution and abstract interpretation. Nor do I think one is needed. Reading the original descriptions of these two techniques should be enough. King, Symbolic Execution and Program Testing, 1976 Cousot, Cousot, Abstract Interpretation: a Unified Lattice Model for Static Analysis of ...


21

Andrej has already explained that $P=\mathit{PSPACE}$ can be written as a $\Sigma^0_2$-sentence. Let me mention that this classification is optimal in the sense that if the statement is equivalent to a $\Pi^0_2$-sentence, then this fact does not relativize. More precisely, the set of oracles $A$ such that $P^A=\mathit{PSPACE}^A$ is definable by a $\Sigma^0_2$...


21

$S^1_2$ is a theory of bounded arithmetic, that is, a weak axiomatic theory obtained by severely restricting the schema of induction of Peano arithmetic. It is one of the theories defined by Sam Buss in his thesis, other general references include Chapter V of Hájek and Pudlák’s Metamathematics of first-order arithmetic, Krajíček’s “Bounded arithmetic, ...


21

($=$ 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 $|$, $+$, and $\le$: $$\begin{align*} \gcd(a,b)=c&\iff c\ge0\land c\mid a\land c\mid b\land\forall d\:(d\mid a\land d\mid b\to d\mid c)\\ &\iff c\ge0\land c\...


19

The basic sum-of-squares proof system, introduced under the name of Positivstellensatz refutations by Grigoriev and Vorobjov, is a “static” proof system for showing that a set of polynomial equations and inequations $$S=\{f_1=0,\dots,f_k=0,h_1\ge0,\dots,h_m\ge0\},$$ where $f_1,\dots,f_k,h_1,\dots,h_m\in\mathbb R[x_1,\dots,x_n]$, has no common solution in $\...


19

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 are asking whether there can be uncountably many terms of a given type. The answer is: obviously not since there are only countably many finite strings, and ...


19

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 mathematician. To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc: We provide a function $f$ which ...


18

LCF is indeed the grand-father of all these system: Coq, Isabelle, HOLs, including the ML programming language (which we see today as OCaml, SML, also F#). Yes, I am including Coq as a member of the greater LCF family. Compared to the US-American proof assistants (notably ACL2), or the totally unrelated Mizar, Coq is culturally quite close to Isabelle and ...


17

Yes, but you have to consider typed combinators. That is, you need to give $S$ and $K$ the following type schemas: $$ \begin{array}{lcl} K & : & A \to B \to A \\ S & : & (A \to B \to C) \to (A \to B) \to (A \to C) \end{array} $$ where $A, B$, and $C$ are meta-variables which can be instantiated to any concrete type at each use. Then, you ...


17

Semantically, a coercion $c : A \leq B$ is just a morphism $c : A \to B$, which gets added to the interpretation of terms at the appropriate points. The basic problem this creates is the issue of coherence: are you guaranteed that a term will have a unique meaning, given that the same term can potentially have coercions hidden in many possible places in the ...


17

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 research field, with a competition (the POPLmark challenge) some years ago. There are even jokes by people in the field about the complexity of approaches to ...


17

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 answered negatively by Turing in his famous 1936 paper "On Computable Numbers, with an application to the Entscheidungsproblem". The word literally means ...


16

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 extended with past-time modalities does not have more logical expressive power than LTL with only future modalities but properties can be defined in an ...


15

I briefly reviewed some areas here, trying to focus on ideas that would appeal to someone with a background in advanced mathematical logic. Finite Model Theory The simplest restriction of classical model theory from the viewpoint of computer science is to study structures over a finite universe. These structures occur in the form of relational databases, ...


15

Proof nets are interesting essentially for three reasons: 1) IDENTITY OF PROOFS. They provide an answer to the problem "when are two proofs the same"? In sequent calculus you may have many different proofs of the same proposition which differ only because sequent calculus forces an order among deduction rules even when this is not necessary. Of course, one ...


15

This is the same idea as Andrej's answer but with more details. Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 < y_1, y_2 < x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. ...


15

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 express Hoare-style properties of the inhabitants of various datatypes. Another possible candidate is the $F^*$ language, which offers similar constructs. There ...


15

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 that spaces of measurable functions generally have no Borel $\sigma$-algebra for which the application function - sometimes called "eval" - is measurable; see ...


14

It is important to understand that there is a spectrum from deep to shallow. You model the parts of your language deeply that should somehow participate in some inductive argument about the construction of it, the remainder is better left in the shallow see of direct semantics of the substrate of the logic. For example, when you want to reason about Hoare ...


14

Our goal is to prove that $\aleph_1 < 2^{\aleph_0}$ in the model $M[G]$, and therefore the Continuum Hypothesis is not true in $M[G]$. This is equivalent to saying that $\aleph_2 \leq 2^{\aleph_0}$. So we need to construct a model $M[G]$ such that there is an injective map $f$ from $\aleph_2$ to $2^{\aleph_0}$ in $M[G]$. Note that each element of $2^{\...


14

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.


14

Let us call a logic "symmetric" where a $-A$ ("not A") assumption means the same as proving $A$ and a proof of $-A$ means the same as an assumption of $A$. Classical logic and linear logic are symmetric in this sense. Intuitionistic logic is not. Girard noticed that natural deduction is asymmetric in exactly this way. That is why it matches up with ...


14

The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau (Journal, ECCC, author's copy). Theorem 2 of the paper states that, given a CNF formula $F$, resolution refutations of width at most $k$ for $F$ are equivalent to winning strategies for Spoiler in the existential $(k+1)$-pebble ...


14

You are looking for an ALL-SAT or all solutions SAT solver. This is a different problem from #SAT. You do not have to enumerate all solutions to count them. I do not know of a tool that solves your problem because people add these algorithms on top of existing SAT solvers but rarely seem to release these extensions. Two papers that should help you in ...


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