I feel like I literally tried everything. I'm exhausted, and could really use some help.
I was instructed to prove some logic proposition using only the symbols $\{\rightarrow,F \}$.
Let me first describe the proof system I'm using.
It is quite long, so please bare with me, or skip ahead if the staff looks familiar to you.

The propositional proof system is the following:

The axioms (schemes) are:
$A_1: \hspace{10pt}(\varphi\rightarrow(\psi\rightarrow\varphi))$
$A_2: \hspace{10pt}((\varphi\rightarrow(\psi\rightarrow\eta))\rightarrow((\varphi\rightarrow\psi)\rightarrow(\varphi\rightarrow\eta)))$
$A_3: \hspace{10pt}(((\varphi\rightarrow F)\rightarrow F)\rightarrow\varphi)$

(I think they called Lyndon Axioms...)

The inference rule is Modus Ponens, namely; given:
We can conclude $\psi$.

As a quick example, given $\Sigma=\{F\}$ let me show how I'll prove $P$. Meaning, I'll show $\Sigma \vdash P$:

(1) $F$ (assumption)
(2) $(F\rightarrow ((P\rightarrow F)\rightarrow F))$ (instantiating $A_1$ with $\varphi=F$ and $\psi=(P\rightarrow F)$)
(3) $((P\rightarrow F)\rightarrow F)$ (Modus Ponens of (1) and (2))
(4) $(((P\rightarrow F)\rightarrow F)\rightarrow P)$ (instantiating $A_3$ with $\varphi=P$)
(5) $P$ (Modus Ponens of (3) and (4))

Now, since even trivial proofs can be insanely long and tedious, I am allowed to use the following four rules:

1. The Deduction Rule:

$\Sigma\vdash \varphi\rightarrow \psi\iff\Sigma\cup\{\varphi\}\vdash\psi$

This rule can make life much easier.
For example, using this rule, this: $\Sigma=\{A\rightarrow(B\rightarrow C)\}\vdash B\rightarrow(A\rightarrow C)$ can be proven real quick.

2. Transitive Rule:

$\{\varphi\rightarrow\psi, \psi\rightarrow \eta\}\vdash \varphi\rightarrow\eta$

Not much to say, quite an intuitive rule.

3. Contra-Positive Rule:

$\{\varphi\rightarrow\psi\}\vdash (\psi\rightarrow F)\rightarrow (\varphi\rightarrow F)$

Also a well known rule.

4. Proof by Cases:

If $\Sigma\cup\{\varphi\}\vdash \psi$ and $\Sigma\cup\{\varphi\rightarrow F\}\vdash \psi$ then $\Sigma\vdash \psi$

This is also intuitive, if you think about it...
My way of understanding it is: If you can prove something with $\varphi$ and you can also prove it with $\neg \varphi$, then it must be that you can prove it regardless of what $\varphi$ is. In some sense, it does not contribute anything.

Now, going back to my problem, this is what I need to prove:
Consider $\Sigma$:
(1) $(D\wedge \neg Y)\rightarrow H$
(2) $H\rightarrow (H\wedge D)\vee(H\wedge Y)$
(3) $\neg (D\wedge H)$
(4) $D\vee H\vee Y$

I need to prove $\Sigma\vdash Y$.

So first, I translated it to propositions over $\{\rightarrow,F\}$:

(1) $(((D\rightarrow Y)\rightarrow F)\rightarrow H)$
(2) $(H\rightarrow((H\rightarrow(D\rightarrow F))\rightarrow ((H\rightarrow(D\rightarrow Y))\rightarrow F)))$
(3) $(D\rightarrow (H\rightarrow F))$
(4) $((((D\rightarrow F)\rightarrow H)\rightarrow F)\rightarrow Y)$

Obviously, there are plenty of ways to translate this propositions, and I'm wondering if it'll be easier to prove with some other translation.

From this group of four propositions, I need to prove $Y$.
I really tried a lot of ways to attack this problem, but it seems that no matter what I try, I keep getting back to the same point - meaning inferring staff I already have as assumptions.

