Skip to main content
Share Your Experience: Take the 2024 Developer Survey
77 votes
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: ...
AI0867's user avatar
  • 690
55 votes

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 ...
Erin's user avatar
  • 511
48 votes

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 \...
Yuval Filmus's user avatar
41 votes

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 ...
Andrej Bauer's user avatar
  • 30.8k
40 votes

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 "...
David Richerby's user avatar
39 votes

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 ...
Yuval Filmus's user avatar
31 votes
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), ...
user21820's user avatar
  • 707
30 votes

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 ...
Andrej Bauer's user avatar
  • 30.8k
26 votes

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 ...
Boris's user avatar
  • 493
26 votes

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 ...
Acccumulation's user avatar
25 votes

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 ...
A. Bollans's user avatar
23 votes

Why do logic gates behave the way they do?

I think the questioner has it backwards. If we have a logical function such that ...
user120366's user avatar
22 votes

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 ...
Anton Trunov's user avatar
  • 3,479
19 votes
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. ...
Noah Schweber's user avatar
17 votes
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 ...
Derek Elkins left SE's user avatar
17 votes

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 ...
Discrete lizard's user avatar
  • 8,248
16 votes

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 ...
Hatshepsut's user avatar
15 votes

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 ...
Joey Eremondi's user avatar
15 votes
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 ...
Anton Trunov's user avatar
  • 3,479
15 votes
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 ...
Andrej Bauer's user avatar
  • 30.8k
14 votes
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."
David Richerby's user avatar
14 votes
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 ...
chi's user avatar
  • 14.6k
14 votes

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 ...
Martin Berger's user avatar
14 votes

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 ...
David Richerby's user avatar
14 votes
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 ...
Gilles 'SO- stop being evil''s user avatar
13 votes
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 ...
D.W.'s user avatar
  • 161k
13 votes
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 ...
The Vee's user avatar
  • 418
13 votes
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 ...
Nathan Davis's user avatar
13 votes
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 ...
David Richerby's user avatar
13 votes
Accepted

Representing binary functions with a finite gate set without exponential blow-up?

No. No matter what representation of functions as circuits/formulas you use, there will exist some functions that require exponential size to represent. This was proven by Shannon in 1949. See ...
D.W.'s user avatar
  • 161k

Only top scored, non community-wiki answers of a minimum length are eligible