Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [lo.logic]

Computational and mathematical logic.

20
votes
0answers
489 views

Model-checking for three-variable logics and restricted structures

Denote the $k$-variable fragment of logic $L$ by $L^{(k)}$. The model-checking problem for a logic $L$ with respect to a class of structures $C$, denoted $MC(L,C)$, is the decision problem $MC(L,C)...
18
votes
0answers
368 views

Courcelle's theorem for bounded clique-width graphs

Courcelle's theorem states that "Every graph property which is expressible in monadic second order logic is decidable in linear time for bounded tree-width graphs". Later it was extended to bounded ...
18
votes
0answers
1k views

What's the expressive power of Simply Typed Lambda calculus?

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) ...
18
votes
0answers
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 ...
17
votes
0answers
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 ...
14
votes
0answers
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 ...
12
votes
0answers
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$...
12
votes
0answers
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 ...
11
votes
0answers
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 ...
10
votes
0answers
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 ...
9
votes
0answers
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 ...
8
votes
0answers
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 ...
7
votes
0answers
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 ...
6
votes
0answers
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$, ...
6
votes
0answers
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 ...
6
votes
0answers
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 (...
6
votes
0answers
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,...
6
votes
0answers
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 ...
6
votes
0answers
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 ...
5
votes
0answers
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 ...
5
votes
0answers
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 ...
5
votes
0answers
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 ...
5
votes
0answers
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 "...
5
votes
0answers
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 ...
4
votes
0answers
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 ...
4
votes
0answers
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 ...
4
votes
0answers
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 ...
4
votes
0answers
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 ...
3
votes
0answers
104 views

Busy Beaver Equivalent for the Untyped Lambda Calculus

In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus: Over all terms in the ULC composed of ...
3
votes
0answers
108 views

Decomposition of rectangular relations

Let $\alpha$ be a binary relation from $\gamma$ to $\chi$ and $\beta$ a binary relation from $\chi$ to $\rho$. If both $\alpha$ and $\beta$ are rectangular, i.e., they satisfy $\alpha \alpha^{-1} \...
3
votes
0answers
134 views

Formalization of proofs and CC paradox? - Part II

This was the second part of my previous question. It is very similar, and probably it has a similar answer (as Emil said in a comment), but I thought it was worth to separate it and ask it as a new ...
3
votes
0answers
84 views

Looking for a specific tree automata model

is there any tree automata model over unranked trees (that is with unbounded number of children for each node), such that: Checking non-emptiness and universality is decidable in elementary time, ...
3
votes
0answers
122 views

Family of formulas for which Gabbay's separation algorithm explodes nonelementarily

It is repeated throughout the literature that Gabbay's algorithm for separation of LTL with Since and Until can produce nonelementary blow-up of the size of the formula, but I have never seen a proof ...
3
votes
0answers
56 views

Decidability of the monadic second-order theory of a class of finite structures

Let $L$ be the set of sentences in some logic. I am interested in cases where $L$ is the set of sentences in monadic second-order logic, or it is its $\Pi^1_1$ fragment. Let $K$ be a class of finite ...
3
votes
0answers
109 views

Applications of the monoidal closed structure in LTL?

A simple model of temporal logic is via time-indexed truth functions. This lets us model the Boolean connectives, as well as the next-step operator and modal always operator: $$ \begin{array}{lclll} ...
3
votes
0answers
93 views

How to develop an effective notation for a partially ordered logic?

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes: In intuitionistic ...
3
votes
0answers
105 views

When can an inner existential quantifier be eliminated in favour of a function relating terms?

I have a question which somehow relates to the great answer by Bauer in the question Techniques for Reversing the Order of Quantifiers, where he discusses how the possibility of quantifier reversing ...
3
votes
0answers
116 views

Expansion normal forms of confluent term rewriting systems

Suppose one has two rewrite rules $\to^\eta,\to^\beta$, both of which are confluent and such that $\to^A := \to^{(\eta \cup \beta)}$ is also confluent. Define a $\beta$-normal form relative to $\eta$ ...
2
votes
0answers
39 views

Is there a complete and finite axiom scheme for conditional independence? (Graphoids)

Note: This is a better-written version of an unanswered question asked before on MathOverflow. Question: Is there a complete and finite axiom scheme for conditional probability? If so, is ...
2
votes
0answers
136 views

Connection between nonmonotonic logic and type theory (lambda calculus)

There is known connection between classical and modal logics and type theory (lambda calculus), but are there connections between nonmonotonic logics (e.g. defeasible logic) and type theory (lambda ...
2
votes
0answers
39 views

Abduction in a Herbrand Constraint System

I have a simple constraint system with a finite set $C$ of constant symbols, an infinite set $V$ of variables, and two relation symbols - $R_1$, a preorder, and $R_2$, an equivalence relation. ...
2
votes
0answers
59 views

applications of institution-independent model theory

To quote wikipedia, The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970s in order to deal with the "population explosion among the logical systems used in ...
2
votes
0answers
349 views

Theorem prover fails to find simple set theory proof?

I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic. Tarski claims in his "a work on mereology" that the goal is provable from assertions 1-3 but he does ...
2
votes
0answers
268 views

Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
2
votes
0answers
93 views

Satisfaction and synthesis of models in logics

It is well known that for propositional logic, the problem of constructing a model of a given formula is equivalent to deciding whether the formula has a model. Satisfiability is NP-complete, and ...
2
votes
0answers
331 views

Encoding a logic in Coq

I want to encode a logic into Coq. The semantics of the logic are very complex and I just want to encode the syntax, axioms, inference rules. I use deep embedding, but I can't use notation like: <...
2
votes
0answers
134 views

Expressive power of (versions of) weighted average

Consider the arithmetic expressions obtained by allowing the constants 0 and 1, boolean variables, and allowing the operations $\min\{s,t\},\max\{s,t\}$, and $1-t$ where $s,t$ are expressions. Clearly ...
1
vote
0answers
152 views

Is it possible to type Ackermann function with (stratified variant of) System F?

I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding: <...
1
vote
0answers
54 views

To what extent supervised learning ERM learn first-order knowledge

Suppose I have a collection of (hidden) first-order rules: $$ \mathcal{R}: \{ Q_i(x) => P_i(x) \}_{i=1}^{k} $$ all defined over $x \in \mathcal{X}$. I can use these rules and (automatically) ...
1
vote
0answers
57 views

On collapsing the Exponential time hierarchy

Define $\Sigma^E_0 = \Pi^E_0=E$, for every $n>0$, define $\Sigma^E_n=NE^{\Sigma^p_{n-1}}$, for every $n>0$, define $\Pi^E_n=CoNE^{\Sigma^p_{n-1}}$. Define the Exponential time hierarchy by $EH=\...