For example, I tried to use "Proof By Cases"; to prove that $\Sigma\cup \{H\}\vdash Y$ and also that $\Sigma\cup \{H\rightarrow F\}\vdash Y$, but this led me nowhere.
I tried to use the axioms: arbitrarily instantiating schemes to see if I can infer anything new, but this quickly became exhausting, as the propositions grew very long, very fast.
I tried to find how can the Induction Rule be used, but couldn't.
I even tried to prove this using the original $\Sigma$, and then work my way back to the $\{\rightarrow,F\}$ symbols, with no luck.
Is this really a non-trivial task, or am I missing something here?

I will very appreciate any comment, thanks for reading through this long post.

  • $\begingroup$ I would save the reduction to $\to$ until later, as that sort of stuff can be managed later on. It might help to draw a table of the 16 possible entries of $D,H,Y$ and show how $\Sigma$ leaves only rows with $Y=1$ that can be true. In particular, use (4),(3), (1), (2). I haven't solved the problem as above, but with a truth table, only rows with $Y=1$ remain. Perhaps you can see if this helps guide the proof using the above rules? $\endgroup$
    – copper.hat
    Apr 23 '15 at 23:48
  • $\begingroup$ Hi @copper.hat. Unfortunately, I must provide a syntactic proof, with no use of propositions semantic. This rules-out the use of truth table, or any inference from truth assignments... $\endgroup$ Apr 23 '15 at 23:52
  • $\begingroup$ I don't understand something in your example: Apparently, starting from the assumption of any arbitrary proposition $F$ you have proven some arbitrary other proposition $P$. That would make this inference system singularly uninteresting. What have I missed there? $\endgroup$ Apr 24 '15 at 0:11
  • $\begingroup$ $F$ is $\perp$. $\endgroup$
    – user21467
    Apr 24 '15 at 0:24
  • $\begingroup$ The purported translations of (1), (2), and (4) don't seem right. For example, the translation of (2) seems to say $H\to (H\wedge D)\vee (H\wedge D\wedge \neg Y)$ instead. $\endgroup$
    – user21467
    Apr 24 '15 at 0:32

I'd suggest proving $\Sigma\vdash D\to Y$ and $\Sigma\vdash H\to Y$ (and $\Sigma\vdash Y\to Y$), then using (4).

Here's a proof of $\Sigma\vdash D\to Y$, first in a "friendly" form, then the (fairly mechanical) translation to a form using just the tools you've listed.

Friendly form: Suppose $D$. Suppose further that not $Y$. By (1), $H$ would follow. But then $D$ and $H$ are both true, contrary to (3). Therefore our assumption that not $Y$ is false, so $Y$ is true. We supposed $D$ and proved $Y$; therefore $D\to Y$.

Using just available tools: First I show that $\Sigma\cup\{D,Y\to F\}\vdash F$. \begin{align*} &\text{a.} && D &&\text{assumption} \\ &\text{b.} && D\to(Y\to F)\to H &&\text{alternative translation of (1)} \\ &\text{c.} && (Y\to F)\to H &&\text{modus ponens, b & a} \\ &\text{d.} && Y\to F &&\text{assumption} \\ &\text{e.} && H &&\text{modus ponens, c & d} \\ &\text{f.} && D\to (H\to F) &&\text{your translation of (3)} \\ &\text{g.} && H\to F &&\text{modus ponens, f & a}\\ &\text{h.} && F &&\text{modus ponens, g & e} \end{align*}

Now we proceed:

