# Questions tagged [lo.logic]

Computational and mathematical logic.

468 questions
Filter by
Sorted by
Tagged with
378 views

### Are there semi-decision procedures for this theory?

I have the following typed theory |- 1_X : X -> X f : A -> B, g : B -> C |- compose(g,f) : A -> C F, f : A -> B |- apply(F,f) : F(A) -> F(B) ...
515 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 ...
288 views

### Cut-elimination for calculus with nats or other inductive datatype?

Does anyone direct me to a paper detailing a cut-elimination theorem for propositional intuitionistic logic, including an inductive datatype such as the natural numbers (lists or trees would be fine, ...
476 views

### What happens if we try to extract a witness but it actually does not exist from a term of existential type?

Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where ...
771 views

### An example of a totally computable function that is not definable in system T?

Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.
698 views

### NP vs co-NP and second-order logic

Assume that NP=co-NP and polynomial $p(x)$ bounds the length of the proof of unsatisfiability for a 3-CNF instance $x$. Then are there any results on what form any proof of unsatisfiability for $x$ of ...
390 views

### Can relativization results be used to prove sentences formally independent?

Is it possible to demonstrate that a sentence must be formally independent based on the fact that it is non-relativizing? In other words, are there examples of sentences in computability/complexity ...
369 views

### Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?

Harvey Friedman showed that there is a neat fixed point result that cannot be proved in ZFC (the usual Zermelo-Frankel set theory with the Axiom of Choice). Many modern logics are built on fixed ...
2k 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 ...
153 views

### Non-interesting numbers via resource-bounded properties?

There is an old joke about the smallest non-interesting number being interesting in itself (I have heard it attributed to Richard Hamming). This is then used to justify the argument that every number ...
661 views

### Techniques for showing non-derivability in logics and other formal proof systems

In proof systems for classical propositional logic if one want to show that a certain formula $\psi$ is not derivable one simply shows that $\neg\psi$ can be derived (although other techniques ...
315 views

### Finding the penumbra of a Constraint Satisfaction Problem

The following question has come up a number of times when testing the security of a system or model. Motivation: Software security flaws often come not from bugs due to valid inputs, but bugs ...
262 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 ...
385 views

### Game semantics for coinductive predicates

Does anyone know of any work on game semantics for coinductive predicates? A coinductive predicate is one where the predicate itself is called in the body of the predicate, and we are taking the ...
563 views

### Ehrenfeucht-Fraïssé games (Ajtai-Fagin in fact) for regular languages.

Immerman (Descriptive Complexity, 1999) presents the EF games for existential monadic second order (Ajtai-Fagin games) on page 127. As $\exists$MSO on words is equivalent to regular languages, the ...
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 ...
916 views

### Handbook of Logic in Computer Science - is it worth it?

I just found the first volume of Handbook of Logic in Computer Science in a library, but unfortunately I won't be able to use it here. It seems like a great resource, but it's insanely expensive to ...