Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
-2
votes
0answers
35 views

The logic expressible in the Z notation: is it first-order logic?

Is the logic expressible in the Z notation (a) higher-order logic? (b) simple type theory, (c) a stylized version of first-order logic? If I'm going to use the Z notation (or some variation on it) in ...
7
votes
0answers
73 views

Proof of $DLOGTIME-CC^0 = MOD[<,bit]$

Let $CC^0[m]$ be the class of constant-depth, polynomial-sized circuits consisting entirely of $MOD_m$ gates, which put out $1$ iff the sum of their inputs $\equiv 0~(\textrm{mod}~m)$. In the same way ...
1
vote
0answers
99 views

$\mathit{FO}[+,\times]$ seems more powerful than $\mathit{DLOGTIME}$-uniform $\mathit{AC}^0$?

I’ve been reading up on the connection between first order logic and small circuit complexity classes, and specifically Barrington, Immerman, and Straubing’s paper “On Uniformity Within $\mathit{NC}^1$...
1
vote
0answers
100 views

Functional abbreviation for Inst expression in Turing's 1936 paper

In Turing's 1936 paper "On Computable Numbers", For a Turing Machine $M$, $Inst(q_i S_j S_k L q_l ) $ means that if $M$ scans symbol $S_j $ under $m-configuration$ $q_i$, then the symbol ...
0
votes
1answer
48 views

Is every countable, finite-branching LTS bisimilar to a tree?

Let $L$ be a finite set of labels, and let $\mathcal{C}$ be the set of finitely-branching transition systems labeled by $L$ and with a countable set of states. Let $\sim$ denote the bisimulation ...
2
votes
1answer
138 views

Is modal $\mu$-calculus “equivalent” to bisimulation?

I know that propositional modal $\mu$-calculus $L\mu$ is bisimulation-invariant. However, I'm curious to what degree it captures bisimulation. Q1: Given two labeled transition systems $T_1$, $T_2$ ...
4
votes
0answers
154 views

Alternative exponential definition of Kolmogorov complexity

In Kikuchi's paper Kolmogorov complexity and the second incompleteness theorem the Kolmogorov Complexity (KC) of $x$ is defined as $$ K(x) = \mu e (\varphi_e(0) \simeq x) \, , $$ the smallest $e$ such ...
1
vote
0answers
82 views

λProlog vs HiLog

λProlog is a well-known higher-order logic programming language. On the other hand, HiLog is described as a logic programming language with higher-order syntax, but first-order model theory. Do I ...
2
votes
2answers
249 views

Uncountability in intuitionistic logic

I've read snippets here and there that inside intuitionistic logic, uncountable can be a subset of the naturals ? What is the correct intuition to think about this? Andrej Bauer replied above, saying ...
2
votes
0answers
141 views

Order-invariant conjunctive queries are FO-definable without the order

I'm looking for a reference for Exercise 6.11 from Libkin's FMT book: Prove that an order-invariant conjunctive query is FO-definable without the order relation. All help is appreciated.
1
vote
1answer
122 views

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

As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $\mathrm{FO^2}$, In order to do this they use Scott's reduction. Which is the ...
5
votes
1answer
111 views

Does focused proof search ever have to backtrack across the choice of focus formula?

There are a lot of different "focused" sequent calculi for lots of different logics, but my understanding is that many or most of them have the following flavor. First one divides the ...
3
votes
1answer
122 views

Normal forms for counting quantifiers?

In the paper by [Erich Grädel and Martin Otto], the authors state that any formula in First Order Logic with two variables with counting quantifiers can be reduced to a formula of the form $$ \forall ...
5
votes
2answers
191 views

Categorical equivalent of higher order logic

From Simply typed lambda calculus and higher order logic, I get the impression that HOL is STLC + equality + equality axioms. I was wondering if there is a particular kind of category modelling this.
11
votes
1answer
174 views

Is there a language of first-order logic such that every r.e. set is Turing-equivalent to some finitely axiomatizable theory in that language?

I hope that mathematical logic / recursion theory type questions are welcome here. I am sorry this question is so long and technical, but I believe that if you read it you will find that it is well-...
3
votes
1answer
71 views

Why REFL rule is primitive in HOL Light?

HOL Light assumed REFL as a primitive. Why does it need to do so? Can't REFL rule be deduced in this way using ...
1
vote
0answers
79 views

Logic of learning

Does Robust logic (Leslie Valiant), Default logic (Raymond Reiter) and Circumscription logic (John McCarthy) have any relation? I was Mathematician and Computer Science (dual degree undergraduate) ...
3
votes
1answer
130 views

What is FO(REGULAR)? (The descriptive complexity equivalent of NC1)

According to Immerman's Descriptive Complexity diagram, there is a logic called $\mathsf{FO(REGULAR)}$ which captures $\mathsf{NC}^1$. However, I can't find the reference where this logic is defined. ...
2
votes
1answer
58 views

FO(TC) lower bounding games?

Is anyone aware of any games/algebraic structures that provide lower-bounding methodologies for $FO(TC)$ formulae? I am aware of EF games as they apply to first-order and second-order statements, but ...
9
votes
1answer
186 views

What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

Suppose I have two boolean formulae (propositions) $P_1$, and $P_2$ (can be assumed to be in CNF) over the same variables and such that there are no "NOT" symbols used. I.e. only conjunction and ...
1
vote
0answers
191 views

How do computers check if two functions are the same?

To prove that two given functions are the same involves proving infinitely many statements. I wonder how to implement so that a computer can check such a statement? An easy example is the following: ...
0
votes
0answers
111 views

