# sentential logic derivations?

• Nov 19th 2009, 11:06 AM
cosmopolitanx
sentential logic derivations?
how do i prove the following is a theorem in SD
[(A -> B)->A]->A
... i started off by assuming [(A -> B)->A] then assume ~A to try to derive A in the end... but now i'm stuck :(

and also:

Suppose we dropped from SD the rule for vE, and adopted in its place the rule of Disjunctive Syllogism (DS), thus giving a modified system SD. Show that
you can derive the SD rule for vE in SD.

I have no idea how to even approach the second question.. any help would be greatly appreciated.. thanks! :D
• Nov 19th 2009, 12:46 PM
clic-clac
Hi

Do you already have SD theorems?

I didn't find an easy solution (but I'm not good at this), some way to do:

$\displaystyle ((A\rightarrow B)\rightarrow A)\vdash (\neg A\rightarrow \neg(A\rightarrow B))$ .... (contraposition) and $\displaystyle \neg A\vdash\neg A$ .... (axiom)

$\displaystyle \neg A, ((A\rightarrow B)\rightarrow A)\vdash \neg(A\rightarrow B)$ .... (with $\displaystyle \rightarrow_e$ )

$\displaystyle \neg (A\rightarrow B)\vdash (A\wedge \neg B)$ .... ( $\displaystyle (A\rightarrow B)\leftrightarrow (\neg A\vee B)$ and de Morgan's laws)

$\displaystyle \neg (A\rightarrow B)\vdash A\$ .... (with $\displaystyle \wedge_e$ )

So we have $\displaystyle \neg A, ((A\rightarrow B)\rightarrow A)\vdash A$ and $\displaystyle \neg A\vdash\neg A$

Hence $\displaystyle \neg A, ((A\rightarrow B)\rightarrow A)\vdash\bot$ .... (with contraction and $\displaystyle \neg_e$ )

And from there you can conclude. But if you cannot use de Morgan's laws, contraposition and some stuff, it will take some time.
• Nov 19th 2009, 01:20 PM
emakarov
Hello,

I'll look into this, but first I have a statement and a question.

Statement: Unfortunately, in logic there are many different but equivalent ways to define many concepts. E.g., one can take \/, /\, -> and _|_ (falsehood) as primitive connectives, or take only -> and _|_ and consider the rest of the connectives as abbreviations. To make things worse, there are at least three general ways to define proofs: one (Hilbert's style) deals with formulas and has only inference rule but many axioms, the second (Natural Deduction) also deals with formulas but has many rules and no axioms, and the third (Sequent Calculus) deals with sets of formulas and also has many rules and no axioms. Therefore, if you look at ten different logic textbooks, you will probably find ten different notations, primitive connectives, inference rules, etc., though in the end they all give equivalent logics.

Question: What are the inference rules that were given to you? Is it Natural Deduction (ND)? ND has introduction and elimination rules for each connective, and it has open and closed assumptions. You mentioned \/E (disjunction elimination rule); does it look like this?
Code:

A    B

A \/ B      C    C
----------------------
C

The proof that you are looking for depends a lot on the definition of the proof, i.e., inference rules.

Edit1: Also, what exactly is Disjunctive Syllogism?
Edit2: Grammar.

Evgeny
• Nov 19th 2009, 03:01 PM
Soroban
Hello, cosmopolitanx!

I'm not familiar with the term "SD".
I can solve it symbolically.

We need some theorems for referencer:

. . $\displaystyle (P \to Q) \;=\; (\sim\!P \vee Q)$ . . . Alternate definition of Implication (ADI)

. . $\displaystyle [1]\;P\: \vee \sim\!P \;=\;t$

. . $\displaystyle [2]\; P \wedge t \;=\;P$

. . $\displaystyle [3]\;P \vee t \;=\;t$

Quote:

Prove: .$\displaystyle \bigg[(A \to B) \to A\bigg] \to A$

. . $\displaystyle \begin{array}{ccc}\bigg[(A \to B) \to A\bigg] \to A && \text{Given} \\ \\ \bigg[(\sim\!A \vee B) \to A\bigg] \to A && \text{ADI} \\ \\ \bigg[\sim(\sim\!A \vee B) \vee A\bigg] \to A && \text{ADI}\end{array}$

. . $\displaystyle \begin{array}{cccc} \bigg[(A \:\wedge \sim\!B) \vee A\bigg] \to A && \text{DeMorgan} \\ \\ \sim\bigg[(A \;\wedge \sim\!B) \vee A\bigg] \vee A && \text{ADI} \\ \\ \bigg[\sim(A \:\wedge \sim\!B) \:\wedge \sim\!A\bigg] \vee A && \text{DeMorgan} \end{array}$

. . $\displaystyle \begin{array}{ccccc} \bigg[(\sim\!A \vee B) \:\wedge \sim\!A\bigg] \vee A && \text{DeMorgan} \\ \\ \bigg[(\sim\!A \vee B) \vee A\bigg] \wedge \bigg[\sim\!A \vee A\bigg] && \text{Distributive} \\ \\ \bigg[(\sim\!A \vee B) \vee A\bigg] \wedge t && [1] \\ \\ (\sim\!A \vee B) \vee A && [2] \end{array}$

. . . . . . . $\displaystyle \begin{array}{cccccc} (\sim\!A \vee A) \vee B &&&&& \text{Comm/Assoc} \\ \\ t \vee B &&&&& [1] \\ \\ t &&&&& [3] \end{array}$

• Nov 19th 2009, 03:27 PM
xalk
Quote:

Originally Posted by cosmopolitanx
how do i prove the following is a theorem in SD
[(A -> B)->A]->A
... i started off by assuming [(A -> B)->A] then assume ~A to try to derive A in the end... but now i'm stuck :(

and also:

Suppose we dropped from SD the rule for vE, and adopted in its place the rule of Disjunctive Syllogism (DS), thus giving a modified system SD. Show that
you can derive the SD rule for vE in SD.

I have no idea how to even approach the second question.. any help would be greatly appreciated.. thanks! :D

You started correctly by assuming [(A->B)->A] and then ~A.

Now [(A ->B)->A] IS equivalent to :~A ->~(A ->B) ,by contrapositive law.
From that formula and ~A ,by using M.Ponens you get :

~(A ->B) .

From that formula by using De Morgan and the fact that (A ->B) IS equivalent to (~AvB) you have:

A and ~B .

From that formula and by using addition elimination you get:

A