Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.

Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
5
votes
1answer
514 views

Sparsification Lemma for k-SAT and Exponential Time Hypothesis

According to R. Impagliazzo, R. Paturi and F. Zane, 2001 an instance of $k$-SAT is called sparse if $m = O(n)$ where $m$ denotes the number of clauses and $n$ the number of variables. The ...
3
votes
0answers
90 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, ...
2
votes
1answer
106 views

Is Eulerian Path (or Eulerian Cycle) definable in Monadic Second Order Logic?

Does there exist a monadic second order logic formula which is satisfied by a graph if and only if it has an Eulerian path (or Eulerian cycle). I am looking for properties of graphs which are ...
6
votes
0answers
219 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$, ...
2
votes
0answers
44 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 ...
3
votes
1answer
122 views

Connection between algebraic logic and computational complexity of logics?

I'm learning a bit about algebraic logic and I was wondering how knowing the algebraic semantics of a given logic might help the study of the logic itself from a computational point of view. In ...
8
votes
1answer
394 views

Complexity of modal logic IK5

What is the complexity of local satisfiability problem for modal logic $\mathit{IK5}$? Herein we denote by $IK5$ the modal logic over euclidean frames extended with inverse modality. Could you provide ...
3
votes
4answers
296 views

Philosophy behind monotonicity requirement for inductive types

Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions? According to my understanding of the Bishop/...
0
votes
1answer
49 views

Head variables of terms after application

We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\...
4
votes
2answers
450 views

Efficiently modeling Turing machines in Peano Arithmetic

The (undecidable) Peano Arithmetic (PA) is powerful enough to model Turing machines. Consider a standard first order axiomatization of Peano Arithmetic and a standard Hilbert-style proof system $\...
3
votes
0answers
125 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 ...
6
votes
1answer
162 views

Normal forms for intuitionistic formulas?

It is well-known that DNFs/CNFs and prenex normal forms generally do not exist for intuitionistic logic. Are there any nice results about formula normalization for IL? I've tried googling this but ...
1
vote
0answers
70 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=\...
11
votes
2answers
395 views

State of the Art for the Monadic Class?

Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete. ...
6
votes
1answer
222 views

Algebraic account of Gaussian elimination?

For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting question about the interpretation of double-negation-...
13
votes
1answer
197 views

Conclusions from reverse mathematical strength of graph minor theorem

Say we have a graph property which can be checked in nondeterministic polynomial time, and a proof in a weak formal system (say RCA0) that the property is minor closed. Can we say anything about the ...
1
vote
0answers
75 views

What logic(s) exist for attributing belief?

I'm looking for an appropriate formalism to represent "traceability" in claims, especially connecting conclusions to source materials in a rigorous way. For example, I'd like to be able to represent ...
3
votes
2answers
365 views

Automated proving that a program doesn't halt

If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)...
10
votes
1answer
218 views

Equilibrium in a Halting Game

Consider the following 2-player game: Nature randomly picks a program Each player plays a number in [0, infinity] inclusive in response to nature's move Take the minimum of the players’ numbers, and ...
1
vote
2answers
111 views

Determine if a structure is a model of an inductively defined predicate

