11 votes
Accepted

Existing implementation of Scott's reduction?

You might check the FO2 solver by Tomer Kotek et. al (ICDT 2017): https://forsyte.at/alumni/kotek/fo2-solver/ as well as an FO2 solver by Tony Tan and his students (LICS 2021): https://arxiv.org/abs/...
Bartosz Bednarczyk's user avatar
9 votes
Accepted

For any two non-isomorphic graphs $G, H$, does there exist a polysize, polylog quantifier depth first order formula which witnesses this?

Thanks to my colleague Maxim Zhukovskii for suggesting this answer. It turns out that the answer is negative, and the counterexample is rather simple. Just take $G=K_m\sqcup \overline{K_m}$ and $H=K_{...
Daniil Musatov's user avatar
8 votes
Accepted

Validity problem of intuitionistic two-variable logic

The two-variable fragment of intuitionistic first-order logic is undecidable, as proved in Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev: Undecidability of First-Order Intuitionistic and ...
Emil Jeřábek's user avatar
7 votes
Accepted

Kleene Algebra for star-free regular expressions

You might be interested in bounded synchronization delay expressions. See [1] for details on these expressions. To sum up, they are equivalent to star-free expressions, but instead of using complement,...
Denis's user avatar
  • 8,678
6 votes

The theory of definitions in first order logic

I don't have the books handy at the moment, but I think Shoenfield's "Mathematical Logic" and Hinman's "Fundamentals of Mathemtical Logic" would contain much if not all of what you're looking for. ...
Andreas Blass's user avatar
6 votes

Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals

Ryan O'Donnell (professor at Carnegie Mellon) has a wonderful undergraduate complexity theory series that goes through the fundamentals quite well, and he's an engaging lecturer. He also has a similar ...
Jake's user avatar
  • 1,214
5 votes

Evaluating asymptotic probabilities of First Order Logic Formulas?

By slightly modifying Grandjean's algorithm (reference in Emil's answer), one can show that for any fixed $k\geq 1$ and for a fixed finite (relational) language $L$, the problem of determining the ...
Reijo Jaakkola's user avatar
5 votes
Accepted

Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?

Yes. Just employ the formula $\forall{x}\forall{y} \; R(x,y) \leftrightarrow (x=y)$ (for a fresh binary predicate $R$), which allows you to "hide" the equality inside the $\forall\forall$-...
Bartosz Bednarczyk's user avatar
4 votes
Accepted

Normal forms for counting quantifiers?

I believe that the formula with the quantifier prefix you want to achieve are strictly less expressive than the two-variable logic with counting quantifiers. So there is no hope that you can translate ...
Bartosz Bednarczyk's user avatar
4 votes

Can modern SAT-Solvers utilise the symmetry of First Order Logic?

There exist first order (FO) logic systems that allow you to actually write FO constraints, and to reason with them in very intricate ways. E.g., see the IDP system. For instance, I took a small ...
HolKann's user avatar
  • 141
4 votes

A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?

The two obvious references are: Chapter 7 of Term Rewriting and All That, notable for its pedagogy and accessible examples Chapter 7 of Term Rewriting Systems, notable for its completeness and ...
cody's user avatar
  • 13.8k
4 votes

A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$

I would recommend looking at higher-order logics (HOL), for instance Lambek and Scott's Introduction to Higher-Order Categorical Logic. Such a logic will set up binding of bound variables and treat ...
Andrej Bauer's user avatar
  • 28.7k
4 votes
Accepted

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

It depends what precisely do you want to learn. A good reference is the finite model theory book by Libkin. https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf (chapters 2 and 7). If you want more ...
Bartosz Bednarczyk's user avatar
4 votes

Evaluating asymptotic probabilities of First Order Logic Formulas?

I assume you are talking about purely relational sentences, as otherwise the 0–1 law does not hold. As should be explained somewhere in those notes, an FO sentence in a finite relational language $L$ ...
Emil Jeřábek's user avatar
3 votes
Accepted

Scott's normal form for $\exists y \forall x R(x,y) $

