# Questions tagged [propositional-logic]

The tag has no usage guidance.

204 questions
Filter by
Sorted by
Tagged with
13k views

### Why is A implies B true if A is false and B is false?

It seems to me that the 'implies' in English language does not mean the same thing as the logical operator 'implies', in a similar way how 'OR' word in most cases means 'Exclusive OR' in our everyday ...
• 818
4k views

### Why is $A \lor (A \land \neg B) \equiv A$?

I would like to know if there is a rule to prove this. For example, if I use the distributive law I will get only $(A \lor A) \land (A \lor \neg B)$.
• 229
6k views

### Can proof by contradiction work without the law of excluded middle?

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
• 3,040
4k views

### Why does soundness imply consistency?

I was reading the question Consistency and completeness imply soundness? and the first statement in it says: I understand that soundness implies consistency. Which I was quite puzzled about ...
• 3,040
4k views

• 153
854 views

### What is the connection between combinatorial circuits and finite state automata?

The diagram on the Wikipedia page of FSA shows the hierarchy of the computational devices, in that diagram it is denoted that the finite state machines are superior to the combinatorial circuits. ...
256 views

### How to find a minimum set of axioms within a set of propositions?

I have a set of propositions, for example $\{a_1,a_2,\dots,a_n\}$. Some propositions depend on others (for example, $a_1,a_2\Rightarrow a_3$, means if $a_1,a_2$ are true, then $a_3$ is true). I want ...
• 153
516 views

133 views

### Tseitin formula on 2-connected graph

How can we prove that for $\\\\$ every $\\\\$ 2-connected graph G with an odd number of vertices, the unsatisfiable Tseitin formula for it is minimally unsatisfiable, that is, if we remove even a ...
465 views

### A Quine–McCluskey variant for conjunctive normal form?

There is the Quine–McCluskey algorithm for finding a minimal expression of a boolean expression in dis-junctive normal form. Would applying DeMorgan's rule to the minimal DNF result in the minimal CNF?...
• 141
265 views

• 131
1k views

### Why is SAT based on the CNF?

I have been reading up on Boolean logic and, specifically, the Boolean satisfiability problem. I have seen several people mention that the expression must be converted to conjunctive normal form (CNF) ...
• 133
393 views

### 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

Of course, it isn't possible to construct them directly since we hasn't these type constructors, but only function constructor (arrow). But suppose there are 2 types $A$ and $B$, from which we need to ...
2k views

### Is it necessary to learn how to prove Mathematical theorems as a CS Student? [closed]

I've just started my undergraduate course and have tried my hands on MIT's OpenCourseWare on Discrete Math on Logic and Proofs. There was a particular question asking to prove Cantor's Theorem: ...
• 21
3k views

### Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable? If this is the case, why is ...
• 469
41 views

### Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$

I was reading "Open Logic book", "Sequent Calculus". Given the fact that all antecedents must hold for at least one succedent to hold, I can't get rid off the impression that using ...
• 123
57 views

### Does it hold that $F \equiv \sigma(F)$ for a CNF formula $F$ and a permutation $\sigma$ s.t. $F \vDash \sigma(F)$?

Suppose we have a CNF formula $F$ and a permutation $\sigma$ of its literals such that for any literal $x, \sigma(\neg x)=\neg \sigma(x)$ and $F \vDash \sigma(F)$. Does it hold that \$F \equiv \sigma(...
• 332