Propositional logic without rules of inference and assumptions (except MP)

Question

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 uses 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: Prove double negation introduction WITHOUT elimination, in a propositional logic axiom system.

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)

Answer 1

Note that the axiom set you listed is sound and complete for classical propositional logic. In order to add expressivity, one may use other operators such as $\lor$, $\land$ and $\leftrightarrow$.

If you don’t want to add any other axioms, then you’d need to define the other operators as a shorthand for formulas already expressible with $\to$ and $\neg$. For example, $(p \lor q):=(\neg p \to q)$, and $(p \land q):=\neg (p \to \neg q)$.

If you count using definitions as being an inference rule, then you won’t be able to actually prove the formulas with different operators in the calculus defined by the mentioned axioms. In that case, you’d have to prove the version using only negation and implication, and then operate at a meta-level to get the exact formula you want. Otherwise, you’d have to add axioms for the other operators.