# Questions tagged [lo.logic]

Computational and mathematical logic.

448 questions
2answers
265 views

### About the position of side conditions in an inference rule

Sometimes I see people put side conditions above the inference line as if they were premises of an inference rule. This feels strange. My understanding (which may be wrong) is that a side condition ...
2answers
491 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 ...
2answers
129 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, ...
2answers
286 views

### What is the benefit of Krivine's notation?

I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
1answer
101 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-...
2answers
884 views

### What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

I am in possession of a book, which, inspired by Russell's Principia Mathematica (PM) and logical positivism, attempts to formalize a specific domain by determining axioms and deducing theorems from ...
7answers
3k views

### Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

Mathematicians sometimes worry about the Axiom of Choice (AC) and Axiom of Determinancy (AD). Axiom of Choice: Given any collection ${\cal C}$ of nonempty sets, there is a function $f$ that, given a ...
1answer
239 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 ...
2answers
217 views

0answers
85 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 ...
2answers
293 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 ...
3answers
2k views

### Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
1answer
175 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 ...
5answers
5k views

### What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
2answers
155 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 ...
1answer
896 views

### Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
1answer
53 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 ...
0answers
125 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 ...
3answers
200 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 ...
5answers
359 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 ...
0answers
43 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 ...
1answer
68 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 ...
1answer
502 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 ...
1answer
185 views

### Temporal Logic and Access Control Models

What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
1answer
124 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 ...
1answer
84 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 ...
1answer
440 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 ...
1answer
50 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 (...
1answer
338 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 ...
1answer
47 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: ...
4answers
540 views

### Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( https://dl.acm.org/citation.cfm?id=2359499). In this paper, they internalize unary ...
1answer
102 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 ...
1answer
86 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 ...
2answers
97 views

0answers
110 views

2answers
482 views

### First order expression for functional dependency

I'm puzzled with functional dependency formula in first order logic. It is triggered by http://rjlipton.wordpress.com/2010/01/17/a-limit-of-first-order-logic/ where there seems to be a confusion ...
0answers
165 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 ...
0answers
124 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 ...
0answers
84 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, ...