Questions tagged [lo.logic]
Computational and mathematical logic.
498
questions
0
votes
0answers
31 views
Satisfiability and a Galois Theory Analog
Let $v(a, b)$ be a binary predicate, and define $\phi$ as follows:
$$\phi: v(a_1, b_1) \land v(a_1, b_2) \land (a_1, b_3)$$
where our universe consists of two sorts $A: \{a_1, a_2, a_3\}$ and $B: \{...
1
vote
1answer
78 views
Defining functions on non-inductive types using LEM in Coq
I'm trying to prove statements about homomorphisms in Coq. Specifically, about in which cases the existence of some set of homomorphisms implies the existence of a specific other homomorphism. I'm ...
8
votes
3answers
516 views
What's the logical counterpart to jumps with arguments on CPS terms?
It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
9
votes
1answer
113 views
Validity problem of intuitionistic two-variable logic
The two-variable fragment $\mathrm{FO}^2$ consist of those sentences of first-order logic $\mathrm{FO}$ in which precisely two variables occur (e.g. $\exists x \exists y \exists z R(x,y,z)$ is not a ...
2
votes
0answers
84 views
Recovering the inputs to Boolean circuits after partial evaluation
This question discusses Boolean Circuits and Boolean functions from $n>1$ inputs to one Boolean output. Notation: $\textit{arity}(\mathcal{C})=n$ if $\mathcal{C}$ takes $n$ inputs, similarly for ...
-1
votes
1answer
66 views
Is there a fundamental link between Nash's equilibrium and Turing's halting problem?
Since Nash equilibrium exists, is there a computational analogue of this equilibrium point? I am trying to approach Nash equilibrium from computational point of view to see if the equilibrium point ...
1
vote
0answers
92 views
Where does "Quine's Method" in propositional logic originate?
Hein (407-408) states that Quine's method "...uses these (14) properties together with basic equivalences to determine whether a wff is a tautology, a contradiction, or a contingency." The ...
3
votes
0answers
55 views
Is relativization statement-dependent or proof-dependent?
I'm relearning some computability theory, and have encountered the idea of relativization of results to arbitrary subsets of $\omega$ and the subtlety of figuring out what the correct relativized ...
8
votes
0answers
158 views
Constructive Strong Normalization of the Extended Calculus of Constructions
The extended calculus of constructions (ECC) is basically the calculus of constructions with cumulative universes. I use the definition which Zhaohui Luo used in his PhD theses which contained a proof ...
2
votes
1answer
170 views
Alternatives to Normalization by Evaluation
Reading about lambda calculus I got the impression that normalization is evaluation.
So I don't understand what is meant by Normalization by Evaluation (used e.g. in several publications of A. Abel).
...
-2
votes
1answer
64 views
Linear Integer Arithmetic Satisfiability with Three Literals [closed]
I'm stuck on trying to find an unsatisfiable conjunction of the form $a \wedge b \wedge c$ where:
$a \wedge b$ is satisfiable
$a \wedge c$ is satisfiable
$b \wedge c$ is satisfiable
$a, b, c$ are ...
3
votes
0answers
87 views
Boltzmann sampling for containers/dependent polynomials?
I’d like to randomly sample from dependently-typed data structures.
Has anyone looked at extending Boltzmann sampling to containers or dependent polynomials?
3
votes
1answer
265 views
Proof and computational complexity
I couldn't find documents elaborating on this: if the Curry Howard correspondence is to be interpreted as establishing a strong relation between proofs and programs, should there not be a strong ...
2
votes
1answer
100 views
How long does it take at most for $k$ boolean variables to map back to themselves with a positive disjunctive update rule?
I have a vector of boolean variables $v=(x_1,\dots,x_k)$. In each step each variable is updated according to a positive disjunction like so:
$x_1 \leftarrow x_i \vee \dots \vee x_j$
$\dots$
$x_k \...
3
votes
2answers
138 views
Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals [closed]
Looking for some lecture videos (introductory level) on logic, models of computation as well as computational complexity/ other theoretical computer science fundamentals
1
vote
1answer
66 views
Variable wire weights in DLOGTIME-uniform circuits
The definition of a $DLOGTIME$-uniform circuit family is based on a Turing machine that accepts the language $\langle t, a, b \rangle$, where gate $a$ is of type $t$ and has gate $b$ as a child, ...
1
vote
0answers
71 views
Complexity class name for the class of languages that are $\Sigma^1_1$-definable over finite domains
Let ${\cal L}=\{Y_1,..., Y_k, X\}$ be a finite relational language such that $X$ is a unary relation name. Let $\phi(X,\bar{Y})\in{\cal L}$ be a first-order formula (the formula can have the equality ...
21
votes
2answers
1k views
Decidability of diophantine equations over {=, +, gcd}
It is well-known that polynomial diophantine equations are undecidable (Hilbert's 10th problem): that is, given a quantifier-free formula over the language $\{=, +, \cdot, 1\}$ (of equality, addition, ...
9
votes
1answer
116 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
114 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
107 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
69 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
163 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
166 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
104 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
293 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
163 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.
2
votes
1answer
153 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
131 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
141 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
226 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
227 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
82 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 ...
4
votes
0answers
100 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) ...
4
votes
1answer
163 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
68 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 ...
11
votes
1answer
372 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
213 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
129 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
108 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
209 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
324 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
92 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
210 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
97 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
301 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
487 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 ...
7
votes
2answers
520 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
47 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 ...
4
votes
1answer
174 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 ...
