Propositional calculus
The propositional calculus^{}
Unlike firstorder logic, propositional logic does not deal with nonlogical objects, predicates about them, or quantifiers. However, all the machinery of propositional logic is included in firstorder logic and higherorder logics. In this sense, propositional logic is the foundation of firstorder logic and higherorder logic.
Propositional logic is typically studied with a formal language, in which propositions are represented by letters, which are called propositional variables. These are then used, together with symbols for connectives, to make compound propositions. Because of this, the propositional variables are called atomic formulas of a formal zerothorder language.^{[10]}^{[2]} While the atomic propositions are typically represented by letters of the alphabet,^{[10]} there is a variety of notations to represent the logical connectives. The following table shows the main notational variants for each of the connectives in propositional logic.
Connective  Symbol 

AND  , , , , 
equivalent  , , 
implies  , , 
NAND  , , 
nonequivalent  , , 
NOR  , , 
NOT  , , , 
OR  , , , 
XNOR  
XOR  , 
The most thoroughly researched branch of propositional logic is classical truthfunctional propositional logic,^{[1]} in which formulas are interpreted as having precisely one of two possible truth values, the truth value of true or the truth value of false.^{[15]} The principle of bivalence and the law of excluded middle are upheld. By comparison with firstorder logic, truthfunctional propositional logic is considered to be zerothorder logic.^{[4]}^{[5]}
History
Although propositional logic (also called propositional calculus) had been hinted by earlier philosophers, it was developed into a formal logic (
Within works by Frege^{}
Sentences
Propositional logic, as currently studied in universities, is a specification of a standard of logical consequence in which only the meanings of propositional connectives are considered in evaluating the conditions for the truth of a sentence, or whether a sentence logically follows from some other sentence or group of sentences.^{[2]}
Declarative sentences
Propositional logic deals with statements, which are defined as declarative sentences having truth value.^{[25]}^{[1]} Examples of statements might include:
 Wikipedia is a free online encyclopedia that anyone can edit.
 London is the capital of England.
 All Wikipedia editors speak at least three languages.
Declarative sentences are contrasted with questions, such as "What is Wikipedia?", and imperative statements, such as "Please add citations to support the claims in this article.".^{[26]}^{[27]} Such nondeclarative sentences have no truth value,^{[28]} and are only dealt with in nonclassical logics, called erotetic and imperative logics.
Compounding sentences with connectives
In propositional logic, a statement can contain one or more other statements as parts.^{[1]} Compound sentences are formed from simpler sentences and express relationships among the constituent sentences.^{[29]} This is done by combining them with logical connectives:^{[29]}^{[30]} the main types of compound sentences are negations, conjunctions, disjunctions, implications, and biconditionals,^{[29]} which are formed by using the corresponding connectives to connect propositions.^{[31]}^{[32]} In English, these connectives are expressed by the words "and" (conjunction), "or" (disjunction), "not" (negation), "if" (material conditional), and "if and only if" (biconditional).^{[1]}^{[9]} Examples of such compound sentences might include:
 Wikipedia is a free online encyclopedia that anyone can edit, and millions already have. (conjunction)
 It is not true that all Wikipedia editors speak at least three languages. (negation)
 Either London is the capital of England, or London is the capital of the United Kingdom, or both. (disjunction)^{[b]}
If sentences lack any logical connectives, they are called simple sentences,^{[1]} or atomic sentences;^{[30]} if they contain one or more logical connectives, they are called compound sentences,^{[29]} or molecular sentences.^{[30]}
Sentential connectives are a broader category that includes logical connectives.^{[2]}^{[30]} Sentential connectives are any linguistic particles that bind sentences to create a new compound sentence,^{[2]}^{[30]} or that inflect a single sentence to create a new sentence.^{[2]} A logical connective, or propositional connective, is a kind of sentential connective with the characteristic feature that, when the original sentences it operates on are (or express) propositions, the new sentence that results from its application also is (or expresses) a proposition.^{[2]} Philosophers disagree about what exactly a proposition is,^{[6]}^{[2]} as well as about which sentential connectives in natural languages should be counted as logical connectives.^{[30]}^{[2]} Sentential connectives are also called sentencefunctors,^{[33]} and logical connectives are also called truthfunctors.^{[33]}
Arguments
An argument is defined as a pair of things, namely a set of sentences, called the premises,^{[c]} and a sentence, called the conclusion.^{[34]}^{[30]}^{[33]} The conclusion is claimed to follow from the premises,^{[33]} and the premises are claimed to support the conclusion.^{[30]}
Example argument
The following is an example of an argument within the scope of propositional logic:
 Premise 1: If it's raining, then it's cloudy.
 Premise 2: It's raining.
 Conclusion: It's cloudy.
The logical form of this argument is known as modus ponens,^{[35]} which is a classically valid form.^{[36]} 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 example argument will be reused when explaining § Formalization.
Validity and soundness
An argument is valid if, and only if, it is necessary that, if all its premises are true, its conclusion is true.^{[34]}^{[37]}^{[38]} Alternatively, an argument is valid if, and only if, it is impossible for all the premises to be true while the conclusion is false.^{[38]}^{[34]}
Validity is contrasted with soundness.^{[38]} An argument is sound if, and only if, it is valid and all its premises are true.^{[34]}^{[38]} Otherwise, it is unsound.^{[38]}
Logic, in general, aims to precisely specify valid arguments.^{[30]} This is done by defining a valid argument as one in which its conclusion is a logical consequence of its premises,^{[30]} which, when this is understood as semantic consequence, means that there is no case in which the premises are true but the conclusion is not true^{[30]} – see § Semantics below.
Formalization
Propositional logic is typically studied through a
Propositional variables
Since propositional logic is not concerned with the structure of propositions beyond the point where they cannot be decomposed any more by logical connectives,^{[35]}^{[1]} it is typically studied by replacing such atomic (indivisible) statements with letters of the alphabet, which are interpreted as variables representing statements (propositional variables).^{[1]} With propositional variables, the § Example argument would then be symbolized as follows:
 Premise 1:
 Premise 2:
 Conclusion:
When P is interpreted as "It's raining" and Q as "it's cloudy" these symbolic expressions correspond exactly with the original expression in natural language. Not only that, but they will also correspond with any other inference with the same logical form.
When a formal system is used to represent formal logic, only statement letters (usually capital roman letters such as , and ) are represented directly. The natural language propositions that arise when they're interpreted are outside the scope of the system, and the relation between the formal system and its interpretation is likewise outside the formal system itself.
Gentzen notation
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.^{[39]} The premises are shown above a line, called the inference line,^{[11]} separated by a comma, which indicates combination of premises.^{[40]} The conclusion is written below the inference line.^{[11]} The inference line represents syntactic consequence,^{[11]} sometimes called deductive consequence,^{[41]} which is also symbolized with ⊢.^{[42]}^{[41]} So the above can also be written in one line as .^{[d]}
Syntactic consequence is contrasted with semantic consequence,^{[43]} which is symbolized with ⊧.^{[42]}^{[41]} In this case, the conclusion follows syntactically because the natural deduction inference rule of modus ponens has been assumed. For more on inference rules, see the sections on proof systems below.
Language
Part of Formal languages 
The language (commonly called )^{[41]}^{[44]}^{[30]} of a propositional calculus is defined in terms of:^{[2]}^{[10]}
 a set of primitive symbols, called atomic formulas, atomic sentences,^{[35]}^{[30]} atoms,^{[45]} placeholders, prime formulas,^{[45]} proposition letters, sentence letters,^{[35]} or variables, and
 a set of operator symbols, called connectives,^{[14]}^{[1]}^{[46]} logical connectives,^{[1]} logical operators,^{[1]} truthfunctional connectives,^{[1]} truthfunctors,^{[33]} or propositional connectives.^{[2]}
A wellformed formula is any atomic formula, or any formula that can be built up from atomic formulas by means of operator symbols according to the rules of the grammar. The language , then, is defined either as being identical to its set of wellformed formulas,^{[44]} or as containing that set (together with, for instance, its set of connectives and variables).^{[10]}^{[30]}
Usually the syntax of is defined recursively by just a few definitions, as seen next; some authors explicitly include parentheses as punctuation marks when defining their language's syntax,^{[30]}^{[47]} while others use them without comment.^{[2]}^{[10]}
Syntax
Given a set of atomic propositional variables , , , ..., and a set of propositional connectives , , , ..., , , , ..., , , , ..., a formula of propositional logic is defined recursively by these definitions:^{[2]}^{[10]}^{[46]}^{[e]}
 Definition 1: Atomic propositional variables are formulas.
 Definition 2: If is a propositional connective, and A, B, C, … is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applying to A, B, C, … is a formula.
 Definition 3: Nothing else is a formula.
Writing the result of applying to A, B, C, … in functional notation, as (A, B, C, …), we have the following as examples of wellformed formulas:
What was given as Definition 2 above, which is responsible for the composition of formulas, is referred to by Colin Howson as the principle of composition.^{[35]}^{[f]} It is this recursion in the definition of a language's syntax which justifies the use of the word "atomic" to refer to propositional variables, since all formulas in the language are built up from the atoms as ultimate building blocks.^{[2]} Composite formulas (all formulas besides atoms) are called molecules,^{[45]} or molecular sentences.^{[30]} (This is an imperfect analogy with chemistry, since a chemical molecule may sometimes have only one atom, as in monatomic gases.)^{[45]}
The definition that "nothing else is a formula", given above as Definition 3, excludes any formula from the language which is not specifically required by the other definitions in the syntax.^{[33]} In particular, it excludes infinitely long formulas from being wellformed.^{[33]}
CF grammar in BNF
An alternative to the syntax definitions given above is to write a contextfree (CF) grammar for the language in BackusNaur form (BNF).^{[49]}^{[50]} This is more common in computer science than in philosophy.^{[50]} It can be done in many ways,^{[49]} of which a particularly brief one, for the common set of five connectives, is this single clause:^{[50]}^{[51]}
This clause, due to its selfreferential nature (since is in some branches of the definition of ), also acts as a recursive definition, and therefore specifies the entire language. To expand it to add modal operators, one need only add … to the end of the clause.^{[50]}
Constants and schemata
Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition,^{[52]} while propositional variables range over the set of all atomic propositions.^{[52]} Schemata, or schematic letters, however, range over all formulas.^{[33]}^{[1]} (Schematic letters are also called metavariables.)^{[34]} It is common to represent propositional constants by A, B, and C, propositional variables by P, Q, and R, and schematic letters are often Greek letters, most often φ, ψ, and χ.^{[33]}^{[1]}
However, some authors recognize only two "propositional constants" in their formal system: the special symbol , called "truth", which always evaluates to True, and the special symbol , called "falsity", which always evaluates to False.^{}
Semantics
To serve as a model of the logic of a given
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.^{[56]}^{[59]}^{[33]} To learn about nonclassical logics with more than two truthvalues, and their unique semantics, one may consult the articles on "Manyvalued logic", "Threevalued logic", "Finitevalued logic", and "Infinitevalued logic".
Interpretation (case) and argument
For a given language , an interpretation,^{}
For distinct propositional symbols there are distinct possible interpretations. For any particular symbol , for example, there are possible interpretations: either is assigned T, or is assigned F. And for the pair , there are possible interpretations: either both are assigned T, or both are assigned F, or is assigned T and is assigned F, or is assigned F and is assigned T.^{[64]} Since has , that is,
Where is an interpretation and and represent formulas, the definition of an argument, given in § Arguments, may then be stated as a pair , where is the set of premises and is the conclusion. The definition of an argument's validity, i.e. its property that , can then be stated as its absence of a counterexample, where a counterexample is defined as a case in which the argument's premises are all true but the conclusion is not true.^{[30]}^{[35]} As will be seen in § Semantic truth, validity, consequence, this is the same as to say that the conclusion is a semantic consequence of the premises.
Propositional connective semantics
An interpretation assigns semantic values to atomic formulas directly.^{[60]}^{[30]} Molecular formulas are assigned a function of the value of their constituent atoms, according to the connective used;^{[60]}^{[30]} the connectives are defined in such a way that the truthvalue of a sentence formed from atoms with connectives depends on the truthvalues of the atoms that they're applied to, and only on those.^{[60]}^{[30]} This assumption is referred to by Colin Howson as the assumption of the truthfunctionality of the connectives.^{[35]}
Semantics via truth tables
Logical connectives  



Related concepts  
Applications  
Category  
Since logical connectives are defined semantically only in terms of the truth values that they take when the propositional variables that they're applied to take either of the two possible truth values,^{[1]}^{[30]} the semantic definition of the connectives is usually represented as a truth table for each of the connectives,^{[1]}^{[30]}^{[65]} as seen below:
p  q  p ∧ q  p ∨ q  p → q  p ↔ q  ¬p  ¬q 

T  T  T  T  T  T  F  F 
T  F  F  T  F  F  F  T 
F  T  F  T  T  F  T  F 
F  F  F  F  T  T  T  T 
This table covers each of the main five logical connectives:^{[9]}^{[10]}^{[11]}^{[12]} conjunction (here notated p ∧ q), disjunction (p ∨ q), implication (p → q), biconditional (p ↔ q) and negation, (¬p, or ¬q, as the case may be). It is sufficient for determining the semantics of each of these operators.^{[1]}^{[66]}^{[30]} For more truth tables for more different kinds of connectives, see the article "Truth table".
Semantics via assignment expressions
Some authors (viz., all the authors cited in this subsection) write out the connective semantics using a list of statements instead of a table. In this format, where is the interpretation of , the five connectives are defined as:^{[33]}^{[47]}
 if, and only if,
 if, and only if, and
 if, and only if, or
 if, and only if, it is true that, if , then
 if, and only if, it is true that if, and only if,
Instead of , the interpretation of may be written out as ,^{[33]}^{[67]} or, for definitions such as the above, may be written simply as the English sentence " is given the value ".^{[47]} Yet other authors^{[68]}^{[69]} may prefer to speak of a Tarskian model for the language, so that instead they'll use the notation , which is equivalent to saying , where is the interpretation function for .^{[69]}
Connective definition methods
Some of these connectives may be defined in terms of others: for instance, implication, p → q, may be defined in terms of disjunction and negation, as ¬p ∨ q;^{[70]} and disjunction may be defined in terms of negation and conjunction, as ¬(¬p ∧ ¬q).^{[47]} In fact, a truthfunctionally complete system,^{[h]} in the sense that all and only the classical propositional tautologies are theorems, may be derived using only disjunction and negation (as Russell, Whitehead, and Hilbert did),^{[2]} or using only implication and negation (as Frege did),^{[2]} or using only conjunction and negation,^{[2]} or even using only a single connective for "not and" (the Sheffer stroke),^{[3]}^{[2]} as Jean Nicod did.^{[2]} A joint denial connective (logical NOR) will also suffice, by itself, to define all other connectives,^{[47]} but no other connectives have this property.^{[47]}
Some authors, namely Howson^{[35]} and Cunningham,^{[72]} distinguish equivalence from the biconditional. (As to equivalence, Howson calls it "truthfunctional equivalence", while Cunningham calls it "logical equivalence".) Equivalence is symbolized with ⇔ and is a metalanguage symbol, while a biconditional is symbolized with ↔ and is a logical connective in the object language . 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",^{[11]} and/or the symbol ⇔,^{[73]} to denote their object language's biconditional connective.
Semantic truth, validity, consequence
Given and as
 Truthinacase:^{[30]} A sentence of is true under an interpretation if assigns the truth value T to .^{[62]}^{[64]} If is true under , then is called a model of .^{[64]}
 Falsityinacase:^{[30]} is false under an interpretation if, and only if, is true under .^{[64]}^{[74]}^{[30]} This is the "truth of negation" definition of falsityinacase.^{[30]} Falsityinacase may also be defined by the "complement" definition: is false under an interpretation if, and only if, is not true under .^{[62]}^{[64]} In classical logic, these definitions are equivalent, but in nonclassical logics, they are not.^{[30]}
 Semantic consequence: A sentence of is a semantic consequence () of a sentence if there is no interpretation under which is true and is not true.^{[62]}^{[64]}^{[30]}
 Valid formula (tautology): A sentence of is logically valid (),^{[j]} or a tautology,^{[75]}^{[76]}^{[47]} if it is true under every interpretation,^{[62]}^{[64]} or true in every case.^{[30]}
 Consistent sentence: A sentence of is consistent if it is true under at least one interpretation. It is inconsistent if it is not consistent.^{[62]}^{[64]} An inconsistent formula is also called selfcontradictory,^{[1]} and said to be a selfcontradiction,^{[1]} or simply a contradiction,^{[77]}^{[78]}^{[79]} although this latter name is sometimes reserved specifically for statements of the form .^{[1]}
For interpretations (cases) of , these definitions are sometimes given:
 Complete case: A case is complete if, and only if, either is truein or is truein, for any in .^{[30]}^{[80]}
 Consistent case: A case is consistent if, and only if, there is no in such that both and are truein.^{[30]}^{[81]}
For classical logic, which assumes that all cases are complete and consistent,^{[30]} the following theorems apply:
 For any given interpretation, a given formula is either true or false under it.^{[64]}^{[74]}
 No formula is both true and false under the same interpretation.^{[64]}^{[74]}
 is true under if, and only if, is false under ;^{[64]}^{[74]} is true under if, and only if, is not true under .^{[64]}
 If and are both true under , then is true under .^{[64]}^{[74]}
 If and , then .^{[64]}
 is true under if, and only if, either is not true under , or is true under .^{[64]}
 if, and only if, is logically valid, that is, if, and only if, .^{[64]}^{[74]}
Proof systems
Proof systems in propositional logic can be broadly classified into semantic proof systems and syntactic proof systems,^{[82]}^{[83]}^{[84]} according to the kind of logical consequence that they rely on: semantic proof systems rely on semantic consequence (),^{[85]} whereas syntactic proof systems rely on syntactic consequence ().^{}
Semantic proof systems
Semantic proof systems rely on the concept of semantic consequence, symbolized as , which indicates that if is true, then must also be true in every possible interpretation.^{[87]}
Truth tables
A truth table is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.^{[88]} By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.^{[89]} See § Semantic proof via truth tables.
Semantic tableaux
A
Syntactic proof systems
Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence, , signifies that can be derived from using the rules of the formal system.^{[87]}
Axiomatic systems
An axiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived.^{[92]} In propositional logic, axiomatic systems define a base set of propositions considered to be selfevidently true, and theorems are proved by applying deduction rules to these axioms.^{[93]} See § Syntactic proof via axioms.
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.^{[94]} Each rule reflects a particular logical connective and shows how it can be introduced or eliminated.^{[94]} See § Syntactic proof via natural deduction.
Sequent calculus
The sequent calculus is a formal system that represents logical deductions as sequences or "sequents" of formulas.^{[95]} 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.^{[95]}^{[96]}
Semantic proof via truth tables
Taking advantage of the semantic concept of validity (truth in every interpretation), it is possible to prove a formula's validity by using a truth table, which gives every possible interpretation (assignment of truth values to variables) of a formula.^{[89]}^{[45]}^{[33]} If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation).^{[89]}^{[45]} Further, if (and only if) is valid, then is inconsistent.^{[77]}^{[78]}^{[79]}
For instance, this table shows that "p → (q ∨ r → (r → ¬p))" is not valid:^{[45]}
p  q  r  q ∨ r  r → ¬p  q ∨ r → (r → ¬p)  p → (q ∨ r → (r → ¬p)) 

T  T  T  T  F  F  F 
T  T  F  T  T  T  T 
T  F  T  T  F  F  F 
T  F  F  F  T  T  T 
F  T  T  T  T  T  T 
F  T  F  T  T  T  T 
F  F  T  T  T  T  T 
F  F  F  F  T  T  T 
The computation of the last column of the third line may be displayed as follows:^{[45]}
p  →  (q  ∨  r  →  (r  →  ¬  p)) 

T  →  (F  ∨  T  →  (T  →  ¬  T)) 
T  →  (  T  →  (T  →  F  ))  
T  →  (  T  →  F  )  
T  →  F  
F  
T  F  F  T  T  F  T  F  F  T 
Further, using the theorem that if, and only if, is valid,^{[64]}^{[74]} we can use a truth table to prove that a formula is a semantic consequence of a set of formulas: if, and only if, we can produce a truth table that comes out all true for the formula (that is, if ).^{[97]}^{[98]}
Semantic proof via tableaux
Since truth tables have 2^{n} lines for n variables, they can be tiresomely long for large values of n.^{[35]} Analytic tableaux are a more efficient, but nevertheless mechanical,^{[65]} semantic proof method; they take advantage of the fact that "we learn nothing about the validity of the inference from examining the truthvalue 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."^{[35]}
Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below.^{[47]} These rules use "signed formulas", where a signed formula is an expression or , where is a (unsigned) formula of the language .^{[47]} (Informally, is read " is true", and is read " is false".)^{[47]} Their formal semantic definition is that "under any interpretation, a signed formula is called true if is true, and false if is false, whereas a signed formula is called false if is true, and true if is false."^{[47]}
In this notation, rule 2 means that yields both , whereas branches into . The notation is to be understood analogously for rules 3 and 4.^{[47]} Often, in tableaux for classical logic, the signed formula notation is simplified so that is written simply as , and as , which accounts for naming rule 1 the "Rule of Double Negation".^{[35]}^{[65]}
One constructs a tableau for a set of formulas by applying the rules to produce more lines and tree branches until every line has been used, producing a complete tableau. In some cases, a branch can come to contain both and for some , which is to say, a contradiction. In that case, the branch is said to close.^{[35]} If every branch in a tree closes, the tree itself is said to close.^{[35]} In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself selfcontradictory, and therefore false.^{[35]} Conversely, a tableau can also prove that a logical formula is tautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.^{[35]}
To construct a tableau for an argument , one first writes out the set of premise formulas, , with one formula on each line, signed with (that is, for each in the set);^{[65]} and together with those formulas (the order is unimportant), one also writes out the conclusion, , signed with (that is, ).^{[65]} One then produces a truth tree (analytic tableau) by using all those lines according to the rules.^{[65]} A closed tree will be proof that the argument was valid, in virtue of the fact that if, and only if, is inconsistent (also written as ).^{[65]}
List of classically valid argument forms
Using semantic checking methods, such as truth tables or semantic tableaux, to check for tautologies and semantic consequences, it can be shown that, in classical logic, the following classical argument forms are semantically valid, i.e., these tautologies and semantic consequences hold.^{[33]} We use ⟚ to denote equivalence of and , that is, as an abbreviation for both and ;^{[33]} as an aid to reading the symbols, a description of each formula is given. The description reads the symbol ⊧ (called the "double turnstile") as "therefore", which is a common reading of it,^{[33]}^{[99]} although many authors prefer to read it as "entails",^{[33]}^{[100]} or as "models".^{[101]}
Name  Sequent  Description 

Modus Ponens

^{[30]}  If p then q; p; therefore q 
Modus Tollens

^{[30]}  If p then q; not q; therefore not p 
Hypothetical Syllogism

^{[34]}  If p then q; if q then r; therefore, if p then r 
Disjunctive Syllogism  ^{[102]}  Either p or q, or both; not p; therefore, q 
Constructive Dilemma  ^{[34]}  If p then q; and if r then s; but p or r; therefore q or s 
Destructive Dilemma  If p then q; and if r then s; but not q or not s; therefore not p or not r  
Bidirectional Dilemma  If p then q; and if r then s; but p or not s; therefore q or not r  
Simplification  ^{[30]}  p and q are true; therefore p is true 
Conjunction  ^{[30]}  p and q are true separately; therefore they are true conjointly 
Addition  ^{[30]}^{[102]}  p is true; therefore the disjunction (p or q) is true 
Composition  If p then q; and if p then r; therefore if p is true then q and r are true  
De Morgan's Theorem (1)  ⟚ ^{[30]}  The negation of (p and q) is equiv. to (not p or not q) 
De Morgan's Theorem (2)  ⟚ ^{[30]}  The negation of (p or q) is equiv. to (not p and not q) 
Commutation (1)  ⟚ ^{[102]}  (p or q) is equiv. to (q or p) 
Commutation (2)  ⟚ ^{[102]}  (p and q) is equiv. to (q and p) 
Commutation (3)  ⟚ ^{[102]}  (p iff q) is equiv. to (q iff p) 
Association (1)  ⟚ ^{[35]}  p or (q or r) is equiv. to (p or q) or r 
Association (2)  ⟚ ^{[35]}  p and (q and r) is equiv. to (p and q) and r 
Distribution (1)  ⟚ ^{[102]}  p and (q or r) is equiv. to (p and q) or (p and r) 
Distribution (2)  ⟚ ^{[102]}  p or (q and r) is equiv. to (p or q) and (p or r) 
Double Negation

⟚ ^{[30]}^{[102]}  p is equivalent to the negation of not p 
Transposition

⟚ ^{[30]}  If p then q is equiv. to if not q then not p 
Material Implication  ⟚ ^{[102]}  If p then q is equiv. to not p or q 
Material Equivalence (1)

⟚ ^{[102]}  (p iff q) is equiv. to (if p is true then q is true) and (if q is true then p is true) 
Material Equivalence (2)

⟚ ^{[102]}  (p iff q) is equiv. to either (p and q are true) or (both p and q are false) 
Material Equivalence (3)

⟚  (p iff q) is equiv to., both (p or not q is true) and (not p or q is true) 
Exportation  ^{[103]}  from (if p and q are true then r is true) we can prove (if q is true then r is true, if p is true) 
Importation  ^{[34]}  If p then (if q then r) is equivalent to if p and q then r 
Idempotence of disjunction  ⟚ ^{[102]}  p is true is equiv. to p is true or p is true 
Idempotence of conjunction  ⟚ ^{[102]}  p is true is equiv. to p is true and p is true 
Tertium non datur (Law of Excluded Middle)  ^{[30]}^{[102]}  p or not p is true 
Law of NonContradiction  ^{[30]}^{[102]}  p and not p is false, is a true statement 
Explosion  ^{[30]}  p and not p; therefore q 
Syntactic proof via natural deduction
Natural deduction, since it is a method of syntactical proof, is specified by providing inference rules (also called rules of proof)^{[34]} for a language with the typical set of connectives ; no axioms are used other than these rules.^{[104]} The rules are covered below, and a proof example is given afterwards.
Notation styles
Different authors vary to some extent regarding which inference rules they give, which will be noted. More striking to the look and feel of a proof, however, is the variation in notation styles. The § Gentzen notation, which was covered earlier for a short argument, can actually be stacked to produce large treeshaped natural deduction proofs^{[39]}^{[11]}—not to be confused with "truth trees", which is another name for analytic tableaux.^{[65]} There is also a style due to Stanisław Jaśkowski, where the formulas in the proof are written inside various nested boxes,^{[39]} and there is a simplification of Jaśkowski's style due to Fredric Fitch (Fitch notation), where the boxes are simplified to simple horizontal lines beneath the introductions of suppositions, and vertical lines to the left of the lines that are under the supposition.^{[39]} Lastly, there is the only notation style which will actually be used in this article, which is due to Patrick Suppes,^{[39]} but was much popularized by E.J. Lemmon and Benson Mates.^{[105]} This method has the advantage that, graphically, it is the least intensive to produce and display, which made it a natural choice for the editor who wrote this part of the article, who did not understand the complex LaTeX commands that would be required to produce proofs in the other methods.
A proof, then, laid out in accordance with the Suppes–Lemmon notation style,^{[39]} is a sequence of lines containing sentences,^{[34]} where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence.^{[34]} Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number.^{[34]} The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers.^{[34]} The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.^{[34]} See the § Natural deduction proof example.
Inference rules
Natural deduction inference rules, due ultimately to Gentzen, are given below.^{[104]} There are ten primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rule reductio ad adbsurdum.^{[34]} Disjunctive Syllogism can be used as an easier alternative to the proper ∨elimination,^{[34]} and MTT and DN are commonly given rules,^{[104]} although they are not primitive.^{[34]}
Rule Name  Alternative names  Annotation  Assumption set  Statement 

Rule of Assumptions^{[104]}  Assumption^{[34]}  A^{[104]}^{[34]}  The current line number.^{[34]}  At any stage of the argument, introduce a proposition as an assumption of the argument.^{[104]}^{[34]} 
Conjunction introduction  Ampersand introduction,^{[104]}^{[34]} conjunction (CONJ)^{[34]}^{[106]}  m, n &I^{[34]}^{[104]}  The union of the assumption sets at lines m and n.^{[34]}  From and at lines m and n, infer .^{[104]}^{[34]} 
Conjunction elimination  Simplification (S),^{[34]} ampersand elimination^{[104]}^{[34]}  m &E^{[34]}^{[104]}  The same as at line m.^{[34]}  From at line m, infer and .^{[34]}^{[104]} 
Disjunction introduction^{[104]}  Addition (ADD)^{[34]}  m ∨I^{[34]}^{[104]}  The same as at line m.^{[34]}  From at line m, infer , whatever may be.^{[34]}^{[104]} 
Disjunction elimination  Wedge elimination,^{[104]} dilemma (DL)^{[106]}  j,k,l,m,n ∨E^{[104]}  The lines j,k,l,m,n.^{[104]}  From at line j, and an assumption of at line k, and a derivation of from at line l, and an assumption of at line m, and a derivation of from at line n, infer .^{[104]} 
Disjunctive Syllogism  Wedge elimination (∨E),^{[34]} modus tollendo ponens (MTP)^{[34]}  m,n DS^{[34]}  The union of the assumption sets at lines m and n.^{[34]}  From at line m and at line n, infer ; from at line m and at line n, infer .^{[34]} 
Arrow elimination^{[34]}  Modus ponendo ponens (MPP),^{[104]}^{[34]} modus ponens (MP),^{[106]}^{[34]} conditional elimination  m, n →E^{[34]}^{[104]}  The union of the assumption sets at lines m and n.^{[34]}  From at line m, and at line n, infer .^{[34]} 
Arrow introduction^{[34]}  Conditional proof (CP),^{[106]}^{[104]}^{[34]} conditional introduction  n, →I (m)^{[34]}^{[104]}  Everything in the assumption set at line n, excepting m, the line where the antecedent was assumed.^{[34]}  From at line n, following from the assumption of at line m, infer .^{[34]} 
Reductio ad absurdum^{[104]}  Indirect Proof (IP),^{[34]} negation introduction (−I),^{[34]} negation elimination (−E)^{[34]}  m, n RAA (k)^{[34]}  The union of the assumption sets at lines m and n, excluding k (the denied assumption).^{[34]}  From a sentence and its denial^{[k]} at lines m and n, infer the denial of any assumption appearing in the proof (at line k).^{[34]} 
Double arrow introduction^{[34]}  Biconditional definition (Df ↔),^{[104]} biconditional introduction  m, n ↔ I^{[34]}  The union of the assumption sets at lines m and n.^{[34]}  From and at lines m and n, infer .^{[34]} 
Double arrow elimination^{[34]}  Biconditional definition (Df ↔),^{[104]} biconditional elimination  m ↔ E^{[34]}  The same as at line m.^{[34]}  From at line m, infer either or .^{[34]} 
Double negation^{[104]}^{[106]}  Double negation elimination  m DN^{[104]}  The same as at line m.^{[104]}  From at line m, infer .^{[104]} 
Modus tollendo tollens^{[104]}  Modus tollens (MT)^{[106]}  m, n MTT^{[104]}  The union of the assumption sets at lines m and n.^{[104]}  From at line m, and at line n, infer .^{[104]} 
Natural deduction proof example
The proof below^{[34]} derives from and using only MPP and RAA, which shows that MTT is not a primitive rule, since it can be derived from those two other rules.
Assumption set  Line number  Sentence of proof  Annotation 

1  1  A  
2  2  A  
3  3  A  
1, 3  4  1, 3 →E  
1, 2  5  2, 4 RAA 
Syntactic proof via axioms
It is possible to perform proofs axiomatically, which means that certain tautologies are taken as selfevident and various others are deduced from them using modus ponens as an inference rule, as well as a rule of substitution, which permits replacing any wellformed formula with any substitutioninstance of it.^{[107]} Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.^{[107]}
This section gives the axioms of some historically notable axiomatic systems for propositional logic. For more examples, as well as metalogical theorems that are specific to such axiomatic systems (such as their completeness and consistency), see the article
Frege's Begriffsschrift
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.^{[33]}^{[107]} Frege's system used only implication and negation as connectives,^{[2]} and it had six axioms,^{[107]} which were these ones:^{[108]}^{[109]}
 Proposition 1:
 Proposition 2:
 Proposition 8:
 Proposition 28:
 Proposition 31:
 Proposition 41:
These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truthfunctional propositional logic.^{[108]}
Łukasiewicz's P_{2}
Jan Łukasiewicz showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentence ".^{[109]} Which, taken out of Łukasiewicz's Polish notation into modern notation, means . Hence, Łukasiewicz is credited^{[107]} with this system of three axioms:
Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule.^{[107]} The exact same system was given (with an explicit substitution rule) by Alonzo Church,^{[110]} who referred to it as the system P_{2}^{[110]}^{[111]} and helped popularize it.^{[111]}
Schematic form of P_{2}
One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for any wellformed formulas), the axioms are given as:^{[33]}^{[111]}
The schematic version of P_{2} is attributed to John von Neumann,^{[107]} and is used in the Metamath "set.mm" formal proof database.^{[111]} It has also been attributed to Hilbert,^{[112]} and named in this context.^{[112]}
Proof example in P_{2}
As an example, a proof of in P_{2} is given below. First, the axioms are given names:
 (A1)
 (A2)
 (A3)
