# Proving general proposition using HPC

If I have a general Proposition $c$ in HPC + another axiom that $(a \rightarrow b)$. HPC axioms - $$1 .a \rightarrow (b \rightarrow a)$$. $$2. (a \rightarrow (b \rightarrow c))\rightarrow ((a\rightarrow b)\rightarrow (a\rightarrow c))$$. $$3. ((\neg b\rightarrow \neg a)\rightarrow (a\rightarrow b))$$.

And I want to show that a general proposition $c$ is always true. Should I write a proof using the axioms in HPC that the conclusion is $c$? (I mean like 1.AXIOM 2.AXIOM .3blabla ... -- > c) or using true tables somehow?

Thanks!

• What is "HPC"? Your textbook's name for a paricular proof system? – Henning Makholm May 15 '16 at 8:12
• As much as i know it is a well known proof system . – Barak Mi May 15 '16 at 8:13
• x @Barak: The system may or may not be well known, but the name you're using for it is not. Names for proof systems are very not standardized, and each author tends to invent his own. If you want the reader of your question to know what you're talking about, you need to describe the proof system in your question, rather than just quoting a pithy name for it. – Henning Makholm May 15 '16 at 8:16
• Ok, my bad but still i just want to figure what's the principles for showing that each statement can be true in some proof system. writing a proof using the axioms of the particular system and show that the statement is true ? – Barak Mi May 15 '16 at 8:32
• Tho show that a proposition $c$ is a theorem of the theory having $a \to b$ as single (non-logical) axioms you have to write a derivation, i.e. a list where every formula either is an axiom (logical and non-logical) or can be inferred by modus ponens from previous formulae in the list. – Mauro ALLEGRANZA May 15 '16 at 10:55