\begin{align*} &\text{p.} & \Sigma\cup\{D,Y\to F\} &\vdash F && \text{proof above} \\ &\text{q.} & \Sigma\cup\{D\} &\vdash (Y\to F)\to F && \text{deduction theorem} \\ &\text{r.} & \Sigma\cup\{D\} &\vdash Y && \text{$A_3$ & modus ponens} \\ &\text{s.} & \Sigma &\vdash D\to Y && \text{deduction theorem} \end{align*}

  • $\begingroup$ Beautiful answer, thanks! Couple of questions though. Why am I allowed to prove $\Sigma\vdash D\rightarrow Y$ instead (of $\Sigma \vdash Y$)? It looks like a use in the Deductive Rule, but(!) $D$ is neither in my assumptions, nor can I infer it from them. Second question: When I assume $Y\rightarrow F$ and proves $F$, to what rule does this trick fall to? Thanks again, Steven, this is very helpful. $\endgroup$ Apr 24 '15 at 10:23
  • $\begingroup$ Re proving $D\to Y$ instead of $Y$: It's more that $D\to Y$ is one step towards proving $Y$, as suggested in the first paragraph. The idea is that if $D\to Y$ and $H\to Y$ (and $Y\to Y$), then $D\vee H\vee Y\to Y$. How to render that reasoning within the allowed rules, I leave to you. (It'll depend in part on your choice of translation of (4).) $\endgroup$
    – user21467
    Apr 24 '15 at 11:31
  • $\begingroup$ Re assuming $Y\to F$ and deducing $F$: I'm not sure what you're asking. There's no rule there; I just put $Y\to F$ in my context to the left of $\vdash$ and then referred to it, the same way you used $F$ in your proof that $\{F\}\vdash P$. I guess the deduction rule does come in later on, at "q"; is that what you're asking about? $\endgroup$
    – user21467
    Apr 24 '15 at 11:33
  • $\begingroup$ Yes, exactly. Thank you! $\endgroup$ Apr 24 '15 at 11:41
  • $\begingroup$ OK, I found a much faster way to prove it, I wonder if it is appropriate to post it... $\endgroup$ Apr 24 '15 at 17:59

My problem was insisting on the above translation. Although I was aware that other translations are also possible, I didn't think it will have such a dramatic effect on the proof stages. This was important since, as I mentioned above, even a seemingly trivial proof - using only the axioms - can be painful.
Another problem I had is that it didn't occur to me that there is no restriction on how many time to use the Proof by Cases in my proof, and as I will demonstrate below, that was the key.

An alternative translation to $\Sigma$ can be:
\begin{align*} &(1) &&D\rightarrow ((H\rightarrow F)\rightarrow Y)\\ &(2) &&(D\rightarrow F)\rightarrow (H\rightarrow Y)\\ &(3) &&D\rightarrow (H\rightarrow F)\\ &(4) &&(D\rightarrow F)\rightarrow ((H\rightarrow F)\rightarrow Y) \end{align*}

Using proof by cases, I'll show $\Sigma\cup\{D\}\vdash Y$ and $\Sigma\cup\{D\rightarrow F\}\vdash Y$:

Case 1: $\Sigma\cup\{D\}\vdash Y$
\begin{align*} &(5) && D && \text{assumption} \\ &(6) && H\rightarrow F && \text{MP of (3) and (5)} \\ &(7) && (H\rightarrow F)\rightarrow Y && \text{MP of (1) and (5)} \\ &(8) && Y && \text{MP of (6) and (7)} \\ \end{align*}

Case 2: $\Sigma\cup\{D\rightarrow F\}\vdash Y$
Again, using Proof By Cases, we split the case to two cases.
Denote $\Sigma\,'=\Sigma\cup \{D\rightarrow F\}$, I'll show $\Sigma\,'\cup\{H\}\vdash Y$ and $\Sigma\,'\cup\{H\rightarrow F\}\vdash Y$.

Case 2.1: $\Sigma\,'\cup\{H\}\vdash Y$
\begin{align*} &(6) && H && \text{assumption} \\ &(7) && H\rightarrow Y && \text{MP of (2) and (5)} \\ &(8) && Y && \text{MP of (6) and (7)} \\ \end{align*}

Case 2.2: $\Sigma\,'\cup\{H\rightarrow F\}\vdash Y$
\begin{align*} &(6) && H\rightarrow F && \text{assumption} \\ &(7) && (H\rightarrow F)\rightarrow Y && \text{MP of (4) and (5)} \\ &(8) && Y && \text{MP of (6) and (7)} \\ \end{align*}

Thus I conclude $\Sigma\vdash Y$.


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.