And the proof is as follows:
 (instance of (A1))
 (instance of (A2))
 (from (1) and (2) by modus ponens)
 (instance of (A1))
 (from (4) and (3) by modus ponens)
Solvers
One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is
See also
Higher logical levels
Related topics
 Boolean algebra (logic)
 Boolean algebra (structure)
 Boolean algebra topics
 Boolean domain
 Boolean function
 Booleanvalued function
 Categorical logic
 Combinational logic
 Combinatory logic
 Conceptual graph
 Disjunctive syllogism
 Entitative graph
 Equational logic
 Existential graph
 Implicational propositional calculus
 Intuitionistic propositional calculus
 Jean Buridan
 Laws of Form
 List of logic symbols
 Logical graph
 Logical NOR
 Logical value
 Mathematical logic
 Operation (mathematics)
 Paul of Venice
 Peirce's law
 Peter of Spain (author)
 Propositional formula
 Symmetric difference
 Tautology (rule of inference)
 Truth function
 Truth table
 Walter Burley
 William of Sherwood
Notes
 ^ Many sources write this with a definite article, as the propositional calculus, while others just call it propositional calculus with no article.
 ^ The "or both" makes it clear^{[30]} that it's a logical disjunction, not an exclusive or, which is more common in English.
 ^ The set of premises may be the empty set;^{[33]}^{[34]} an argument from an empty set of premises is valid if, and only if, the conclusion is a tautology.^{[33]}^{[34]}
 ^ The turnstile, for syntactic consequence, is of lower precedence than the comma, which represents premise combination, which in turn is of lower precedence than the arrow, used for material implication; so no parentheses are needed to interpret this formula.^{[40]}
 ^ A very general and abstract syntax is given here, following the notation in the SEP,^{[2]} but including the third definition, which is very commonly given explicitly by other sources, such as Gillon,^{[10]} Bostock,^{[33]} Allen & Hand,^{[34]} and many others. As noted elsewhere in the article, languages variously compose their set of atomic propositional variables from uppercase or lowercase letters (often focusing on P/p, Q/q, and R/r), with or without subscript numerals; and in their set of connectives, they may include either the full set of five typical connectives, , or any of the truthfunctionally complete subsets of it. (And, of course, they may also use any of the notational variants of these connectives.)
 ^ Note that the phrase "principle of composition" has referred to other things in other contexts, and even in the context of logic, since Bertrand Russell used it to refer to the principle that "a proposition which implies each of two propositions implies them both."^{[48]}
 ^ The name "interpretation" is used by some authors and the name "case" by other authors. This article will be indifferent and use either, since it is collaboratively edited and there is no consensus about which terminology to adopt.
 ^ A truthfunctionally complete set of connectives^{[2]} is also called simply functionally complete, or adequate for truthfunctional logic,^{[35]} or expressively adequate,^{[71]} or simply adequate.^{[35]}^{[71]}
 WP:RS) have used both kinds of terminological convention, although usually a given author will use only one of them. Since this article is collaboratively edited and there is no consensus about which convention to use, these variations in terminology have been left standing.
 ^ Conventionally , with nothing to the left of the turnstile, is used to symbolize a tautology. It may be interpreted as saying that is a semantic consequence of the empty set of formulae, i.e., , but with the empty brackets omitted for simplicity;^{[33]} which is just the same as to say that it is a tautology, i.e., that there is no interpretation under which it is false.^{[33]}
 ^ To simplify the statement of the rule, the word "denial" here is used in this way: the denial of a formula that is not a negation is , whereas a negation, , has two denials, viz., and .^{[34]}
