Propositional calculus

{{main|History of logic}}

Although propositional logic (also called propositional calculus) had been hinted by earlier philosophers, it was developed into a formal logic (Stoic logic) by Chrysippus in the 3rd century BC and expanded by his successor Stoics. The logic was focused on propositions. This was different from the traditional syllogistic logic, which focused on terms. However, most of the original writings were lost and, at some time between the 3rd and 6th century CE, Stoic logic faded into oblivion, to be resurrected only in the 20th century, in the wake of the (re)-discovery of propositional logic.

Symbolic logic, which would come to be important to refine propositional logic, was first developed by the 17th/18th-century mathematician Gottfried Leibniz, whose calculus ratiocinator was, however, unknown to the larger logical community. Consequently, many of the advances achieved by Leibniz were recreated by logicians like George Boole and Augustus De Morgan, completely independent of Leibniz.

Gottlob Frege's predicate logic builds upon propositional logic, and has been described as combining "the distinctive features of syllogistic logic and propositional logic." Consequently, predicate logic ushered in a new era in logic's history; however, advances in propositional logic were still made after Frege, including natural deduction, truth trees and truth tables. Natural deduction was invented by Gerhard Gentzen and Stanisław Jaśkowski. Truth trees were invented by Evert Willem Beth. The invention of truth tables, however, is of uncertain attribution.

Within works by Frege and Bertrand Russell, 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). Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole, Charles Sanders Peirce, 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. Ultimately, some have concluded, like John Shosky, that "It is far from clear that any one person should be given the title of 'inventor' of truth-tables".

{{Main article|Proposition}}

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.

Propositional logic deals with statements, which are defined as declarative sentences having truth value. 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.". Such non-declarative sentences have no truth value, and are only dealt with in nonclassical logics, called erotetic and imperative logics.

{{See also|Atomic formula|Atomic sentence}}

In propositional logic, a statement can contain one or more other statements as parts. Compound sentences are formed from simpler sentences and express relationships among the constituent sentences. This is done by combining them with logical connectives: the main types of compound sentences are negations, conjunctions, disjunctions, implications, and biconditionals, which are formed by using the corresponding connectives to connect propositions. In English, these connectives are expressed by the words "and" (conjunction), "or" (disjunction), "not" (negation), "if" (material conditional), and "if and only if" (biconditional). 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){{refn|group=lower-alpha|The "or both" makes it clear that it's a logical disjunction, not an exclusive or, which is more common in English.}}

If sentences lack any logical connectives, they are called simple sentences, or atomic sentences; if they contain one or more logical connectives, they are called compound sentences, or molecular sentences.

Sentential connectives are a broader category that includes logical connectives. Sentential connectives are any linguistic particles that bind sentences to create a new compound sentence, or that inflect a single sentence to create a new sentence. 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. Philosophers disagree about what exactly a proposition is, as well as about which sentential connectives in natural languages should be counted as logical connectives. Sentential connectives are also called sentence-functors, and logical connectives are also called truth-functors.

{{Main article|Argument}}

An argument is defined as a pair of things, namely a set of sentences, called the premises,{{refn|group=lower-alpha|The set of premises may be the empty set; an argument from an empty set of premises is valid if, and only if, the conclusion is a tautology.}} and a sentence, called the conclusion. The conclusion is claimed to follow from the premises, and the premises are claimed to support the conclusion.

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, which is a classically valid form. 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 {{section link||Formalization}}.

{{Main article|Validity (logic)|Soundness}}

An argument is valid if, and only if, it is necessary that, if all its premises are true, its conclusion is true. Alternatively, an argument is valid if, and only if, it is impossible for all the premises to be true while the conclusion is false.

Validity is contrasted with soundness. An argument is sound if, and only if, it is valid and all its premises are true. Otherwise, it is unsound.

Logic, in general, aims to precisely specify valid arguments. This is done by defining a valid argument as one in which its conclusion is a logical consequence of its premises, 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 – see {{section link||Semantics}} below.

Propositional logic is typically studied through a formal system in which formulas of a formal language are interpreted to represent propositions. 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. This section will show how this works by formalizing the {{section link||Example argument}}. The formal language for a propositional calculus will be fully specified in {{section link||Language}}, and an overview of proof systems will be given in {{section link||Proof systems}}.

{{Main article|Propositional variable}}

Since propositional logic is not concerned with the structure of propositions beyond the point where they cannot be decomposed any more by logical connectives, it is typically studied by replacing such atomic (indivisible) statements with letters of the alphabet, which are interpreted as variables representing statements (propositional variables). With propositional variables, the {{section link||Example argument}} would then be symbolized as follows:

:Premise 1: $P\; \backslash to\; Q$

:Premise 2: $P$

:Conclusion: $Q$

When {{mvar|P}} is interpreted as "It's raining" and {{mvar|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 $P$, $Q$ and $R$) 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.

If we assume that the validity of modus ponens has been accepted as an axiom, then the same {{section link||Example argument}} can also be depicted like this:

:$\backslash frac\{P\; \backslash to\; Q,\; P\}\{Q\}$

This method of displaying it is Gentzen's notation for natural deduction and sequent calculus. The premises are shown above a line, called the inference line, separated by a comma, which indicates combination of premises. The conclusion is written below the inference line. The inference line represents syntactic consequence, sometimes called deductive consequence,> which is also symbolized with ⊢. So the above can also be written in one line as $P\; \backslash to\; Q,\; P\; \backslash vdash\; Q$.{{refn|group=lower-alpha|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.}}

Syntactic consequence is contrasted with semantic consequence, which is symbolized with ⊧. 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.

{{Formal languages}}

The language (commonly called $\backslash mathcal\{L\}$) of a propositional calculus is defined in terms of:

1. a set of primitive symbols, called atomic formulas, atomic sentences, atoms, placeholders, prime formulas, proposition letters, sentence letters, or variables, and
2. a set of operator symbols, called connectives, logical connectives, logical operators, truth-functional connectives, truth-functors, or propositional connectives.

A well-formed 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 $\backslash mathcal\{L\}$, then, is defined either as being identical to its set of well-formed formulas, or as containing that set (together with, for instance, its set of connectives and variables).

Usually the syntax of $\backslash mathcal\{L\}$ 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, while others use them without comment.

Given a set of atomic propositional variables $p\_1$, $p\_2$, $p\_3$, ..., and a set of propositional connectives $c\_1^1$, $c\_2^1$, $c\_3^1$, ..., $c\_1^2$, $c\_2^2$, $c\_3^2$, ..., $c\_1^3$, $c\_2^3$, $c\_3^3$, ..., a formula of propositional logic is defined recursively by these definitions:{{refn|group=lower-alpha|A very general and abstract syntax is given here, following the notation in the SEP, but including the third definition, which is very commonly given explicitly by other sources, such as Gillon, Bostock, Allen & Hand, 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, $\backslash \{\; \backslash neg,\; \backslash land,\; \backslash lor,\; \backslash to,\; \backslash leftrightarrow\; \backslash \}$, or any of the truth-functionally complete subsets of it. (And, of course, they may also use any of the notational variants of these connectives.)}}

:Definition 1: Atomic propositional variables are formulas.

:Definition 2: If $c\_n^m$ is a propositional connective, and $\backslash langle$A, B, C, …$\backslash rangle$ is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applying $c\_n^m$ to $\backslash langle$A, B, C, …$\backslash rangle$ is a formula.

:Definition 3: Nothing else is a formula.

Writing the result of applying $c\_n^m$ to $\backslash langle$A, B, C, …$\backslash rangle$ in functional notation, as $c\_n^m$(A, B, C, …), we have the following as examples of well-formed formulas:

• $p\_5$
• $c\_3^2(p\_2,\; p\_9)$
• $c\_3^2(p\_1,\; c\_2^1(p\_3))$
• $c\_1^3(p\_4,\; p\_6,\; c\_2^2(p\_1,\; p\_2))$
• $c\_4^2(c\_1^1(p\_7),\; c\_3^1(p\_8))$
• $c\_2^3(c\_1^2(p\_3,\; p\_4),\; c\_2^1(p\_5),\; c\_3^2(p\_6,\; p\_7))$
• $c\_3^1(c\_1^3(p\_2,\; p\_3,\; c\_2^2(p\_4,\; p\_5)))$

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.{{refn|group=lower-alpha|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."}} 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 $\backslash mathcal\{L\}$ are built up from the atoms as ultimate building blocks. Composite formulas (all formulas besides atoms) are called molecules, or molecular sentences. (This is an imperfect analogy with chemistry, since a chemical molecule may sometimes have only one atom, as in monatomic gases.)

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. In particular, it excludes infinitely long formulas from being well-formed.

An alternative to the syntax definitions given above is to write a context-free (CF) grammar for the language $\backslash mathcal\{L\}$ in Backus-Naur form (BNF). This is more common in computer science than in philosophy. It can be done in many ways, of which a particularly brief one, for the common set of five connectives, is this single clause:

:

This clause, due to its self-referential nature (since $\backslash phi$ is in some branches of the definition of $\backslash phi$), also acts as a recursive definition, and therefore specifies the entire language. To expand it to add modal operators, one need only add … $|\; ~\; \backslash Box\backslash phi\; ~\; |\; ~\; \backslash Diamond\backslash phi$ to the end of the clause.

Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schemata, or schematic letters, however, range over all formulas. (Schematic letters are also called metavariables.) It is common to represent propositional constants by {{mvar|A}}, {{mvar|B}}, and {{mvar|C}}, propositional variables by {{mvar|P}}, {{mvar|Q}}, and {{mvar|R}}, and schematic letters are often Greek letters, most often {{mvar|φ}}, {{mvar|ψ}}, and {{mvar|χ}}.

However, some authors recognize only two "propositional constants" in their formal system: the special symbol $\backslash top$, called "truth", which always evaluates to True, and the special symbol $\backslash bot$, called "falsity", which always evaluates to False. Other authors also include these symbols, with the same meaning, but consider them to be "zero-place truth-functors", or equivalently, "nullary connectives".

{{Main article|Semantics of logic|Model theory}}

To serve as a model of the logic of a given natural language, a formal language must be semantically interpreted. In classical logic, all propositions evaluate to exactly one of two truth-values: True or False. For example, "Wikipedia is a free online encyclopedia that anyone can edit" evaluates to True, while "Wikipedia is a paper encyclopedia" evaluates to False.

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. To learn about nonclassical logics with more than two truth-values, and their unique semantics, one may consult the articles on "Many-valued logic", "Three-valued logic", "Finite-valued logic", and "Infinite-valued logic".

{{Main|Interpretation (logic)}}

For a given language $\backslash mathcal\{L\}$, an interpretation, valuation, Boolean valuation, or case,{{refn|group=lower-alpha|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.}} is an assignment of semantic values to each formula of $\backslash mathcal\{L\}$. For a formal language of classical logic, a case is defined as an assignment, to each formula of $\backslash mathcal\{L\}$, of one or the other, but not both, of the truth values, namely truth (T, or 1) and falsity (F, or 0). An interpretation that follows the rules of classical logic is sometimes called a Boolean valuation. An interpretation of a formal language for classical logic is often expressed in terms of truth tables. Since each formula is only assigned a single truth-value, an interpretation may be viewed as a function, whose domain is $\backslash mathcal\{L\}$, and whose range is its set of semantic values $\backslash mathcal\{V\}\; =\; \backslash \{\backslash mathsf\{T\},\; \backslash mathsf\{F\}\backslash \}$, or $\backslash mathcal\{V\}\; =\; \backslash \{1,\; 0\backslash \}$.

For $n$ distinct propositional symbols there are $2^n$ distinct possible interpretations. For any particular symbol $a$, for example, there are $2^1=2$ possible interpretations: either $a$ is assigned T, or $a$ is assigned F. And for the pair $a$, $b$ there are $2^2=4$ possible interpretations: either both are assigned T, or both are assigned F, or $a$ is assigned T and $b$ is assigned F, or $a$ is assigned F and $b$ is assigned T. Since $\backslash mathcal\{L\}$ has $\backslash aleph\_0$, that is, denumerably many propositional symbols, there are $2^\{\backslash aleph\_0\}=\backslash mathfrak\; c$, and therefore uncountably many distinct possible interpretations of $\backslash mathcal\{L\}$ as a whole.

Where $\backslash mathcal\{I\}$ is an interpretation and $\backslash varphi$ and $\backslash psi$ represent formulas, the definition of an argument, given in {{section link||Arguments}}, may then be stated as a pair $\backslash langle\; \backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}\; ,\; \backslash psi\; \backslash rangle$, where $\backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}$ is the set of premises and $\backslash psi$ is the conclusion. The definition of an argument's validity, i.e. its property that $\backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}\; \backslash models\; \backslash psi$, can then be stated as its absence of a counterexample, where a counterexample is defined as a case $\backslash mathcal\{I\}$ in which the argument's premises $\backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}$ are all true but the conclusion $\backslash psi$ is not true. As will be seen in {{section link||Semantic truth, validity, consequence}}, this is the same as to say that the conclusion is a semantic consequence of the premises.

{{Main article|Logical connective|Truth function}}An interpretation assigns semantic values to atomic formulas directly. Molecular formulas are assigned a function of the value of their constituent atoms, according to the connective used; the connectives are defined in such a way that the truth-value of a sentence formed from atoms with connectives depends on the truth-values of the atoms that they're applied to, and only on those. This assumption is referred to by Colin Howson as the assumption of the truth-functionality of the connectives.

{{Logical connectives sidebar}}

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, the semantic definition of the connectives is usually represented as a truth table for each of the connectives, as seen below:

{| class="wikitable" style="margin:1em auto; text-align:center;"

|-

! p

! q

! {{math|p ∧ q}}

! {{math|p ∨ q}}

! {{math|p → q}}

! {{math|p ↔ q}}

! ¬p

! ¬q

|-

| {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Failure|}}F

|-

| {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T

|-

| {{Failure|}}F || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Failure|}}F

|-

| {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T

|}

This table covers each of the main five logical connectives: conjunction (here notated {{math|p ∧ q}}), disjunction ({{math|p ∨ q}}), implication ({{math|p → q}}), biconditional ({{math|p ↔ q}}) and negation, (¬p, or ¬q, as the case may be). It is sufficient for determining the semantics of each of these operators. For more truth tables for more different kinds of connectives, see the article "Truth table".

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 $\backslash mathcal\{I\}(\backslash varphi)$ is the interpretation of $\backslash varphi$, the five connectives are defined as:

• $\backslash mathcal\{I\}(\backslash neg\; P)\; =\; \backslash mathsf\{T\}$ if, and only if, $\backslash mathcal\{I\}(P)\; =\; \backslash mathsf\{F\}$
• $\backslash mathcal\{I\}(P\; \backslash land\; Q)\; =\; \backslash mathsf\{T\}$ if, and only if, $\backslash mathcal\{I\}(P)\; =\; \backslash mathsf\{T\}$ and $\backslash mathcal\{I\}(Q)\; =\; \backslash mathsf\{T\}$
• $\backslash mathcal\{I\}(P\; \backslash lor\; Q)\; =\; \backslash mathsf\{T\}$ if, and only if, $\backslash mathcal\{I\}(P)\; =\; \backslash mathsf\{T\}$ or $\backslash mathcal\{I\}(Q)\; =\; \backslash mathsf\{T\}$
• $\backslash mathcal\{I\}(P\; \backslash to\; Q)\; =\; \backslash mathsf\{T\}$ if, and only if, it is true that, if $\backslash mathcal\{I\}(P)\; =\; \backslash mathsf\{T\}$, then $\backslash mathcal\{I\}(Q)\; =\; \backslash mathsf\{T\}$
• $\backslash mathcal\{I\}(P\; \backslash leftrightarrow\; Q)\; =\; \backslash mathsf\{T\}$ if, and only if, it is true that $\backslash mathcal\{I\}(P)\; =\; \backslash mathsf\{T\}$ if, and only if, $\backslash mathcal\{I\}(Q)\; =\; \backslash mathsf\{T\}$

Instead of $\backslash mathcal\{I\}(\backslash varphi)$, the interpretation of $\backslash varphi$ may be written out as $|\backslash varphi|$, or, for definitions such as the above, $\backslash mathcal\{I\}(\backslash varphi)\; =\; \backslash mathsf\{T\}$ may be written simply as the English sentence "$\backslash varphi$ is given the value $\backslash mathsf\{T\}$". Yet other authors may prefer to speak of a Tarskian model $\backslash mathfrak\{M\}$ for the language, so that instead they'll use the notation $\backslash mathfrak\{M\}\; \backslash models\; \backslash varphi$, which is equivalent to saying $\backslash mathcal\{I\}(\backslash varphi)\; =\; \backslash mathsf\{T\}$, where $\backslash mathcal\{I\}$ is the interpretation function for $\backslash mathfrak\{M\}$.

Some of these connectives may be defined in terms of others: for instance, implication, {{math|p → q}}, may be defined in terms of disjunction and negation, as {{math|¬p ∨ q}}; and disjunction may be defined in terms of negation and conjunction, as {{math|¬(¬p ∧ ¬q)}}. In fact, a truth-functionally complete system,{{refn|group=lower-alpha|A truth-functionally complete set of connectives is also called simply functionally complete, or adequate for truth-functional logic, or expressively adequate, or simply adequate.}} 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), or using only implication and negation (as Frege did), or using only conjunction and negation, or even using only a single connective for "not and" (the Sheffer stroke), as Jean Nicod did. A joint denial connective (logical NOR) will also suffice, by itself, to define all other connectives. Besides NOR and NAND, no other connectives have this property.{{efn|See a table of all 16 bivalent truth functions.}}

