Questions tagged [lo.logic]

Computational and mathematical logic.

Filter by
Sorted by
Tagged with
5 votes
0 answers
164 views

The evaluation problem for AC$^0_d$ formulas is in FO

Let $d \in \mathbb{N}$ be arbitrary. Let $\mathsf{AC^0_d}$-Eval be the following promise problem: Input: A depth $d$ formula $\varphi(x)$ and a binary string $a$. Output: $\varphi(a)$ I am looking for ...
Kaveh's user avatar
  • 21.6k
19 votes
1 answer
480 views

Minor closed properties that are explicitly MSO expressible

Below, MSO denotes the monadic second order logic of graphs with vertex-set and edge-set quantifications. Let $\mathcal{F}$ be a minor closed family of graphs. It follows from Robertson and Seymour'...
Mateus de Oliveira Oliveira's user avatar
9 votes
1 answer
547 views

Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

On one hand, Gödel's Second Incompleteness Theorem states that any consistent formal theory that is strong enough to express any basic arithmetical statements can't prove its own consistency. On the ...
StudentType's user avatar
7 votes
2 answers
350 views

Are there any propositional proof systems which are not Cook-Reckhow proof systems?

An abstract proof system is a polynomial time function $f$ whose range is equal to the set of tautologies. If $\tau$ is a tautology, then an $f$-proof of $\tau$ is any value $\pi$ such that $f(\pi) =...
Slacked's user avatar
  • 71
8 votes
1 answer
235 views

What is the significance of nominal techniques?

What is the significance of nominal techniques, as far as their application to the formal theory of bound variables is concerned? I have been reading M. J. Gabbay's expository work on the topic that ...
Gonbê Nanasino's user avatar
2 votes
0 answers
44 views

Abduction in a Herbrand Constraint System

I have a simple constraint system with a finite set $C$ of constant symbols, an infinite set $V$ of variables, and two relation symbols - $R_1$, a preorder, and $R_2$, an equivalence relation. ...
Gowtham Kaki's user avatar
15 votes
1 answer
588 views

Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
Max New's user avatar
  • 1,685
1 vote
0 answers
110 views

Is Logic Done on Superpositional Bit Values Useful?

Let's say I have a way to represent $N$ bits such that those bits are in a superposition of the $2^N$ possible states those bits can have and that I can do XOR and AND on those superpositional bits to ...
Alan Wolfe's user avatar
10 votes
3 answers
1k views

Universal and existential types

I'm trying to wrap my head around the concepts of universal and existential types but everywhere I look, I see either logical or operational intuitions (or implementations) (e.g. TAPL book by B. ...
socumbersome's user avatar
10 votes
1 answer
415 views

Is `sort` typeable on elementary affine logic?

The following λ-term, here in normal form: ...
MaiaVictor's user avatar
  • 3,137
1 vote
1 answer
797 views

What's wrong with this LEAN proof? [closed]

I'm learning to use the LEAN theorem prover and I got stuck in a proof of a simple fact in first-order logic: $$ p(x) \rightarrow \forall x p(x) $$ My code is the following: variables (A : Type) (p q ...
StudentType's user avatar
12 votes
1 answer
459 views

An example where smallest normal lambda term is not fastest

Let the $size$ of $\lambda$-terms be defined as follows: $size(x) = 1$, $size(λx.t) = size(t) + 1$, $size(t s) = size(t) + size(s) + 1$. Let the complexity of a $\lambda$-term $t$ be defined as the ...
MaiaVictor's user avatar
  • 3,137
7 votes
2 answers
471 views

Concatenative binary lambda calculus/combinatory logic

John Tromp defines a version of the lambda calculus that is encoded in binary: https://tromp.github.io/cl/cl.html a) Does there exist a concatenative version of this language (or its combinatory ...
NietzscheanAI's user avatar
2 votes
0 answers
74 views

applications of institution-independent model theory

To quote wikipedia, The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970s in order to deal with the "population explosion among the logical systems used in ...
SorcererofDM's user avatar
2 votes
1 answer
180 views

Would a proof that the traveling salesman algorithm can't be encoded on LAL also prove P!=NP?

An answer to the traveling salesman (and similar) problems can be easily verified on light lambda-calculi. Also, if I understand correctly, the light lambda-calculi can compute every polinomial-time ...
MaiaVictor's user avatar
  • 3,137
5 votes
1 answer
187 views

