I was wondering whether it would be possible to do propositional logic without any rules of inference and assumptions (except modus ponens).


I have the following axioms:


1. $ p \to (q \to p) $
2. $ (p \to (q \to r)) \to ((p \to q) \to (p \to r)) $
3. $ (\lnot p \to \lnot q) \to (q \to p) $
4. MP: From $ p $ and $ p \to q $, infer $ q $.


The other connectives ($ \lor $ and $ \land $) are defined like this:


$ p \lor q := \lnot p \to q $


$ p \land q := \lnot (p \to \lnot q) $


For example, [double negation](https://en.wikipedia.org/wiki/Double_negation#Proofs) uses [hypothetical syllogism](https://en.wikipedia.org/wiki/Hypothetical_syllogism): from $ p \to q $ and $ q \to r $, infer $ p \to r $.


Moreover, I can't find proofs for (or prove myself) common rules of inference in natural deduction, such as:


* $ (p \to q) \to (\lnot q \to \lnot p) $
* $ p \to \lnot \lnot p $
* $ p \to (p \lor q) $
* $ (p \land q) \to p $
* $ ((p \to q) \land (q \to r)) \to (p \to r) $


My question is whether it is possible to not use rules of inference and assumptions (except MP) in propositional logic, or that you can't prove these statements without them.


I found this question, but it does not have any answers yet: <https://math.stackexchange.com/questions/2468217/prove-double-negation-introduction-without-elimination-in-a-propositional-logic>


Example proof
-------------


I hope this clarifies some things, here's something that I managed to prove:


1. $ p \to ( p \to p ) $ (Axiom 1)
2. $ p \to ( ( p \to p ) \to p ) $ (Axiom 1)
3. $ ( p \to ( ( p \to p ) \to p ) ) \to ( ( p \to ( p \to p ) ) \to ( p \to p ) ) $ (Axiom 2)
4. $ ( p \to ( p \to p ) ) \to ( p \to p ) $ (MP 2, 3)
5. $ p \to p $ (MP 1, 4)



Propositional logic without rules of inference and assumptions (except MP)
I'll do one of them, $p \to (p \vee q)$.  

**Define** $a \vee b$ as $\lnot b \to a$.


We want to prove
$$
p \to (p \vee q) .
$$
This is now merely alternate notation for
$$
p \to (\lnot q \to p) .
$$
But this is an instance of Axiom 1.


