Questions tagged [lo.logic]
Computational and mathematical logic.
521
questions
1
vote
1
answer
34
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 - ...
- 27.6k
1
vote
0
answers
19
views
Confusion about $T$ and $El$ when defining universes in LF
This is a technical follow-up question to Formulation of Tarski-style universes in LF
Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes ...
- 135
1
vote
1
answer
59
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 ...
- 27.6k
1
vote
3
answers
216
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 ...
- 852
10
votes
12
answers
4k
views
Theoretical Computer Science vs other Sciences?
So I‘m in my third 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, ...
- 790
3
votes
0
answers
36
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,416
16
votes
2
answers
1k
views
A mathematical (categorical) description of type classes
A functional language can be viewed as a category where its objects are types and morphisms functions between them.
How do type classes fit in this model?
I assume we should only consider those ...
- 181
4
votes
1
answer
150
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$?
- 8,223
3
votes
1
answer
151
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 ...
- 51
5
votes
0
answers
126
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 ...
- 889
0
votes
1
answer
49
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 ...
- 1,165
5
votes
1
answer
157
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-...
- 816
10
votes
2
answers
744
views
Functional Completeness of 3-valued logic
In the context of some recent work, we have been defining a language based on a three-valued logic à la Kleene, where $1$ stands for true, $0$ for false, and $\bot$ for error or don't-know. In order ...
- 21
13
votes
1
answer
308
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-...
- 506
6
votes
1
answer
285
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$-...
- 869
23
votes
1
answer
2k
views
What's the expressive power of Simply Typed Lambda calculus?
The standard approach to simply typed lambda calculus considers computations over Church numerals.
If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) ...
3
votes
1
answer
147
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, ...
0
votes
0
answers
34
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,416
12
votes
2
answers
976
views
Expressiveness of Büchi vs CTL(*)
What is the relationship between the expressiveness of LTL, Büchi/QPTL, CTL and CTL*?
Can you give some references that cover as many of these temporal logics as possible (especially between linear- ...
- 355
4
votes
0
answers
73
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 ...
7
votes
2
answers
427
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 ....
- 132
5
votes
1
answer
203
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) ...
- 15.4k
1
vote
1
answer
167
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 ...
- 8,223
1
vote
0
answers
70
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
30
votes
3
answers
2k
views
Translating SAT to HornSAT
Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT seems to imply that it is, but I have not been able to chase down ...
- 15.4k
1
vote
0
answers
86
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 ...
- 557
8
votes
1
answer
441
views
What is an unambiguous language in the sense of Schützenberger?
I'm reading Thomas Wilke's survey on the connections between Temporal Logic and finite automata, finite semigroups and first-order logic.
In Theorem 6 (by Kamp), the fragment $\mathrm{TL}[\mathsf{F},\...
- 355
1
vote
0
answers
133
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
81
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,416
4
votes
0
answers
77
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
121
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 ...
- 15.4k
17
votes
7
answers
1k
views
Pointers for CS applications of logic
I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set theory....
- 131
0
votes
1
answer
58
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 ...
- 775
9
votes
0
answers
388
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 ...
- 191
6
votes
0
answers
213
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: \{...
- 540
21
votes
1
answer
822
views
Combinators for the Primitive Recursive Functions
It is well-known that the S and K combinators are Turing Complete. Are there combinators that suffice to yield (only) the primitive recursive functions?
1
vote
1
answer
144
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
3
answers
688
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 ...
- 123
9
votes
1
answer
141
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 ...
- 15.4k
7
votes
2
answers
3k
views
Do past time LTL and future time LTL have the same expressiveness?
I would like to ask if anybody is aware of a paper comparing the expressiveness of past time LTL and that of (future time) LTL.
- 5,501
23
votes
1
answer
4k
views
Prove proof irrelevance in Coq?
Is there a way to prove the following theorem in Coq?
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
EDIT: An attempt to give a brief ...
- 945
2
votes
0
answers
94
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 ...
- 414
9
votes
1
answer
131
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,015
10
votes
3
answers
407
views
Does the order of declarations in an inductive type matter?
I was wondering if the order of declarations of an inductive type can matter.
For example in Coq you can define Nat either by:
...
- 945
0
votes
1
answer
79
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 ...
- 13.8k
12
votes
1
answer
467
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 ...
- 4,361
44
votes
4
answers
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 ...
1
vote
0
answers
99
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
59
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
9
votes
0
answers
194
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 ...
- 375