Fagin's Theorem implications

I was going through Fagin's Theorem (summary on wiki) and if I understood correctly Existential Second Order Logic (ESO) can be used to represent any NP problem, the same can be said for a Non-...
2
votes
0answers
84 views

Cover set of Boolean formulas with conjunctions

I want to cover a set of Boolean formulas (over the same variables) with disjunctive conjunctions. Here's an example with two formulas $p_1$ and $p_2$ over the set of variables $\{A, B, X, Y\}$: I ...
10
votes
0answers
196 views

On Courcelle's question about Monadic second-order logic with cardinality predicates

I have found the following question at openproblemgarden.org: The problem concerns the extension of Monadic Second Order Logic (over a binary relation representing the edge relation) with the ...
11
votes
0answers
310 views

Is unary $\Pi_2$-SUBSETSUM coNP-complete?

Consider the following problem: for given integers $a_1, \ldots, a_{2n}$ and $A$ that are given in unary representation define is it true that for every $S \subseteq \{1, ..., 2n \}$ such that $|...
5
votes
0answers
80 views

Are there languages require many variables to achieve $\Sigma_n^0$ completeness?

The proof of Post's Theorem that I am familiar with assumes you have access to as many variables as you wish in your language. Matiyasevich's Theorem by contrast gives a $\Sigma_n^0$-complete formula ...
14
votes
0answers
196 views

Counting solutions to extended MSO formulas, and sampling — do these appear in the literature?

I am trying to determine if the literature contains various extensions of Courcelle's theorem. Since I haven't been able to find these in the literature, I guess that these are folklore results, or ...
2
votes
0answers
90 views

Forward chaining algorithms

I am interested in learning about the current state of the art regarding forward chaining production systems. I understand that things haven't changed much (regarding the basic algorithms) since 1995'...
6
votes
0answers
261 views

Reverse Skolemization?

I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications. I'm ...
0
votes
1answer
314 views

How to build comparison operator (comparator) in an arithmetic circuit

I am trying to convert a basic program into an arithmetic circuit. I am stuck on the step of converting the greater than operator into an arithmetic circuit. To be specific, I do not know how to ...
4
votes
2answers
325 views

How do continuations represent negations (under the Curry–Howard correspondence)?

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
3
votes
0answers
45 views

Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy

Let $\Sigma$ be some finite alphabet. Then consider the logical language $\mathcal L = \{ R_a : a \in \Sigma \} \cup \{ <,= \}$ and first order formulas. For a given first order formula $\varphi$ a ...
3
votes
1answer
157 views

Reductions in Descriptive Complexity

Reducing one problem to another are well known in various settings, such as many-one, randomized, truth-table, logspace or a whole slew of other reductions. Descriptive complexity can alternately ...
2
votes
0answers
103 views

Notion of “quotient” or “inverse” for recognizable tree languages?

Related to my previous question but this time I have a better idea of what I'm actually asking. I'm looking at the following operation on recognizable tree languages (i.e. regular tree grammars, ...
7
votes
2answers
759 views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
3
votes
2answers
174 views

Compactness of domino tilings

I've read in Lemma 2 of the paper 1 that if every square region of the plane admits a tiling, then the whole plain admits a tiling, but the proof is omitted. This sounds like a compactness property, ...
1
vote
1answer
126 views

Dependent C-style types with subtyping rule

I'm looking for previous work regarding an extension of a C-style type system in which types may have constraints and have a defined subtyping rule. In particular, I'm interested in defining algebra-...
9
votes
1answer
281 views

What is the reference for the proof Gödel's first incompleteness theorem based on the undecidability of the halting problem?

A weaker form of Gödel's First Incompleteness Theorem, direct proofs of which in Gödel's manner are lengthy, involved and at some place rather counter-intuitive, has a simple and intuitive proof based ...
10
votes
1answer
236 views

P and Descriptive Complexity

In the Complexity Zoo, it says [1] that, in descriptive complexity, $P$ can be defined by three different kind of formulae, $FO(LFP)$ which is also $FO(n^{O(1)})$, and also as $SO(HORN)$. However, ...
6
votes
2answers
261 views

Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

There are many closed terms of a given type. For instance, both of these terms: $$ \lambda x . x $$ $$ \lambda x . (\lambda y . y) x $$ have a type of a polymorphic identity function: $$ \forall X ....
7
votes
3answers
341 views

When a type is a value?

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
3
votes
1answer
248 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 ...
11
votes
2answers
366 views

Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
9
votes
0answers
116 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 ...
9
votes
1answer
250 views

Understanding the Proof of Strong Normalization of the Calculus of Constructions

I have difficulties in understanding the proof of strong normalization for the calculus of constructions. I try to follow the proof in the paper of Herman Geuvers "A short and flexible proof of Strong ...
1
vote
1answer
79 views

Soft Truth Values in the PSL model

This might sound like a trivial question. But since am starting out with my research in an area that is entirely new to me, I would really appreciate it if someone could kindly elucidate what Soft ...
10
votes
0answers
146 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 ...
3
votes
2answers
206 views

What does the category of RDF models look like in Institution Theory?

The Question in short Here is the question in its pure form. Details of my reasoning can be found below. The RDF1.1 spec semantics defines a model to consist of a set IR of objects and IP of ...
6
votes
3answers
234 views

Why/when do we ever need transfinite loop variants?

I do not understand why one would ever need a transfinite loop variant. Why do natural-number-valued variants not suffice? My simple (but perhaps too naive) argument is: if a loop $L$ terminates ...
8
votes
0answers
45 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 ...

1
2 3 4 5
10