# Questions tagged [lo.logic]

Computational and mathematical logic.

548 questions
Filter by
Sorted by
Tagged with
1 vote
24 views

### Why is order/choice an issue for a logic for PTIME

As I'm reading on the question of a logic for PTIME and in particular about CPT and its variants, whilst things make sense and I follow along, I came to realise that I don't fundamentally understand ...
56 views

### Is there a generalized SAT problem for many-valued logics?

Is there a generalized SAT problem for many-valued logics? related: "Is there a generalized SAT problem for higher-order logics?"
• 105
91 views

### Is there a generalized SAT problem for higher-order logics?

The SAT problem is based upon Boolean expressions, but is there a generalized SAT problem based upon higher order logics?
• 105
335 views

### In logic programming, what would a language with second-order model theory gain?

HiLog is described as a logic programming language with higher-order syntax, but first-order model theory. For example, it allows you to define a map over lists: ...
• 259
1 vote
64 views

### Why is the model-checking problem for MSO $\textsf{PSPACE}$-complete?

I am currently reading "Parameterized Complexity Theory" by J. Flum and M. Grohe. In Chapter 10.3 they state in the first paragraph: Let us remind the reader that the model-checking problem ...
• 181
94 views

### Original formulation of Spira's Lemma

I'm currently reading the book "Proof Complexity" by Jan Krajíček (2019), where Spira's Lemma is mentioned: Let $T$ be a finite $k$-ary tree and $|T| > 1$. Then there is a node $a \in T$ ...
• 181
94 views

### On the polynomial-size Frege proof of the propositional pigeonhole principle

I'm reading a lecture note on the proof of PHP, which mentioned that a "basic fact" $$\left(\sum\limits_{i=1}^{s-1} A_i\ge a\right) \land A_s \to \sum\limits_{i=1}^s A_i\ge a$$ is ...
• 187
1 vote
321 views

### Sparsification and critical clauses in SAT

I have been studying the Exponential-Time Hypothesis, ETH, from this paper, there defined $s_k = \inf\{\delta \geq 0 | k\text{-}SAT \in RTIME[2^{\delta n}]\}$. But in that paper's page number 10, I ...
• 109
47 views

1 vote
62 views

### Primitive recursion relative to a logical system

In various places I have read that the normally considered non-primitive recursive Ackermann function is primitive recursive in higher-order logic. It's claimed to be due to "Reynolds, 1985",...
• 920
47 views

### Using Simplex for Difference Logic

I'm interested in what happens when using the Simplex algorithm on Difference logic, inspired by problem 5.4 in Kroening and Strichman's Decision Procedures. Clearly, in this case, all constraints of ...
• 161
1 vote
122 views

### Do realizable systems always have some non-well-founded sets?

Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following: LEM is not realized (e.g. this MSE answer) The traditional ...
• 271
100 views

### Are MSO formulae on graphs expressible with bounded quantifier alternation?

