Prove that propositional Aczel slash is closed under deduction

63 Views Asked by At

I have already proved that $ \Gamma |\phi \Rightarrow \Gamma \vdash_{IPC} \phi $.

On the other hand, I have tried to prove the other side. I used induction on the length of the proof.(I used natural deduction without RAA rule). But I could not prove it for the or-elimination rule.

Propositional Aczel slash:

$ \Gamma | P \equiv \Gamma \vdash_{IPC} P \text{ for prime sentences P} $

$ \Gamma | \phi_{1} \land \phi_{2} \equiv \Gamma | \phi_{1} \text{ and } \Gamma |\phi_{2} $

$ \Gamma | \phi_{1} \lor \phi_{2} \equiv \Gamma | \phi_{1} \text{ or } \Gamma |\phi_{2} $

$ \Gamma | \phi_{1} \rightarrow \phi_{2} \equiv \Gamma \vdash_{IP} \phi_{1} \rightarrow \phi_{2} \text{ and, if }\Gamma | \phi_{1} \text{ then } \Gamma |\phi_{2} $

or-elimination: or-elimination

Please help me for the case of or-elimination.