Your solution is correct. It suffices to see that the formulae $\exists{y} P(y)$ and $\forall{x} \exists{y} P(y)$ are equi-satisfiable, which allows you to put your formulae in the desired form.
Bartosz Bednarczyk's user avatar
3 votes

Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals

Prof. Tim Roughgarden (Stanford University) Lectures on algorithms and more are also great. He is one of the best lecturers out there... https://www.youtube.com/channel/UCcH4Ga14Y4ELFKrEYM1vXCg/...
Avi Tal's user avatar
  • 1,606
3 votes

Evaluating asymptotic probabilities of First Order Logic Formulas?

As stated, the problem can be reduced to the query evaluation problem over the Rado graph (or the corresponding structure for non-binary vocabularies). Hence, there is a huge chance that the problem ...
Bartosz Bednarczyk's user avatar
3 votes
Accepted

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

The answer occurred to me right after I finished typing up the post. Rather than delete it, I figured I would post it anyway in case anyone else has the same question. Answer The mistake in the ...
Johnny's user avatar
  • 201
3 votes
Accepted

State of the Art for the Monadic Class?

I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS. In particular see the thesis of Ann-Christin Knoll, On Resolution Decision Procedures for ...
cody's user avatar
  • 13.8k
3 votes

State of the Art for the Monadic Class?

In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are ...
Neel Krishnaswami's user avatar
2 votes
Accepted

Tableau method for two-variable first-order logic

Apparently a tableau for $FO^2$ has not been given explicitly but a tableau for the expressively equivalent description logic $ALBO^{id}$ has been given in: Renate Schmidt and Dmitry Tishkovsky, Using ...
Nicola Gigante's user avatar
2 votes

Tableau method for two-variable first-order logic

You might check the FO2 solver by Tomer Kotek: https://forsyte.at/alumni/kotek/fo2-solver/ This is the only existing FO2 solver (Tony Tan with his student have a paper under submission, in which they ...
Bartosz Bednarczyk's user avatar
2 votes

A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?

There is a rather technically-detailed description to be found in any of the following: D.F. Holt, D.B.A. Epstein, and S. Rees. The use of knuth-bendix methods to solve the word problem in automatic ...
NietzscheanAI's user avatar
2 votes

Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?

Reading the discussion below the other answer made me realize that it’s not immediately obvious what is the complexity of translation of FO sentences in this language to equivalent FO1 sentences. ...
Emil Jeřábek's user avatar
2 votes
Accepted

References on second-order quantifier elimination and related topics

Since there are no answer I think it may be useful to post what I've found: Dov M. Gabbay, Renate A. Schmidt, Andrzej Szalas Second-Order Quantifier Elimination - Foundations, Computational Aspects ...
Nicola Gigante's user avatar
2 votes

Second-order reachability in second-order logic

In fact, we can always stay in the second-order realm (as long as our "base structure" is infinite)! First, let's look at the particular case where our base structure is $\mathcal{N}=(\...
Noah Schweber's user avatar
1 vote
Accepted

Inexpressibility results for first-order logic that fail extending the language

As noted in the comments it takes some care to phrase this question in a nontrivial way. However, this can be done in at least a couple ways, one yielding a positive answer and the other yielding a ...
Noah Schweber's user avatar
1 vote
Accepted

Number of equivalent formulas in a function-free first order logic language?

One can prove in a quite straightforward manner an upper bound on the number of non-equivalent formulas with quantifier rank at most $q$ over a fixed finite relational vocabulary. I will sketch an ...
Reijo Jaakkola's user avatar
1 vote
Accepted

reducing this problem to a decision problem

Your problem is coNP-hard, by reduction from SAT. In particular, using inequalities $x \ge 1$, $x \le 0$ and interpreting $0$ as false and $1$ as true, we can encode any SAT formula $\varphi$ into ...
D.W.'s user avatar
  • 12k
1 vote
Accepted

Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?

Answering your second question, the logic you mean is known as Monadic FO or Monadic Predicate Calculus. It is known the logic is equivalent to FO1 (as Emil Jeřábek suggested) by some very old works ...
Bartosz Bednarczyk's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible