0
$\begingroup$

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!

$\endgroup$
7
  • $\begingroup$ What is "HPC"? Your textbook's name for a paricular proof system? $\endgroup$
    – hmakholm left over Monica
    Commented May 15, 2016 at 8:12
  • $\begingroup$ As much as i know it is a well known proof system . $\endgroup$
    – Barak Mi
    Commented May 15, 2016 at 8:13
  • $\begingroup$ 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. $\endgroup$
    – hmakholm left over Monica
    Commented May 15, 2016 at 8:16
  • $\begingroup$ 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 ? $\endgroup$
    – Barak Mi
    Commented May 15, 2016 at 8:32
  • $\begingroup$ 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. $\endgroup$
    – Mauro ALLEGRANZA
    Commented May 15, 2016 at 10:55

1 Answer 1

Reset to default
0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ what do u mean by a with any axiom? , just to write a? $\endgroup$
    – Barak Mi
    Commented May 17, 2016 at 5:47
  • $\begingroup$ 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. $\endgroup$
    – Doug Spoonwood
    Commented May 17, 2016 at 13:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .