55

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 inside A. Their junction is not counted because it is inside A but not outside B. OR means it is covered by either one or both. Both of them cover the part of A ...


46

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 \land \top = A. $$


37

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 promise says nothing about what I might do if you fail to do $A$. In fact, I might do $B$ anyhow, and that would not make me a liar. For instance, suppose your ...


30

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 inconsistent, then proof by contradiction is problematic. But this is not the case at all. If logic is inconsistent then proof by contradiction is still very much ...


22

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 is not correct'.


16

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 used in mathematics is that of material implication, which in particular assigns a true value to any vacuous implication. One could of course use a different ...


16

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 specifically about formal logic can present a warped picture of what logic is. The issue is that most of the time when mathematicians talk about "logic", they (...


13

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 or piece of paper and point. Yes, ~~R is equivalent to R.


10

"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 take "If the sun is green then the grass is green". In the long form it is translated to "If the sun is green then I claim that the grass is green; if the sun is ...


9

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 something you have to assume. Formal verification doesn't eliminate all assumptions; it just helps you be clearer about what you are assuming, and maybe helps ...


8

You could just construct the truth tables for the two formulas: there are only three variables, so the tables are only eight lines. Use de Morgan's laws, distributivity and so on to rearrange one formula into the other. Use similar techniques to show that $[P\rightarrow (Q\rightarrow R)] \leftrightarrow [(P\wedge Q)\to R]$ is equivalent to true. Use similar ...


8

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 \to R), (P \lor Q) \vdash R$$ So let's assume $A \lor (A \land \neg B)$. Set $P = A$, $Q = A \land \neg B$, $R = A$ and apply the rule: If $P$ ($= A$) we are ...


8

There are many interesting philosophical points that your post touches on. Consistency of Boolean logic The issue of consistency of proof theory in classical logic isn't as dire as you make it out to be. It basically reduces to the following: We can define Boolean logic as a collection of logical operations functions on the truth values 1 and 0. But how ...


6

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 notation this can be written as $P1 \Rightarrow P2 $. The stronger the proposition the harder it usually is to prove. On the other hand, if proven it provides more ...


6

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 states that any element of $x$ that satisfies $P$ must be equal to $a$. It doesn't claim anything about elements not satisfying $P$. If $b$ doesn't satisfy $P$ ...


6

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 have not been able to prove your intuition. You cannot prove a definition! What you are really saying is that the concept of mutual exclusion is vacuous if no ...


6

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 logic a particular programming language represents. In particular, Haskell lacks dependent types. That means that it can't express statements with "forall x" or "...


5

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 ambiguity you mention. Operator precedences can be used for implicit parenthesisation. You seem to be asking if there are agreed-upon operator precedences in logic. ...


5

TSP is actually OptP-complete and so are many other optimization problems, including Knapsack, MAX-SAT, 0-1 Integer Linear Programming. This class and proof technique is largely the work of Mark Krentel; orig paper STC'86. The journal version of the paper has more details, including the fact that OptP is subclass of FPNP. LEX-MIN-SAT, finding the ...


5

You are not doing anything "wrong", you just missed the point of the incompleteness theorem, a bit. What you claim (correctly) is that a proof system with no axioms is incomplete. You also say that this is not very impressive... What Godel showed is something much stronger: consider the theory of Peano arithmetic, then there does not exist a complete ...


5

You have to understand that this is a convention. Conjunctions and disjunctions are supposed to be applied to formulas. Sometimes we want to keep things general, so that we may have to allow "empty disjunctions" and "empty conjunctions", and to that purpose we define what they are. Here is one way to see why this convention is used. Let us consider a binary ...


5

Given $P$, $Q$ and $(P \to Q) \to R$, there is no way to apply modus ponens. You would need to have $(P \to Q)$. If you had $P$, $Q$ and $P \to (Q \to R)$, then you could apply modus ponens twice the way you did, but $P \to (Q \to R)$ and $(P \to Q) \to R$ are different. $P \to (Q \to R)$ says “if I have P, then if I have Q, then I can get R”. $(P \to Q) \...


5

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 subroutine. For example, consider the following set of propositions: $$P = \{v_1, v_3 \vee v_2, v_1 \wedge v_3\} $$ A minimum set of axioms from this set is $\{...


5

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 which we are by no means innocent), neither has anything to do with reality, experienced or imagined, and with the idea of truth that is dealt with by empirical ...


5

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 $\varphi$ true also make $\psi$ true. This is the case iff $\vDash \varphi\Rightarrow\psi$, i.e., if the formula $\varphi\Rightarrow\psi$ is true in all ...


5

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 clause. Both $k$-CNF and $k$-DNF are efficiently, properly PAC learnable, when $k$ is constant. In contrast, as far as I am aware, it is not known whether CNF ...


5

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 efficiently decide the validity of any formula $G$ as follows. Take $A$ to be any atom not in $G$. Craft $F := \lnot (G \land (\top \lor A))$, and use $M$ to decide ...


5

"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 result is what pushes the algorithm out of P. In addition it is possible to create a subformula that you cannot simplify that way. For example a formula that is ...


5

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$) back. In your case, $C = A \land \lnot B$ and $D = A$, and the implication trivially holds.


5

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 your types are advanced enough to capture logic, then there's no algorithm which takes in a type and outputs a program of that type, if it exists. Just like ...


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