Some authors, namely Howson and Cunningham, distinguish equivalence from the biconditional. (As to equivalence, Howson calls it "truth-functional 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 $\backslash mathcal\{L\}$. 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", and/or the symbol ⇔, to denote their object language's biconditional connective.

Given $\backslash varphi$ and $\backslash psi$ as formulas (or sentences) of a language $\backslash mathcal\{L\}$, and $\backslash mathcal\{I\}$ as an interpretation (or case){{refn|group=lower-alpha|Some of these definitions use the word "interpretation", and speak of sentences/formulas being true or false "under" it, and some will use the word "case", and speak of sentences/formulas being true or false "in" it. Published reliable sources (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.}} of $\backslash mathcal\{L\}$, then the following definitions apply:

• Truth-in-a-case: A sentence $\backslash varphi$ of $\backslash mathcal\{L\}$ is true under an interpretation $\backslash mathcal\{I\}$ if $\backslash mathcal\{I\}$ assigns the truth value T to $\backslash varphi$. If $\backslash varphi$ is true under $\backslash mathcal\{I\}$, then $\backslash mathcal\{I\}$ is called a model of $\backslash varphi$.
• Falsity-in-a-case: $\backslash varphi$ is false under an interpretation $\backslash mathcal\{I\}$ if, and only if, $\backslash neg\backslash varphi$ is true under $\backslash mathcal\{I\}$. This is the "truth of negation" definition of falsity-in-a-case. Falsity-in-a-case may also be defined by the "complement" definition: $\backslash varphi$ is false under an interpretation $\backslash mathcal\{I\}$ if, and only if, $\backslash varphi$ is not true under $\backslash mathcal\{I\}$. In classical logic, these definitions are equivalent, but in nonclassical logics, they are not.
• Semantic consequence: A sentence $\backslash psi$ of $\backslash mathcal\{L\}$ is a semantic consequence ($\backslash varphi\; \backslash models\; \backslash psi$) of a sentence $\backslash varphi$ if there is no interpretation under which $\backslash varphi$ is true and $\backslash psi$ is not true.
• Valid formula (tautology): A sentence $\backslash varphi$ of $\backslash mathcal\{L\}$ is logically valid ($\backslash models\backslash varphi$),{{refn|group=lower-alpha|Conventionally $\backslash models\backslash varphi$, with nothing to the left of the turnstile, is used to symbolize a tautology. It may be interpreted as saying that $\backslash varphi$ is a semantic consequence of the empty set of formulae, i.e., $\backslash \{\backslash \}\backslash models\backslash varphi$, but with the empty brackets omitted for simplicity; 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.}} or a tautology,ref name="ms32 if it is true under every interpretation, or true in every case.
• Consistent sentence: A sentence of $\backslash mathcal\{L\}$ is consistent if it is true under at least one interpretation. It is inconsistent if it is not consistent. An inconsistent formula is also called self-contradictory, and said to be a self-contradiction, or simply a contradiction, although this latter name is sometimes reserved specifically for statements of the form $(p\; \backslash land\; \backslash neg\; p)$.

For interpretations (cases) $\backslash mathcal\{I\}$ of $\backslash mathcal\{L\}$, these definitions are sometimes given:

• Complete case: A case $\backslash mathcal\{I\}$ is complete if, and only if, either $\backslash varphi$ is true-in-$\backslash mathcal\{I\}$ or $\backslash neg\backslash varphi$ is true-in-$\backslash mathcal\{I\}$, for any $\backslash varphi$ in $\backslash mathcal\{L\}$.
• Consistent case: A case $\backslash mathcal\{I\}$ is consistent if, and only if, there is no $\backslash varphi$ in $\backslash mathcal\{L\}$ such that both $\backslash varphi$ and $\backslash neg\backslash varphi$ are true-in-$\backslash mathcal\{I\}$.

For classical logic, which assumes that all cases are complete and consistent, the following theorems apply:

• For any given interpretation, a given formula is either true or false under it.
• No formula is both true and false under the same interpretation.
• $\backslash varphi$ is true under $\backslash mathcal\{I\}$ if, and only if, $\backslash neg\backslash varphi$ is false under $\backslash mathcal\{I\}$; $\backslash neg\backslash varphi$ is true under $\backslash mathcal\{I\}$ if, and only if, $\backslash varphi$ is not true under $\backslash mathcal\{I\}$.
• If $\backslash varphi$ and $(\backslash varphi\; \backslash to\; \backslash psi)$ are both true under $\backslash mathcal\{I\}$, then $\backslash psi$ is true under $\backslash mathcal\{I\}$.
• If $\backslash models\backslash varphi$ and $\backslash models(\backslash varphi\; \backslash to\; \backslash psi)$, then $\backslash models\backslash psi$.
• $(\backslash varphi\; \backslash to\; \backslash psi)$ is true under $\backslash mathcal\{I\}$ if, and only if, either $\backslash varphi$ is not true under $\backslash mathcal\{I\}$, or $\backslash psi$ is true under $\backslash mathcal\{I\}$.
• $\backslash varphi\; \backslash models\; \backslash psi$ if, and only if, $(\backslash varphi\; \backslash to\; \backslash psi)$ is logically valid, that is, $\backslash varphi\; \backslash models\; \backslash psi$ if, and only if, $\backslash models(\backslash varphi\; \backslash to\; \backslash psi)$.

{{See also|Proof theory|Proof calculus}}

Proof systems in propositional logic can be broadly classified into semantic proof systems and syntactic proof systems, according to the kind of logical consequence that they rely on: semantic proof systems rely on semantic consequence ($\backslash varphi\; \backslash models\; \backslash psi$), whereas syntactic proof systems rely on syntactic consequence ($\backslash varphi\; \backslash vdash\; \backslash psi$). 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. This section gives a very brief overview of the kinds of proof systems, with anchors to the relevant sections of this article on each one, as well as to the separate Wikipedia articles on each one.

{{Image frame|content=$\backslash 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}

|width=200|align=right|caption=Example of a truth table}}

File:Partially built tableau.svg]]

Semantic proof systems rely on the concept of semantic consequence, symbolized as $\backslash varphi\; \backslash models\; \backslash psi$, which indicates that if $\backslash varphi$ is true, then $\backslash psi$ must also be true in every possible interpretation.

{{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. By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory. See {{section link||Semantic proof via truth tables}}.

{{Main article|Method of analytic tableaux}}

A semantic tableau is another semantic proof technique that systematically explores the truth of a proposition. It constructs a tree where each branch represents a possible interpretation of the propositions involved. If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered a tautology. See {{section link||Semantic proof via tableaux}}.

File:LK groupe logique.png LK, in Gentzen notation]]

Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence, $\backslash varphi\; \backslash vdash\; \backslash psi$, signifies that $\backslash psi$ can be derived from $\backslash varphi$ using the rules of the formal system.

{{Main article|Axiomatic system (logic)}}

An axiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived. 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. See {{section link||Syntactic proof via axioms}}.

{{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. Each rule reflects a particular logical connective and shows how it can be introduced or eliminated. See {{section link||Syntactic proof via natural deduction}}.

{{Main article|Sequent calculus}}

The sequent calculus is a formal system that represents logical deductions as sequences or "sequents" of formulas. 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.

{{See also|Truth table}}

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. If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation). Further, if (and only if) $\backslash neg\backslash varphi$ is valid, then $\backslash varphi$ is inconsistent.

For instance, this table shows that "{{math|p → (q ∨ r → (r → ¬p))}}" is not valid:

{| class="wikitable" style="margin:1em auto; text-align:center;"

|-

! p

! q

! r

! {{math|q ∨ r}}

! {{math|r → ¬p}}

! {{math|q ∨ r → (r → ¬p)}}

! {{math|p → (q ∨ r → (r → ¬p))}}

|-

| {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F

|-

| {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T

|-

| {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F

|-

| {{Success|}}T || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T

|-

| {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T

|-

| {{Failure|}}F || {{Success|}}T || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T

|-

| {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T || {{Success|}}T

|-

| {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Failure|}}F || {{Success|}}T || {{Success|}}T || {{Success|}}T

|}

The computation of the last column of the third line may be displayed as follows:

{| class="wikitable" style="margin:1em auto; text-align:center;"

|-

! 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 $\backslash varphi\; \backslash models\; \backslash psi$ if, and only if, $(\backslash varphi\; \backslash to\; \backslash psi)$ is valid, we can use a truth table to prove that a formula is a semantic consequence of a set of formulas: $\backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}\; \backslash models\; \backslash psi$ if, and only if, we can produce a truth table that comes out all true for the formula $\backslash left(\; \backslash left(\backslash bigwedge\; \_\{i=1\}^n\; \backslash varphi\_i\; \backslash right)\; \backslash rightarrow\; \backslash psi\; \backslash right)$ (that is, if $\backslash models\; \backslash left(\; \backslash left(\backslash bigwedge\; \_\{i=1\}^n\; \backslash varphi\_i\; \backslash right)\; \backslash rightarrow\; \backslash psi\; \backslash right)$).

{{Main article|Method of analytic tableaux}}

Since truth tables have 2ⁿ lines for n variables, they can be tiresomely long for large values of n. Analytic tableaux are a more efficient, but nevertheless mechanical, 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."

Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below. These rules use "signed formulas", where a signed formula is an expression $TX$ or $FX$, where $X$ is a (unsigned) formula of the language $\backslash mathcal\{L\}$. (Informally, $TX$ is read "$X$ is true", and $FX$ is read "$X$ is false".) Their formal semantic definition is that "under any interpretation, a signed formula $TX$ is called true if $X$ is true, and false if $X$ is false, whereas a signed formula $FX$ is called false if $X$ is true, and true if $X$ is false."

\begin{align}

&1) \quad \frac{T \sim X}{FX} \quad &&\frac{F \sim X}{TX} \\

\phantom{spacer} \\

&2) \quad \frac{T(X \land Y)}{\begin{matrix} TX \\ TY \end{matrix}} \quad &&\frac{F(X \land Y)}{FX | FY} \\

\phantom{spacer} \\

&3) \quad \frac{T(X \lor Y)}{TX | TY} \quad &&\frac{F(X \lor Y)}{\begin{matrix} FX \\ FY \end{matrix}} \\

\phantom{spacer} \\

&4) \quad \frac{T(X \supset Y)}{FX | TY} \quad &&\frac{F(X \supset Y)}{\begin{matrix} TX \\ FY \end{matrix}}

\end{align}

In this notation, rule 2 means that $T(X\; \backslash land\; Y)$ yields both $TX,\; TY$, whereas $F(X\; \backslash land\; Y)$ branches into $FX,\; FY$. The notation is to be understood analogously for rules 3 and 4. Often, in tableaux for classical logic, the signed formula notation is simplified so that $T\backslash varphi$ is written simply as $\backslash varphi$, and $F\backslash varphi$ as $\backslash neg\backslash varphi$, which accounts for naming rule 1 the "Rule of Double Negation".

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 $TX$ and $FX$ for some $X$, which is to say, a contradiction. In that case, the branch is said to close. If every branch in a tree closes, the tree itself is said to close. 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 self-contradictory, and therefore false. 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.

To construct a tableau for an argument $\backslash langle\; \backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}\; ,\; \backslash psi\; \backslash rangle$, one first writes out the set of premise formulas, $\backslash \{\backslash varphi\_1,\; \backslash varphi\_2,\; \backslash varphi\_3,\; ...,\; \backslash varphi\_n\backslash \}$, with one formula on each line, signed with $T$ (that is, $T\backslash varphi$ for each $T\backslash varphi$ in the set); and together with those formulas (the order is unimportant), one also writes out the conclusion, $\backslash psi$, signed with $F$ (that is, $F\backslash psi$). One then produces a truth tree (analytic tableau) by using all those lines according to the rules. A closed tree will be proof that the argument was valid, in virtue of the fact that $\backslash varphi\; \backslash models\; \backslash psi$ if, and only if, $\backslash \{\; \backslash varphi,\; \backslash sim\backslash psi\; \backslash \}$ is inconsistent (also written as $\backslash varphi,\; \backslash sim\backslash psi\; \backslash models$).

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. We use $\backslash varphi$ ⟚ $\backslash psi$ to denote equivalence of $\backslash varphi$ and $\backslash psi$, that is, as an abbreviation for both $\backslash varphi\; \backslash models\; \backslash psi$ and $\backslash psi\; \backslash models\; \backslash varphi$; 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, although many authors prefer to read it as "entails", or as "models".

{| class="wikitable" style="margin:auto;"

|- "

! Name

! Sequent

! Description

|-

| Modus Ponens

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; p)\; \backslash models\; q$

| If {{mvar|p}} then {{mvar|q}}; {{mvar|p}}; therefore {{mvar|q}}

|-

| Modus Tollens

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; \backslash neg\; q)\; \backslash models\; \backslash neg\; p$

| If {{mvar|p}} then {{mvar|q}}; not {{mvar|q}}; therefore not {{mvar|p}}

|-

| Hypothetical Syllogism

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; (q\; \backslash to\; r))\; \backslash models\; (p\; \backslash to\; r)$

| If {{mvar|p}} then {{mvar|q}}; if {{mvar|q}} then {{mvar|r}}; therefore, if {{mvar|p}} then {{mvar|r}}

|-

| Disjunctive Syllogism

| style="text-align:center;" | $((p\; \backslash lor\; q)\; \backslash land\; \backslash neg\; p)\; \backslash models\; q$

| Either {{mvar|p}} or {{mvar|q}}, or both; not {{mvar|p}}; therefore, {{mvar|q}}

|-

| Constructive Dilemma

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; (r\; \backslash to\; s)\; \backslash land\; (p\; \backslash lor\; r))\; \backslash models\; (q\; \backslash lor\; s)$

| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|r}} then {{mvar|s}}; but {{mvar|p}} or {{mvar|r}}; therefore {{mvar|q}} or {{mvar|s}}

|-

| Destructive Dilemma

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; (r\; \backslash to\; s)\; \backslash land(\backslash neg\; q\; \backslash lor\; \backslash neg\; s))\; \backslash models\; (\backslash neg\; p\; \backslash lor\; \backslash neg\; r)$

| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|r}} then {{mvar|s}}; but not {{mvar|q}} or not {{mvar|s}}; therefore not {{mvar|p}} or not {{mvar|r}}

|-

| Bidirectional Dilemma

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; (r\; \backslash to\; s)\; \backslash land(p\; \backslash lor\; \backslash neg\; s))\; \backslash models\; (q\; \backslash lor\; \backslash neg\; r)$

| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|r}} then {{mvar|s}}; but {{mvar|p}} or not {{mvar|s}}; therefore {{mvar|q}} or not {{mvar|r}}

|-

| Simplification

| style="text-align:center;" | $(p\; \backslash land\; q)\; \backslash models\; p$

| {{mvar|p}} and {{mvar|q}} are true; therefore {{mvar|p}} is true

|-

| Conjunction

| style="text-align:center;" | $p,\; q\; \backslash models\; (p\; \backslash land\; q)$

| {{mvar|p}} and {{mvar|q}} are true separately; therefore they are true conjointly

|-

| Addition

| style="text-align:center;" | $p\; \backslash models\; (p\; \backslash lor\; q)$

| {{mvar|p}} is true; therefore the disjunction ({{mvar|p}} or {{mvar|q}}) is true

|-

| Composition of conjunction

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash land\; (p\; \backslash to\; r))$ ⟚ $(p\; \backslash to\; (q\; \backslash land\; r))$

| If {{mvar|p}} then {{mvar|q}}; and if {{mvar|p}} then {{mvar|r}}; therefore if {{mvar|p}} is true then {{mvar|q}} and {{mvar|r}} are true

|-

| Composition of disjunction

| style="text-align:center;" | $((p\; \backslash to\; q)\; \backslash lor\; (p\; \backslash to\; r))$ ⟚ $(p\; \backslash to\; (q\; \backslash lor\; r))$

| If {{mvar|p}} then {{mvar|q}}; or if {{mvar|p}} then {{mvar|r}}; therefore if {{mvar|p}} is true then {{mvar|q}} or {{mvar|r}} is true

|-

| De Morgan's Theorem (1)

| style="text-align:center;" | $\backslash neg\; (p\; \backslash land\; q)$ ⟚ $(\backslash neg\; p\; \backslash lor\; \backslash neg\; q)$

| The negation of ({{mvar|p}} and {{mvar|q}}) is equiv. to (not {{mvar|p}} or not {{mvar|q}})

|-

| De Morgan's Theorem (2)

| style="text-align:center;" | $\backslash neg\; (p\; \backslash lor\; q)$ ⟚ $(\backslash neg\; p\; \backslash land\; \backslash neg\; q)$

| The negation of ({{mvar|p}} or {{mvar|q}}) is equiv. to (not {{mvar|p}} and not {{mvar|q}})

|-

| Commutation (1)

| style="text-align:center;" | $(p\; \backslash lor\; q)$ ⟚ $(q\; \backslash lor\; p)$

| ({{mvar|p}} or {{mvar|q}}) is equiv. to ({{mvar|q}} or {{mvar|p}})

|-

| Commutation (2)

| style="text-align:center;" | $(p\; \backslash land\; q)$ ⟚ $(q\; \backslash land\; p)$

| ({{mvar|p}} and {{mvar|q}}) is equiv. to ({{mvar|q}} and {{mvar|p}})

|-

| Commutation (3)

| style="text-align:center;" | $(p\; \backslash leftrightarrow\; q)$ ⟚ $(q\; \backslash leftrightarrow\; p)$

| ({{mvar|p}} iff {{mvar|q}}) is equiv. to ({{mvar|q}} iff {{mvar|p}})

|-

| Association (1)

| style="text-align:center;" | $(p\; \backslash lor\; (q\; \backslash lor\; r))$ ⟚ $((p\; \backslash lor\; q)\; \backslash lor\; r)$

| {{mvar|p}} or ({{mvar|q}} or {{mvar|r}}) is equiv. to ({{mvar|p}} or {{mvar|q}}) or {{mvar|r}}

|-

| Association (2)

| style="text-align:center;" | $(p\; \backslash land\; (q\; \backslash land\; r))$ ⟚ $((p\; \backslash land\; q)\; \backslash land\; r)$

| {{mvar|p}} and ({{mvar|q}} and {{mvar|r}}) is equiv. to ({{mvar|p}} and {{mvar|q}}) and {{mvar|r}}

|-

| Distribution (1)

| style="text-align:center;" | $(p\; \backslash land\; (q\; \backslash lor\; r))$ ⟚ $((p\; \backslash land\; q)\; \backslash lor\; (p\; \backslash land\; r))$

| {{mvar|p}} and ({{mvar|q}} or {{mvar|r}}) is equiv. to ({{mvar|p}} and {{mvar|q}}) or ({{mvar|p}} and {{mvar|r}})

|-

| Distribution (2)

| style="text-align:center;" | $(p\; \backslash lor\; (q\; \backslash land\; r))$ ⟚ $((p\; \backslash lor\; q)\; \backslash land\; (p\; \backslash lor\; r))$

| {{mvar|p}} or ({{mvar|q}} and {{mvar|r}}) is equiv. to ({{mvar|p}} or {{mvar|q}}) and ({{mvar|p}} or {{mvar|r}})

|-

| Double Negation

| style="text-align:center;" | $p$ ⟚ $\backslash neg\; \backslash neg\; p$

| {{mvar|p}} is equivalent to the negation of not {{mvar|p}}

|-

| Transposition

| style="text-align:center;" | $(p\; \backslash to\; q)$ ⟚ $(\backslash neg\; q\; \backslash to\; \backslash neg\; p)$

| If {{mvar|p}} then {{mvar|q}} is equiv. to if not {{mvar|q}} then not {{mvar|p}}

|-

| Material Implication

| style="text-align:center;" | $(p\; \backslash to\; q)$ ⟚ $(\backslash neg\; p\; \backslash lor\; q)$

| If {{mvar|p}} then {{mvar|q}} is equiv. to not {{mvar|p}} or {{mvar|q}}

|-

| Material Equivalence (1)

| style="text-align:center;" | $(p\; \backslash leftrightarrow\; q)$ ⟚ $((p\; \backslash to\; q)\; \backslash land\; (q\; \backslash to\; p))$

| ({{mvar|p}} {{not a typo|iff}} {{mvar|q}}) is equiv. to (if {{mvar|p}} is true then {{mvar|q}} is true) and (if {{mvar|q}} is true then {{mvar|p}} is true)

|-

| Material Equivalence (2)

| style="text-align:center;" | $(p\; \backslash leftrightarrow\; q)$ ⟚ $((p\; \backslash land\; q)\; \backslash lor\; (\backslash neg\; p\; \backslash land\; \backslash neg\; q))$

| ({{mvar|p}} {{not a typo|iff}} {{mvar|q}}) is equiv. to either ({{mvar|p}} and {{mvar|q}} are true) or (both {{mvar|p}} and {{mvar|q}} are false)

|-

| Material Equivalence (3)

| style="text-align:center;" | $(p\; \backslash leftrightarrow\; q)$ ⟚ $((p\; \backslash lor\; \backslash neg\; q)\; \backslash land\; (\backslash neg\; p\; \backslash lor\; q))$

| ({{mvar|p}} {{not a typo|iff}} {{mvar|q}}) is equiv to., both ({{mvar|p}} or not {{mvar|q}} is true) and (not {{mvar|p}} or {{mvar|q}} is true)

|-

| Exportation

| style="text-align:center;" | $((p\; \backslash land\; q)\; \backslash to\; r)\; \backslash models\; (p\; \backslash to\; (q\; \backslash to\; r))$

| from (if {{mvar|p}} and {{mvar|q}} are true then {{mvar|r}} is true) we can prove (if {{mvar|q}} is true then {{mvar|r}} is true, if {{mvar|p}} is true)

|-

| Importation

| style="text-align:center;" | $(p\; \backslash to\; (q\; \backslash to\; r))\backslash models((p\; \backslash land\; q)\; \backslash to\; r)$

| If {{mvar|p}} then (if {{mvar|q}} then {{mvar|r}}) is equivalent to if {{mvar|p}} and {{mvar|q}} then {{mvar|r}}

|-

| Idempotence of disjunction

| style="text-align:center;" | $p$ ⟚ $(p\; \backslash lor\; p)$

| {{mvar|p}} is true is equiv. to {{mvar|p}} is true or {{mvar|p}} is true

|-

| Idempotence of conjunction

| style="text-align:center;" | $p$ ⟚ $(p\; \backslash land\; p)$

| {{mvar|p}} is true is equiv. to {{mvar|p}} is true and {{mvar|p}} is true

|-

| Tertium non datur (Law of Excluded Middle)

| style="text-align:center;" | $\backslash models\; (p\; \backslash lor\; \backslash neg\; p)$

| {{mvar|p}} or not {{mvar|p}} is true

|-

| Law of Non-Contradiction

| style="text-align:center;" | $\backslash models\; \backslash neg\; (p\; \backslash land\; \backslash neg\; p)$

| {{mvar|p}} and not {{mvar|p}} is false, is a true statement

|-

|Explosion

| style="text-align:center;" | $(p\; \backslash land\; \backslash neg\; p)\; \backslash models\; q$

| {{mvar|p}} and not {{mvar|p}}; therefore {{mvar|q}}

|}

{{Main article|Natural deduction}}{{Transformation rules}}Natural deduction, since it is a method of syntactical proof, is specified by providing inference rules (also called rules of proof) for a language with the typical set of connectives ; no axioms are used other than these rules. The rules are covered below, and a proof example is given afterwards.

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 {{section link||Gentzen notation}}, which was covered earlier for a short argument, can actually be stacked to produce large tree-shaped natural deduction proofs—not to be confused with "truth trees", which is another name for analytic tableaux. There is also a style due to Stanisław Jaśkowski, where the formulas in the proof are written inside various nested boxes, 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. Lastly, there is the only notation style which will actually be used in this article, which is due to Patrick Suppes, but was much popularized by E.J. Lemmon and Benson Mates. 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, is a sequence of lines containing sentences, where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence. Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number. The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers. The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence. See the {{section link||Natural deduction proof example}}.

Natural deduction inference rules, due ultimately to Gentzen, are given below. 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. Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination, and MTT and DN are commonly given rules, although they are not primitive.

