Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
3
votes
1answer
134 views

Can we verify satisfiability of first order statements via saturation in sub-exponential time?

In first order logic, we can prove satisfiability several ways: Finite model generation, truthful monadic abstractions, and also saturation. With finite model generation techniques, we can verify the ...
1
vote
2answers
114 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
109 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 ...
41
votes
4answers
4k views

How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
18
votes
4answers
3k views

What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...
5
votes
1answer
134 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 ...
11
votes
2answers
172 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} $ ...
3
votes
2answers
220 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
73 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
503 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 ...
3
votes
0answers
140 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
62 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 ...
2
votes
1answer
377 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: ...
6
votes
0answers
154 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 ...
4
votes
0answers
77 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 ...
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
97 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
138 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
732 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
792 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
112 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
266 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
343 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 ...
5
votes
3answers
877 views

Law of excluded middle in MLTT

Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it ...
11
votes
0answers
203 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
154 views

Intuitionistic fragments of classical logic

For what conditions on P and Q, does P ⊢ Q in classical logic imply ...
8
votes
1answer
131 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 ...
6
votes
3answers
1k views

What is First-Order Rewritable (and FO-Query)?

I just wonder what FO Rewritable is, put an example to make it clearer for me. Also, I heard that a language that is FO Rewritable is very good, in what sense? It is said as follow: A class C of ...
2
votes
0answers
113 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} ...
9
votes
5answers
963 views

Writing universal recursive function [closed]

Is there a short explicit construction of an universal recursive function? All definitions I have seen involve numbering of Turing machines in some way, which is possible yet seems hard and ...
10
votes
1answer
207 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
199 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
90 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
196 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
114 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 ...
6
votes
0answers
128 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,...
18
votes
0answers
404 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 ...
2
votes
0answers
156 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 ...
3
votes
0answers
129 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 ...
13
votes
2answers
765 views

Can you explain an intuition behind Coherent Spaces?

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 ...
6
votes
1answer
270 views

Forms of types in the calculus of constructions

In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result: every closed term ...
3
votes
2answers
142 views

Boundary between decidability and undecidability for small theories

There is a lot of research on the boundary between decidability and undecidability of the halting problem for small models of computation: Turing machines, tag systems, CAs, ... This boundary is ...
10
votes
1answer
282 views

Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete? I believe the answer is ...
2
votes
1answer
236 views

Damas-Milner-like subset of the calculus of constructions with global type inference

Damas-Milner is a subset of System Fω that gives up expressivity (type-level computation) for usability (type inference). The experience with Haskell and ML attests to the practical value of this ...
11
votes
4answers
494 views

Finding a finite model

I know that the question "does a first order formula $\phi$ have a model" is undecidable in general. Could anyone give me a link or a book which give the answer for finite models. If I have a first ...
5
votes
3answers
425 views

Definition for MSO2 for arbitrary structures

I am not able to find a rigorous definition of MSO_2 logic for arbitrary structures (which I can cite). MSO_2 for graphs is often used and defined, i.e. in On the Parameterised Intractability of ...
1
vote
0answers
133 views

Consistency of MSOL over trees

I couldn't find any source speaking about the consistency of [Weak] Monadic Second Order Logic over Binary Trees (or over graphs with finite tree/clique width). I did find decidability results, and it ...
6
votes
0answers
270 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
1answer
337 views

Standard reference for basic model theory definitions

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...

1 2
3
4 5
10