2
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.