Example of $MSO_2$ definable NP-hard problem on bounded clique-width graphs

All $MSO_1$ and $MSO_2$ definable graph problems can be solved in linear time on bounded tree-width graphs by Courcelle's theorem. But it seems this theorem doesn't work for $MSO_2$ definable graph ...
Kumar's user avatar
  • 2,044
21 votes
3 answers
2k views

Smallest possible universal combinator

I am looking for the smallest possible universal combinator, measured by the number of abstractions and applications required to specify such a combinator in the lambda calculus. Examples of universal ...
user76284's user avatar
  • 662
7 votes
1 answer
228 views

Formalized priority argument

A priority argument, an important proof technique in recursion theory, was introduced by Friedberg and Muchnik, to solve Post's Problem, i.e., the existence of two r.e. sets that do not Turing reduce ...
Pteromys's user avatar
  • 895
2 votes
1 answer
234 views

Reference for CTL* logic

I need a reference for CTL* logic (preferably easy to understand). I have gathered some disperse information regarding temporal and CTL logic but I need a more orderly coverage. A chapter of the ...
wmac's user avatar
  • 129
19 votes
0 answers
538 views

Courcelle's theorem for bounded clique-width graphs

Courcelle's theorem states that "Every graph property which is expressible in monadic second order logic is decidable in linear time for bounded tree-width graphs". Later it was extended to bounded ...
Kumar's user avatar
  • 2,044
6 votes
0 answers
177 views

What is the Kolmogorov complexity of arithmetic?

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(n) > L$ where $K(n)$ is the Kolmogorov complexity of the number $n$ and $L$ is a sufficiently large ...
Russell Easterly's user avatar
5 votes
1 answer
633 views

Calculating least fixed points in equations

Given a set of relations/equations in some logic like LTL would it be possible to find a least fixed point for those equations? For example take the equations in LTL $$ P = Play ~\land X(P \cup S)\\ ...
epsilon_0's user avatar
16 votes
3 answers
1k views

Why do constructivists not seem to care too much about call/cc

So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
Jake's user avatar
  • 1,203
2 votes
1 answer
167 views

Deciding satisfiability and non-validity

For propositional logic, a decision procedure for satisfiability can be turned into a decision procedure for non-validity by giving it the negated version of a formula. Does this hold for all logics ...
Kobold's user avatar
  • 41
11 votes
3 answers
1k views

Ramification of An Impredicative Type Theory

Most type theories that I'm aware of are predicative by which I mean that Void : Prop Void = (x : Prop) -> x isn't well-typed in most theorem provers as this ...
daniel gratzer's user avatar
1 vote
1 answer
45 views

Is there a rule-based implementation of weighted abduction other than the PTTP?

Is there an implementation of weighted abduction other than the PT theorem prover? A Google search reveals the PTTP and a few statistical approaches but I'm interested in a rule-based approach. The ...
Atamiri's user avatar
  • 185
4 votes
3 answers
506 views

Distinguishing semantics vs syntactic techniques and the syntax of your semantic domains

Consider a denotational semantics from simply-typed $\lambda$-calculus into dependent type theory. Is that actually a (trivial) term transformation into that dependent type theory? After all, type ...
Blaisorblade's user avatar
  • 2,059
14 votes
1 answer
2k views

Why was there a need for Martin-Löf to create intuitionistic type theory?

I've been reading up on Intuitionistic Type Theory (ITT) and it does make sense. But what I'm struggling to understand is "why" was it created in the first place? Intuitionistic Logic (IL) and Simply-...
PhD's user avatar
  • 5,305
6 votes
0 answers
148 views

Comparing the Kolmogorov complexity of theories - Part 2

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(x) > L$ where $K(x)$ is the Kolmogorov complexity of natural number $x$ and $L$ is a sufficiently ...
Russell Easterly's user avatar
8 votes
1 answer
761 views

Squash type vs Propositional truncation type

Homotopy type theory has a notion of propositional truncation type. It seems to me that it's strongly related to a notion of squash types. (See https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ...
Konstantin Solomatov's user avatar
11 votes
1 answer
998 views

Logical framework vs type theory

What is the difference between logical framework and type theory? Both of them have types, terms, and are based on dependently typed lambda calculus. We have Edinburg LF which is based on lambda-pi ...
Konstantin Solomatov's user avatar
15 votes
1 answer
672 views

Why was Schönfinkel's work on eliminating "bound variables" in logic so crucial?

