Rule of Conjunction/Proof Rule

From ProofWiki
Jump to navigation Jump to search

Proof Rule

The rule of conjunction is a valid argument in types of logic dealing with conjunctions $\land$.

This includes propositional logic and predicate logic, and in particular natural deduction.


As a proof rule it is expressed in the form:

If we can conclude both $\phi$ and $\psi$, we may infer the compound statement $\phi \land \psi$.


It can be written:

$\ds {\phi \qquad \psi \over \phi \land \psi} \land_i$


Tableau Form

Let $\phi$ and $\psi$ be two well-formed formulas in a tableau proof.

The Rule of Conjunction is invoked for $\phi$ and $\psi$ in the following manner:

Pool:    The pooled assumptions of each of $\phi$ and $\psi$      
Formula:    $\phi \land \psi$      
Description:    Rule of Conjunction      
Depends on:    Both of the lines containing $\phi$ and $\psi$      
Abbreviation:    $\operatorname {Conj}$ or $\land \II$      


Explanation

The Rule of Conjunction can be expressed in natural language as:

If we can show that two statements are true, then we may build a compound statement expressing this fact, and be certain that this is also true.


Also known as

The Rule of Conjunction can also be referred to as:

  • the rule of and-introduction
  • the rule of adjunction.


Also see


Technical Note

When invoking the Rule of Conjunction in a tableau proof, use the {{Conjunction}} template:

{{Conjunction|line|pool|statement|first|second}}

or:

{{Conjunction|line|pool|statement|first|second|comment}}

where:

line is the number of the line on the tableau proof where the Rule of Conjunction is to be invoked
pool is the pool of assumptions (comma-separated list)
statement is the statement of logic that is to be displayed in the Formula column, without the $ ... $ delimiters
first is the first of the two lines of the tableau proof upon which this line directly depends
second is the second of the two lines of the tableau proof upon which this line directly depends
comment is the (optional) comment that is to be displayed in the Notes column.


Sources