Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
38
votes
4answers
3k views

Are there any proofs the undecidability of the halting problem that does not depend on self-referencing or diagonalization ?

This is a question related to this one. Putting it again in a much simpler form after a lot of discussion there, that it felt like a totally different question. The classical proof of the ...
103
votes
7answers
7k 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 ...
26
votes
3answers
2k views

Translating SAT to HornSAT

Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT seems to imply that it is, but I have not been able to chase down ...
14
votes
1answer
474 views

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

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
66
votes
7answers
3k views

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD). Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a ...
47
votes
8answers
4k views

Are there non-constructive algorithm existence proofs?

I remember I might have encountered references to problems that have been proven to be solvable with a particular complexity, but with no known algorithm to actually reach this complexity. I struggle ...
47
votes
3answers
4k views

Shallow versus Deep Embeddings

When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written ...
37
votes
2answers
3k views

Axioms necessary for theoretical computer science

This question is inspired by a similar question about applied mathematics on mathoverflow, and that nagging thought that important questions of TCS such as P vs. NP might be independent of ZFC (or ...
38
votes
5answers
1k views

Is there a logic without induction that captures much of P?

The Immerman-Vardi theorem states that PTIME (or P) is precisely the class of languages that can be described by a sentence of First-Order Logic together with a fixed-point operator, over the class of ...
24
votes
4answers
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? ...
18
votes
3answers
2k views

Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
26
votes
5answers
1k views

What is the difference between proofs and programs (or between propositions and types)?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?
12
votes
3answers
744 views

What are natural examples of non-relativizable proofs?

As I understand it, a proof that P=NP or P≠NP would need to be non-relativizable (as in recursion theory oracles). Virtually all proofs seem to be relativizable, though. What are good examples of ...
16
votes
2answers
1k views

What do we know about restricted versions of the halting problem

(UPDATE: a better formed question is posed here as the comments for the accepted answer below show that this question is not well-defined) The classical proof of the impossibility of the halting ...
19
votes
1answer
552 views

Combinators for the Primitive Recursive Functions

It is well-known that the S and K combinators are Turing Complete. Are there combinators that suffice to yield (only) the primitive recursive functions?
15
votes
1answer
918 views

Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
14
votes
1answer
270 views

Characterising invisible equivalences by confluent rewrite rules

In response to another question, Extensions of beta theory of lambda calculus, Evgenij offered the answer: beta + the rule {s = t | s and t are closed unsolvable terms} where a term M is solvable if ...
9
votes
2answers
267 views

Intuition behind proof systems

I'm trying to under stand the paper On p-Optimal Proof Systems and Logic for PTIME. There is a notion called proof systems in the paper and I do not get the intution: $\Sigma = \{0,1\}$ ... We ...
9
votes
2answers
293 views

What is the benefit of Krivine's notation?

I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
15
votes
1answer
420 views

Is MALL + unrestricted recursive types Turing-complete?

If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator: $$ \begin{array}{lcl} \omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\...
46
votes
5answers
5k views

What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
39
votes
4answers
3k views

How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
44
votes
3answers
3k views

How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
40
votes
2answers
5k views

Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
14
votes
1answer
2k views

What are the classic papers from the recursion theoretic area of complexity theory?

Two papers I would include are: D. Kozen, "Indexing of subrecursive classes", STOC, 1978. R. Ladner, "On the Structure of Polynomial Time Reducibility", JACM, 1975.
27
votes
4answers
5k views

Church's Theorem and Gödel's Incompleteness Theorems

I have recently been reading up on some of the ideas and history of the ground-breaking work done by various logicians and mathematicians regarding computability. While the individual concepts are ...
23
votes
4answers
2k views

Why do we need formal semantics for predicate logic?

Consider this question solved. I will not pick a best answer as all of them have contributed to my understanding of the topic. Im unsure what benefit we have by formally defining the semantics of ...
37
votes
5answers
1k views

Results in Theoretical CS independent of ZFC

I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish. QUESTION: Are you aware of any interesting result in CS ...
29
votes
4answers
3k views

What are the differences between logical relations and simulations?

I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused ...
29
votes
3answers
2k views

Curry-Howard and programs from non-constructive proofs

This is a follow up question to What is the difference between proofs and programs (or between propositions and types)? What program would correspond to a non-constructive (classical) proof of the ...
33
votes
3answers
4k views

Extended Church-Turing Thesis

One of the most discussed questions on the site has been What it Would Mean to Disprove the Church-Turing Thesis. This is partly because Dershowitz and Gurevich published a proof of the Church-Turing ...
33
votes
4answers
854 views

Correspondence between complexity classes and logic

I took a class once on Computability and Logic. The material included a correlation between complexity / computability classes (R, RE, co-RE, P, NP, Logspace, ...) and Logics (Predicate calculus, ...
24
votes
6answers
2k views

How should I think about proof nets?

In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of ...
18
votes
4answers
3k 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 ...
26
votes
1answer
516 views

Interesting algorithms in the formalization of the Feit-Thompson theorem?

It looks like George Gonthier and his collaborators have finished formalizing the Odd Order Theorem. In his earlier work on the Four Color Theorem, Gonthier invented a bunch of new algorithms (...
25
votes
1answer
1k views

Are types propositions? (What are types exactly?)

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
28
votes
1answer
821 views

Is there a reasonable automated proof system for TCS theorems?

Suppose I wanted to formalize Turing's proof regarding the halting problem so that a machine could check it. Some of the well-known automated theorem proving systems include Mizar, Coq, and HOL4. I ...
17
votes
2answers
945 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 ...
9
votes
2answers
915 views

How can we express “$P=PSPACE$” as a first-order formula? [closed]

How can we express "$P=PSPACE$" as a first-order formula? Which level of the arithmetic hierarchy contains this formula (and what is the currently known minimum level of the hierarchy that contains it)...
17
votes
1answer
632 views

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

Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. -...
15
votes
2answers
2k views

Is propositional resolution a complete proof system?

This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution". This question is something extremely basic but it has been bothering me ...
14
votes
1answer
263 views

Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
15
votes
1answer
324 views

How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, ...
12
votes
3answers
236 views

Is there a natural restriction of VO logic which captures P or NP?

The paper Lauri Hella and José María Turull-Torres, Computing queries with higher-order logics, TCS 355 197–214, 2006. doi: 10.1016/j.tcs.2006.01.009 proposes logic VO, variable-order logic. This ...
18
votes
0answers
1k views

What's the expressive power of Simply Typed Lambda calculus?

The standard approach to simply typed lambda calculus considers computations over Church numerals. If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) ...
14
votes
1answer
437 views

Comparing the Kolmogorov complexity of theories

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(s) > L$ where $K(s)$ is the Kolmogorov complexity of string $s$ and $L$ is a sufficiently large ...
13
votes
1answer
346 views

Good reference about approximate methods for solving logic problems

It is known that many logic problems (e.g. satisfiability problems of several modal logics) are not decidable. There are also many undecidable problems in algorithm theory, e.g. in combinatorial ...
7
votes
2answers
1k views

Automated theorem proving via unsupervised approaches

This question Where and how did computers help prove a theorem? considers some automated theorem proving successes. However they seem to be mostly supervised approaches, such as with the 4 color graph ...
21
votes
1answer
1k 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 ...
17
votes
3answers
600 views

What is the minimal extension of FO that captures the class of regular languages?

Context: relations between logic and automata Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that ...