Conjunction elimination

In propositional logic, conjunction elimination (also called and elimination, ∧ elimination,^[1] or simplification)^[2]^[3]^[4] is a valid immediate inference, argument form and rule of inference which makes the inference that, if the conjunction A and B is true, then A is true, and B is true. The rule makes it possible to shorten longer proofs by deriving one of the conjuncts of a conjunction on a line by itself.

An example in English:

It's raining and it's pouring.

Therefore it's raining.

The rule consists of two separate sub-rules, which can be expressed in formal language as:

{\frac {P\land Q}{\therefore P}}

and

{\frac {P\land Q}{\therefore Q}}

The two sub-rules together mean that, whenever an instance of " $P\land Q$ " appears on a line of a proof, either " $P$ " or " $Q$ " can be placed on a subsequent line by itself. The above example in English is an application of the first sub-rule.

Formal notation[edit]

The conjunction elimination sub-rules may be written in sequent notation:

(P\land Q)\vdash P

and

(P\land Q)\vdash Q

where $\vdash$ is a metalogical symbol meaning that $P$ is a syntactic consequence of $P\land Q$ and $Q$ is also a syntactic consequence of $P\land Q$ in logical system;

and expressed as truth-functional tautologies or theorems of propositional logic:

(P\land Q)\to P

and

(P\land Q)\to Q

where $P$ and $Q$ are propositions expressed in some formal system.

References[edit]

^ David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley. Sect.3.1.2.1, p.46
^ Copi and Cohen^{[citation needed]}
^ Moore and Parker^{[citation needed]}
^ Hurley^{[citation needed]}

[1] David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley. Sect.3.1.2.1, p.46

[2] Copi and Cohen^{[citation needed]}

[3] Moore and Parker^{[citation needed]}

[4] Hurley^{[citation needed]}

[1]

[2]

[3]

[4]

anhducwiki

Saturday, July 25, 2020