Editing Propositional calculus (section)

==Proof systems==
{{See also|Proof theory|Proof calculus}}
Proof systems in propositional logic can be broadly classified into ''semantic proof systems'' and ''syntactic proof systems'',<ref  name="ms59"/><ref name="ms37"/><ref name="ms38"/> according to the kind of [[logical consequence]] that they rely on: semantic proof systems rely on semantic consequence (<math>\varphi \models \psi</math>),<ref name="ms39"/> whereas syntactic proof systems rely on syntactic consequence (<math>\varphi \vdash \psi</math>).<ref name="ms40"/> Semantic consequence deals with the truth values of propositions in all possible interpretations, whereas syntactic consequence concerns the derivation of conclusions from premises based on rules and axioms within a formal system.<ref name=":16"/> This section gives a very brief overview of the kinds of proof systems, with [[Anchor (HTML)|anchors]] to the relevant sections of this article on each one, as well as to the separate Wikipedia articles on each one.

===Semantic proof systems===
{{Image frame|content=<math>\begin{array}{|c|c|c|c|}
x_0 & x_1 & \bar{x_1} & x_0 \& \bar{x_1} \\
\hline
0 & 0 & 1 & 0 \\
0 & 1 & 0 & 0 \\
1 & 0 & 1 & 1 \\
1 & 1 & 0 & 0
\end{array}</math>
|width=200|align=right|caption=Example of a [[truth table]]}}
[[File:Partially built tableau.svg|thumb|200px|A graphical representation of a partially built [[Method of analytic tableaux|propositional tableau]]]]
Semantic proof systems rely on the concept of semantic consequence, symbolized as <math>\varphi \models \psi</math>, which indicates that if <math>\varphi</math> is true, then <math>\psi</math> must also be true in every possible interpretation.<ref name=":16" />

====Truth tables====
{{Main article|Truth table}}
A [[truth table]] is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.<ref name="ms41"/> By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.<ref name=":27"/> See {{section link||Semantic proof via truth tables}}.

====Semantic tableaux====
{{Main article|Method of analytic tableaux}}
A [[semantic tableau]] is another semantic proof technique that systematically explores the truth of a proposition.<ref name="ms42"/> It constructs a tree where each branch represents a possible interpretation of the propositions involved.<ref name="ms43"/> If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered a [[Tautology (logic)|tautology]].<ref name=":13"/> See {{section link||Semantic proof via tableaux}}.

===Syntactic proof systems===
[[File:LK groupe logique.png|300px|right|thumb|Rules for the propositional [[sequent calculus]] LK, in [[Gerhard Gentzen|Gentzen]] notation]]
Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence, <math>\varphi \vdash \psi</math>, signifies that <math>\psi</math> can be derived from <math>\varphi</math> using the rules of the formal system.<ref name=":16" />

====Axiomatic systems====
{{Main article|Axiomatic system (logic)}}
An [[axiomatic system]] is a set of axioms or assumptions from which other statements (theorems) are logically derived.<ref name="ms44"/> In propositional logic, axiomatic systems define a base set of propositions considered to be self-evidently true, and theorems are proved by applying deduction rules to these axioms.<ref name="ms45"/> See {{section link||Syntactic proof via axioms}}.

====Natural deduction====
{{Main article|Natural deduction}}
[[Natural deduction]] is a syntactic method of proof that emphasizes the derivation of conclusions from premises through the use of intuitive rules reflecting ordinary reasoning.<ref name=":14"/> Each rule reflects a particular logical connective and shows how it can be introduced or eliminated.<ref name=":14" /> See {{section link||Syntactic proof via natural deduction}}.

====Sequent calculus====
{{Main article|Sequent calculus}}
The [[sequent calculus]] is a formal system that represents logical deductions as sequences or "sequents" of formulas.<ref name=":15"/> Developed by [[Gerhard Gentzen]], this approach focuses on the structural properties of logical deductions and provides a powerful framework for proving statements within propositional logic.<ref name=":15" /><ref name="ms46"/>