{| class="wikitable" style="margin:auto;"

|+ List of Inference Rules

|-

! Rule Name

! Alternative names

! Annotation

!Assumption set

! Statement

|-

| Rule of Assumptions|| Assumption|| A

|The current line number.|| At any stage of the argument, introduce a proposition as an assumption of the argument.

|-

| Conjunction introduction|| Ampersand introduction, conjunction (CONJ)|| m, n &I

|The union of the assumption sets at lines m and n.|| From $\backslash varphi$ and $\backslash psi$ at lines m and n, infer .

|-

| Conjunction elimination|| Simplification (S), ampersand elimination|| m &E

|The same as at line m.|| From at line m, infer $\backslash varphi$ and $\backslash psi$.

|-

| Disjunction introduction|| Addition (ADD)|| m ∨I

|The same as at line m.|| From $\backslash varphi$ at line m, infer $\backslash varphi\; \backslash lor\; \backslash psi$, whatever $\backslash psi$ may be.

|-

| Disjunction elimination|| Wedge elimination, dilemma (DL)|| j,k,l,m,n ∨E

|The lines j,k,l,m,n.|| From $\backslash varphi\; \backslash lor\; \backslash psi$ at line j, and an assumption of $\backslash varphi$ at line k, and a derivation of $\backslash chi$ from $\backslash varphi$ at line l, and an assumption of $\backslash psi$ at line m, and a derivation of $\backslash chi$ from $\backslash psi$ at line n, infer $\backslash chi$.

|-

|Disjunctive Syllogism

|Wedge elimination (∨E), modus tollendo ponens (MTP)

|m,n DS

|The union of the assumption sets at lines m and n.

|From $\backslash varphi\; \backslash lor\; \backslash psi$ at line m and $-\; \backslash varphi$ at line n, infer $\backslash psi$; from $\backslash varphi\; \backslash lor\; \backslash psi$ at line m and $-\; \backslash psi$ at line n, infer $\backslash varphi$.

|-

| Arrow elimination|| Modus ponendo ponens (MPP), modus ponens (MP), conditional elimination || m, n →E

|The union of the assumption sets at lines m and n.|| From $\backslash varphi\; \backslash to\; \backslash psi$ at line m, and $\backslash varphi$ at line n, infer $\backslash psi$.

|-

| Arrow introduction|| Conditional proof (CP), conditional introduction || n, →I (m)

|Everything in the assumption set at line n, excepting m, the line where the antecedent was assumed.|| From $\backslash psi$ at line n, following from the assumption of $\backslash varphi$ at line m, infer $\backslash varphi\; \backslash to\; \backslash psi$.

|-

| Reductio ad absurdum|| Indirect Proof (IP), negation introduction (−I), negation elimination (−E)|| m, n RAA (k)

|The union of the assumption sets at lines m and n, excluding k (the denied assumption).|| From a sentence and its denial{{refn|group=lower-alpha|To simplify the statement of the rule, the word "denial" here is used in this way: the denial of a formula $\backslash varphi$ that is not a negation is $-\; \backslash varphi$, whereas a negation, $-\; \backslash varphi$, has two denials, viz., $\backslash varphi$ and $-\; -\; \backslash varphi$.}} at lines m and n, infer the denial of any assumption appearing in the proof (at line k).

|-

| Double arrow introduction|| Biconditional definition (Df ↔), biconditional introduction|| m, n ↔ I

|The union of the assumption sets at lines m and n.|| From $\backslash varphi\; \backslash to\; \backslash psi$ and $\backslash psi\; \backslash to\; \backslash varphi$ at lines m and n, infer $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$.

|-

| Double arrow elimination|| Biconditional definition (Df ↔), biconditional elimination|| m ↔ E

|The same as at line m.|| From $\backslash varphi\; \backslash leftrightarrow\; \backslash psi$ at line m, infer either $\backslash varphi\; \backslash to\; \backslash psi$ or $\backslash psi\; \backslash to\; \backslash varphi$.

|-

| Double negation|| Double negation elimination|| m DN

|The same as at line m.|| From $-\; -\; \backslash varphi$ at line m, infer $\backslash varphi$.

|-

| Modus tollendo tollens|| Modus tollens (MT)|| m, n MTT

|The union of the assumption sets at lines m and n.|| From $\backslash varphi\; \backslash to\; \backslash psi$ at line m, and $-\; \backslash psi$ at line n, infer $-\; \backslash varphi$.

|}

The proof below derives $-P$ from $P\; \backslash to\; Q$ and $-Q$ using only MPP and RAA, which shows that MTT is not a primitive rule, since it can be derived from those two other rules.

{| class="wikitable" style="margin:auto;"

|+ Derivation of MTT from MPP and RAA

|-

! Assumption set

! Line number

! Sentence of proof

! Annotation

|-

| {{EquationRef|1}}|| {{EquationRef|1}} || $P\; \backslash to\; Q$ || A

|-

| {{EquationRef|2}} || {{EquationRef|2}} || $-Q$ || A

|-

| {{EquationRef|3}} || {{EquationRef|3}} || $P$ || A

|-

| {{EquationRef|1}}, {{EquationRef|3}} || {{EquationRef|4}} || $Q$ || {{EquationRef|1}}, {{EquationRef|3}} →E

|-

| {{EquationRef|1}}, {{EquationRef|2}} || {{EquationRef|5}} || $-P$ || {{EquationRef|2}}, {{EquationRef|4}} RAA

|}

{{Main article|Hilbert system}}

It is possible to perform proofs axiomatically, which means that certain tautologies are taken as self-evident 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 well-formed formula with any {{glossary link|substitution-instance|glossary=Glossary of logic}} of it. Alternatively, one uses axiom schemas instead of axioms, and no rule of substitution is used.

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 Axiomatic system (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. Frege's system used only implication and negation as connectives. It had six axioms:

• Proposition 1: $a\; \backslash to\; (b\; \backslash to\; a)$
• Proposition 2: $(c\; \backslash to\; (b\; \backslash to\; a))\; \backslash to\; ((c\; \backslash to\; b)\; \backslash to\; (c\; \backslash to\; a))$
• Proposition 8: $(d\; \backslash to\; (b\; \backslash to\; a))\; \backslash to\; (b\; \backslash to\; (d\; \backslash to\; a))$
• Proposition 28: $(b\; \backslash to\; a)\; \backslash to\; (\backslash neg\; a\; \backslash to\; \backslash neg\; b)$
• Proposition 31: $\backslash neg\; \backslash neg\; a\; \backslash to\; a$
• Proposition 41: $a\; \backslash to\; \backslash neg\; \backslash neg\; a$

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 truth-functional propositional logic.

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 $CCNpNqCpq$". Which, taken out of Łukasiewicz's Polish notation into modern notation, means $(\backslash neg\; p\; \backslash rightarrow\; \backslash neg\; q)\; \backslash rightarrow\; (p\; \backslash rightarrow\; q)$. Hence, Łukasiewicz is credited with this system of three axioms:

• $p\; \backslash to\; (q\; \backslash to\; p)$
• $(p\; \backslash to\; (q\; \backslash to\; r))\; \backslash to\; ((p\; \backslash to\; q)\; \backslash to\; (p\; \backslash to\; r))$
• $(\backslash neg\; p\; \backslash to\; \backslash neg\; q)\; \backslash to\; (q\; \backslash to\; p)$

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule. The exact same system was given (with an explicit substitution rule) by Alonzo Church, who referred to it as the system P₂ and helped popularize it.

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 well-formed formulas), the axioms are given as:

• $\backslash varphi\; \backslash to\; (\backslash psi\; \backslash to\; \backslash varphi)$
• $(\backslash varphi\; \backslash to\; (\backslash psi\; \backslash to\; \backslash chi))\; \backslash to\; ((\backslash varphi\; \backslash to\; \backslash psi)\; \backslash to\; (\backslash varphi\; \backslash to\; \backslash chi))$
• $(\backslash neg\; \backslash varphi\; \backslash to\; \backslash neg\; \backslash psi)\; \backslash to\; (\backslash psi\; \backslash to\; \backslash varphi)$

The schematic version of P₂ is attributed to John von Neumann, and is used in the Metamath "set.mm" formal proof database. It has also been attributed to Hilbert, and named $\backslash mathcal\{H\}$ in this context.

As an example, a proof of $A\; \backslash to\; A$ in P₂ is given below. First, the axioms are given names:

:(A1) $(p\; \backslash to\; (q\; \backslash to\; p))$

:(A2) $((p\; \backslash to\; (q\; \backslash to\; r))\; \backslash to\; ((p\; \backslash to\; q)\; \backslash to\; (p\; \backslash to\; r)))$

:(A3) $((\backslash neg\; p\; \backslash to\; \backslash neg\; q)\; \backslash to\; (q\; \backslash to\; p))$

And the proof is as follows:

1. $A\; \backslash to\; ((B\; \backslash to\; A)\; \backslash to\; A)$       (instance of (A1))
2. $(A\; \backslash to\; ((B\; \backslash to\; A)\; \backslash to\; A))\; \backslash to\; ((A\; \backslash to\; (B\; \backslash to\; A))\; \backslash to\; (A\; \backslash to\; A))$       (instance of (A2))
3. $(A\; \backslash to\; (B\; \backslash to\; A))\; \backslash to\; (A\; \backslash to\; A)$       (from (1) and (2) by modus ponens)
4. $A\; \backslash to\; (B\; \backslash to\; A)$       (instance of (A1))
5. $A\; \backslash to\; A$       (from (4) and (3) by modus ponens)

One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is decidable.{{rp|p=81}} Deciding satisfiability of propositional logic formulas is an NP-complete problem. However, practical methods exist (e.g., DPLL algorithm, 1962; Chaff algorithm, 2001) that are very fast for many useful cases. Recent work has extended the SAT solver algorithms to work with propositions containing arithmetic expressions; these are the SMT solvers.

{{Portal|Philosophy}}

• First-order logic
• Second-order propositional logic
• Second-order logic
• Higher-order logic

{{Div col|colwidth=20em}}

• Boolean algebra (logic)
• Boolean algebra (structure)
• Boolean algebra topics
• Boolean domain
• Boolean function
• Boolean-valued 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

{{Div col end}}

{{reflist|group=lower-alpha}}

