In
propositional logic
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations ...
, conjunction elimination (also called ''and'' elimination, ∧ elimination, or simplification)
[Hurley] is a
valid
Validity or Valid may refer to:
Science/mathematics/statistics:
* Validity (logic), a property of a logical argument
* Scientific:
** Internal validity, the validity of causal inferences within scientific studies, usually based on experiments
** ...
immediate inference,
argument form
In logic, logical form of a statement is a precisely-specified semantic version of that statement in a formal system. Informally, the logical form attempts to formalize a possibly ambiguous statement into a statement with a precise, unambigu ...
and
rule of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
which makes the
inference
Inferences are steps in reasoning, moving from premises to logical consequences; etymologically, the word '' infer'' means to "carry forward". Inference is theoretically traditionally divided into deduction and induction, a distinction that ...
that, if the
conjunction
Conjunction may refer to:
* Conjunction (grammar), a part of speech
* Logical conjunction, a mathematical operator
** Conjunction introduction, a rule of inference of propositional logic
* Conjunction (astronomy), in which two astronomical bodies ...
''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
In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.
The alphabet of a formal language consists of s ...
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
In mathematical logic, a sequent is a very general kind of conditional assertion.
: A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n.
A sequent may have any number ''m'' of condition formulas ''Ai'' (called " antecedents") and any number ''n'' of ass ...
notation:
:
and
:
where
is a
metalogic
Metalogic is the study of the metatheory of logic. Whereas ''logic'' studies how logical systems can be used to construct valid and sound arguments, metalogic studies the properties of logical systems.Harry GenslerIntroduction to Logic Routledge, 2 ...
al symbol meaning that
is a
syntactic consequence of
and
is also a syntactic consequence of
in
logical system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A for ...
;
and expressed as truth-functional
tautologies or
theorems
In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...
of propositional logic:
:
and
:
where
and
are propositions expressed in some
formal system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A for ...
.
References
{{reflist
Rules of inference
Theorems in propositional logic
sv:Matematiskt uttryck#Förenkling