Editing Rule of inference (section)

== Formalisms ==
Various formalisms or [[proof system]]s have been suggested as distinct ways of codifying reasoning and demonstrating the validity of arguments. Unlike different systems of logic, these formalisms do not impact what can be proven; they only influence how proofs are formulated. Influential frameworks include [[natural deduction]] systems, [[Hilbert systems]], and [[sequent calculi]].<ref>{{multiref | {{harvnb|Nederpelt|Geuvers|2014|pp=[https://books.google.com/books?id=orsrBQAAQBAJ&pg=PA159 159–162]}} | {{harvnb|Sørensen|Urzyczyn|2006|pp=[https://books.google.com/books?id=_mtnm-9KtbEC&pg=PA161 161–162]}} }}</ref>

Natural deduction systems aim to reflect how people naturally reason by introducing many intuitive rules of inference to make logical derivations more accessible. They break complex arguments into simple steps, often using subproofs based on temporary premises. The rules of inference in natural deduction target specific logical operators, governing how an operator can be added with introduction rules or removed with elimination rules. For example, the rule of [[conjunction introduction]] asserts that one can infer <math>P \land Q</math> from the premises <math>P</math> and <math>Q</math>, thereby producing a conclusion with the conjunction operator from premises that do not contain it. Conversely, the rule of [[conjunction elimination]] asserts that one can infer <math>P</math> from <math>P \land Q</math>, thereby producing a conclusion that no longer includes the conjunction operator. Similar rules of inference are [[disjunction introduction]] and [[Disjunction elimination|elimination]], [[implication introduction]] and [[Implication elimination|elimination]], [[negation introduction]] and [[Negation elimination|elimination]], and [[biconditional introduction]] and [[Biconditional elimination|elimination]]. As a result, systems of natural deduction usually include many rules of inference.<ref>{{multiref | {{harvnb|Pelletier|Hazen|2024|loc=Lead section, § 2.2 Modern Versions of Jaśkowski's Method, § 5.1 Normalization of Intuitionistic Logic}} | {{harvnb|Nederpelt|Geuvers|2014|pp=[https://books.google.com/books?id=orsrBQAAQBAJ&pg=PA159 159–162]}} | {{harvnb|Copi|Cohen|Flage|2016|p=244}} }}</ref>{{efn|The [[Fitch notation]] is an influential way of presenting proofs in natural deduction systems.<ref>{{harvnb|Akiba|2024|p=[https://books.google.com/books?id=ftksEQAAQBAJ&pg=PA7 7]}}</ref>}}

Hilbert systems, by contrast, aim to provide a minimal and efficient framework of logical reasoning by including as few rules of inference as possible. Many Hilbert systems only have ''modus ponens'' as the sole rule of inference. To ensure that all theorems can be deduced from this minimal foundation, they introduce [[Axiom schema|axiom schemes]].<ref>{{multiref | {{harvnb|Bacon|2023|pp=[https://books.google.com/books?id=qa3WEAAAQBAJ&pg=PA423 423–424]}} | {{harvnb|Nederpelt|Geuvers|2014|pp=[https://books.google.com/books?id=orsrBQAAQBAJ&pg=PA159 159–162]}} | {{harvnb|Sørensen|Urzyczyn|2006|pp=[https://books.google.com/books?id=_mtnm-9KtbEC&pg=PA161 161–162]}} }}</ref> An axiom scheme is a template to create axioms or true statements. It uses metavariables, which are placeholders that can be replaced by specific terms or formulas to generate an infinite number of true statements.<ref>{{multiref | {{harvnb|Reynolds|1998|p=[https://books.google.com/books?id=X_ToAwAAQBAJ&pg=PA12 12]}} | {{harvnb|Cook|2009|p=26}} }}</ref> For example, propositional logic can be defined with the following three axiom schemes: (1) <math>P \to (Q \to P)</math>, (2) <math>(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))</math>, and (3) <math>(\lnot P \to \lnot Q) \to (Q \to P)</math>.<ref>{{harvnb|Smullyan|2014|pp=[https://books.google.com/books?id=n6S-AwAAQBAJ&pg=PA102 102–103]}}</ref> To formulate proofs, logicians create new statements from axiom schemes and then apply ''modus ponens'' to these statements to derive conclusions. Compared to natural deduction, this procedure tends to be less intuitive since its heavy reliance on symbolic manipulation can obscure the underlying logical reasoning.<ref>{{multiref | {{harvnb|Metcalfe|Paoli|Tsinakis|2023|pp=[https://books.google.com/books?id=CkPsEAAAQBAJ&pg=PA36 36–37]}} | {{harvnb|Nederpelt|Geuvers|2014|pp=[https://books.google.com/books?id=orsrBQAAQBAJ&pg=PA159 159–162]}} | {{harvnb|Sørensen|Urzyczyn|2006|pp=[https://books.google.com/books?id=_mtnm-9KtbEC&pg=PA161 161–162]}} }}</ref>

[[Sequent calculi]], another approach, introduce [[sequent]]s as formal representations of arguments. A sequent has the form <math>A_1 , \dots , A_m \vdash B_1, \dots , B_n</math>, where <math>A_i</math> and <math>B_i</math> stand for propositions. Sequents are conditional assertions stating that at least one <math>B_i</math> is true if all <math>A_i</math> are true. Rules of inference operate on sequents to produce additional sequents. Sequent calculi define two rules of inference for each logical operator: one to introduce it on the left side of a sequent and another to introduce it on the right side. For example, through the rule for introducing the operator <math>\lnot</math> on the left side, one can infer <math>\lnot R, P \vdash Q</math> from <math>P \vdash Q, R</math>. The [[cut rule]], an additional rule of inference, makes it possible to simplify sequents by removing certain propositions.<ref>{{multiref | {{harvnb|Rathjen|Sieg|2024|loc=§ 2.2 Sequent Calculi}} | {{harvnb|Sørensen|Urzyczyn|2006|pp=[https://books.google.com/books?id=_mtnm-9KtbEC&pg=PA161 161–165]}} }}</ref>