Skip to main content
Share Your Experience: Take the 2024 Developer Survey
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
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
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
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
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
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
12 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 $\...
David Richerby's user avatar
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 ...
gnasher729's user avatar
  • 30.4k
10 votes
Accepted

Does Either...Or means Exclusive Or or Inclusive Or?

Don't try to force formal definitions over common english language. "Either… or" means whatever you want it to mean. There is no convention. Just be precise when you want a formal definition....
Nathaniel's user avatar
  • 15.7k
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 \...
CompuChip's user avatar
  • 203
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 ...
Yuval Filmus's user avatar
7 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 ...
Joey Eremondi's user avatar
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.'s user avatar
  • 161k
7 votes

I've heard that it isn't possible to encode product types and sum types in a simply typed lambda calculus, but it seems for me that it's false

A phrase like "it is not possible to encode product types in the simply-typed $\lambda$-calculus (without product types)" means: it is not true that for every type $A$ and type $B$, there ...
varkor's user avatar
  • 661
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 ...
Yuval Filmus's user avatar
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 ...
Dima Chubarov's user avatar
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 ...
ratchet freak's user avatar
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 ...
Joey Eremondi's user avatar
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 ...
Yuval Filmus's user avatar
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.'s user avatar
  • 161k
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 ...
Lieuwe Vinkhuijzen's user avatar
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 ...
André Souza Lemos's user avatar
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 ...
chi's user avatar
  • 14.6k
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$) ...
chi's user avatar
  • 14.6k
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 ...
Yuval Filmus's user avatar
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 ...
Kyle Jones's user avatar
  • 8,091
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 ...
Andrej Bauer's user avatar
  • 30.8k

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