Computational and mathematical logic.
5
votes
1answer
140 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
32 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
107 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
139 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
186 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 ...
7
votes
0answers
40 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 ...
2
votes
1answer
60 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 ...
10
votes
5answers
321 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
108 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
77 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
75 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 ...
7
votes
1answer
224 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
84 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
83 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
126 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
84 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
48 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
96 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
42 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
51 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) ...
3
votes
0answers
107 views
Decomposition of rectangular relations
Let $\alpha$ be a binary relation from $\gamma$ to $\chi$ and $\beta$ a binary relation from $\chi$ to $\rho$. If both $\alpha$ and $\beta$ are rectangular, i.e., they satisfy $\alpha \alpha^{-1} \...
3
votes
0answers
131 views
Formalization of proofs and CC paradox? - Part II
This was the second part of my previous question. It is very similar, and probably it has a similar answer (as Emil said in a comment), but I thought it was worth to separate it and ask it as a new ...
0
votes
0answers
33 views
closed Horn clause Datalog fragment identification
I am trying to identify the appropriate fragment of Datalog containing rules of the type:
A(x,y):-B(x,z),c(z,y)
where B(x,z) ...
6
votes
1answer
332 views
Formalization of proofs and computational complexity paradox?
While reading some articles on formal proofs (see also my previous question on cstheory about the length of ZFC proofs versus human written proofs), I came up with this apparent paradox.
Let $M_{...
5
votes
0answers
145 views
Is Agda sound as a proof system? [closed]
I've asked the same question on CSSE but with no luck (https://cs.stackexchange.com/questions/89611/is-agda-sound-as-a-proof-system). Therefore I ask it again here in cstheory and hope that more ...
4
votes
1answer
221 views
Sparsification Lemma for k-SAT and Exponential Time Hypothesis
According to R. Impagliazzo, R. Paturi and F. Zane, 2001 an instance of $k$-SAT is called sparse if $m = O(n)$ where $m$ denotes the number of clauses and $n$ the number of variables. The ...
3
votes
0answers
83 views
Looking for a specific tree automata model
is there any tree automata model over unranked trees (that is with unbounded number of children for each node), such that:
Checking non-emptiness and universality is decidable in elementary time,
...
2
votes
1answer
85 views
Is Eulerian Path (or Eulerian Cycle) definable in Monadic Second Order Logic?
Does there exist a monadic second order logic formula which is satisfied by a graph if and only if it has an Eulerian path (or Eulerian cycle).
I am looking for properties of graphs which are ...
6
votes
0answers
207 views
Fischer and Rabin's theorem (1974) for theories of “additive” structures
Fischer and Rabin's Super-Exponential Complexity of Presburger Arithmetic (1974) has the following theorem.
(Theorem 12) Let $U$ be any class of additive structures, so if $A = (A, +) \in U$,
...
2
votes
0answers
37 views
Is there a complete and finite axiom scheme for conditional independence? (Graphoids)
Note: This is a better-written version of an unanswered question asked before on MathOverflow.
Question: Is there a complete and finite axiom scheme for conditional probability?
If so, is ...
3
votes
1answer
104 views
Connection between algebraic logic and computational complexity of logics?
I'm learning a bit about algebraic logic and I was wondering how knowing the algebraic semantics of a given logic might help the study of the logic itself from a computational point of view.
In ...
8
votes
1answer
364 views
Complexity of modal logic IK5
What is the complexity of local satisfiability problem for modal logic $\mathit{IK5}$? Herein we denote by $IK5$ the modal logic over euclidean frames extended with inverse modality. Could you provide ...
3
votes
4answers
275 views
Philosophy behind monotonicity requirement for inductive types
Is there a good philosophical reason for why inductive types with negative occurrences or non-monotonicity should not be considered valid constructions? According to my understanding of the Bishop/...
0
votes
1answer
46 views
Head variables of terms after application
We work in the Church-style simply typed lambda calculus. All terms shall be considered in long normal form. Any term of type $A_1\rightarrow A_2\ldots\rightarrow A_n \rightarrow 0$ is of the form $\...
4
votes
2answers
317 views
Efficiently modeling Turing machines in Peano Arithmetic
The (undecidable) Peano Arithmetic (PA) is powerful enough to model Turing machines.
Consider a standard first order axiomatization of Peano Arithmetic and a standard Hilbert-style proof system $\...
3
votes
0answers
121 views
Family of formulas for which Gabbay's separation algorithm explodes nonelementarily
It is repeated throughout the literature that Gabbay's algorithm for
separation of LTL with Since and Until can produce nonelementary blow-up
of the size of the formula, but I have never seen a proof ...
5
votes
1answer
117 views
Normal forms for intuitionistic formulas?
It is well-known that DNFs/CNFs and prenex normal forms generally do not exist for intuitionistic logic.
Are there any nice results about formula normalization for IL? I've tried googling this but ...
0
votes
0answers
47 views
FOL sentence encoding acyclic graphs using only universal quantifiers
This question was also posted on Math.SE
Suppose that we have a binary relation $E(x,y)$ representing edges of a graph along with some constraints on $E$. For example, one possible constraint is that ...
0
votes
0answers
101 views
Is it possible to transform a theory written in FOL into an equivalent theory that uses conditional equational logic plus Boolean Algebra?
I am studying the relationship between First Order Logic (FOL) specification methods (e.g. CASL) and equational based specification (e.g. CafeOBJ). My question is:
Is it generally possible to ...
1
vote
0answers
54 views
On collapsing the Exponential time hierarchy
Define $\Sigma^E_0 = \Pi^E_0=E$,
for every $n>0$, define $\Sigma^E_n=NE^{\Sigma^p_{n-1}}$,
for every $n>0$, define $\Pi^E_n=CoNE^{\Sigma^p_{n-1}}$.
Define the Exponential time hierarchy by $EH=\...
10
votes
2answers
380 views
State of the Art for the Monadic Class?
Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete.
...
6
votes
1answer
200 views
Algebraic account of Gaussian elimination?
For fun, I've been looking at the interpretation of linear logic in terms of finite-dimensional vector spaces, and ran into an interesting
question about the interpretation of double-negation-...
13
votes
1answer
173 views
Conclusions from reverse mathematical strength of graph minor theorem
Say we have a graph property which can be checked in nondeterministic polynomial time, and a proof in a weak formal system (say RCA0) that the property is minor closed. Can we say anything about the ...
1
vote
0answers
72 views
What logic(s) exist for attributing belief?
I'm looking for an appropriate formalism to represent "traceability" in claims, especially connecting conclusions to source materials in a rigorous way. For example, I'd like to be able to represent ...
3
votes
2answers
355 views
Automated proving that a program doesn't halt
If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)...
0
votes
0answers
27 views
Expressiveness of bounded difference constraints with sets
Consider a restricted first-order theory over sets and natural numbers, with only bounded difference predicates such as $x-y<c$ where $c$ is a constant, and universal quantifiers. For instance, we ...
9
votes
1answer
203 views
Equilibrium in a Halting Game
Consider the following 2-player game:
Nature randomly picks a program
Each player plays a number in [0, infinity] inclusive in response to nature's move
Take the minimum of the players’ numbers, and ...
1
vote
2answers
108 views
Determine if a structure is a model of an inductively defined predicate
My setting is first-order logic. As an example, consider an inductive definition of a linked list:
$List(l)$ = $Null(l)$ $\vee~(Node(l) \wedge \exists sublist. List(sublist) \wedge next(l,...
1
vote
0answers
84 views
Definitions of strongest postconditions [closed]
The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer
$X ~\mapsto \neg G \wedge ...
11
votes
2answers
144 views
Does the first order theory of a finite structure have bounded quantifier rank?
Let $\mathfrak{A} $ be any finite structure.
Does its first order theory $ \mathfrak{T} := \mathfrak{TH}(\mathfrak{A}) $ have bounded quantifier rank, in the sense that there is a $ q\in\mathbb{N} $ ...
