Questions tagged [lo.logic]
Computational and mathematical logic.
468
questions
4
votes
1answer
68 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
74 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
108 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
56 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 ...
1
vote
0answers
61 views
What is an Herbrand interpreration and model? [closed]
I was reading the book "Foundations of Logic Programming" written by J.W.LIoyd. In the book, there were definitions of interpretation and model, and when it comes to Herbrand interpretation and model, ...
9
votes
1answer
162 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 ...
2
votes
0answers
187 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
102 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-...
1
vote
0answers
80 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
192 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
308 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
79 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
193 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
89 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'...
7
votes
0answers
253 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
237 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
293 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
145 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
101 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
709 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
166 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
125 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
275 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
228 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
257 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
335 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
216 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
359 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
113 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
238 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
76 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
138 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 ...
4
votes
2answers
195 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
223 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
44 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 ...
6
votes
2answers
109 views
Multimodal logic with quantification over modal operators
I take a multimodal logic to be a logic with multiple (potentially infinitely many) primitive modal operators. I am curious if anyone has studied a logic that allows one to quantify over the modal ...
11
votes
5answers
435 views
Representing bound variables with a function from uses to binders
The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
4
votes
1answer
179 views
Is graph connectivity definable in existential MSO with vertices and edges?
Can $\exists$MSO$_2$ express graph connectivity?
Monadic SO (MSO) is the fragment of second-order logic in which the second-order quantifiers range over relations of arity 1 only.
$\exists$MSO is the ...
2
votes
1answer
96 views
Representable functions on System T
In Proof and Types by Girard et alii. Section 7.4.2, I think that the authors want to show that:
(1) The set of functions definable in System T coincides with the set of
recursive functions whose ...
1
vote
1answer
110 views
What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?
Let $\Lambda$ be a set of strongly normalizing lambda terms.
Let $\mathtt{NF} : \Lambda \rightarrow \Lambda$ be evaluation to the normal form.
Let $ \lvert x\rvert : \Lambda \rightarrow \mathbb{N}$ be ...
6
votes
1answer
595 views
Is Church-pentation implementable in Agda?
Inspired by suggestion in this question, I've implemented predicative Church encoding of Peano arithmetic. Exponentiation works fine, unfortunately tetration requires the level of one of the arguments ...
5
votes
2answers
136 views
A stronger multiplexing rule for soft linear logic?
In (intuitionistic) linear logic the usual rules for the storage modality $!$ are promotion, dereliction, contraction, and weakening:
$$\frac{!\Gamma\vdash A}{!\Gamma\vdash !A}(prom) \qquad \frac{\...
4
votes
1answer
127 views
What's the difference between proving weak normalization and implementing evaluator?
Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation ...
1
vote
0answers
243 views
Is it possible to type Ackermann function with (stratified variant of) System F?
I was surprised to find no open-source implementation of Ackermann function in pure System F as an illustrative example. I finally managed to implement it myself in Haskell using Church encoding:
<...
2
votes
1answer
124 views
Is there a formalization of normalization of impredicative system F?
In particular Agda seems not strong enough to prove that.
Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient?
How about with the impredicative Prop?
1
vote
1answer
63 views
Is there a standard format for Dependent QBF?
I know there is a standard input format DIMACS for a formula is in conjunctive normal form (CNF) and QDIMACS for quantified Boolean formulas. Is there a similar standard format for the Dependent-QBF (...
7
votes
1answer
147 views
Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?
In Multiplicative Linear Logic (MLL), addition of the mix rule eliminates 'connectedness' from Danos-Regnier criterion. I'm investigating how the criterion changes if we do not distinguish between ...
3
votes
1answer
49 views
Algorithm for finding smallest set and instanciation for a given constraint system
I have a system of constraints described by a set of clauses of the form
$x_1 \neq x_2 \lor \dots \lor x_{i-1} \neq x_i$, for instance:
...
1
vote
0answers
66 views
To what extent supervised learning ERM learn first-order knowledge
Suppose I have a collection of (hidden) first-order rules:
$$
\mathcal{R}: \{ Q_i(x) => P_i(x) \}_{i=1}^{k}
$$
all defined over $x \in \mathcal{X}$.
I can use these rules and (automatically) ...