Is there some $k$ such that, given any formula $\varphi$ in the monadic second order theory of graphs (this question applies for either MSO with sets of vertices and edges or just MSO with sets of ...
• 429
255 views

### Are MSO formulae expressible as existential SO formulae over arbitrary structures?

Given an MSO formulae φ, which may contain arbitrary quantifier alternation, is there always an ESO formula ψ, such that φ and ψ have the same (finite) models? (This statement holds when the models we ...
102 views

### Probabilistic Logic Programming vs Stochastic Logic Programming

I'm reading the paper DeepStochLog: Neural Stochastic Logic Programming. The authors differentiate between Probabilistic Logic Programming (PLP) and Stochastic Logic Programming (SLP), but I can't ...
• 3
1 vote
43 views

### What are the applications of Belief Revision?

In my Computer Science graduation, I came across this concept of Belief Revision, which focus on knowledge representation and the possible operations that can be done with the facts that a "...
• 111
1 vote
62 views

### Automatizability of Extended Resolution

According to Krajícek, Jan and Pavel Pudlák. “Some Consequences of Cryptographical Conjectures for S12 and EF.” Inf. Comput. 140 (1998): 82-94., the extended Frege proof system is not automatizable ...
• 187
2k views

### Where is the model theory in programming language theory?

I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
• 823
1 vote
163 views

### Which are the rules for minimal logic in both sequent calculus and natural deduction styles?

Are there any references I could use which explictly contain the rules for minimal logic, both as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!) To give ...
• 377
116 views

### Logical Equivalents of Finite State Transducers

There's a notion of "regular" function on words in automata theory that corresponds nicely to functions in WS1S/Büchi Arithmetic/the logic of words with a prefix and equal-length relation. ...
• 429
75 views

### What's the difference between "modular" and "compositional"?

When talking about reducing complexity in a software system, we often talk about making it "modular" by breaking it up into multiple modules that are all linked together to form the overall ...
1 vote
75 views

### Do soundness and completeness need to be exact converses of eachother?

This question concerns the derivational soundness and completeness of the first-order proof system LK (without equality) as presented in Logical Foundations of Proof Complexity by Cook and Nguyen. In ...
• 201
1 vote
78 views

### Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?

The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained I've ...
• 201
1 vote
92 views

### Intuition behind UTT's internal logic

The "internal logic" of type theory UTT is defined in LF as follows: What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
• 125
1 vote
139 views

### Formulation of Tarski-style universes in LF

Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well. I'm looking at this note ...
• 125
45 views

### Can you compute Shannon expansion of a Boolean formula more efficiently by using a QBF solver?

Maybe this is not enough research level, but I've been scratching my head on it for a while... I'm interested in the Shannon expansion of an existentially quantified Boolean formula of the form:  \...
• 1,588
5k views

### Theoretical Computer Science vs other Sciences?

So I‘m in my fifth semester studying Computer Science at a German university, so I‘ve only scratched the surface of Theoretical Computer Science, namely Logic, Formal Languages, Automata Theory, ...
• 147
1 vote
274 views

### Turing Machines and Logic

It is well known that Monadic Second Order Logic (over words) and finite automata can express the same set of languages. Is there a logic over words (perhaps a nth order logic) such that it and turing ...
• 125
206 views

### Shortest path property and monadic second order logic

I know that induced paths and Hamiltonian cycles can be expressed with monadic second-order logic ($MS_2$). Is it possible to express the shortest path in $MS_2$?
• 45
71 views

### Resources for first-order and second-order monadic logics with a model-checking objective

What are some good books and surveys for learning about first-order logic and monadic second-order logic? I'm a graduate student in computer science with a focus on algorithms. For model-checking on ...
• 45
239 views

### Stronger "induction" principles than induction-recursion

Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-...
287 views

### Concrete family of propositional formulas

Let $k,n \in \mathbb{N}$, where $k$ can be thought of as being fixed constant. For each $1 \leq \ell \leq k$ and $1 \leq i \leq n$ we have a proposition symbol $p_{(\ell,i)}$ (so in total we have $nk$-...
38 views

### Making primary keys explicit in a Boolean relation

Suppose we have a Boolean formula $\phi(X,Y)$ over the sets of Boolean variables $X$ and $Y$, representing a binary relation. There are in general many tuples in this relation. Is there a way to ...
• 1,588
77 views

### Lower bound on the size of Skolem functions

Consider a quantified Boolean formula $f$. We can convert it into Skolem Normal Form formula $f^*$ such that $f$ is satisfiable iff $f^*$ is satisfiable, by replacing variables that are existentially ...
215 views

### Can you define recursive predicates in 2nd order intuitionistic logic?

This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here. Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) ...
• 13.9k
197 views

### How far is the distance between Mahlo Universe and Mahlo Cardinal?

There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge. More explicitly, I would ...
• 161
1 vote
175 views

### Complexity of "discrete-time" SAT

I'm interested in the complexity of deciding satisfiability of the following family of formulae: $\exists j. I[j(0)] \land \forall t. S[j(t),j(t+1)]$ where: $j:\mathbb{N} \to \{0,1\}^n$ has finite ...
• 1,017
1 vote
90 views

### On completeness of LTL

I am reading the seminal paper "On the temporal analysis of fairness" by Gabbay, Pnueli, Shelah, Stavi, available at shelah.logic.at/papers/134/ In Section 3, completeness of a set of axioms ...
• 11
117 views

### Gurevich's theorem on primitive recursive functions being logspace-computable

I recently came across the following result attributed to Gurevich, according to which I understood that the class of problems solvable by primitive recursive functions is precisely the class L of ...
• 988
1 vote
155 views

### What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?

The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
• 81