References
 ^ ^{a} ^{b} ^{c} ^{d} ^{e} ^{f} ^{g} ^{h} ^{i} ^{j} ^{k} ^{l} ^{m} ^{n} ^{o} ^{p} ^{q} ^{r} ^{s} ^{t} ^{u} ^{v} ^{w} ^{x} ^{y} "Propositional Logic  Internet Encyclopedia of Philosophy". Retrieved 22 March 2024.
 ^ ^{a} ^{b} ^{c} ^{d} ^{e} ^{f} ^{g} ^{h} ^{i} ^{j} ^{k} ^{l} ^{m} ^{n} ^{o} ^{p} ^{q} ^{r} ^{s} ^{t} ^{u} ^{v} ^{w} Franks, Curtis (2023), "Propositional Logic", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ ^{a} ^{b} Weisstein, Eric W. "Propositional Calculus". mathworld.wolfram.com. Retrieved 22 March 2024.
 ^ ISBN 9780190200015.
 ^ .
 ^ ^{a} ^{b} McGrath, Matthew; Frank, Devin (2023), "Propositions", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Winter 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ "Predicate Logic". www3.cs.stonybrook.edu. Retrieved 22 March 2024.
 ^ "Philosophy 404: Lecture Five". www.webpages.uidaho.edu. Retrieved 22 March 2024.
 ^ ^{a} ^{b} ^{c} "3.1 Propositional Logic". www.teach.cs.toronto.edu. Retrieved 22 March 2024.
 ^ ISBN 9780195136975.
 ^ .
 ^ ^{a} ^{b} "Propositional Logic". www.cs.miami.edu. Retrieved 22 March 2024.
 ISBN 9781107036598.
 ^ ^{a} ^{b} Weisstein, Eric W. "Connective". mathworld.wolfram.com. Retrieved 22 March 2024.
 ^ "Propositional Logic  Brilliant Math & Science Wiki". brilliant.org. Retrieved 20 August 2020.
 ^ Bobzien, Susanne (1 January 2016). "Ancient Logic". In Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University – via Stanford Encyclopedia of Philosophy.
 ^ "Propositional Logic  Internet Encyclopedia of Philosophy". Retrieved 20 August 2020.
 ^ Bobzien, Susanne (2020), "Ancient Logic", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Summer 2020 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ Peckhaus, Volker (1 January 2014). "Leibniz's Influence on 19th Century Logic". In Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University – via Stanford Encyclopedia of Philosophy.
 ^ Hurley, Patrick (2007). A Concise Introduction to Logic 10th edition. Wadsworth Publishing. p. 392.
 ^ Beth, Evert W.; "Semantic entailment and formal derivability", series: Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, Nieuwe Reeks, vol. 18, no. 13, NoordHollandsche Uitg. Mij., Amsterdam, 1955, pp. 309–42. Reprinted in Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969
 ^ ^{a} ^{b} Truth in Frege
 ^ ^{a} ^{b} ^{c} "Russell: the Journal of Bertrand Russell Studies".
 S2CID 170654885.
 ^ "Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables". www.math.fsu.edu. Retrieved 22 March 2024.
 ^ "Lecture Notes on Logical Organization and Critical Thinking". www2.hawaii.edu. Retrieved 22 March 2024.
 ^ "Logical Connectives". sites.millersville.edu. Retrieved 22 March 2024.
 ^ "Lecture1". www.cs.columbia.edu. Retrieved 22 March 2024.
 ^ ^{a} ^{b} ^{c} ^{d} "Introduction to Logic  Chapter 2". intrologic.stanford.edu. Retrieved 22 March 2024.
 ^ ISBN 9780203851555.
 ^ "Watson". watson.latech.edu. Retrieved 22 March 2024.
 ^ "Introduction to Theoretical Computer Science, Chapter 1". www.cs.odu.edu. Retrieved 22 March 2024.
 ^ ISBN 9780198751410.
 ^ .
 ^ .
 .
 ^ Dutilh Novaes, Catarina (2022), "Argument and Argumentation", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2022 ed.), Metaphysics Research Lab, Stanford University, retrieved 5 April 2024
 ^ ^{a} ^{b} ^{c} ^{d} ^{e} "Validity and Soundness  Internet Encyclopedia of Philosophy". Retrieved 5 April 2024.
 ^ ^{a} ^{b} ^{c} ^{d} ^{e} ^{f} Pelletier, Francis Jeffry; Hazen, Allen (2024), "Natural Deduction Systems in Logic", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Spring 2024 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ ^{a} ^{b} Restall, Greg (2018), "Substructural Logics", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ ^{a} ^{b} ^{c} ^{d} "Compactness  Internet Encyclopedia of Philosophy". Retrieved 22 March 2024.
 ^ ^{a} ^{b} "Lecture Topics for Discrete Math Students". math.colorado.edu. Retrieved 22 March 2024.
 ^ Paseau, Alexander; Pregel, Fabian (2023), "Deductivism in the Philosophy of Mathematics", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ ^{a} ^{b} Demey, Lorenz; Kooi, Barteld; Sack, Joshua (2023), "Logic and Probability", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
 ^ ISBN 9780486425337.
 ^ .
 ^ .
 .
 ^ .
 ^ .
 .
 ^ .
 .
 ^ "Propositional Logic". www.cs.rochester.edu. Retrieved 22 March 2024.
 ^ "Propositional calculus". www.cs.cornell.edu. Retrieved 22 March 2024.
 ^ ^{a} ^{b} Shramko, Yaroslav; Wansing, Heinrich (2021), "Truth Values", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Winter 2021 ed.), Metaphysics Research Lab, Stanford University, retrieved 23 March 2024
 PMID 22179287.
 .
 ^ Shapiro, Stewart; Kouri Kissel, Teresa (2024), "Classical Logic", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Spring 2024 ed.), Metaphysics Research Lab, Stanford University, retrieved 25 March 2024
 ^ ISSN 09244662.
 .
 ^ .
 .
 ^ .
 ^ .
 ^ Aloni, Maria (2023), "Disjunction", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Spring 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 23 March 2024
 ISBN 9783030673956.
 .
 ^ .
 ^ Levin, Oscar. Propositional Logic.
 ^ ISBN 9780521008044. (Defines "expressively adequate", shortened to "adequate set of connectives" in a section heading.)
 .
 .
 ^ .
 ^ "6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation". leanprover.github.io. Retrieved 28 March 2024.
 ^ "Knowledge Representation and Reasoning: Basics of Logics". www.emse.fr. Retrieved 28 March 2024.
 ^ ^{a} ^{b} "1.4: Tautologies and contradictions". Mathematics LibreTexts. 9 September 2021. Retrieved 29 March 2024.
 ^ ^{a} ^{b} Sylvestre, Jeremy. EF Tautologies and contradictions.
 ^ ^{a} ^{b} DeLancey, Craig; Woodrow, Jenna (2017). Elementary Formal Logic (1 ed.). Pressbooks.
 OCLC 681481210.
 .
 .
 .
 ^ DeLancey, Craig (2017). "A Concise Introduction to Logic: §4. Proofs". Milne Publishing. Retrieved 23 March 2024.
 ISBN 9780191816802, retrieved 23 March 2024
 , retrieved 23 March 2024
 ^ .
 ^ "Truth table  Boolean, Operators, Rules  Britannica". www.britannica.com. 14 March 2024. Retrieved 23 March 2024.
 ^ ^{a} ^{b} ^{c} "MathematicalLogic". www.cs.yale.edu. Retrieved 23 March 2024.
 ^ "Analytic Tableaux". www3.cs.stonybrook.edu. Retrieved 23 March 2024.
 ^ "Formal logic  Semantic Tableaux, Proofs, Rules  Britannica". www.britannica.com. Retrieved 23 March 2024.
 ^ "Axiomatic method  Logic, Proofs & Foundations  Britannica". www.britannica.com. Retrieved 23 March 2024.
 ^ "Propositional Logic". mally.stanford.edu. Retrieved 23 March 2024.
 ^ ^{a} ^{b} "Natural Deduction  Internet Encyclopedia of Philosophy". Retrieved 23 March 2024.
 ^ ^{a} ^{b} Weisstein, Eric W. "Sequent Calculus". mathworld.wolfram.com. Retrieved 23 March 2024.
 ^ "Interactive Tutorial of the Sequent Calculus". logitext.mit.edu. Retrieved 23 March 2024.
 ISBN 9780201416404.
 ^ Bachmair, Leo (2009). "CSE541 Logic in Computer Science" (PDF). Stony Brook University.
 ISBN 9780815386643.
 .
 .
 ^ .
 ^ Toida, Shunichi (2 August 2009). "Proof of Implications". CS381 Discrete Structures/Discrete Mathematics Web Course Material. Department of Computer Science, Old Dominion University. Retrieved 10 March 2010.
 ^ ISBN 9780412380907.
 ^ "Natural Deduction Systems in Logic > Notes (Stanford Encyclopedia of Philosophy)". plato.stanford.edu. Retrieved 19 April 2024.
 ^ OCLC 962129086.
 ^ .
 ^ .
 ^ ^{a} ^{b} Łukasiewicz, Jan (1970). Jan Lukasiewicz: Selected Works. NorthHolland. p. 136.
 ^ ISBN 9780691029061.
 ^ ^{a} ^{b} ^{c} ^{d} "Proof Explorer  Home Page  Metamath". us.metamath.org. Retrieved 2 July 2024.
 ^ ISBN 9789814719957.
 ^ W. V. O. Quine, Mathematical Logic (1980), p.81. Harvard University Press, 0674554515