{{Reflist|30em|refs=

{{Cite book |title=Semantics: a reader |date=2004 |publisher=Oxford University Press |isbn=978-0-19-513697-5 |editor-last=Davis |editor-first=Steven |location=New York |editor-last2=Gillon |editor-first2=Brendan S.}}

{{Cite book |last1=Ayala-Rincón |first1=Mauricio |url=https://link.springer.com/book/10.1007/978-3-319-51653-0 |title=Applied Logic for Computer Scientists |last2=de Moura |first2=Flávio L.C. |series=Undergraduate Topics in Computer Science |date=2017 |publisher=Springer |pages=2 |language=en |doi=10.1007/978-3-319-51653-0|isbn=978-3-319-51651-6 }}

{{Cite encyclopedia | last = Klement| first = Kevin C. | title = Propositional Logic | encyclopedia = Internet Encyclopedia of Philosophy | date = | url=https://iep.utm.edu/propositional-logic-sentential-logic/ | editor-last1 = Fieser | editor-first1 = James | editor-last2 = Dowden | editor-first2 = Bradley | access-date = 2025-04-07 }}

{{Cite book |last1=Bělohlávek |first1=Radim |title=Fuzzy logic and mathematics: a historical perspective |last2=Dauben |first2=Joseph Warren |last3=Klir |first3=George J. |date=2017 |publisher=Oxford University Press |isbn=978-0-19-020001-5 |location=New York, NY, United States of America |pages=463}}

{{Cite book |last=Manzano |first=María |title=Extensions of first order logic |date=2005 |publisher=Cambridge University Press |isbn=978-0-521-35435-6 |edition=Digitally printed first paperback version |series=Cambridge tracts in theoretical computer science |location=Cambridge |pages=180}}

{{Cite web |title=Propositional Logic |url=https://www.cs.miami.edu/home/geoff/Courses/CSC648-12S/Content/Propositional.shtml |access-date=2024-03-22 |website=www.cs.miami.edu}}

{{Cite book |last=Howson |first=Colin |title=Logic with trees: an introduction to symbolic logic |date=1997 |publisher=Routledge |isbn=978-0-415-13342-5 |location=London; New York |pages=ix, x,5–6, 15–16, 20, 24–29, 38, 42–43, 47}}

{{Cite web |title=Natural Deduction {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/natural-deduction/ |access-date=2024-03-23 |language=en-US}}

{{Cite web |last=Weisstein |first=Eric W. |title=Sequent Calculus |url=https://mathworld.wolfram.com/ |access-date=2024-03-23 |website=mathworld.wolfram.com |language=en}}

{{Cite book |last=Cook |first=Roy T. |title=A dictionary of philosophical logic |date=2009 |publisher=Edinburgh University Press |isbn=978-0-7486-2559-8 |location=Edinburgh |pages=82,176 |language=en}}

{{Cite web |last=Weisstein |first=Eric W. |title=Propositional Calculus |url=https://mathworld.wolfram.com/ |access-date=2024-03-22 |website=mathworld.wolfram.com |language=en}}

{{Cite journal |last=Chowdhary |first=K.R. |date=2020 |title=Fundamentals of Artificial Intelligence |url=https://doi.org/10.1007/978-81-322-3972-7 |journal=SpringerLink |language=en |pages=31–34 |doi=10.1007/978-81-322-3972-7|isbn=978-81-322-3970-3 }}

{{Cite encyclopedia | last = Franks | first = Curtis | title = Propositional Logic | encyclopedia = Stanford Encyclopedia of Philosophy | editor-last1 = Zalta | editor-first1 = Edward N. | editor-last2 = Nodelman | editor-first2 = Uri | publisher = Metaphysics Research Lab, Stanford University | edition = Winter 2024 | date = 2024 | url = https://plato.stanford.edu/archives/win2024/entries/logic-propositional/ | access-date = 2025-04-07 }}

{{Cite book |last=Rogers |first=Robert L. |url=http://dx.doi.org/10.1016/c2013-0-11894-6 |title=Mathematical Logic and Formalized Theories |date=1971 |publisher=Elsevier |isbn=978-0-7204-2098-2 |pages=38–39 |doi=10.1016/c2013-0-11894-6 |language=en}}

{{Cite book |last=Beall |first=Jeffrey C. |title=Logic: the basics |date=2010 |publisher=Routledge |isbn=978-0-203-85155-5 |edition=1. publ |location=London |pages=6, 8, 14–16, 19–20, 44–48, 50–53, 56 |language=en}}

{{Citation |last1=McGrath |first1=Matthew |title=Propositions |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/win2023/entries/propositions/ |access-date=2024-03-22 |edition=Winter 2023 |publisher=Metaphysics Research Lab, Stanford University |last2=Frank |first2=Devin |editor2-last=Nodelman |editor2-first=Uri}}

{{Cite web |last=Weisstein |first=Eric W. |title=Connective |url=https://mathworld.wolfram.com/ |access-date=2024-03-22 |website=mathworld.wolfram.com |language=en}}

{{Cite journal |last=Landman |first=Fred |date=1991 |title=Structures for Semantics |url=https://doi.org/10.1007/978-94-011-3212-1 |journal=Studies in Linguistics and Philosophy |language=en |volume=45 |pages=127 |doi=10.1007/978-94-011-3212-1 |isbn=978-0-7923-1240-6 |issn=0924-4662}}

{{Citation |last1=Demey |first1=Lorenz |title=Logic and Probability |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2023/entries/logic-probability/ |access-date=2024-03-22 |edition=Fall 2023 |publisher=Metaphysics Research Lab, Stanford University |last2=Kooi |first2=Barteld |last3=Sack |first3=Joshua |editor2-last=Nodelman |editor2-first=Uri}}

{{Citation |last1=Shramko |first1=Yaroslav |title=Truth Values |date=2021 |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/win2021/entriesruth-values/ |access-date=2024-03-23 |edition=Winter 2021 |publisher=Metaphysics Research Lab, Stanford University |last2=Wansing |first2=Heinrich |encyclopedia=The Stanford Encyclopedia of Philosophy}}

{{Cite web |title=MathematicalLogic |url=https://www.cs.yale.edu/homes/aspnes/pinewiki/MathematicalLogic.html |access-date=2024-03-23 |website=www.cs.yale.edu}}

{{Cite book |last=Hodges |first=Wilfrid |title=Logic |date=2001 |publisher=Penguin Books |isbn=978-0-14-100314-6 |edition=2 |location=London |pages=130–131 |language=en}}

{{Cite book |last=Smullyan |first=Raymond M.|author-link=Raymond Smullyan |title=First-Order Logic |date=1995 |orig-year=1968|publisher=Dover Publications|isbn=978-0-486-68370-6 |location=New York |pages=5, 10–11, 14 |language=en}}

{{Cite book |last=Plato |first=Jan von |title=Elements of logical reasoning |date=2013 |publisher=Cambridge University press |isbn=978-1-107-03659-8 |edition=1. publ |location=Cambridge |pages=9,32,121}}

{{Cite web |date=2021-09-09 |title=1.4: Tautologies and contradictions |url=https://math.libretexts.org/Bookshelves/Combinatorics_and_Discrete_Mathematics/Elementary_Foundations%3A_An_Introduction_to_Topics_in_Discrete_Mathematics_(Sylvestre)/01%3A_Symbolic_language/1.04%3A_Tautologies_and_contradictions |access-date=2024-03-29 |website=Mathematics LibreTexts |language=en}}

{{Cite book |last=Sylvestre |first=Jeremy |url=https://sites.ualberta.ca/~jsylvest/books/EF/section-symb-lang-taut-contra.html |title=EF Tautologies and contradictions |language=en-US}}

{{Cite book |last1=DeLancey |first1=Craig |url=https://intrologicimport.pressbooks.tru.ca/chapter/9-if-and-only-if-using-theorems-a-concise-introduction-to-logic/ |title=Elementary Formal Logic |last2=Woodrow |first2=Jenna |publisher=Pressbooks |year=2017 |edition=1}}

{{Cite book |last=Humberstone |first=Lloyd |url=https://www.worldcat.org/title/694679197 |title=The connectives |date=2011 |publisher=MIT Press |isbn=978-0-262-01654-4 |location=Cambridge, Mass |pages=118, 702 |oclc=694679197}}

{{Citation |last=Restall |first=Greg |title=Substructural Logics |date=2018 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2018/entries/logic-substructural/ |access-date=2024-03-22 |edition=Spring 2018 |publisher=Metaphysics Research Lab, Stanford University}}

{{Cite book |last1=Allen |first1=Colin |title=Logic primer |last2=Hand |first2=Michael |date=2022 |publisher=The MIT Press |isbn=978-0-262-54364-4 |edition=3rd |location=Cambridge, Massachusetts}}

{{Cite web |title=Validity and Soundness {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/val-snd/ |access-date=2024-04-05 |language=en-US}}

{{Cite book |last=Restall |first=Greg |title=Logic: an introduction |date=2010 |publisher=Routledge |isbn=978-0-415-40068-8 |series=Fundamentals of philosophy |location=London |pages=5, 36–41, 55–60, 69}}

{{Cite book |last=Lemmon |first=Edward John |title=Beginning logic |date=1998 |publisher=Chapman & Hall/CRC |isbn=978-0-412-38090-7 |location=Boca Raton, FL |pages=passim, especially 39–40}}

{{Cite book |last=Arthur |first=Richard T. W. |url=https://www.worldcat.org/title/962129086 |title=An introduction to logic: using natural deduction, real arguments, a little history, and some humour |date=2017 |publisher=Broadview Press |isbn=978-1-55481-332-2 |edition=2nd |location=Peterborough, Ontario |oclc=962129086}}

{{Cite web |title=Introduction to Logic - Chapter 2 |url=http://intrologic.stanford.edu/chapters/chapter_02.html |access-date=2024-03-22 |website=intrologic.stanford.edu}}

{{Citation |last1=Pelletier |first1=Francis Jeffry |title=Natural Deduction Systems in Logic |date=2024 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2024/entries/natural-deduction/ |access-date=2024-03-22 |edition=Spring 2024 |publisher=Metaphysics Research Lab, Stanford University |last2=Hazen |first2=Allen |editor2-last=Nodelman |editor2-first=Uri}}

{{Cite book |last=Hodges |first=Wilfrid |title=Logic |date=1977 |publisher=Penguin |isbn=978-0-14-021985-2 |location=Harmondsworth; New York |pages=80–85}}

{{Cite book |last1=Hansson |first1=Sven Ove |title=Introduction to formal philosophy |last2=Hendricks |first2=Vincent F. |date=2018 |publisher=Springer |isbn=978-3-030-08454-7 |series=Springer undergraduate texts in philosophy |location=Cham |pages=38}}

{{Cite book |last1=Beall |first1=J. C. |url=https://books.google.com/books?id=qrUUDAAAQBAJ |title=Logical Pluralism |last2=Restall |first2=Greg |date=2006 |publisher=Clarendon Press |isbn=978-0-19-928840-3 |pages=38 |language=en}}

{{Cite book |last=Smullyan |first=Raymond M. |url=https://books.google.com/books?id=n6S-AwAAQBAJ |title=A Beginner's Guide to Mathematical Logic |date=2014-07-23 |publisher=Courier Corporation |isbn=978-0-486-49237-7 |pages=102–103 |language=en}}

{{Cite book |last=Mendelsohn |first=Richard L. |url=https://books.google.com/books?id=G6_90xFwUbUC |title=The Philosophy of Gottlob Frege |date=2005-01-10 |publisher=Cambridge University Press |isbn=978-1-139-44403-3 |pages=185 |language=en}}

{{Cite book |last=Łukasiewicz |first=Jan |url=https://books.google.com/books?id=Jb_zOwAACAAJ |title=Jan Lukasiewicz: Selected Works |date=1970 |publisher=North-Holland |pages=136 |language=en}}

{{Cite book |last=Church |first=Alonzo |url=https://books.google.com/books?id=JDLQOMKbdScC |title=Introduction to Mathematical Logic |date=1996 |publisher=Princeton University Press |isbn=978-0-691-02906-1 |pages=119 |language=en}}

{{Cite web |title=Proof Explorer - Home Page - Metamath |url=https://us.metamath.org/mpegif/mmset.html#scaxioms |access-date=2024-07-02 |website=us.metamath.org |language=EN-US}}

{{Cite book |last=Walicki |first=Michał |title=Introduction to mathematical logic |date=2017 |publisher=World Scientific |isbn=978-981-4719-95-7 |edition=Extended |location=New Jersey |pages=126}}

{{Cite web |title=3.1 Propositional Logic |url=https://www.teach.cs.toronto.edu/~csc110y/fall/notes/03-logic/01-propositional-logic.html |access-date=2024-03-22 |website=www.teach.cs.toronto.edu}}

{{Cite web |title=Lecture Topics for Discrete Math Students |url=https://math.colorado.edu/~kearnes/Teaching/Courses/F23/discretel.html |access-date=2024-03-22 |website=math.colorado.edu}}

{{Cite web |title=Compactness {{!}} Internet Encyclopedia of Philosophy |url=https://iep.utm.edu/compactness/ |access-date=2024-03-22 |language=en-US}}

{{Cite book |last=Kleene |first=Stephen Cole |title=Mathematical logic |date=2002 |publisher=Dover Publications |isbn=978-0-486-42533-7 |edition=Dover |location=Mineola, N.Y}}

{{Cite book |last=Lande |first=Nelson P. |title=Classical logic and its rabbit holes: a first course |date=2013 |publisher=Hackett Publishing Co., Inc |isbn=978-1-60384-948-7 |location=Indianapolis, Ind |pages=20}}

{{Cite book |last=Bostock |first=David |title=Intermediate logic |date=1997 |publisher=Clarendon Press; Oxford University Press |isbn=978-0-19-875141-0 |location=Oxford : New York |pages=4–5, 8–13, 18–19, 22, 27, 29, 191, 194}}

{{Cite book |last=Hunter |first=Geoffrey |title=Metalogic: An Introduction to the Metatheory of Standard First-Order Logic |publisher=University of California Press |year=1971 |isbn=0-520-02356-0}}

{{cite web |title=Russell: the Journal of Bertrand Russell Studies |url=http://digitalcommons.mcmaster.ca/cgi/viewcontent.cgi?article=1219&context=russelljournal |url-status=dead}}

{{citation | last1=Smith | first1=Peter | title=An introduction to formal logic | publisher=Cambridge University Press | isbn=978-0-521-00804-4 | year=2003}}. (Defines "expressively adequate", shortened to "adequate set of connectives" in a section heading.)

{{citation| last = Tao | first = Terence | authorlink = Terence Tao |chapter = The completeness and compactness theorems of first-order logic| doi = 10.1090/mbk/077| isbn = 978-0-8218-5280-4| mr = 2780010| pages = 27–31| publisher = American Mathematical Society| title = An epsilon of room, II| section-url = https://terrytao.wordpress.com/2009/04/10/the-completeness-and-compactness-theorems-of-first-order-logic/| year = 2010}}

[https://web.archive.org/web/20120807235445/http://frege.brown.edu/heck/pdf/unpublished/TruthInFrege.pdf Truth in Frege]

{{cite book|first1=D. |last1=Hilbert |first2=W. |last2=Ackermann |title=Principles of Mathematical Logic |oclc=372927 |year=1950 |publisher=Chelsea Publishing Company}}

{{cite book|url=http://plato.stanford.edu/archives/spr2016/entries/logic-ancient/|title=The Stanford Encyclopedia of Philosophy|first=Susanne|last=Bobzien|chapter=Ancient Logic |editor-first=Edward N.|editor-last=Zalta|date=1 January 2016|publisher=Metaphysics Research Lab, Stanford University |via=Stanford Encyclopedia of Philosophy}}

{{Cite web|title=Propositional Logic {{!}} Internet Encyclopedia of Philosophy|url=https://iep.utm.edu/prop-log/|access-date=2020-08-20|language=en-US}}

{{Citation |last=Bobzien |first=Susanne |title=Ancient Logic |date=2020 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/sum2020/entries/logic-ancient/ |access-date=2024-03-22 |edition=Summer 2020 |publisher=Metaphysics Research Lab, Stanford University}}

{{cite book|url=http://plato.stanford.edu/archives/spr2014/entries/leibniz-logic-influence/|title=The Stanford Encyclopedia of Philosophy|first=Volker|last=Peckhaus|chapter=Leibniz's Influence on 19th Century Logic |editor-first=Edward N.|editor-last=Zalta|date=1 January 2014|publisher=Metaphysics Research Lab, Stanford University |via=Stanford Encyclopedia of Philosophy}}

{{cite book |title=A Concise Introduction to Logic 10th edition |last=Hurley |first=Patrick |year=2007 |publisher=Wadsworth Publishing |page=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, Noord-Hollandsche Uitg. Mij., Amsterdam, 1955, pp. 309–42. Reprinted in Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969

{{cite journal|last1=Anellis|first1=Irving H.|authorlink=Irving Anellis|title=Peirce's Truth-functional Analysis and the Origin of the Truth Table|journal=History and Philosophy of Logic|date=2012|volume=33|pages=87–97|doi=10.1080/01445340.2011.621702|s2cid=170654885 }}

{{Cite web |title=Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables |url=https://www.math.fsu.edu/~wooland/hm2ed/Part2Module1/Part2Module1.html |access-date=2024-03-22 |website=www.math.fsu.edu}}

{{Cite web |title=Lecture Notes on Logical Organization and Critical Thinking |url=https://www2.hawaii.edu/~sugihara/courses/HCU2016s_TC/notes/CriticalThinking.html |access-date=2024-03-22 |website=www2.hawaii.edu}}

{{Cite web |title=Logical Connectives |url=https://sites.millersville.edu/bikenaga/math-proof/logical-connectives/logical-connectives.html |access-date=2024-03-22 |website=sites.millersville.edu}}

{{Cite web |title=Lecture1 |url=https://www.cs.columbia.edu/~rgu/courses/e6998/fall2018/Lecture1.html |access-date=2024-03-22 |website=www.cs.columbia.edu}}

{{Cite web |title=Watson |url=http://watson.latech.edu/book/intelligence/intelligenceApproaches2b1.html |access-date=2024-03-22 |website=watson.latech.edu}}

{{Cite web |title=Introduction to Theoretical Computer Science, Chapter 1 |url=https://www.cs.odu.edu/~toida/nerzic/390teched/math/logic.html |access-date=2024-03-22 |website=www.cs.odu.edu}}

{{Cite journal |last=Stojnić |first=Una |date=2017 |title=One's Modus Ponens: Modality, Coherence and Logic |url=https://www.jstor.org/stable/48578954 |journal=Philosophy and Phenomenological Research |volume=95 |issue=1 |pages=167–214 |doi=10.1111/phpr.12307 |jstor=48578954 |issn=0031-8205}}

{{Citation |last=Dutilh Novaes |first=Catarina |title=Argument and Argumentation |date=2022 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2022/entries/argument/ |access-date=2024-04-05 |edition=Fall 2022 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri}}

{{Citation |last1=Paseau |first1=Alexander |title=Deductivism in the Philosophy of Mathematics |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/fall2023/entries/deductivism-mathematics/ |access-date=2024-03-22 |edition=Fall 2023 |publisher=Metaphysics Research Lab, Stanford University |last2=Pregel |first2=Fabian |editor2-last=Nodelman |editor2-first=Uri}}

{{Cite book |last=Russell |first=Bertrand |title=Principles of mathematics |date=2010 |publisher=Routledge |isbn=978-0-415-48741-2 |series=Routledge classics |location=London |pages=17}}

{{Cite book |last=Goldrei |first=Derek |title=Propositional and predicate calculus: a model of argument |date=2005 |publisher=Springer |isbn=978-1-85233-921-0 |location=London |pages=69 |language=en}}

{{Cite web |title=Propositional Logic |url=https://www.cs.rochester.edu/u/nelson/courses/csc_173/proplogic/expressions.html |access-date=2024-03-22 |website=www.cs.rochester.edu}}

{{Cite web |title=Propositional calculus |url=https://www.cs.cornell.edu/courses/cs671/1999fa/typed%20logic/node18.html |access-date=2024-03-22 |website=www.cs.cornell.edu}}

{{Cite journal |last1=Metcalfe |first1=David |last2=Powell |first2=John |date=2011 |title=Should doctors spurn Wikipedia? |journal=Journal of the Royal Society of Medicine |language=en |volume=104 |issue=12 |pages=488–489 |doi=10.1258/jrsm.2011.110227 |issn=0141-0768 |pmc=3241521 |pmid=22179287}}

{{Cite book |last1=Ayers |first1=Phoebe |url=https://www.worldcat.org/title/185698411 |title=How Wikipedia works: and how you can be a part of it |last2=Matthews |first2=Charles |last3=Yates |first3=Ben |date=2008 |publisher=No Starch Press |isbn=978-1-59327-176-3 |location=San Francisco |pages=22 |oclc=185698411}}

{{Citation |last1=Shapiro |first1=Stewart |title=Classical Logic |date=2024 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2024/entries/logic-classical/ |access-date=2024-03-25 |edition=Spring 2024 |publisher=Metaphysics Research Lab, Stanford University |last2=Kouri Kissel |first2=Teresa |editor2-last=Nodelman |editor2-first=Uri}}

{{Cite book |last=Fitting |first=Melvin |url=https://books.google.com/books?id=133kBwAAQBAJ&pg=PA16 |title=First-Order Logic and Automated Theorem Proving |date=2012-12-06 |publisher=Springer Science & Business Media |isbn=978-1-4612-2360-3 |pages=16 |language=en}}

{{Cite book |last=Nascimento |first=Marco Antonio Chaer |title=Frontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013) |date=2015 |publisher=Springer |others=International Workshop on Quantum Systems in Chemistry and Physics |isbn=978-3-319-14397-2 |series=Progress in theoretical chemistry and physics |location=Cham |pages=255 |language=en}}

{{Cite book |last1=Restall |first1=Greg |url=https://books.google.com/books?id=IJVnEAAAQBAJ |title=Logical Methods |last2=Standefer |first2=Shawn |date=2023-01-03 |publisher=MIT Press |isbn=978-0-262-54484-9 |pages=76 |language=en}}

{{Citation |last=Aloni |first=Maria |title=Disjunction |date=2023 |encyclopedia=The Stanford Encyclopedia of Philosophy |editor-last=Zalta |editor-first=Edward N. |url=https://plato.stanford.edu/archives/spr2023/entries/disjunction/ |access-date=2024-03-23 |edition=Spring 2023 |publisher=Metaphysics Research Lab, Stanford University |editor2-last=Nodelman |editor2-first=Uri}}

{{Cite book |last=Makridis |first=Odysseus |title=Symbolic logic |date=2022 |publisher=Palgrave Macmillan |isbn=978-3-030-67395-6 |series=Palgrave philosophy today |location=Cham, Switzerland |pages=119}}

{{Cite book |last=Burgess |first=John P. |url=https://www.worldcat.org/title/276141382 |title=Philosophical logic |date=2009 |publisher=Princeton University Press |isbn=978-0-691-13789-6 |series=Princeton foundations of contemporary philosophy |location=Princeton |pages=5 |oclc=276141382}}

{{Cite book |last=Levin |first=Oscar |url=https://discrete.openmathbooks.org/dmoi3/sec_propositional.html |title=Propositional Logic |language=en-US}}

{{Cite book |last=Cunningham |first=Daniel W. |title=Set theory: a first course |date=2016 |publisher=Cambridge University Press |isbn=978-1-107-12032-7 |series=Cambridge mathematical textbooks |location=New York, NY}}

{{Cite book |last1=Genesereth |first1=Michael |url=https://link.springer.com/10.1007/978-3-031-01801-5 |title=Introduction to Logic |last2=Kao |first2=Eric J. |date=2017 |publisher=Springer International Publishing |isbn=978-3-031-00673-9 |series=Synthesis Lectures on Computer Science |location=Cham |pages=18 |language=en |doi=10.1007/978-3-031-01801-5}}

{{Cite web |title=6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation |url=https://leanprover.github.io/logic_and_proof/semantics_of_propositional_logic.html |access-date=2024-03-28 |website=leanprover.github.io}}

{{Cite web |title=Knowledge Representation and Reasoning: Basics of Logics |url=https://www.emse.fr/~zimmermann/Teaching/KRR/generalities.html |access-date=2024-03-28 |website=www.emse.fr}}

{{Cite book |url=https://www.worldcat.org/title/681481210 |title=Computational logic in multi-agent systems: 10th international workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009: revised selected and invited papers |date=2010 |publisher=Springer |isbn=978-3-642-16866-6 |editor-last=Dix |editor-first=J. |series=Lecture notes in computer science |location=Berlin; New York |pages=49 |oclc=681481210 |editor-last2=Fisher |editor-first2=Michael |editor-last3=Novak |editor-first3=Peter}}

{{Cite book |title=Computational models of argument: proceedings of comma 2020 |date=2020 |publisher=IOS Press |isbn=978-1-64368-106-1 |editor-last=Prakken |editor-first=Henry |series=Frontiers in artificial intelligence and applications |location=Washington |pages=252 |editor-last2=Bistarelli |editor-first2=Stefano |editor-last3=Santini |editor-first3=Francesco |editor-last4=Taticchi |editor-first4=Carlo}}

{{Cite book |title=Advances in Mathematics Education Research on Proof and Proving: An International Perspective |date=2018 |publisher=Springer International Publishing : Imprint: Springer |isbn=978-3-319-70996-3 |editor-last=Harel |editor-first=Guershon |edition=1st ed. 2018 |series=ICME-13 Monographs |location=Cham |pages=181 |editor-last2=Stylianides |editor-first2=Andreas J.}}

{{Cite journal |last=DeLancey |first=Craig |date=2017 |title=A Concise Introduction to Logic: §4. Proofs |url=https://milnepublishing.geneseo.edu/concise-introduction-to-logic/chapter/4-proofs/ |access-date=2024-03-23 |website=Milne Publishing}}

{{Citation |last1=Ferguson |first1=Thomas Macaulay |title=semantic consequence |date=2016-06-23 |work=A Dictionary of Logic |url=https://www.oxfordreference.com/display/10.1093/acref/9780191816802.001.0001/acref-9780191816802-e-387 |access-date=2024-03-23 |publisher=Oxford University Press |language=en |doi=10.1093/acref/9780191816802.001.0001 |isbn=978-0-19-181680-2 |last2=Priest |first2=Graham}}

{{Citation |last1=Ferguson |first1=Thomas Macaulay |title=syntactic consequence |date=2016-06-23 |work=A Dictionary of Logic |url=https://www.oxfordreference.com/display/10.1093/acref/9780191816802.001.0001/acref-9780191816802-e-440 |access-date=2024-03-23 |publisher=Oxford University Press |language=en |doi=10.1093/acref/9780191816802.001.0001 |isbn=978-0-19-181680-2 |last2=Priest |first2=Graham}}

{{Cite web |date=2024-03-14 |title=Truth table {{!}} Boolean, Operators, Rules {{!}} Britannica |url=https://www.britannica.com/topic/truth-table |access-date=2024-03-23 |website=www.britannica.com |language=en}}

{{Cite web |title=Analytic Tableaux |url=https://www3.cs.stonybrook.edu/~skiena/113/lectures/lecture5/lecture5.html |access-date=2024-03-23 |website=www3.cs.stonybrook.edu}}

{{Cite web |title=Formal logic - Semantic Tableaux, Proofs, Rules {{!}} Britannica |url=https://www.britannica.com/topic/formal-logic/Semantic-tableaux |access-date=2024-03-23 |website=www.britannica.com |language=en}}

{{Cite web |title=Axiomatic method {{!}} Logic, Proofs & Foundations {{!}} Britannica |url=https://www.britannica.com/science/axiomatic-method |access-date=2024-03-23 |website=www.britannica.com |language=en}}

{{Cite web |title=Propositional Logic |url=https://mally.stanford.edu/tutorial/sentential.html |access-date=2024-03-23 |website=mally.stanford.edu}}

{{Cite web |title=Interactive Tutorial of the Sequent Calculus |url=http://logitext.mit.edu/tutorial |access-date=2024-03-23 |website=logitext.mit.edu}}

{{Cite book |last=Lawson |first=Mark V. |title=A first course in logic |date=2019 |publisher=CRC Press, Taylor & Francis Group |isbn=978-0-8153-8664-3 |location=Boca Raton |pages=example 1.58}}

{{Cite book |last=Dean |first=Neville |title=Logic and language |date=2003 |publisher=Palgrave Macmillan |isbn=978-0-333-91977-4 |location=Basingstoke |pages=66}}

{{Cite book |last1=Chiswell |first1=Ian |title=Mathematical logic |last2=Hodges |first2=Wilfrid |date=2007 |publisher=Oxford university press |isbn=978-0-19-857100-1 |series=Oxford texts in logic |location=Oxford |pages=3}}

{{cite web |last=Toida |first=Shunichi |date=2 August 2009 |title=Proof of Implications |url=http://www.cs.odu.edu/~toida/nerzic/content/logic/prop_logic/implications/implication_proof.html |access-date=10 March 2010 |work=CS381 Discrete Structures/Discrete Mathematics Web Course Material |publisher=Department of Computer Science, Old Dominion University}}

{{Cite web |title=Natural Deduction Systems in Logic > Notes (Stanford Encyclopedia of Philosophy) |url=https://plato.stanford.edu/entries/natural-deduction/notes.html#note-21 |access-date=2024-04-19 |website=plato.stanford.edu |language=en}}

{{citation|last = Andrews |first = Peter B. |doi = 10.1007/978-94-015-9934-4 |edition = Second |isbn = 1-4020-0763-9| mr = 1932484| page = 201| publisher = Kluwer Academic Publishers, Dordrecht| series = Applied Logic Series | title = An introduction to mathematical logic and type theory: to truth through proof | url = https://books.google.com/books?id=nV4zAsWAvT0C&pg=PA201| volume = 27| year = 2002}}

{{Cite book |last=Matthes |first=Ralph |url=https://books.google.com/books?id=MnfcyigJ898C |title=Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types |date=1999 |publisher=Herbert Utz Verlag |isbn=978-3-89675-578-0 |pages=23 |language=en}}

{{Cite web |title=Predicate Logic |url=https://www3.cs.stonybrook.edu/~skiena/113/lectures/lecture26/lecture26.html |access-date=2024-03-22 |website=www3.cs.stonybrook.edu}}

{{Cite web |title=Philosophy 404: Lecture Five |url=https://www.webpages.uidaho.edu/~morourke/404-phil/Summer-99/Lecture%20Notes/5.htm |access-date=2024-03-22 |website=www.webpages.uidaho.edu}}

{{Cite book |last=Plato |first=Jan von |title=Elements of logical reasoning |date=2013 |publisher=Cambridge University press |isbn=978-1-107-03659-8 |edition=1. publ |location=Cambridge |pages=9}}

{{Cite web |title=Propositional Logic {{!}} Brilliant Math & Science Wiki |url=https://brilliant.org/wiki/propositional-logic/ |access-date=2020-08-20 |website=brilliant.org |language=en-us}}

{{Cite book |last=Quine | first= W. V. O. |author-link= Willard Van Orman Quine |title=Mathematical Logic |year=1980|publisher=Harvard University Press |isbn=0-674-55451-5}}

{{Cite book |title=Rudolf Carnap: studies in semantics: the collected works of rudolf carnap, volume 7 |date=2024 |publisher=Oxford University Press |isbn=978-0-19-289487-8 |editor-last=Awodey |editor-first=Steve |location=New York |pages=xxvii |editor-last2=Arnold |editor-first2=Greg Frost-}}

{{Cite book |last1=Lucas |first1=Peter |url=https://www.cs.ru.nl/P.Lucas/teaching/KeR/logicintro.pdf |title=Principles of expert systems |last2=Gaag |first2=Linda van der |date=1991 |publisher=Addison-Wesley |isbn=978-0-201-41640-4 |series=International computer science series |location=Wokingham, England; Reading, Mass |pages=26}}

{{Cite web |last=Bachmair |first=Leo |date=2009 |title=CSE541 Logic in Computer Science |url=https://www3.cs.stonybrook.edu/~cse541/Spring2009/cse541PropLogic.pdf |website=Stony Brook University}}

}}

• 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, North-Holland, 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.

• {{Cite book|last=Hofstadter |first=Douglas |author-link=Douglas Hofstadter |title=Gödel, Escher, Bach: An Eternal Golden Braid |year=1979 |publisher=Basic Books |isbn=978-0-465-02656-2 }}

{{Commons category}}

• {{Cite encyclopedia | last = Klement| first = Kevin C. | title = Propositional Logic | encyclopedia = Internet Encyclopedia of Philosophy | date = | url=https://iep.utm.edu/propositional-logic-sentential-logic/ | editor-last1 = Fieser | editor-first1 = James | editor-last2 = Dowden | editor-first2 = Bradley | access-date = 2025-04-07 }}
• {{Cite encyclopedia | last = Franks | first = Curtis | title = Propositional Logic | encyclopedia = Stanford Encyclopedia of Philosophy | editor-last1 = Zalta | editor-first1 = Edward N. | editor-last2 = Nodelman | editor-first2 = Uri | publisher = Metaphysics Research Lab, Stanford University | edition = Winter 2024 | date = 2024 | url = https://plato.stanford.edu/entries/logic-propositional/ | access-date = 2025-04-07 }}

• [http://www.qedeq.org/current/doc/math/qedeq_formal_logic_v1_en.pdf Formal Predicate Calculus], contains a systematic formal development with axiomatic proof
• [http://www.fecundity.com/logic/ forall x: an introduction to formal logic], by P.D. Magnus, covers formal semantics and proof theory for sentential logic.
• [http://logicinaction.org/docs/ch2.pdf Chapter 2 / Propositional Logic] from [http://logicinaction.org Logic In Action]
• [https://www.nayuki.io/page/propositional-sequent-calculus-prover Propositional sequent calculus prover] on Project Nayuki. (note: implication can be input in the form !X|Y, and a sequent can be a single formula prefixed with > and having no commas)
• [https://docs.google.com/document/d/1DhtRAPcMwJmiQnbdmFcHWaOddQ7kuqqDnWp2LZcGlnY/edit?usp=sharing Propositional Logic - A Generative Grammar]
• [https://propositional-calculator.com/ A Propositional Calculator that helps to understand simple expressions]

{{Classical logic}}

{{Formal Fallacy}}

{{Mathematical logic}}

{{Authority control}}

Category:Logical calculi

Category:Boolean algebra

Category:Classical logic

Category:Analytic philosophy