Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [lo.logic]

Computational and mathematical logic.

4
votes
1answer
215 views

What is a term of the type $\bot\rightarrow A$?

The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial: \begin{align} \bot&\vdash\bot \\ \hline \bot&\vdash A \\ \hline &\vdash\bot\...
19
votes
1answer
740 views

Scott's stochastic lambda calculi

Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
9
votes
1answer
302 views

First order satisfiability that doesn't have finite models

We know from Church's theorem that determining first order satisfiability is undecidable in general, but there are several techniques we can use to determine first order satisfiability. The most ...
24
votes
5answers
2k views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
-1
votes
1answer
101 views

Consistency and completeness of any arbitrary 3-valued logic? [closed]

Based on the explanations here [1] I know that 3-valued first order logic has many different versions, which differ in the definition of their operations (e.g. implication). All of these (as far as I ...
2
votes
1answer
287 views

Three-valued logic solver?

This is not my area, so apologizes if I am asking nonsense! I know that there are very good solver/theorem provers for solving 1st order logic. Now I have a problem, using 3-valued logic, but I am ...
3
votes
1answer
156 views

Decidability of first-order theory of real closed fields with functions

By a famous theorem of Tarski, the first-order theory of real closed fields is decidable, as it admits quantifier elimination. Can this result be extended so that propositions can be quantified over ...
2
votes
0answers
349 views

Theorem prover fails to find simple set theory proof?

I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic. Tarski claims in his "a work on mereology" that the goal is provable from assertions 1-3 but he does ...
0
votes
1answer
482 views

Which formalism is best suited for automated theorem proving in set theory?

Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving. Context ...
1
vote
0answers
182 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 ...
6
votes
3answers
234 views

Solving problems by deciding a logic

I am curious to know when open problems have been solved by expressing them in a specific logic, and then showing that this logic is decidable. I have two distinct cases in mind: The problem is ...
8
votes
1answer
121 views

Hypersequents: proof term assigments or translations to hybrid logic

I've been looking at a modal logic with the axiom $$ (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) $$ Roughly, this says that the ...
6
votes
1answer
124 views

A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
5
votes
1answer
176 views

Expressiveness of Infinitary Logic

I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. ...
10
votes
2answers
822 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 ...
1
vote
0answers
98 views

(co-)Horn formulation of Frankl's union-closed sets conjecture

Based on comments on MO there is simple forumlation of Frankl's union-closed sets conjecture in terms of (co-)Horn. In co-Horn CNF at most one literal is negated in every clause (Horn CNF where every ...
2
votes
1answer
65 views

Infinitary Counting Logics: 1-sorted vs. 2-sorted framework

There are two ways to extend infinitary logic with counting: Grädel's way (cf. p. 11): We extend $L_{\infty\omega}$ by introducing a counting existential quantifier: $$ \mathcal{A} \models \exists^{...
6
votes
1answer
2k views

Does there exist a sentence of first-order logic that is satisfiable only in infinite models that do not have a finite algorithmic representation?

There exist sentences of first-order logic that are satisfiable and are satisfiable only by models of infinite size. However, all such sentences I can think of are satisfied by infinite models that ...
2
votes
2answers
248 views

How to translate general recursion into a set of $\mu$-recursive operator applications?

I'm trying to find a scheme to translate a functional language with let rec into a set of primitives called "generalized arrows", i.e. $\kappa$-calculus with ...
5
votes
1answer
283 views

Can factorial be encoded in the Kappa-calculus with fixed point operator?

Suppose we have a $\kappa$-calculus with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal ...
3
votes
0answers
93 views

How to develop an effective notation for a partially ordered logic?

I am developing a logic for reasoning about programs in a resource-constrained environment. My starting point is intuitionistic linear logic, but I made the following changes: In intuitionistic ...
4
votes
1answer
317 views

Rules about Prop and Set in UTT

In Luo's UTT (type theory which is used in Agda, Idris, and other dependently typed programming languages), there're are two rules for $\Pi$ types. One for $\mathsf{Prop}$ and one for $\mathsf{Set}$. ...
5
votes
1answer
471 views

Types which correspond to sets of cardinality of continuum

Are types which correspond to sets with cardinality of continuum possible in MLTT (or in any other constructive theory)? On the first sight, they aren't, since elements of types are terms and we ...
2
votes
1answer
828 views

Monomorphic vs Polymorphic type theory

I am currently reading the book Programming in Martin-Löf type theory by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic ...
1
vote
1answer
88 views

Do algorithms for solving parity games ignore other possible strategies for player V after finding one?

Solving parity games (from a "start" node) relies on the existence of a history-free winning strategy for player 0 (V) or 1 (R). Whether there is more than one such strategy is probably never ...
5
votes
1answer
226 views

What does consistency mean for “computational theories” corresponding to inductive types?

I am currently reading the book by Luo on computation and reasoning. In the book he contrasts inductive types considered as computational theories with axiomatic theories widespread in "standard" ...
9
votes
1answer
933 views

W-types vs Inductive types

Martin-Löf type theory uses W-types to define inductive structures like integers, lists, etc. However, calculus of inductive constructions doesn't use them in the same way, inductive types there seems ...
10
votes
1answer
1k views

Homotopy type theory and Gödel's incompleteness theorems

Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". Homotopy Type Theory provides an alternative ...
0
votes
0answers
303 views

Equational Logic and First Order Predicate Logic

I am interested in using Equational Theories (ET) together with Equational Logic (EL) found in algebraic specification languages such as CafeOBJ . I wish to use ET+EL to represent and prove sentences ...
2
votes
1answer
324 views

What is logic programming and does it really add anything new to the logic?

I am acquinted with the basics of such notions as logic programming, monotonic and non-monotonic reasoning, modal logic (especially dynamic logic) and now I am wondering - does logic programming ...
8
votes
1answer
175 views

Decidability of inductive invariant existence in Presburger arithmetic

Problem: Consider a finite number of control states (including an "initial" and a "bad" state), a finite number of integer variables, and for each ordered pair of states a transition relation ...
6
votes
2answers
390 views

“Correctness” of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
9
votes
1answer
225 views

Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
3
votes
2answers
360 views

Good description of Calculus of Inductive Construction

I want to learn more about Calculus of Inductive Constructions. What can you recommend to read on this topic? All the materials which I found are either in French or too basic (the Coq'Art book). The ...
3
votes
2answers
160 views

How to use Prop from UTT in Agda

In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?
4
votes
2answers
141 views

Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
14
votes
1answer
437 views

Can we distinguish strictly syntactic and semantic methods in programming language?

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
15
votes
1answer
333 views

Natural theorems proven only “to high probability”?

There are plenty of situations where a randomized "proof" is much easier than a deterministic proof, the canonical example being polynomial identity testing. Question: Are there any natural ...
6
votes
1answer
182 views

Is infinitary logic a logic in the sense of Gurevich?

Gurevich provides an exact definition of what Logic capturing PTIME is. An abstract logic $L$ consists of a set of $L[\tau]$-sentences for each vocabulary $\tau$, and a mapping that maps a property $...
6
votes
4answers
355 views

Simplification of Presburger formulas in practice

I have formulas in Presburger arithmetic (with initial ∀, but I can apply quantifier elimination so they are quantifier-free) that are fairly complicated, yet, in many useful cases, are equivalent to ...
9
votes
3answers
468 views

Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?

Foetus, if you have not heard of it, can be read up on here. It uses a system of 'call matrices' and 'call graphs' to find all 'recursion behaviors' of recursive calls in a function. To show that a ...
12
votes
3answers
717 views

What are natural examples of non-relativizable proofs?

As I understand it, a proof that P=NP or P≠NP would need to be non-relativizable (as in recursion theory oracles). Virtually all proofs seem to be relativizable, though. What are good examples of ...
0
votes
0answers
58 views

Bringing rigor into discussions. Do we have a crowd-sourced sytematic reasoning system?

I am looking for ways to crowd-source systematic reasoning behind common and uncommon convictions, beliefs, science principles, software or product design, political views, etc. Today, discussions on ...
6
votes
0answers
423 views

Generalized sequential machine synthesis subject to language equivalence/inclusion and reachability

A generalized sequential machine (GSM) is a generalization of a Mealy machine where on each transition one input symbol is read and 0 or more output symbols are written. As in a Mealy machine, we ...
0
votes
0answers
115 views

Given a CSL formula, how can we generate an automaton that accepts the formula?

The problem is same as the title, given a Continous Stochastic Logic(CSL) formula how can we create a machine which accepts the formula? Any intuitive ideas or references will be appreciated.
4
votes
1answer
362 views

Distributive expansion of CNF and implicants

I am looking for references for the following theorems. Theorem 1: Distributive expansion of a CNF formula $P_c$ (product of sums) results in a DNF formula (sum of products) consisting of all prime ...
7
votes
2answers
283 views

SAT in some DTIME always via a constructive proof?

Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-...
2
votes
2answers
134 views

Why does IFP< not capture PTIME?

Consider the logic whose $\tau$-sentences are the sentences in $IFP(\tau \cup \{<\})$, and the satisfaction relation is given by $\mathfrak{A} \models^* \phi$ if $(\mathfrak{A}, <) \models \phi$...
0
votes
0answers
201 views

Significance of Logic in Computer Science

I understand the significance of the theory of comptuation, for example NP-hardness of a problem signals us to forget about implementing it's exact solution and rather try approximating it. In the ...
2
votes
0answers
268 views

Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...