Further reading
 Brown, Frank Markham (2003), Boolean Reasoning: The Logic of Boolean Equations, 1st edition, Kluwer Academic Publishers, Norwell, MA. 2nd edition, Dover Publications, Mineola, NY.
 Chang, C.C. and Keisler, H.J. (1973), Model Theory, NorthHolland, Amsterdam, Netherlands.
 Kohavi, Zvi (1978), Switching and Finite Automata Theory, 1st edition, McGraw–Hill, 1970. 2nd edition, McGraw–Hill, 1978.
 Korfhage, Robert R. (1974), Discrete Computational Structures, Academic Press, New York, NY.
 Lambek, J. and Scott, P.J. (1986), Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.
 Mendelson, Elliot (1964), Introduction to Mathematical Logic, D. Van Nostrand Company.
Related works
 ISBN 9780465026562.
External links
 Klement, Kevin C. (2006), "Propositional Logic", in James Fieser and Bradley Dowden (eds.), Internet Encyclopedia of Philosophy, Eprint.
 Formal Predicate Calculus, contains a systematic formal development with axiomatic proof
 forall x: an introduction to formal logic, by P.D. Magnus, covers formal semantics and proof theory for sentential logic.
 Chapter 2 / Propositional Logic from Logic In Action
 Propositional sequent calculus prover on Project Nayuki. (note: implication can be input in the form
!XY
, and a sequent can be a single formula prefixed with>
and having no commas)  Propositional Logic  A Generative Grammar
 A Propositional Calculator that helps to understand simple expressions