# Questions tagged [lo.logic]

Computational and mathematical logic.

548 questions
Filter by
Sorted by
Tagged with
10k views

### Solid applications of category theory in TCS?

I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all ...
• 27.5k
5k views

• 411
2k views

### Where is the proof that Coq + Excluded Middle is consistent

I've seen (and heard) it claimed that it is safe to add the classical axiom of excluded middle to Coq, but I can not seem to find a paper supporting this claim. The papers I see listed on the Coq wiki ...
• 1,690
2k views

### Starting SAT solver papers

I want to make a first SAT solver. I know the SAT competition and the SAT conference, and there are just so many papers on this subject. I'm a starter, an overwhelmed starter. Where should I begin? ...
• 551
4k views

### What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...
• 604
818 views

### Curriculum: Logical/Formal Methods in Security

At present I teach a small course (Four two hour lectures at the Masters level) on Logical Methods in Security, though the title Formal Methods in Security might be more apt. It covers briefly the ...
• 16.7k
5k views

### Prove proof irrelevance in Coq?

Is there a way to prove the following theorem in Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. EDIT: An attempt to give a brief ...
• 2,805
2k views

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

I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church ...
• 5,305
1k views

### Circuit lower bounds and kolmogorov complexity

Consider the following reasoning: Let $K(x)$ denote the Kolmogorov complexity of the string $x$. Chaitin's incompleteness theorem says that for any consistent and sufficiently strong formal ...
• 845
1k views

### How can we know that formal methods work?

An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be ...
• 337
2k views

### Why can Lambda Calculus not represent some combinators?

This paper suggests that there are combinators (representing symbolic computations) that can not be represented by the Lambda calculus (if I understand things correctly):
• 2,581
1k views

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

It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $\{=, +, \cdot, 1\}$ (of equality, addition, ...
543 views

### Are recursive forms of Godel's statement possible?

The self-referentiality of the P/NP problem has sometimes been highlighted as a barrier to its resolution, see, for instance, Scott Aaronson's paper, is P vs. NP formally independent? One of the many ...
2k views

### Smallest possible universal combinator

I am looking for the smallest possible universal combinator, measured by the number of abstractions and applications required to specify such a combinator in the lambda calculus. Examples of universal ...
• 662