Questions tagged [lo.logic]
Computational and mathematical logic.
539
questions
4
votes
1
answer
135
views
Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic
What is the precise connection between:
strong normalization of the simply typed $\lambda$-calculus, and
cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent ...
- 619
2
votes
0
answers
42
views
Variable opening in locally-nameless representation
Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's ...
- 121
10
votes
0
answers
203
views
Is there a text that discusses both the “lambda cube” of pure type theories and Martin-Löf's intuitionistic type theories, and compares them?
I am lost in a maze of twisty little type theories, all different.
There are a number of works (textbooks and papers) that discuss pure type theories, and specifically the ones constituting the ...
- 619
0
votes
0
answers
114
views
Counterexample in Sistla and Clarke's paper
I'm reading Sistla and Clarke's paper "The Complexity of Propositional Linear Temporal Logics". In section 4 they start with the following set up:
Let $S=(s, \xi), T=(t, \pi)$ be structures ...
- 921
2
votes
0
answers
149
views
Deciding Satisfiability of a "Universal" Second-Order Logic Formula
Consider the following decision problem:
Input: a second-order logic formula $\psi$ of the form $\forall X_1 . \ldots . \forall X_n . \phi$ where $X_1, \ldots, X_n$ are a second-order variables and $\...
- 99
1
vote
0
answers
55
views
Primitive recursion relative to a logical system
In various places I have read that the normally considered non-primitive recursive Ackermann function is primitive recursive in higher-order logic. It's claimed to be due to "Reynolds, 1985",...
- 900
0
votes
0
answers
46
views
Using Simplex for Difference Logic
I'm interested in what happens when using the Simplex algorithm on Difference logic, inspired by problem 5.4 in Kroening and Strichman's Decision Procedures.
Clearly, in this case, all constraints of ...
- 161
1
vote
2
answers
96
views
Do realizable systems always have some non-well-founded sets?
Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following:
LEM is not realized (e.g. this MSE answer)
The traditional ...
- 271
2
votes
1
answer
95
views
Are MSO formulae on graphs expressible with bounded quantifier alternation?
Is there some $k$ such that, given any formula $\varphi$ in the monadic second order theory of graphs (this question applies for either MSO with sets of vertices and edges or just MSO with sets of ...
- 279
4
votes
2
answers
248
views
Are MSO formulae expressible as existential SO formulae over arbitrary structures?
Given an MSO formulae φ, which may contain arbitrary quantifier alternation, is there always an ESO formula ψ, such that φ and ψ have the same (finite) models?
(This statement holds when the models we ...
0
votes
1
answer
86
views
Probabilistic Logic Programming vs Stochastic Logic Programming
I'm reading the paper DeepStochLog: Neural Stochastic Logic Programming. The authors differentiate between Probabilistic Logic Programming (PLP) and Stochastic Logic Programming (SLP), but I can't ...
- 3
1
vote
0
answers
40
views
What are the applications of Belief Revision?
In my Computer Science graduation, I came across this concept of Belief Revision, which focus on knowledge representation and the possible operations that can be done with the facts that a "...
- 111
1
vote
0
answers
55
views
Automatizability of Extended Resolution
According to Krajícek, Jan and Pavel Pudlák. “Some Consequences of Cryptographical Conjectures for S12 and EF.” Inf. Comput. 140 (1998): 82-94., the extended Frege proof system is not automatizable ...
- 145
14
votes
4
answers
2k
views
Where is the model theory in programming language theory?
I have a background in mathematical logic and am trying to learn some programming language theory. In the syntax of, say, first-order logic, one of the first distinctions you learn about is between ...
- 803
1
vote
1
answer
148
views
Which are the rules for minimal logic in both sequent calculus and natural deduction styles?
Are there any references I could use which explictly contain the rules for minimal logic, both as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!)
To give ...
- 377
5
votes
1
answer
111
views
Logical Equivalents of Finite State Transducers
There's a notion of "regular" function on words in automata theory that corresponds nicely to functions in WS1S/Büchi Arithmetic/the logic of words with a prefix and equal-length relation. ...
- 279
3
votes
0
answers
66
views
What's the difference between "modular" and "compositional"?
When talking about reducing complexity in a software system, we often talk about making it "modular" by breaking it up into multiple modules that are all linked together to form the overall ...
1
vote
0
answers
72
views
Do soundness and completeness need to be exact converses of eachother?
This question concerns the derivational soundness and completeness of the first-order proof system LK (without equality) as presented in Logical Foundations of Proof Complexity by Cook and Nguyen. In ...
- 201
1
vote
1
answer
75
views
Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?
The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained I've ...
- 201
1
vote
1
answer
81
views
Intuition behind UTT's internal logic
The "internal logic" of type theory UTT is defined in LF as follows:
What's the intuition behind this definition? I can kind of understand the declaration of the the first three constants - ...
- 125
1
vote
1
answer
115
views
Formulation of Tarski-style universes in LF
Lately I've been asking questions on type theory on MSE, and I've been getting great answers, but I decided to give a try to this site and see if it will be helpful as well.
I'm looking at this note ...
- 125
3
votes
0
answers
42
views
Can you compute Shannon expansion of a Boolean formula more efficiently by using a QBF solver?
Maybe this is not enough research level, but I've been scratching my head on it for a while...
I'm interested in the Shannon expansion of an existentially quantified Boolean formula of the form:
$$ \...
- 1,588
11
votes
12
answers
5k
views
Theoretical Computer Science vs other Sciences?
So I‘m in my fifth semester studying Computer Science at a German university, so I‘ve only scratched the surface of Theoretical Computer Science, namely Logic, Formal Languages, Automata Theory, ...
- 127
1
vote
3
answers
255
views
Turing Machines and Logic
It is well known that Monadic Second Order Logic (over words) and finite automata can express the same set of languages.
Is there a logic over words (perhaps a nth order logic) such that it and turing ...
- 125
4
votes
1
answer
191
views
Shortest path property and monadic second order logic
I know that induced paths and Hamiltonian cycles can be expressed with monadic second-order logic ($MS_2$).
Is it possible to express the shortest path in $MS_2$?
- 45
5
votes
0
answers
150
views
Arithmetization of finite automata
Is there any standard way to encode the language accepted by a finite automaton by an arithmetic formula?
A particular way of doing this would be to extend the language of existential integer linear ...
- 921
0
votes
1
answer
66
views
Resources for first-order and second-order monadic logics with a model-checking objective
What are some good books and surveys for learning about first-order logic and monadic second-order logic?
I'm a graduate student in computer science with a focus on algorithms. For model-checking on ...
- 45
6
votes
1
answer
206
views
Stronger "induction" principles than induction-recursion
Are there type theories in the literature with "induction" principles stronger than induction-recursion? This answer gives System F as an example of a theory stronger than MLTT + induction-...
6
votes
1
answer
286
views
Concrete family of propositional formulas
Let $k,n \in \mathbb{N}$, where $k$ can be thought of as being fixed constant. For each $1 \leq \ell \leq k$ and $1 \leq i \leq n$ we have a proposition symbol $p_{(\ell,i)}$ (so in total we have $nk$-...
- 938
0
votes
0
answers
36
views
Making primary keys explicit in a Boolean relation
Suppose we have a Boolean formula $\phi(X,Y)$ over the sets of Boolean variables $X$ and $Y$, representing a binary relation. There are in general many tuples in this relation.
Is there a way to ...
- 1,588
4
votes
0
answers
75
views
Lower bound on the size of Skolem functions
Consider a quantified Boolean formula $f$. We can convert it into Skolem Normal Form formula $f^*$ such that $f$ is satisfiable iff $f^*$ is satisfiable, by replacing variables that are existentially ...
5
votes
1
answer
210
views
Can you define recursive predicates in 2nd order intuitionistic logic?
This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here.
Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) ...
- 13.7k
3
votes
1
answer
184
views
How far is the distance between Mahlo Universe and Mahlo Cardinal?
There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.
More explicitly, I would ...
- 151
1
vote
1
answer
170
views
Complexity of "discrete-time" SAT
I'm interested in the complexity of deciding satisfiability of the following family of formulae:
$\exists j. I[j(0)] \land \forall t. S[j(t),j(t+1)]$
where:
$j:\mathbb{N} \to \{0,1\}^n$ has finite ...
- 921
1
vote
0
answers
77
views
On completeness of LTL
I am reading the seminal paper "On the temporal analysis of fairness" by Gabbay, Pnueli, Shelah, Stavi, available at
shelah.logic.at/papers/134/
In Section 3, completeness of a set of axioms ...
- 11
2
votes
0
answers
105
views
Gurevich's theorem on primitive recursive functions being logspace-computable
I recently came across the following result attributed to Gurevich, according to which I understood that the class of problems solvable by primitive recursive functions is precisely the class L of ...
- 801
1
vote
0
answers
148
views
What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?
The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
- 81
6
votes
0
answers
94
views
Relationship between natural deduction refutation and tableaux for propositional logic
Which kind of relationship is there between natural deduction refutations of a set f propositional logic assumptions, and the corresponding tableaux?
For example, consider the unsatisfiable set $\...
- 1,588
4
votes
0
answers
82
views
Are there classes for that FO-model checking is FPT on hypergraphs?
For graphs, there are many classes that admit FPT-algorithms for model checking of first order logic, e.g. the class of nowhere dense graphs by Grohe et. al.
Are there similar results for ($k$-uniform)...
- 41
3
votes
1
answer
148
views
Efficient transformation into CNF preserving entailment
Suppose you have two propositional formulas $\varphi$ and $\psi$, not necessarily in CNF. I want to convert them to 3CNF efficiently (hence introducing auxiliary variables) in such a way that $\varphi ...
- 801
0
votes
1
answer
59
views
Are there logical devices similar to "existential variables" or "blank nodes" of Semantic Web?
In Semantic Web, alongside permanent names of things also "temporary names" named "existential variables" or "blank nodes" denoted as "_:label" are used. All ...
- 101
9
votes
0
answers
407
views
Examples of simulations in proof complexity that are not p-simulations
I am writing a paper on the complexity of some unorthodox proof systems, where I have two systems $P$ and $Q$ such that $P$ simulates $Q$ in the sense of it being possible to translate a $Q$-proof ...
- 286
6
votes
0
answers
229
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
1
answer
207
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 ...
- 11
8
votes
3
answers
739
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 ...
- 377
9
votes
1
answer
150
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 ...
- 938
2
votes
0
answers
101
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 ...
- 424
0
votes
1
answer
86
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 ...
- 109
1
vote
0
answers
105
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
0
answers
60
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 ...
- 139