1
$\begingroup$

I'm thinking since $(p \wedge \neg p)$ is a contradiction we can do this:

  1. $\;\varphi\rightarrow (p \wedge \neg p)$ --- premise
  2. $\;\bullet\quad \varphi$ --- assumption
  3. $\;\bullet\quad p \wedge \neg p$ --- $\rightarrow$ elim 1,2
  4. $\;\neg\varphi$ --- $\neg$ intro 2 - 3

Is there anything wrong with it?

$\endgroup$
  • $\begingroup$ If that is how your $\neg Intro$ rule is defined, then that is a fine proof $\endgroup$ – Bram28 Sep 19 '17 at 16:28
  • $\begingroup$ @Bram28 Problem is as far as I've seen, assumption needs to lead to a $\bot$ symbol to use $\neg$ intro rule, and to get that symbol here I'd need to use $\wedge$ elim rule to achieve p and $\neg p$ first and then introduce $\bot$ using p and $\neg p$ $\endgroup$ – Pooria Sep 19 '17 at 16:31
  • 1
    $\begingroup$ Just added that as an Answer! :) $\endgroup$ – Bram28 Sep 19 '17 at 16:32
  • $\begingroup$ @Bram28 OMG X'D $\endgroup$ – Pooria Sep 19 '17 at 16:33
2
$\begingroup$

Going by one of your earlier proofs:

Having already proved $A\vdash B$, $B\vdash C$ and $\neg C$, is this a fine proof proving $\vdash\neg A$?

it seems that $\neg Intro$ in your system requires an explicit $\bot$. So, you probably want:

  1. $\;\varphi\rightarrow (p \wedge \neg p)$ --- premise
  2. $\;\bullet\quad \varphi$ --- assumption
  3. $\;\bullet\quad p \wedge \neg p$ --- $\rightarrow$ elim 1,2
  4. $\;\bullet\quad p$ --- $\land$ elim 3
  5. $\;\bullet\quad \neg p$ --- $\land$ elim 3
  6. $\;\bullet\quad \bot$ --- $\bot$ intro 4,5
  7. $\;\neg\varphi$ --- $\neg$ intro 2 - 6
$\endgroup$
  • $\begingroup$ I just had this thought that, since $\bot$ symbol is nothing more than a $\varphi\wedge\neg\varphi$ we could omit it here, seems we should introduce $\bot$ anyway $\endgroup$ – Pooria Sep 19 '17 at 16:35
  • 2
    $\begingroup$ @Pooria Yeah, it's equivalent, but in formal proofs you need the exact symbol patterns $\endgroup$ – Bram28 Sep 19 '17 at 16:45
  • $\begingroup$ @Pooria I find it strange to say that ⊥ is nothing more than (φ∧¬φ). (φ∧¬φ) is a specific contradiction. I usually understand ⊥ as a constant false proposition, or in other words a contradiction. Every single negation of a tautology is a contradiction, so one can potentially think of ⊥ as representing any of those formulas (but only one of them at a time in a particular context). Thinking of (φ∧¬φ) as a shorthand for $\lnot$($\phi$→$\phi$) is not like thinking of ⊥ as a shorthand for $\lnot$($\phi$→$\phi$). Truth functional equivalence is not identity. $\endgroup$ – Doug Spoonwood Sep 19 '17 at 18:09
  • 1
    $\begingroup$ Right. There is a difference between statements being equivalent and statements being identical. Identity means that it is the exact same symbol string. So, $p \land q$ is equivalent to $q \land p$, but it is not identical to it. When you say that statements are the 'same', it is ambiguous whether you are talking about equivalence or identity, so it is best to just avoid that term. $\endgroup$ – Bram28 Sep 20 '17 at 13:41
  • 1
    $\begingroup$ @DougSpoonwood Perice's law is not true in intuitionistic logic :P $\endgroup$ – Kenny Lau Sep 20 '17 at 16:23
1
$\begingroup$

$$\dfrac{\varphi\rightarrow (p \land \neg p)}{\dfrac{\dfrac{\dfrac{\dfrac{[\varphi]}{p \land \neg p}{~\small\text{MP}}}{p \qquad \neg p}{~\small\land\text{E}}}{\bot}}{\neg\varphi}{~\small\neg\text{I}}}$$

$\endgroup$

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.