Questions tagged [lo.logic]

Computational and mathematical logic.

547 questions
Filter by
Sorted by
Tagged with
303 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: ...
859 views

How do continuations represent negations (under the Curry–Howard correspondence)?

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
55 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?"
90 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?
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 ...
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$ ...
1k views

How to think about coherent spaces intuitively?

Linear Logic is interpreted using coherent spaces, and they feature prominently in Girard's papers. I know all the three main ways to formally define them, and they don't really pose any problem to ...
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 ...
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 ...
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",...
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 ...
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 ...
363 views

Is there a language of first-order logic such that every r.e. set is Turing-equivalent to some finitely axiomatizable theory in that language?

I hope that mathematical logic / recursion theory type questions are welcome here. I am sorry this question is so long and technical, but I believe that if you read it you will find that it is well-...
461 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, ...
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 ...
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 ...
101 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 ...
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 "...
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 ...
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 ...
608 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
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 ...
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. ...
73 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 ...
1k views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
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 ...
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 ...
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, ...
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 - ...
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 ...
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 ...
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:  \...
205 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$?
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 ...
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 ...
237 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-...
875 views

Functional Completeness of 3-valued logic

In the context of some recent work, we have been defining a language based on a three-valued logic à la Kleene, where $1$ stands for true, $0$ for false, and $\bot$ for error or don't-know. In order ...
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$-...
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) ...