# Questions tagged [lo.logic]

Computational and mathematical logic.

68 questions
489 views

456 views

### To what extent MSO = WS1S, when adding relations?

[This question has been asked on MathOverflow with no luck a month ago.] Let me first clarify my definitions. For a word $w \in \Sigma^*$, with $\Sigma =\{a_1, \ldots, a_n\}$, I define two ...
325 views

### Descriptive complexity of communication complexity classes

It is well known that some major complexity classes, like P or NP, admit a full logical characterization (e.g NP = existential 2nd order logic by Fagin's theorem). On the other hand, one can also ...
287 views

### Proof assistant formalizations of Finite Model Theory

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
159 views

### Is the theory of asymptotic bounds finitely axiomatizable?

Let $F$ be the set of functions over real numbers. Consider the structure $M = \langle F, <, \leq, =, \geq, > \rangle$ where the $<, \leq, =, \geq, >$ are defined as asymptotic notions $o$...
211 views

### Combinator logic and unification

Summary: if we are trying to use combinator logic to solve first-order logic type problems, is the best method to feed in free variables and use the standard first-order unification algorithm? In ...
171 views

### Categorical semantics for S5 modal logic?

Does anyone know where I can look to find out what the generally categorical semantics of S5 is? For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving ...
118 views

### Do Banach spaces and linear contraction maps form a model of ILL with an exponential?

Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed. This means that Banach spaces and short linear maps ...
77 views

### Results in denotational semantics from model theory?

Denotational semantics interpret the theories of various lambda calculi in various (set-theoretic, domain-theoretic, category-theoretic, game...) models. Let $T$ be the theory of one such lambda ...
41 views

### Relationship between lambda-definability, specification and definability in model theory

I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts: An element $a$ in the domain of a type $A_\sigma$ is ...
267 views

### MLTT vs. [weak] MSOL

I've noted that both Martin-Lof type theory and [Weak] Monadic Second-Order logic (eg over trees) enjoy the ability to express basically any finite computer program, in a decidable manner. I was ...
214 views

### Fischer and Rabin's theorem (1974) for theories of “additive” structures

Fischer and Rabin's Super-Exponential Complexity of Presburger Arithmetic (1974) has the following theorem. (Theorem 12) Let $U$ be any class of additive structures, so if $A = (A, +) \in U$, ...
125 views

### Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
84 views

### Salomaa's axiomatisation of regular languages and the use of regular expression in it

I am reading the classical article of A. Salomaa where he gives two axiom systems for regular sets and proofs consistency and completeness. As I have understood it, an axiomatic system in some logic (...
113 views

### Complexity of validity of first-order logic over finite words with bounded quantifier alternation?

I'm concerned with the validity problem for sentences of first-order logic over finite words, i.e. $FO[\le]$ interpreted over finite subsets of $\mathbb{N}$. AFAIK it should be nonelementary. However,...
139 views

### Comparing the Kolmogorov complexity of theories - Part 2

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(x) > L$ where $K(x)$ is the Kolmogorov complexity of natural number $x$ and $L$ is a sufficiently ...
423 views

### Generalized sequential machine synthesis subject to language equivalence/inclusion and reachability

A generalized sequential machine (GSM) is a generalization of a Mealy machine where on each transition one input symbol is read and 0 or more output symbols are written. As in a Mealy machine, we ...
111 views

### Transferring results on coalgebras in one category to another

Let $F$ and $G$ be endofunctors over categories $C$ and $D$, respectively. Suppose that there is a forgetful functor $C \to D$ that has a left adjoint. Can we infer properties of $F$-coalgebras ...
148 views

### The evaluation problem for AC$^0_d$ formulas is in FO

Let $d \in \mathbb{N}$ be arbitrary. Let $\mathsf{AC^0_d}$-Eval be the following promise problem: Input: A depth $d$ formula $\varphi(x)$ and a binary string $a$. Output: $\varphi(a)$ I am looking ...
140 views

### What is the Kolmogorov complexity of arithmetic?

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(n) > L$ where $K(n)$ is the Kolmogorov complexity of the number $n$ and $L$ is a sufficiently large ...
186 views

### Are there any logics to formalize understanding?

Are there any logics (modal-based or others) to formalize the following statement: "agent A understands p". For example "agent A understands that Titanic sank because it hit an iceberg" Where "...
189 views

### Logic capturing automorphism-invariant $\mathsf{AC^0}$ properties

Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like $\mathsf{AC^0}$ (or $\mathsf{TC^0}$)? Motivation As you ...
60 views

### Finite intersection property of polymorphic type families

Let $\Phi$ be a type functor definable in polymorphic lambda calculus: $$\alpha : * \vdash \Phi(\alpha) : *$$ $$f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$ Suppose further ...
126 views

### Efficiently computing the union of all minimal unsatisfiable constraint sets in a first-order unification problem

Suppose we are given a standard first-order unification problem, represented as a set $D$ of term equality constraints, such that the system $D$ as a whole is unsatisfiable. Consider the minimal ...
70 views

### Coherence spaces and full completeness for the implicative fragment of linear logic

Linear logic isn't complete for coherence space semantics since $1$ and $\top$ get identified. But it is, I believe, complete for the fragment of linear logic whose only connective is $\multimap$. I ...
126 views

### Evaluating boolean formula without knowing all values

I am looking for research approaches for the following problem: assume we have a set of $m$ computers, each carries a bit, and a Boolean formula $\varphi$ over those $m$ variables. The computers are ...