# Tag Info

## Hot answers tagged lo.logic

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{... 31 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 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$". ... 25 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 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 ... 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 ... 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\... 20 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 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 inequationsS=\{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 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 ... 18 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 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 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 ... 14 An \omega-regular language is actually quite low in the Borel hierarchy (inside \Delta_3), a result due to R. McNaughton, Testing and generating infinite sequences by a finite automaton, Information and Control 9 (1966), 521-530. For a proof and more details, you can look at Chapter 3 of the following book D. Perrin et J.-É. Pin, Infinite words, ... 14 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 compositional method of giving semantics to a programming language. However, you can build denotational models out of a structural operational semantics by using a ... 14 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 types as a (n-ary) relation R \subseteq \cal A^n. This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. ... 14 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 theorem. (See comment section below for further discussion.) Let K(x) be the Kolmogorov complexity of string x. lemma. K is not computable. Proof. ... 13 I'm assuming you mean Krivine's notation from Lambda Calculus: Types and Models. This notation, used as a data representation, makes many algorithms on lambda-terms simpler to implement and prove correct. That is, given a lambda term f\; e_1\; e_2\; \ldots\; e_n, you want to view it as a head f, together with a list of arguments [e_1, e_2, \ldots, ... 13 Here's a slightly different perspective on Fredrik's answer. It's generally the case that impredicative Church encodings of types will satisfy the relevant \beta laws, but will not satisfy the \eta laws. So this means we can define a dependent pair as follows:$$ \exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \...

13

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 logic and Milner's encoding of functions into processes, as described here: From Process Logic to Program Logic The work by Régis-Gianas et al mentioned in ...

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