Is it possible to prove that $p\to q$ from these axioms and theorems? My professor insists this is possible, I say it isn't.  What say you?

Certain theorems and axioms have been established or assumed.
Axiom 1: $p\rightarrow {\sim y}$
Axiom 2: ${\sim q}\rightarrow r$
Theorem 1: $p\rightarrow {\sim z}$
Theorem 2: $x\rightarrow \text{either }q\text{ or }z$
Theorem 3: $r\rightarrow \text{either }x\text{ or }y$
Prove, in outline form, that $p\rightarrow q$.  

 A: Direct proof (that is, not by contradiction)
\begin{equation}
\begin{split}
\textrm{ (1.1) }& \textrm{  for Theorem 2: }& \sim z \rightarrow \sim x \textrm{ or } (x \textrm{ and } q)\\ 
\textrm{ (1.2) }& \textrm{  for Theorem 1 and (1.1): }& p \rightarrow \sim x \textrm{ or } (x \textrm{ and } q)\\ 
\textrm{ (2.1) }& \textrm{ for (1.2) and Axiom 1: }&  p \rightarrow (\sim x \textrm{ and } \sim y) \textrm{ or } (x \textrm{ and } q  \textrm{ and } \sim y) \\
\textrm{ (3.1) }& \textrm{ for Theorem 3: }&  \sim x \textrm{ and } \sim y \rightarrow  \sim r\\
\textrm{ (3.2) }& \textrm{ }&  x \textrm{ and } q  \textrm{ and } \sim y \rightarrow  q\\
\textrm{ (3.3) }& \textrm{ for (2.1), (3.1), and (3.2): }& p \rightarrow \sim r \textrm{ or }q \\
\textrm{ (4.1) }& \textrm{ for Axiom 2: }& \sim r \rightarrow q \\
\textrm{ (4.2) }& \textrm{ for (3.3) and (4.1): }& p \rightarrow q \\
\end{split}
\end{equation}
A: Yes it is possible. Assume that $p\to q$ is false that is $p\wedge \neg q$ is true.


*

*(hyp) $p\wedge \neg q$.

*(1. and Axiom 1) $p\wedge (p\to \neg y)\implies \neg y$ 

*(1. and Axiom 2) $\neg q\wedge (\neg q\to r)\implies r$ 

*(2., 3. and Theorem 3)    $r\wedge \neg y\wedge (r\to x \oplus y)\implies x$

*(1., 4. and Theorem 2)    $x\wedge \neg q \wedge (x\to q \oplus z)\implies z$

*(5. and Theorem 1)    $z\wedge  (z\to \neg p)\implies \neg p$

*(1. and 6.) $p\wedge \neg p$ (contradiction)
Hence $p\to q$ is proved. 
P.S. $\wedge$  is the AND operator, $\neg$ is the NOT operator and $\oplus$ is the EXCLUSIVE OR operator.
A: Assuming that 


*

*the axioms are using the arrow and tilde to mean implication and negation respectively and that

*the axioms establish four primitive constants $p,\,y,\,q,\,r$ and that

*the theorems treat $x$ and $z$ as variables which can take on the values of any of the four primitive constants


then by Theorem 1


*

*$p \rightarrow\neg p$

*$p \rightarrow\neg\neg p\rightarrow p$

*$p \rightarrow\neg y$

*$p \rightarrow\neg\neg y\rightarrow y$

*$p \rightarrow\neg r$

*$p \rightarrow\neg\neg r\rightarrow r$

*$p \rightarrow\neg q$

*$p \rightarrow\neg\neg q\rightarrow q$


Of course, only this last implication is needed.
