Propositional logic question for designing new proof system Try to solve question from Logic in Computer Science 2nd by  Huth & Ryan
Natural deduction is not the only possible formal framework for proofs in propositional
logic. As an abbreviation, we write Γ to denote any finite sequence of
formulas φ1, φ2, . . . , φn (n ≥ 0). Thus, any sequent may be written as Γ  ψ for
an appropriate, possibly empty, Γ. In this exercise we propose a different notion
of proof, which states rules for transforming valid sequents into valid sequents.
For example, if we have already a proof for the sequent Γ, φ  ψ, then we obtain
a proof of the sequent Γ  φ → ψ by augmenting this very proof with one
application of the rule →i. The new approach expresses this as an inference rule
between sequents:
Γ, φ |-- ψ
------------- →i.
Γ  φ → ψ
The rule ‘assumption’ is written as
φ  φ
assumption
i.e. the premise is empty. Such rules are called axioms.
(a) Express all remaining proof rules of (^,~,~~)in such a form. (Hint: some
of your rules may have more than one premise.)
(b) Explain why proofs of Γ  ψ in this new system have a tree-like structure
with Γ  ψ as root.
(c) Prove p ∨ (p ∧ q)  p in your new proof system.
Can anyone guide me write rules for ^,~,~~.I will be gratefull
 A: I prefer to write the rules with the symbol : $\vdash$ for derivability always explicit.
Thus, the above rule is :


$$\frac{\Gamma, \varphi \vdash \psi }{\Gamma \vdash \varphi \rightarrow \psi} \quad (\rightarrow-i)$$


They are the rules of Natural Deduction in "sequent calculus-style" and you can find them for example in Jan von Plato, Elements of Logical Reasoning (2013), page 65 :


$$\frac{\Gamma, \vdash \varphi }{\Gamma \vdash \varphi \lor \psi} \quad (\lor-i_1)$$
$$\frac{\Gamma \vdash \psi }{\Gamma \vdash \varphi \lor \psi} \quad (\lor-i_2)$$
$$\frac{\Gamma \vdash \varphi \quad \Gamma \vdash \psi}{\Gamma \vdash \varphi \land \psi} \quad (\land-i)$$
$$\frac{\Gamma, \varphi \vdash \psi \quad \Gamma, \varphi \vdash \lnot \psi}{\Gamma \vdash \lnot \varphi} \quad (\lnot-i)$$


and the corresponding elimination rules :


$$\frac{\Gamma \vdash \varphi \rightarrow \psi }{\Gamma, \varphi \vdash \psi} \quad (\rightarrow-e)$$
$$\frac{\Gamma, \varphi \vdash \tau \quad \Gamma, \psi \vdash \tau \quad \Gamma \vdash  \varphi \lor \psi}{\Gamma \vdash \tau} \quad (\lor-e)$$
$$\frac{\Gamma \vdash \varphi \land \psi }{\Gamma \vdash \varphi} \quad (\land-e_1)$$
$$\frac{\Gamma \vdash \varphi \land \psi }{\Gamma \vdash \psi} \quad (\land-e_2)$$
$$\frac{\Gamma \vdash \lnot \lnot \varphi }{\Gamma \vdash \varphi} \quad (\lnot-e)$$


