Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
10
votes
2answers
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) ...
20
votes
3answers
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 ...
14
votes
2answers
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, ...
12
votes
2answers
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 ...
7
votes
2answers
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.
11
votes
1answer
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 ...
12
votes
1answer
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 ...
10
votes
1answer
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 ...
17
votes
2answers
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 ...
6
votes
1answer
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 ...
18
votes
1answer
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 ...
12
votes
1answer
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 ...
12
votes
3answers
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 ...
8
votes
2answers
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 ...
11
votes
1answer
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 ...
26
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 ...
5
votes
2answers
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 ...
14
votes
1answer
294 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 ...

1
6 7 8 9
10