0
$\begingroup$

Let's consider the next proposition: A⇔B⊨A∨B

I used a truth table to show that there exists model1={A=False, B=False} where (A⇔B) is True but (A∨B) is False. It means A⇔B does Not entail A∨B.

Can you please suggest how to use deduction rules and what is a general mechanism to show that Statement1 does not entail Statement2?

Should I prove that (Statement1 ⊨ ¬Statement2)? Or prove that (Statement1 ∧ ¬Statement2)? And this will show that (Statement1 ⊨ Statement2) is a contradiction.

$\endgroup$
8
  • 2
    $\begingroup$ It is possible for both $S1 \models S2$ and $S1 \models \neg S2$ to be false. Proving the statements you mentioned does not disprove the proposition; using the truth table is the way to go. $\endgroup$
    – player3236
    Jan 6, 2021 at 12:27
  • 1
    $\begingroup$ When S1 and S2 are two arbitrary statements, you cannot infer one from the other, hence the "do not entail". $\endgroup$
    – player3236
    Jan 6, 2021 at 14:41
  • 1
    $\begingroup$ The whole idea of deductive rules and deductive proofs is to show that something is logically entailed by something else. Proofs can not be used to show that something is not entailed. So, you did all you could do: find a counterexample. Truth-tables are very good for that. There are some other methods as well ... but the method of doing a deductive proof isn't one of those. $\endgroup$
    – Bram28
    Jan 6, 2021 at 16:31
  • 1
    $\begingroup$ @OlegDats Fort the most part: No! But to be really clear: First: we typically make a fairly clear distinction between the methods of deductive proofs and resolution. And, you can not use a 'typical' system of deduction to demonstrate that something is satisfiable ... you can use it to show that something is not satisfiable, e.g. by deriving a contradiction from it. (continued ...) $\endgroup$
    – Bram28
    Jan 6, 2021 at 16:57
  • 1
    $\begingroup$ @OlegDats With the method of resolution things get a little more nuanced. Typically, here too, you would use resolution only to show that something is not satisfiable (by deriving an empty clause), rather than that something is satisfiable. However, since (for propositional logic), the resolution rule can only be applied a finite number of times given a finite number of finitely long statements, you could say that if you reach some point where you can not apply the rule of resolution anymore, but you haven't reached the empty clause either, then the original clause set is satisfiable. $\endgroup$
    – Bram28
    Jan 6, 2021 at 17:01

1 Answer 1

Reset to default
1
$\begingroup$

Deduction rules are used to generate formal proofs $\varphi\vdash\psi$. The existence of a formal proof implies the corresponding entailment $\varphi\models\psi$. Deduction rules cannot be used to demonstrate non-entailments. For this, you need countermodels (like the row of your truth table).

$\endgroup$
6
  • $\begingroup$ α⊨β if and only if the sentence (α∧¬β) is unsatisfiable. Do you mean there is no equivalent formal proof by contradiction for non-entailments? $\endgroup$
    – Oleg Dats
    Jan 6, 2021 at 14:32
  • $\begingroup$ Right. So $\alpha\not\models\beta$ if and only if $\alpha\land\lnot\beta$ is satisfiable. How do you show a sentence is satisfiable? You exhibit a model (in propositional logic, this is a satisfying assignment of truth values to the basic propositions). $\endgroup$
    – Alex Kruckman
    Jan 6, 2021 at 15:04
  • $\begingroup$ Be careful not to mix levels here. You can use a proof by contradiction in a formal proof system to prove the negation of a sentence. But "$\alpha\not\models\beta$" is not a sentence, it's a statement of the meta-level (a statement of ordinary mathematics, not formalized mathematics like the sentences of propositional logic). Of course you can use a proof by contradiction at the meta-level to prove such a statement. But this would not be a proof "using deduction rules". $\endgroup$
    – Alex Kruckman
    Jan 6, 2021 at 15:10
  • $\begingroup$ If I show that 𝛼∧¬𝛽 is satisfiable then I prove 𝛼⊭𝛽. A⇔B⊨A∨B becomes (A⇔B)∧¬(A∨B). CNF form: (A∨¬B)∧(¬A∨B)∧¬A∧¬B. This statement is the SAT. End of proof. Correct? $\endgroup$
    – Oleg Dats
    Jan 6, 2021 at 16:18
  • $\begingroup$ I don't know what "this statement is the SAT" means. $\endgroup$
    – Alex Kruckman
    Jan 6, 2021 at 16:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.