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 \...
- 274k
40
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 ...
- 29.4k
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 ...
- 29.4k
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,459
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 ...
- 11.9k
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
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.♦
- 152k
11
votes
Accepted
How is implication same as entailment
Let $\varphi$ and $\psi$ be formulas of propositional logic. We write, as Norvig says, $\varphi\vDash \psi$ iff $M(\varphi)\subseteq M(\psi)$: that is, iff every truth assignment that makes $\...
- 81.1k
10
votes
Accepted
Boolean algebraic expression vs Propositional logic expression
They are not the same, but I don't blame you for thinking that they are. The reason why it doesn't seem clear that they are the same is that you've only seen one example of each.
So let's step back, ...
- 20.2k
10
votes
Why is A implies B true if A is false and B is false?
"A implies B" means (short) "if A is true then B is true".
It means (a bit longer) "if A is true then I claim that B is true; if A is false then I don't make any claim about B whatsoever".
Now ...
- 27.4k
9
votes
Why is $A \lor (A \land \neg B) \equiv A$?
I would use my least favourite inference rule: Disjunction Elimination. Basically, it says that if $R$ follows from $P$, and $R$ follows from $Q$, then $R$ must be true if $P \vee Q$: $$(P \to R), (Q \...
- 203
7
votes
Accepted
Operator precedence in propositional logic
If you look at formal definitions of the syntax of propositional logic, you will find that
$\qquad p \land \lnot q \to r$
is not a proper sentence; parentheses are needed to avoid exactly the ...
- 71.7k
7
votes
Accepted
Does mutual exclusion hold in this case?
Your friend is correct. In your context, mutual exclusion holds if at most one process is at a critical section at any given time.
You state that you feel that this interpretation is wrong, but you ...
- 274k
7
votes
Can proof by contradiction work without the law of excluded middle?
I think your question boils down to "when doing formal verification with some sort of formal logic, what sort of guarantee do I have that the logic is consistent?". And the answer is: none. That's ...
D.W.♦
- 152k
6
votes
Accepted
Deciding which logical proposition is stronger
The notion of strength of a proposition comes from its power to constrain the model. For instance the proposition $P1 : x = 2$ is stronger than $P2 : x \geq 2$ in Arithmetic. And in propositional ...
- 1,409
6
votes
Why is A implies B true if A is false and B is false?
Let's take an example. Suppose that we want to express that $a$ is the only element of the set $S$ that satisfies property $P$. Then we can write
$$
\forall x \in S \;\; P(x) \Rightarrow x = a
$$
This ...
- 274k
6
votes
Accepted
Is this possible to solve boolean satisfiablility by using karnaugh maps to simplify the whole given boolean formula by simplifying subformulas?
"arbitrary chosen" in a NP problem where the followup results in a P algorithm typically means that the choice matters a lot and trying them all and backtracking over bad choices looking for the ...
- 4,226
6
votes
Accepted
Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?
The fact of the matter is, if a proof exists, then a Curry-Howard version of the program exists too. That doesn't mean that it's easy to find, though.
Undecidability still holds for Curry-Howard: if ...
- 29.5k
6
votes
Accepted
Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence
Proofs in Haskell?
Okay, first let's talk about the Curry-Howard correspondence. This says that one can view theorems as types and proofs as programs. However, it says nothing about which specific ...
- 29.5k
6
votes
Why is SAT based on the CNF?
Conjunctive normal form first appears, in this context, in Davis and Putnam's A computing procedure for quantification theory, in which they describe a primitive form of the DPLL algorithm (which ...
- 274k
5
votes
Accepted
How to find a minimum set of axioms within a set of propositions?
Determining whether a proposition follows from a set of axioms is an NP-Complete problem. Finding a minimal set of axioms from a set of propositions naturally invokes this problem many times as a ...
- 4,237
5
votes
Accepted
Contingent sentences can always be true
In mathematical logic - the discipline of logic that has interested computer scientists the most - there is a difference between proof-theoretic truth and model-theoretic truth.
Beyond metaphor (of ...
- 3,256
5
votes
Accepted
Why is learning DNF harder than learning CNF?
It's important to distinguish between $k$-CNF and CNF. A $k$-CNF formula is a CNF formula where every clauses has at most $k$ literals; a CNF formula has no limit on the number of literals in each ...
D.W.♦
- 152k
5
votes
Accepted
"Implied atomic propositions" in propositional boolean formula
Suppose we had a TM $M$ which, given $F$ and some atomic $A$ occurring in $F$ it can efficiently (PTIME) decide whether all models of $F$ make $A$ true, i.e. whether $F \models A$.
Then we can ...
- 14.4k
5
votes
Why is $A \lor (A \land \neg B) \equiv A$?
Note that, when we know that $C$ implies $D$, we have $C \lor D = D$. This is analogous to taking the union of a set (corresponding to $D$) and one of its subsets ($C$): we get the largest set ($D$) ...
- 14.4k
5
votes
Accepted
What is the connection between combinatorial circuits and finite state automata?
You can associate with a combinatorial circuit with $n$ inputs and a single output the language consisting of the $n$-bit strings on which the circuit outputs $1$. This language is finite and so, in ...
- 274k
5
votes
Accepted
Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?
There is a preprocessing method called vivification$^1$ that can be used to detect subsumed clauses. It relies on unit propagation to work.
To vivify a clause, make a partial variable assignment ...
- 8,003
5
votes
Accepted
Can this set of propositions be represented and proved in Haskell?
Your Haskell encoding fails to capture proofs in propositional calculus (which is what the book you referred to does). The failure is not due to your using Haskell, but because of your encoding ...
- 29.4k
Only top scored, non community-wiki answers of a minimum length are eligible