My setting is first-order logic. As an example, consider an inductive definition of a linked list: $List(l)$ = $Null(l)$ $\vee~(Node(l) \wedge \exists sublist. List(sublist) \wedge next(l,...
1
vote
0answers
101 views

Definitions of strongest postconditions [closed]

The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer $X ~\mapsto \neg G \wedge ...
11
votes
2answers
149 views

Does the first order theory of a finite structure have bounded quantifier rank?

Let $\mathfrak{A} $ be any finite structure. Does its first order theory $ \mathfrak{T} := \mathfrak{TH}(\mathfrak{A}) $ have bounded quantifier rank, in the sense that there is a $ q\in\mathbb{N} $ ...
5
votes
1answer
119 views

Using ϵ -unification and Knuth-Bendix completion to automatically proof theorems about groups

This is a follow-up question. In my previous question, I presented Welder proof assistant and I stated that I want to automate proofs about basic field theory. The only answer to this post states that ...
3
votes
2answers
212 views

Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
1
vote
0answers
72 views

Question on Turings Dissertation *Systems of Logic based on Ordinals*, Axiomatic Properties [closed]

I have a question on Alan Turing's Dissertation Systems of Logic Based on Ordinals, a scanned copy you can find here, or rewritten in LaTeX here, and also a copy of the published version here (but in ...
11
votes
1answer
456 views

What is the intuition behind linear logic?

I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means $A$ is ...
4
votes
0answers
61 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 ...
3
votes
0answers
128 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 ...
6
votes
0answers
142 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 ...
2
votes
1answer
316 views

How to generate Skolem function in practice

Context: Skolemization is the process of removing the existential quantifiers in a first-order formula. The existential bounded variables are replaced with existential quantified function. Questions: ...
4
votes
0answers
72 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 ...
1
vote
2answers
58 views

Algorithms to synthesize optimal plans satisfying temporal logic constraints

I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online. I am ...
3
votes
2answers
133 views

Construct proof systems for common algorithmic task, like equivalence of regular expressions

A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto. For $y \in L$ ...
5
votes
0answers
88 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
1answer
132 views

How to mechanically derive the recursor of a type from its constructors?

In Martin-Löf Dependent Type Theory a type is commonly prescribed by how to construct its canonical terms and how to show that its canonical terms are definitionally equal. This means that the ...
17
votes
1answer
648 views

Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. -...
11
votes
1answer
706 views

Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

So I've been wondering if the Law of Excluded Middle (LEM) implies the so-called Axiom K in Martin-Löf's Intensional Type Theory. The Axiom K states that $$\Pi_{A : Type} \Pi_{x : A} \Pi_{p : \text{Id}...
4
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 ...
11
votes
1answer
241 views

Entscheidungsproblem vs. Unvollständigkeitssatz (soft question)

The first term is used by Hilbert in his 1928 work, but in Gödel's later work, the same thing is referred to as Unvollständigkeitssatz ("incompleteness theorem"). For today's German CS researchers, it ...
6
votes
2answers
340 views

Is there an algorithm which gets incrementally “smarter” as it runs?

Mind the following program: n = 0 best = 0 while (true): if (hash(n) > best): best = hash(n) ++n If you leave this program running for 10 years, when ...
11
votes
0answers
199 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 ...
7
votes
1answer
153 views

Intuitionistic fragments of classical logic

For what conditions on P and Q, does P ⊢ Q in classical logic imply ...
8
votes
1answer
124 views

About the origin of the names “immune” and “simple”

I have been wondering for a while about the origin of the names "immune" and "simple". I also posed the same question to Andrea Sorbi, who in turn involved a few more colleagues in the discussion. ...
2
votes
0answers
57 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 ...
2
votes
0answers
110 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} ...
10
votes
1answer
184 views

Typo in the calculus of constructions paper?

In the classic the calculus of constructions paper there is a rule that states (page 7 of the pdf, page 101 of the original document) This rule would mean that any context is reducible to a member ...
16
votes
0answers
197 views

What is the background in algebraic geometry and representation theory needed for geometric complexity theory? [duplicate]

I'm a mathematics student in my junior year and I'm interested in computational complexity and specially geometric complexity theory. I'm going to learn algebraic geometry and representation theory ...
1
vote
0answers
89 views

Is there a signature of a first-order language that characterize the class of regular languages?

A previous question on this site was about extending the first-order logic with logical constants (quantifiers, fixed-point operators, etc.) to obtain a logical characterization of the class of ...
3
votes
0answers
177 views

Formal definition of Turing Completeness [closed]

Wikipedia states: In computability theory, a system of data-manipulation rules […] is said to be Turing complete or computationally universal if it can be used to simulate any single-taped Turing ...
4
votes
1answer
106 views

Sequent calculus for nonmonotonic/defeasible logics?

Is it possible to construct sequent calculus for nonmonotonic/defeasible logic? If it is possible then those logics can be encoded in proof assistants which require sequent calculus for logic to be ...