Propositional logic question for designing new proof system

Question

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

Answer 1

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)$$