# 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

## 1 Answer

If (a→b) is an additional axiom, then you can prove 'c' simply by substituting b with c in (a→b), and a with any axiom in (a→b), and then applying detachment to derive c.

• what do u mean by a with any axiom? , just to write a? – Barak Mi May 17 '16 at 5:47
• If you have say (a -> b) and you substitute a with axiom t, you obtain (t -> b). Thus, in order to derive c, if (a - > b) is an axiom, we could say substitute a with (a -> b) and b with c. This yields ((a -> b) -> c) as a theorem. Since (a -> b) is an axiom, by detachment we obtain c. – Doug Spoonwood May 17 '16 at 13:52