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:
...
- 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 ...
- 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 \...
- 275k
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 ...
- 30k
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 "...
- 81.4k
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 ...
- 275k
37
votes
Is it possible to write an AND gate using XOR gates?
You cant.
Since $XOR$ is associative, i.e. $(x_1\oplus x_2)\oplus x_3=x_1\oplus(x_2\oplus x_3)$, you can only implement functions of the form $x_{i_1}\oplus...\oplus x_{i_k}$ where $x_{i_j}\in\{x_1,...
- 13.3k
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), ...
- 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 ...
- 30k
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 ...
- 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 ...
- 710
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 ...
- 351
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
...
- 231
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 ...
- 3,469
19
votes
Is it possible to write an AND gate using XOR gates?
Hmmm. It can't be done with boolean algebra that's for sure, but I could wire one up physically. The trick is wiring one of the inputs to a power lead of an XOR gate.
...
- 380
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. ...
- 2,713
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 ...
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 ...
- 7,768
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 ...
- 261
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 ...
- 29.7k
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 ...
- 3,469
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 ...
- 30k
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."
- 81.4k
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 ...
- 14.4k
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 ...
- 8,308
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 ...
- 81.4k
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 ...
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.♦
- 156k
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 ...
- 418
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.♦
- 156k
Only top scored, non community-wiki answers of a minimum length are eligible