Share Your Experience: Take the 2024 Developer Survey

# Tag Info

Accepted

### Why do logic gates behave the way they do?

As stated by user120366, 16 possible 2-input logic gates exist, I've tabulated them for you here: ...
• 690

### Why is $A \lor (A \land \neg B) \equiv A$?

I find pictures are great for anything simple enough to use them, which this is. Remember: AND means the area taken up by both things. So the middle one is what is taken up outside B, but also ...
• 511

### Why is $A \lor (A \land \neg B) \equiv A$?

There are many ways to see this. One is a truth table. Another is to use the distributive rule:  A \lor (A \land \lnot B) = (A \land \top) \lor (A \land \lnot B) = A \land (\top \lor \lnot B) = A \...
• 278k

### Why is A implies B true if A is false and B is false?

Humans are bad at logic until they have to employ it to figure out human affairs. Think of "if $A$ then $B$" as a kind of promise: "I promise to you that if you do $A$ then I will do $B$". Such a ...
• 30.8k

### What exactly is a logic?

Fundamentally, a logic consists of two things. Syntax is a set of rules that determine what is and is not a formula. Semantics is a set of rules that determine what formulae are "true" and what are "...
• 81.8k

### Could Gödel’s incompleteness theorem be circumvented with a quine?

Here is the proof of Gödel's incompleteness theorem, in a nutshell, for a theory $T$. We construct a sentence $\Pi$ which states that "$T$ proves that $\Pi$ is false". The sentence mentions ...
• 278k
Accepted

### Is it provably true/false that for a program, there exists a proof whether it halts or not?

Actually this is no different from the halting problem unsolvability. If you have any formal system T with a proof verifier program V that can reason about programs (as you desire in your question), ...
• 707

### Can proof by contradiction work without the law of excluded middle?

You asked (I am making your question a bit crisper): "What formal guarantee is there that it cannot happen that both $\lnot p$ and $p$ lead to a contradiction?" You seem to worry that if logic is ...
• 30.8k

### What exactly is a logic?

While fields such as computer science, mathematics and physics are relatively well-organized, Logic has a chaotic history. Its organization is really confusing so I think it's important to read some ...
• 493

### Could Gödel’s incompleteness theorem be circumvented with a quine?

Mainly because that proof would be part of mathematics too, and hence need proving itself. And that leads to an infinite loop in logic. No, that's not the flaw identified by Gödel’s incompleteness ...

### Why do logic gates behave the way they do?

It's easiest to think of $1$ representing a true statement and $0$ representing a false statement. The logic gates then act as truth functions. Say you put two statements, $p,q$, together to form a ...
• 351

### Why do logic gates behave the way they do?

I think the questioner has it backwards. If we have a logical function such that ...
• 231

### How to read out a double negation in propositional logic

The answer by @D.W. is valid in classical logic, however if you are on the intuitionistic side, then you can't eliminate double negation (~~). I'd read the formula as 'It is not true that my program ...
• 3,479
Accepted

### Language to define perfectly a programming problem

This question is somewhat unclear to me; however, under one interpretation there is a result which indicates that the answer is unsatisfyingly yes: namely, the existence of Friedberg numberings. ...
• 2,783
Accepted

### Why does soundness imply consistency?

I recommend looking into formal logic beyond vague, hand-wavy descriptions. It's interesting and highly relevant to computer science. Unfortunately, the terminology and narrow focus of even textbooks ...
• 12.1k

### Why do ¬, ∀ and ∃ have the same precedence?

Order of precedence is simply a notional convenience. There is no notion of strength here, just notation. All three operators are unary operators with notation "$\circ\ \cdot$", where $\circ$ denotes ...
• 8,248

### Why is A implies B true if A is false and B is false?

It's a convention -- we could use a different one, but this one is convenient. Here's what Terence Tao says: This is discussed in Appendix A.2 of my book [Analysis 1]. The notion of implication ...
• 261

### Testing whether an arbitrary proof is circular?

The vast majority of proof systems don't allow for infinite, circular proofs, but they do so by making their langauges non-Turing complete. In a normal functional language, the only way to make a ...
• 29.8k
Accepted

### Proving tautology with coq

You cannot prove it in "vanilla" Coq, because it is based on intuitionistic logic: From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of ...
• 3,479
Accepted

### What is a "contradiction" in constructive logic?

It is immaterial whether we speak about constructive or classical logic in this situation. If you read your questions again, you will see that they apply to boths kinds. The only difference that we ...
• 30.8k
Accepted

### Predicate Logic Notation: What does a "dot" mean?

The dot just means "such that"; it's often omitted. The difference between the two formulas is the difference between "everybody has a mother" and "there is somebody who is everybody's mother."
• 81.8k
Accepted

### What is the difference between strong normalization and weak normalization in the context of rewrite systems?

Weak normalization means that any term has a terminating rewriting sequence, i.e. admits a finite amount of rewritings which lead to a normal form (no more rewritings from that). Strong normalization ...
• 14.6k

### Deterministic SAT solver

Core algorithms like DPLL and its refinements like CDCL are completely deterministic. Note that non-determinism doesn't necessarily mean that an algorithm may lead to a wrong result. For example we ...
• 8,328

### Is the halting problem theorem really proven

Any proof of the undecidability of the halting problem is specific to some model of computation. The proof is usually stated using Turing machines, which don't have call stacks or any other bells or ...
• 81.8k
Accepted

### Question on the "Tutorial implementation of dependently typed lambda calculus"

$\mathsf{id}$ and $\mathsf{const}$ are not variables of the calculus, but syntactic sugar for $\lambda x \rightarrow x$ and $\lambda x \rightarrow \lambda y \rightarrow x$ respectively. This is stated ...
Accepted

### How to read out a double negation in propositional logic

One way to pronounce "~" is as "not", so one could pronounce that as "not not R". But frankly, pronouncing complex logic formulas can be ugly, and often it's better to just write it on a whiteboard ...
• 161k
Accepted

### Intuition behind the Hadamard gate

The Hadamard gate might be your first encounter with superposition creation. When you say you can relate the usefulness of the Pauli $X$ gate (a.k.a. NOT) to its ...
• 418
Accepted

### Is this a generic way to convert any recursive procedure to tail-recursion?

Your description of your algorithm is really too vague to evaluate it at this point. But, here are some things to consider. CPS In fact, there is a way to transform any code into a form that uses ...
• 632
Accepted

### Monadic Second Order Logic for Dummies

What is second order logic in contrast to first order logic? What is monadic vs non monadic logic? Monadic second-order logic is first-order logic plus quantification over sets. So, as well as ...
• 81.8k