Propositional calculus

The following table shows the main notational variants for each of the connectives in propositional logic.

Within works by Frege[26] and Bertrand Russell,[27] are ideas influential to the invention of truth tables.

The actual tabular structure (being formatted as a table), itself, is generally credited to either Ludwig Wittgenstein or Emil Post (or both, independently).

[26] Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole, Charles Sanders Peirce,[28] and Ernst Schröder.

Others credited with the tabular structure include Jan Łukasiewicz, Alfred North Whitehead, William Stanley Jevons, John Venn, and Clarence Irving Lewis.

[2] Propositional logic deals with statements, which are defined as declarative sentences having truth value.

[35][36] In English, these connectives are expressed by the words "and" (conjunction), "or" (disjunction), "not" (negation), "if" (material conditional), and "if and only if" (biconditional).

[40] So, in classical logic, the argument is valid, although it may or may not be sound, depending on the meteorological facts in a given context.

This formal language is the basis for proof systems, which allow a conclusion to be derived from premises if, and only if, it is a logical consequence of them.

If we assume that the validity of modus ponens has been accepted as an axiom, then the same § Example argument can also be depicted like this: This method of displaying it is Gentzen's notation for natural deduction and sequent calculus.

[46][45] In this case, the conclusion follows syntactically because the natural deduction inference rule of modus ponens has been assumed.

, ..., a formula of propositional logic is defined recursively by these definitions:[2][14][50][i] Writing the result of applying

[57][58][59] Other authors also include these symbols, with the same meaning, but consider them to be "zero-place truth-functors",[37] or equivalently, "nullary connectives".

[62] In other respects, the following formal semantics can apply to the language of any propositional logic, but the assumptions that there are only two semantic values (bivalence), that only one of the two is assigned to each formula in the language (noncontradiction), and that every formula gets assigned a value (excluded middle), are distinctive features of classical logic.

[51][68] An interpretation of a formal language for classical logic is often expressed in terms of truth tables.

Regardless, an equivalence or biconditional is true if, and only if, the formulas connected by it are assigned the same semantic value under every interpretation.

Other authors often do not make this distinction, and may use the word "equivalence",[15] and/or the symbol ⇔,[78] to denote their object language's biconditional connective.

Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules.

[92] An axiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived.

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.

[82][83][84] For instance, this table shows that "p → (q ∨ r → (r → ¬p))" is not valid:[49] The computation of the last column of the third line may be displayed as follows:[49] Further, using the theorem that

[102][103] Since truth tables have 2n lines for n variables, they can be tiresomely long for large values of n.[39] Analytic tableaux are a more efficient, but nevertheless mechanical,[70] semantic proof method; they take advantage of the fact that "we learn nothing about the validity of the inference from examining the truth-value distributions which make either the premises false or the conclusion true: the only relevant distributions when considering deductive validity are clearly just those which make the premises true or the conclusion false.

"[39] Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below.

The § Gentzen notation, which was covered earlier for a short argument, can actually be stacked to produce large tree-shaped natural deduction proofs[43][15]—not to be confused with "truth trees", which is another name for analytic tableaux.

[43] Lastly, there is the only notation style which will actually be used in this article, which is due to Patrick Suppes,[43] but was much popularized by E.J.

[38] The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.

[38] Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,[38] and MTT and DN are commonly given rules,[109] although they are not primitive.

[112] This section gives the axioms of some historically notable axiomatic systems for propositional logic.

Although axiomatic proof has been used since the famous Ancient Greek textbook, Euclid's Elements of Geometry, in propositional logic it dates back to Gottlob Frege's 1879 Begriffsschrift.

Hence, using Greek letters to represent schemata (metalogical variables that may stand for any well-formed formulas), the axioms are given as:[37][116] The schematic version of P2 is attributed to John von Neumann,[112] and is used in the Metamath "set.mm" formal proof database.