# Propositional Logic proof of $\land$ and $\lor$

I am trying to work out some basic logic stuff and currently am working with this, given 1 unary operator, denoted $\neg$ and one binary, denoted $\implies$, with the following rules given $$\neg\neg a=a$$ $$a\implies b = \neg b\implies \neg a$$ $$a\implies(b\implies c)=(a\implies b)\implies(a\implies c)$$ $$a=b\implies a$$

I set out to prove the properties of $\land$ and $\lor$ defined as $a\land b=\neg(a\implies \neg b)$ and $a\lor b=\neg a\implies b$. I am working here on purely symbolic manipulations and considering "truth values" now wouldn't sate it because then we are adding some intepritations of this. Of course I am using the ordinary symbols now because it eases reading and shows what my intent is. So please do not go on about truth values.

Now what I have done is proven that $\land$ and $\lor$ are commutative and De Morgans laws, but when I try associative or distributive I am comming to a grinding halt. I have attacked it from left or right parenthesis but can't get it to go anywhere. I got $$(a\lor b)\lor c = \neg(\neg a\implies b)\implies c$$ $$= \neg c\implies(\neg a\implies b)$$ $$= (\neg c\implies\neg a)\implies (\neg c\implies b)$$ $$= (a \implies c)\implies (\neg c\implies b)$$

and quite frankly I don't know where to go here. I might need some smaller lemmas but I don't know which. As said I am trying to build it up from those basics for fun and thinking but I am stuck here.

• I suppose that $=$ means the bi-conditional (also: $\equiv$). If so, $a = b \to a$ is $(a \equiv b) \to a$ or $a \equiv (b \to a)$ ? They are not valid: with $a$ and $b$ both false, the first formula boils down to $T \to F$, which is false, while the second is $F \equiv (F \to F)$ which again is false. – Mauro ALLEGRANZA Oct 22 '17 at 18:50
• I your proof, you have to move from $\lnot c \to (\lnot a \to b)$ to $\lnot a \to (\lnot c \to b)$ equiv to: $\lnot a \to (c \lor b)$ equiv to: $\lnot a \to (b \lor c)$ equiv to: $a \lor (b \lor c)$. – Mauro ALLEGRANZA Oct 22 '17 at 18:58
• A collection of lemmas for your calculus into: E.Mendelson, Introduction to ML. – Mauro ALLEGRANZA Oct 22 '17 at 19:00
• @MauroALLEGRANZA Again, you are assuming traditional intepritation when you say "both false", which is not what I am doing here. – Zelos Malum Oct 23 '17 at 3:22