Question: In my textbook I have this (syntactic) definition of inconsistency:

We say that $\Sigma$ ($\subseteq\textrm{Prop}(A)$) is inconsistent if $\Sigma\vdash\bot$.

I think the intuitive definition of inconsistency is that some set $\Sigma$ of propositional formulas is inconsistent if it contains contradiction (to be more precise, if the contradiction is provable), that is if there exists a formula $p$, such that $\{p,\neg p\}\subseteq\Sigma$.

I would like to check whether the intuitive definition of consistency is consistent with the one from my text book. (:

I would do it like this:

Lets suppose that there exists a proposition $p$, such that $\{p,\neg p\}\subseteq\Sigma$. Now, among my (the ones defined in my textbook) propositional axioms I have this one $$p\rightarrow(\neg p \rightarrow \bot).$$ So by applying modus ponens to $p$ and $p\rightarrow(\neg p \rightarrow \bot)$ I infer that $$\Sigma\vdash (\neg p \rightarrow \bot).$$ Now I again apply modus ponens to $\neg p$ and $\neg p\rightarrow \bot$ and infer that $$\Sigma\vdash\bot.$$ This yields a contradiction, because one of my propositional axioms is also $\top$.

Is this a correct way to prove that those definitions are equivalent?

Thank you for your answers!

--pizet

Answer: 
Note that $\Sigma$ being inconsistent does not mean that $\Sigma$ contains $\{p,\lnot p\}$ for some $p$.

For example $\Sigma=\{p\land\lnot p\}$ is clearly inconsistent, but does not contain *two* propositions at all.

You are correct that inconsistency is the same as contradiction being provable. But as I remarked above, it is not the same thing as containing $p$ and $\lnot p$ of some formula.
As a footnote to Asaf's answer, I suspect that what the OP was after by way of an "intuitive definition" was in fact the idea that 

> 
> (A) A set of wffs $\Sigma$ is inconsistent just when there is a proposition $A$ such that $\Sigma \vdash A$ and $\Sigma \vdash \neg A$.
> 
> 
> 

And the question is how this relates to the textbook definition

> 
> (B) A set of wffs $\Sigma$ is inconsistent iff $\Sigma \vdash \bot$.
> 
> 
> 

There's a third familiar definition

> 
> (C) A set of wffs $\Sigma$ is inconsistent iff, for all wffs $A$ (of the relevant language) $\Sigma \vdash A$.
> 
> 
> 

Well, these come to just the same in a classical (and intuitionist) setting. The OP's sketched proof-idea, together with the rule that $\bot$ entails anything, can be re-used to show that (A) is equivalent to (B) and to (C). (In fancier logics, or more restricted logics these definitions can of course peel apart.)