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:
Γ, φ |-- ψ
Γ φ → ψ
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