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:

and

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

Formal notation

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

and

where is a metalogical symbol meaning that is a syntactic consequence of and is also a syntactic consequence of in logical system;

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

and

where and are propositions expressed in some formal system.

gollark: But they don't.
gollark: I would be fine with C if people actually used it for small amounts of low-level stuff you can audit very well.
gollark: Well, you could argue it's with people using C for odd things.
gollark: OpenSSL had Heartbleed for ages. They have competent programmers, and yet this issue - which a more memory safe language could not easily have - persisted for ages.
gollark: A good language should be safe *automatically*, and actually *warn* you about things.

References

  1. David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley. Sect.3.1.2.1, p.46
  2. Copi and Cohen
  3. Moore and Parker
  4. Hurley
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.