AFAIK, The first evidence of using higher order functions goes back to Schönfinkel's 1924 paper: "On the Building Blocks of Mathematical Logic" - where he allowed one to pass functions as ...
PhD's user avatar
  • 5,305
23 votes
2 answers
2k views

What was the original intent for the creation of Lambda calculus?

I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church ...
PhD's user avatar
  • 5,305
8 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.
sean's user avatar
  • 722
-4 votes
1 answer
176 views

Temporal Logic - Until [closed]

I have a doubt, in Linear Temporal Logic LTL, does the Until operator require that the first occurrence is the first term of the formula? ex: a U b does require ...
Nk SP's user avatar
  • 131
13 votes
1 answer
528 views

Comparing the Kolmogorov complexity of theories

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(s) > L$ where $K(s)$ is the Kolmogorov complexity of string $s$ and $L$ is a sufficiently large ...
Russell Easterly's user avatar
12 votes
1 answer
640 views

Practical applications of parity games

Are there examples of practical applications of parity games, ie systems, in the real world, that can be represented as parity games ? Usually related documentation on parity games has almost never a ...
kafka's user avatar
  • 349
11 votes
2 answers
331 views

What is the complexity of the equivalence problem for read-once decision trees?

A read-once decision tree is defined as follows: $True$ and $False$ are read-once decision trees. If $A$ and $B$ are read-once decision trees and $x$ is a variable not occurring in $A$ and $B$, then $...
Marc's user avatar
  • 686
12 votes
1 answer
318 views

Reference for the fact that (0=1) implies false requires a universe in MLTT

It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe. The proof is also fairly ...
Neel Krishnaswami's user avatar
5 votes
3 answers
1k views

Law of excluded middle in MLTT

Is it possible to add law of excluded middle to Martin-Löf type theory as an axiom? It seems to me, that it's possible to add it to Coq since Coq has a module for non-constructive reasoning. Also, it ...
Konstantin Solomatov's user avatar
13 votes
3 answers
670 views

Uses of $\infty$-categories in TCS

I'm not a theoretical computer scientist. I'm a stable homotopy theorist using $\infty$-categories. I've seen applications of category theory and topos theory to theoretical computer science, and I ...
user avatar
5 votes
0 answers
194 views

Are there any logics to formalize understanding?

Are there any logics (modal-based or others) to formalize the following statement: "agent A understands p". For example "agent A understands that Titanic sank because it hit an iceberg" Where "...
user avatar
3 votes
1 answer
159 views

Can we verify satisfiability of first order statements via saturation in sub-exponential time?

In first order logic, we can prove satisfiability several ways: Finite model generation, truthful monadic abstractions, and also saturation. With finite model generation techniques, we can verify the ...
dezakin's user avatar
  • 318
5 votes
1 answer
124 views

Logics for timed resource control

I'm studying proof theory and I've seen that linear logic can be used as a way to control resource usage, since by the propositions-as-types it is equivalent to the linear lambda calculus. Is there a ...
Rodrigo Ribeiro's user avatar
2 votes
2 answers
179 views

Recommendations for References on undecidability of First Order Logic

I am currently reading Computability and Logic by Boolos Burgess Geoffrey for the proof on "undecidability of first order logic". however, I find the notations a bit confusing. Can anyone recommend ...
GermanShepherd's user avatar
0 votes
2 answers
235 views

Logic with Linear Programming

Can first-order logic be modeled/simulated as linear programming or integer programming? What about other forms of logic (say second order)? Update: am actually not a theory person, but more on the ...
Daniel's user avatar
  • 749
3 votes
1 answer
171 views

Presburger Arithmetic Decision Procedures

What are good textbook references for Presburger Arithmetic decision procedures?
Tony Johnson's user avatar
14 votes
1 answer
916 views

Simply typed lambda calculus and higher order logic

What is the relation between simply typed lambda calculus and higher order logic? Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related ...
lambda2's user avatar
  • 195
1 vote
0 answers
57 views

what is the meaning of "indicate substitution by priming metavariables"

This is a question about the usage of "indicate substitution by priming metavariables". For example, in the separation logic(it is not important whether familiar to this logic), I can understand the ...
liyu's user avatar
  • 11
15 votes
2 answers
1k views

Fixed points in computability and logic

This question has also been posted on Math.SE, https://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic I hope it is ok to also post it here. If not, or if it is too ...
Hanno's user avatar
  • 151

1
3 4
5
6 7
11