# 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? Commented May 15, 2016 at 8:12
• As much as i know it is a well known proof system . Commented May 15, 2016 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. Commented May 15, 2016 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 ? Commented May 15, 2016 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. Commented May 15, 2016 at 10:55