Propositional calculus

From Wikipedia, the free encyclopedia

The propositional calculus[a] is a branch of logic.[1] It is also called propositional logic,[2] statement logic,[1] sentential calculus,[3] sentential logic,[1] or sometimes zeroth-order logic.[4][5] It deals with propositions[1] (which can be true or false)[6] and relations between propositions,[7] including the construction of arguments based on them.[8] Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, equivalence, and negation.[9][10][11][12] Some sources include other connectives, as in the table below.

Unlike first-order logic, propositional logic does not deal with non-logical objects, predicates about them, or quantifiers. However, all the machinery of propositional logic is included in first-order logic and higher-order logics. In this sense, propositional logic is the foundation of first-order logic and higher-order logic.

Propositional logic is typically studied with a formal language, in which propositions are represented by letters, which are called propositional variables. These are then used, together with symbols for connectives, to make compound propositions. Because of this, the propositional variables are called atomic formulas of a formal zeroth-order language.[10][2] While the atomic propositions are typically represented by letters of the alphabet,[10] there is a variety of notations to represent the logical connectives. The following table shows the main notational variants for each of the connectives in propositional logic.

Notational variants of the connectives[13][14]
Connective Symbol
AND , , , ,
equivalent , ,
implies , ,
NAND , ,
nonequivalent , ,
NOR , ,
NOT , , ,
OR , , ,
XNOR XNOR
XOR ,

History[edit]

Although propositional logic (which is interchangeable with propositional calculus) had been hinted by earlier philosophers, it was developed into a formal logic (Stoic logic) by Chrysippus in the 3rd century BC[15] 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[16] 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.[17]

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.[18]

Gottlob Frege's predicate logic builds upon propositional logic, and has been described as combining "the distinctive features of syllogistic logic and propositional logic."[19] 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.[20] The invention of truth tables, however, is of uncertain attribution.

Within works by Frege[21] and Bertrand Russell,[22] 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).[21] Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole, Charles Sanders Peirce,[23] 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.[22] 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.".[22]

Characteristics[edit]

Propositional logic, as currently studied in universities, is a specification of a standard of logical consequence in which only the meanings of propositional connectives are considered in evaluating the conditions for the truth of a sentence, or whether a sentence logically follows from some other sentence or group of sentences.[2]

Declarative sentences[edit]

Propositional logic deals with statements, which are defined as declarative sentences having truth value.[24][1] Examples of statements might include:

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.".[25][26] Such non-declarative sentences have no truth value,[27] and are only dealt with in nonclassical logics, called erotetic and imperative logics.

Compounding sentences with connectives[edit]

In propositional logic, a statement can contain one or more other statements as parts.[1] Compound sentences are formed from simpler sentences and express relationships among the constituent sentences.[28] This is done by combining them with logical connectives:[28][29] the main types of compound sentences are negations, conjunctions, disjunctions, implications, and biconditionals,[28] which are formed by using the corresponding connectives to connect propositions.[30][31] In English, these connectives are expressed by the words "and" (conjunction), "or" (disjunction), "not" (negation) and "if" (material conditional), and "if and only if" (biconditional).[1][9] Examples of such compound sentences might include:

  • Wikipedia is a free online encyclopedia that anyone can edit, and millions already have. (conjunction)
  • It is not true that all Wikipedia editors speak at least three languages. (negation)
  • Either London is the capital of England, or London is the capital of the United Kingdom, or both. (disjunction)[b]

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

Sentential connectives are a broader category that includes logical connectives.[2][29] Sentential connectives are any linguistic particles that bind sentences to create a new compound sentence,[2][29] or that inflect a single sentence to create a new sentence.[2] A logical connective, or propositional connective, is a kind of sentential connective with the characteristic feature that, when the original sentences it operates on are (or express) propositions, the new sentence that results from its application also is (or expresses) a proposition.[2] Philosophers disagree about what exactly a proposition is,[6][2] as well as about which sentential connectives in natural languages should be counted as logical connectives.[29][2]

Inference[edit]

The following is an example of an inference 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.

Both premises and the conclusion are propositions. The premises are taken for granted, and with the application of modus ponens (an inference rule),[32] the conclusion follows.

Propositional variables[edit]

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

Premise 1:
Premise 2:
Conclusion:

When P is interpreted as "It's raining" and Q as "it's cloudy" these symbolic expressions correspond exactly with the original expression in natural language. Not only that, but they will also correspond with any other inference with the same logical form.

Gentzen notation[edit]

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

This method of displaying it is Gentzen's notation for natural deduction and sequent calculus.[33] The premises are shown above a line, called the inference line,[11] separated by a comma, which indicates combination of premises.[34] The conclusion is written below the inference line.[11] The inference line represents syntactic consequence,[11] sometimes called deductive consequence,[35] which is also symbolized with ⊢.[36][35] So the above can also be written in one line as .[c]

Syntactic consequence is contrasted with semantic consequence,[37] which is symbolized with ⊧.[36][35] 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.

Formalization[edit]

Propositional logic may be studied through a formal system in which formulas of a formal language may be interpreted to represent propositions. A proof system allows certain formulas to be derived. These derived formulas are called theorems and may be interpreted to be true propositions. A constructed sequence of such formulas is known as a derivation or proof and the last formula of the sequence is the theorem. The derivation may be interpreted as proof of the proposition represented by the theorem.

When a formal system is used to represent formal logic, only statement letters (usually capital roman letters such as , and ) are represented directly. The natural language propositions that arise when they're interpreted are outside the scope of the system, and the relation between the formal system and its interpretation is likewise outside the formal system itself.

The most thoroughly researched branch of propositional logic is classical truth-functional propositional logic,[1] in which formulas are interpreted as having precisely one of two possible truth values, the truth value of true or the truth value of false.[38] The principle of bivalence and the law of excluded middle are upheld. By comparison with first-order logic, truth-functional propositional logic is considered to be zeroth-order logic.[4][5]

Language[edit]

The language (commonly called )[39][40][29] of a propositional calculus is defined in terms of:[2][10]

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

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 , then, is defined either as being identical to its set of well-formed formulas,[40] or as containing that set (together with, for instance, its set of connectives and variables).[10][29]

Composition of formulas[edit]

More specifically, given a set of atomic propositional variables , , , ..., and a set of propositional connectives , , , ..., , , , ..., , , , ..., a formula of propositional logic is defined recursively by these definitions:[2][10][42]

Definition 1: Atomic propositional variables are formulas.
Definition 2: If is a propositional connective, and A, B, C, … is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applying to to A, B, C, … is a formula.
Definition 3: Nothing else is a formula.

Writing the result of applying to A, B, C, … in functional notation, as (A, B, C, …), we have the following as examples of well-formed formulas:

It is sort of recursive definition which justifies the use of "atomic" for propositional variables, since all formulas in the language are built up from the atoms as ultimate building blocks.[2] Composite formulas (all formulas besides atoms) are called molecules,[41] or molecular sentences.[29] (This is an imperfect analogy with chemistry, since a chemical molecule may sometimes have only one atom, as in monatomic gases.)[41]

Constants and schemata[edit]

Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition,[43] while propositional variables range over the set of all atomic propositions.[43] Schemata, or schematic letters, however, range over all formulas.[44][1] It is common to represent propositional constants by A, B, and C, propositional variables by P, Q, and R, and schematic letters are often Greek letters, most often φ, ψ, and χ.[44][1]

However, some authors recognize only two "propositional constants" in their formal system: the special symbol , called "truth", which always evaluates to True, and the special symbol , called "falsity", which always evaluates to False.[45][46][47]

Semantics[edit]

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

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.[48][51][52] 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".

Interpretation of a language[edit]

For a given language , an interpretation,[53] or case,[29] is an assignment of semantic values to each formula of .[29] For a formal language of classical logic, a case is defined as an assignment, to each formula of , of one or the other, but not both, of the truth values, namely truth (T, or 1) and falsity (F, or 0).[54][55] An interpretation of a formal language for classical logic is often expressed in terms of truth tables.[56][1] Since each formula is only assigned a single truth-value, an interpretation may be viewed as a function, whose domain is , and whose range is its set of semantic values ,[2] or .[29]

For distinct propositional symbols there are distinct possible interpretations. For any particular symbol , for example, there are possible interpretations: either is assigned T, or is assigned F. And for the pair , there are possible interpretations: either both are assigned T, or both are assigned F, or is assigned T and is assigned F, or is assigned F and is assigned T.[56] Since has , that is, denumerably many propositional symbols, there are , and therefore uncountably many distinct possible interpretations of as a whole.[56]

Propositional connective semantics[edit]

An interpretation assigns semantic values to atomic formulas directly.[53][29] Molecular formulas are assigned a function of the value of their constituent atoms, according to the connective used;[53][29] this is done by defining the connectives, as follows.[53][29]

Logical connectives are defined semantically in terms of the truth values that they take when the propositional variables that they're applied to take either of the two possible truth values.[1][29] This is usually represented as a truth table for each of the connectives,[1][29] as seen below:

p q pq pq pq pq ¬p ¬q
T T T T T T F F
T F F T F F F T
F T F T T F T F
F F F F T T T T

This table covers each of the main five logical connectives:[9][10][11][12] conjunction (here notated p ∧ q), disjunction (p ∨ q), implication (p → q), equivalence (p ⇔ q) and negation, (¬p, or ¬q, as the case may be). It is sufficient for determining the semantics of each of these operators.[1][57][29] For more detail on each of the five, see the articles on each specific one, as well as the articles "Logical connective" and "Truth function". For more truth tables for more different kinds of connectives, see the article "Truth table".

Some of these connectives may be defined in terms of others: for instance, implication, p → q, may be defined in terms of disjunction and negation, as ¬p ∨ q.[58] In fact, a truth-functionally complete system, in the sense that all and only the classical propositional tautologies are theorems, may be derived using only disjunction and negation (as Russell, Whitehead, and Hilbert did),[2] or using only implication and negation (as Frege did),[2] or using only conjunction and negation,[2] or even using only a single connective for "not and" (the Sheffer stroke),[3][2] as Jean Nicod did.[2]

Semantic truth, validity, consequence[edit]

Given and as formulas of a language , and as an interpretation of , then the following definitions apply:[56][55]

  • Truth-in-a-case:[29] A sentence of is true under an interpretation if assigns the truth value T to .[55][56] If is true under , then is called a model of .[56]
  • Falsity-in-a-case:[29] is false under an interpretation if, and only if, is true under .[56][59][29] This is the "truth of negation" definition of falsity-in-a-case.[29] Falsity-in-a-case may also be defined by the "complement" definition: is false under an interpretation if, and only if, is not true under .[55][56] In classical logic, these definitions are equivalent, but in nonclassical logics, they are not.[29]
  • Semantic consequence: A sentence of is a semantic consequence () of a sentence if there is no interpretation under which is true and is false.[55][56][29]
  • Validity (or tautology): A sentence of is logically valid (),[d] or a tautology,[60][61] if it is true under every interpretation,[55][56] or true in every case.[29]
  • Consistency: A sentence of is consistent if it is true under at least one interpretation. It is inconsistent if it is not consistent.[55][56]

For classical logic, the following theorems apply:

  • For any given interpretation, a given formula is either true or false.[56][59]
  • No formula is both true and false under the same interpretation.[56][59]
  • is true under if, and only if, is false under ;[56][59] is true under if, and only if, is not true under .[56]
  • If and are both true under , then is true under .[56][59]
  • If and , then .[56]
  • is true under if, and only if, either is not true under , or is true under .[56]
  • if, and only if, is logically valid, that is, if, and only if, .[56][59]

Proof systems[edit]

Proof systems in propositional logic can be broadly classified into semantic proof systems and syntactic proof systems,[62][63][64] according to the kind of logical consequence that they rely on: semantic proof systems rely on semantic consequence (),[65] whereas syntactic proof systems rely on syntactic consequence ().[66] 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.[67]

Semantic proof systems[edit]

Example of a truth table
A graphical representation of a partially built propositional tableau

Semantic proof systems rely on the concept of semantic consequence, symbolized as , which indicates that if is true, then must also be true in every possible interpretation.[67]

Truth tables[edit]

A truth table is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.[68] By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.[69]

Semantic tableaux[edit]

A semantic tableau is another semantic proof technique that systematically explores the truth of a proposition.[70] It constructs a tree where each branch represents a possible interpretation of the propositions involved.[71] If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered a tautology.[72]

Syntactic proof systems[edit]

Rules for the propositional sequent calculus 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, , signifies that can be derived from using the rules of the formal system.[67]

Axiomatic systems[edit]

An axiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived.[73] 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.[74]

Natural deduction[edit]

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.[75] Each rule reflects a particular logical connective and shows how it can be introduced or eliminated.[75]

Sequent calculus[edit]

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

Semantic proof via truth tables[edit]

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.[69][41][44] If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation).[69][41] Further, if is valid, then is inconsistent.[78]

For instance, this table shows that "p → (q ∨ r → (r → ¬p))" is not valid:[41]

p q r qr r → ¬p qr → (r → ¬p) p → (qr → (r → ¬p))
T T T T F F F
T T F T T T T
T F T T F F F
T F F F T T T
F T T T T T T
F T F T T T T
F F T T T T T
F F F F T T T

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

p (q r (r ¬ p))
T (F T (T ¬ T))
T ( T (T F ))
T ( T F )
T F
F
T F F T T F T F F T

Further, using the theorem that if, and only if, is valid,[56][59] we can use a truth table to prove that a formula is a semantic consequence of a set of formulas: if, and only if, we can produce a truth table that comes out all true for the formula (that is, if ).[79][80]

List of classically valid argument forms[edit]

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.[44] We use to denote equivalence of and , that is, as an abbreviation for both and ;[44] as an aid to reading the symbols, a description of each formula is given.

Name Sequent Description
Modus Ponens [29] If p then q; p; therefore q
Modus Tollens [29] If p then q; not q; therefore not p
Hypothetical Syllogism If p then q; if q then r; therefore, if p then r
Disjunctive Syllogism [81] Either p or q, or both; not p; therefore, q
Constructive Dilemma If p then q; and if r then s; but p or r; therefore q or s
Destructive Dilemma If p then q; and if r then s; but not q or not s; therefore not p or not r
Bidirectional Dilemma If p then q; and if r then s; but p or not s; therefore q or not r
Simplification [29] p and q are true; therefore p is true
Conjunction [29] p and q are true separately; therefore they are true conjointly
Addition [29][81] p is true; therefore the disjunction (p or q) is true
Composition If p then q; and if p then r; therefore if p is true then q and r are true
De Morgan's Theorem (1) [29] The negation of (p and q) is equiv. to (not p or not q)
De Morgan's Theorem (2) [29] The negation of (p or q) is equiv. to (not p and not q)
Commutation (1) [81] (p or q) is equiv. to (q or p)
Commutation (2) [81] (p and q) is equiv. to (q and p)
Commutation (3) [81] (p iff q) is equiv. to (q iff p)
Association (1) p or (q or r) is equiv. to (p or q) or r
Association (2) p and (q and r) is equiv. to (p and q) and r
Distribution (1) [81] p and (q or r) is equiv. to (p and q) or (p and r)
Distribution (2) [81] p or (q and r) is equiv. to (p or q) and (p or r)
Double Negation [29][81] p is equivalent to the negation of not p
Transposition [29] If p then q is equiv. to if not q then not p
Material Implication [81] If p then q is equiv. to not p or q
Material Equivalence (1) [81] (p iff q) is equiv. to (if p is true then q is true) and (if q is true then p is true)
Material Equivalence (2) [81] (p iff q) is equiv. to either (p and q are true) or (both p and q are false)
Material Equivalence (3) (p iff q) is equiv to., both (p or not q is true) and (not p or q is true)
Exportation [82] from (if p and q are true then r is true) we can prove (if q is true then r is true, if p is true)
Importation If p then (if q then r) is equivalent to if p and q then r
Tautology (1) [81] p is true is equiv. to p is true or p is true
Tautology (2) [81] p is true is equiv. to p is true and p is true
Tertium non datur (Law of Excluded Middle) [29][81] p or not p is true
Law of Non-Contradiction [29][81] p and not p is false, is a true statement
Explosion [29] If p and (not p) are both true, then q follows, whatever q may be

Example syntactic proof systems[edit]

In a syntactic proof system for the propositional calculus, an argument is defined as a list of propositions. A valid argument is a list of propositions, the last of which follows from—or is implied by—the rest. All other arguments are invalid. The simplest valid argument is modus ponens, one instance of which is the following list of propositions:

This is a list of three propositions, each line is a proposition, and the last follows from the rest. The first two lines are called premises, and the last line the conclusion. We say that any proposition C follows from any set of propositions , if C must be true whenever every member of the set is true. In the argument above, for any P and Q, whenever PQ and P are true, necessarily Q is true. Notice that, when P is true, we cannot consider cases 3 and 4 (from the truth table). When PQ is true, we cannot consider case 2. This leaves only case 1, in which Q is also true. Thus Q is implied by the premises.

This generalizes schematically. Thus, where φ and ψ may be any propositions at all,

Other argument forms are convenient, but not necessary. Given a complete set of axioms (see below for one such set), modus ponens is sufficient to prove all other argument forms in propositional logic, thus they may be considered to be a derivative. Note, this is not true of the extension of propositional logic to other logics like first-order logic. First-order logic requires at least one additional rule of inference in order to obtain completeness.

The significance of argument in formal logic is that one may obtain new truths from established truths. In the first example above, given the two premises, the truth of Q is not yet known or stated. After the argument is made, Q is deduced. In this way, we define a deduction system to be a set of all propositions that may be deduced from another set of propositions. For instance, given the set of propositions , we can define a deduction system, Γ, which is the set of all propositions which follow from A. Reiteration is always assumed, so . Also, from the first element of A, last element, as well as modus ponens, R is a consequence, and so . Because we have not included sufficiently complete axioms, though, nothing else may be deduced. Thus, even though most deduction systems studied in propositional logic are able to deduce , this one is too weak to prove such a proposition.

Formal structure for example systems[edit]

One of the main uses of a propositional calculus, when interpreted for logical applications, is to determine relations of logical equivalence between propositional formulas. These relationships are determined by means of the available transformation rules, sequences of which are called derivations or proofs.

The following examples of proof systems for a propositional calculus will assume a calculus defined as a formal system , where:

  • The alpha set is a countably infinite set of 's atomic formulas or propositional variables. In the examples to follow, the elements of are typically the letters p, q, r, and so on.
  • The omega set Ω is a finite set of elements called operator symbols or logical connectives. The set Ω is partitioned into disjoint subsets as , where, is the set of operator symbols of arity j. For instance, a partition of Ω for the typical five connectives would have and Also, the constant logical values are treated as operators of arity zero, so that
  • The zeta set is a finite set of transformation rules, called inference rules when they acquire logical applications.
  • The iota set is a countable set of initial points that are called axioms when they receive logical interpretations.

The language is its set of well-formed formulas, inductively defined by the following rules:

  1. Base: Any element of the alpha set is a formula of .
  2. If are formulas and is in , then is a formula.
  3. Closed: Nothing else is a formula of .

Repeated applications of these rules permits the construction of complex formulas. Examples of formulas that follow these rules include "p" (by rule 1), "" (by rule 2), "q" (by rule 1), and "" (by rule 2).[e]

In the discussion to follow, after a proof system is defined, a proof is presented as a sequence of numbered lines, with each line consisting of a single formula followed by a reason or justification for introducing that formula. Each premise of the argument, that is, an assumption introduced as a hypothesis of the argument, is listed at the beginning of the sequence and is marked as a "premise" in lieu of other justification. The conclusion is listed on the last line. A proof is complete if every line follows from the previous ones by the correct application of a transformation rule. (For a contrasting approach, see proof-trees).

Natural deduction proof system example[edit]

Let , where , , , are defined as follows:

  • The alpha set , is a countably infinite set of symbols, thus:
  • The omega set partitions as and

In the following example of a propositional calculus, the transformation rules are intended to be interpreted as the inference rules of a so-called natural deduction system. The particular system presented here has no initial points, which means that its interpretation for logical applications derives its theorems from an empty axiom set.

  • The set of initial points is empty, that is, .
  • The set of transformation rules, , is described as follows:

Our propositional calculus has eleven inference rules. These rules allow us to derive other true formulas given a set of formulas that are assumed to be true. The first ten simply state that we can infer certain well-formed formulas from other well-formed formulas. The last rule however uses hypothetical reasoning in the sense that in the premise of the rule we temporarily assume an (unproven) hypothesis to be part of the set of inferred formulas to see if we can infer a certain other formula. Since the first ten rules do not do this they are usually described as non-hypothetical rules, and the last one as a hypothetical rule.

In describing the transformation rules, we may introduce a metalanguage symbol . It is basically a convenient shorthand for saying "infer that". The format is , in which Γ is a (possibly empty) set of formulas called premises, and ψ is a formula called conclusion. The transformation rule means that if every proposition in Γ is a theorem (or has the same truth value as the axioms), then ψ is also a theorem. Considering the following rule Conjunction introduction, we will know whenever Γ has more than one formula, we can always safely reduce it into one formula using conjunction. So for short, from that time on we may represent Γ as one formula instead of a set. Another omission for convenience is when Γ is an empty set, in which case Γ may not appear.

Inference rules[edit]

  • Negation introduction: From and , infer ; that is, .
  • Negation elimination: From , infer ; that is, .
  • Double negation elimination: From , infer p; that is, .
  • Conjunction introduction: From p and q, infer ; that is, .
  • Conjunction elimination: From , infer p, and from , infer q; that is, and .
  • Disjunction introduction: From p, infer .
From q, infer ; that is, and .
  • Disjunction elimination: From and and , infer r; that is, .
  • Biconditional introduction: From and , infer ; that is, .
  • Biconditional elimination: From , infer , and from , infer ; that is, and .
  • Modus ponens (conditional elimination) : From p and , infer q; that is, .
  • Conditional proof (conditional introduction) : From [accepting p allows a proof of q], infer ; that is, .

Example of a proof in natural deduction system[edit]

  • To be shown that AA.
  • One possible proof of this (which, though valid, happens to contain more steps than are necessary) may be arranged as follows:
Example of a proof
Number Formula Reason
1 premise
2 From (1) by disjunction introduction
3 From (1) and (2) by conjunction introduction
4 From (3) by conjunction elimination
5 Summary of (1) through (4)
6 From (5) by conditional proof

Interpret as "Assuming A, infer A". Read as "Assuming nothing, infer that A implies A", or "It is a tautology that A implies A", or "It is always true that A implies A".

Jan Łukasiewicz axiomatic proof system example[edit]

Let , where , , , are defined as follows:

  • The set , the countably infinite set of symbols that serve to represent logical propositions:
  • The functionally complete set of logical operators (logical connectives and negation) is as follows. Of the three connectives for conjunction, disjunction, and implication (, and ), one can be taken as primitive and the other two can be defined in terms of it and negation (¬).[83] Alternatively, all of the logical operators may be defined in terms of a sole sufficient operator, such as the Sheffer stroke (nand). The biconditional () can of course be defined in terms of conjunction and implication as . Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set partitioned as and Then is defined as , and is defined as .
  • The set (the set of initial points of logical deduction, i.e., logical axioms) is the axiom system proposed by Jan Łukasiewicz, and used as the propositional-calculus part of a Hilbert system. The axioms are all substitution instances of:
  • The set of transformation rules (rules of inference) is the sole rule modus ponens (i.e., from any formulas of the form and , infer ).

This system is used in Metamath set.mm formal proof database.

Example of a proof in an axiomatic propositional calculus system[edit]

We now prove the same theorem in the axiomatic system by Jan Łukasiewicz described above, which is an example of a Hilbert-style deductive system for the classical propositional calculus.

The axioms are:

(A1)
(A2)
(A3)

And the proof is as follows:

  1.       (instance of (A1))
  2.       (instance of (A2))
  3.       (from (1) and (2) by modus ponens)
  4.       (instance of (A1))
  5.       (from (4) and (3) by modus ponens)

Soundness and completeness of the rules[edit]

The crucial properties of this set of rules are that they are sound and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows. The proofs for the soundness and completeness of the propositional logic are not themselves proofs in propositional logic; these are theorems in ZFC used as a metatheory to prove properties of propositional logic.

We define a truth assignment as a function that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs (or possible world) where certain statements are true and others are not. The semantics of formulas can then be formalized by defining for which "state of affairs" they are considered to be true, which is what is done by the following definition.

We define when such a truth assignment A satisfies a certain well-formed formula with the following rules:

  • A satisfies the propositional variable P if and only if A(P) = true
  • A satisfies ¬φ if and only if A does not satisfy φ
  • A satisfies (φψ) if and only if A satisfies both φ and ψ
  • A satisfies (φψ) if and only if A satisfies at least one of either φ or ψ
  • A satisfies (φψ) if and only if it is not the case that A satisfies φ but not ψ
  • A satisfies (φψ) if and only if A satisfies both φ and ψ or satisfies neither one of them

With this definition we can now formalize what it means for a formula φ to be implied by a certain set S of formulas. Informally this is true if in all worlds that are possible given the set of formulas S the formula φ also holds. This leads to the following formal definition: We say that a set S of well-formed formulas semantically entails (or implies) a certain well-formed formula φ if all truth assignments that satisfy all the formulas in S also satisfy φ.

Finally we define syntactical entailment such that φ is syntactically entailed by S if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:

Soundness: If the set of well-formed formulas S syntactically entails the well-formed formula φ then S semantically entails φ.

Completeness: If the set of well-formed formulas S semantically entails the well-formed formula φ then S syntactically entails φ.

For the above set of rules this is indeed the case.

Sketch of a soundness proof[edit]

(For most logical systems, this is the comparatively "simple" direction of proof)

Notational conventions: Let G be a variable ranging over sets of sentences. Let A, B and C range over sentences. For "G syntactically entails A" we write "G proves A". For "G semantically entails A" we write "G implies A".

We want to show: (A)(G) (if G proves A, then G implies A).

We note that "G proves A" has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If G proves A, then ...". So our proof proceeds by induction.

  1. Basis. Show: If A is a member of G, then G implies A.
  2. Basis. Show: If A is an axiom, then G implies A.
  3. Inductive step (induction on n, the length of the proof):
    1. Assume for arbitrary G and A that if G proves A in n or fewer steps, then G implies A.
    2. For each possible application of a rule of inference at step n + 1, leading to a new theorem B, show that G implies B.

Notice that Basis Step II can be omitted for natural deduction systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth.

The Basis steps demonstrate that the simplest provable sentences from G are also implied by G, for any G. (The proof is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable—by considering each case where we might reach a logical conclusion using an inference rule—and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from "A" we can derive "A or B". In III.a We assume that if A is provable it is implied. We also know that if A is provable then "A or B" is provable. We have to show that then "A or B" too is implied. We do so by appeal to the semantic definition and the assumption we just made. A is provable from G, we assume. So it is also implied by G. So any semantic valuation making all of G true makes A true. But any valuation making A true makes "A or B" true, by the defined semantics for "or". So any valuation which makes all of G true makes "A or B" true. So "A or B" is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case analysis of all the rules of inference, showing that each "preserves" semantic implication.

By the definition of provability, there are no sentences provable other than by being a member of G, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.

Sketch of completeness proof[edit]

(This is usually the much harder direction of proof.)

We adopt the same notational conventions as above.

We want to show: If G implies A, then G proves A. We proceed by contraposition: We show instead that if G does not prove A then G does not imply A. If we show that there is a model where A does not hold despite G being true, then obviously G does not imply A. The idea is to build such a model out of our very assumption that G does not prove A.

  1. G does not prove A. (Assumption)
  2. If G does not prove A, then we can construct an (infinite) maximal set, G, which is a superset of G and which also does not prove A.
    1. Place an ordering (with order type ω) on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them (E1, E2, ...)
    2. Define a series Gn of sets (G0, G1, ...) inductively:
      1. If proves A, then
      2. If does not prove A, then
    3. Define G as the union of all the Gn. (That is, G is the set of all the sentences that are in any Gn.)
    4. It can be easily shown that
      1. G contains (is a superset of) G (by (b.i));
      2. G does not prove A (because the proof would contain only finitely many sentences and when the last of them is introduced in some Gn, that Gn would prove A contrary to the definition of Gn); and
      3. G is a maximal set with respect to A: If any more sentences whatever were added to G, it would prove A. (Because if it were possible to add any more sentences, they should have been added when they were encountered during the construction of the Gn, again by definition)
  3. If G is a maximal set with respect to A, then it is truth-like. This means that it contains C if and only if it does not contain ¬C; If it contains C and contains "If C then B" then it also contains B; and so forth. In order to show this, one has to show the axiomatic system is strong enough for the following:
    • For any formulas C and D, if it proves both C and ¬C, then it proves D. From this it follows, that a maximal set with respect to A cannot prove both C and ¬C, as otherwise it would prove A.
    • For any formulas C and D, if it proves both CD and ¬CD, then it proves D. This is used, together with the deduction theorem, to show that for any formula, either it or its negation is in G: Let B be a formula not in G; then G with the addition of B proves A. Thus from the deduction theorem it follows that G proves BA. But suppose ¬B were also not in G, then by the same logic G also proves ¬BA; but then G proves A, which we have already shown to be false.
    • For any formulas C and D, if it proves C and D, then it proves CD.
    • For any formulas C and D, if it proves C and ¬D, then it proves ¬(CD).
    • For any formulas C and D, if it proves ¬C, then it proves CD.
    If additional logical operation (such as conjunction and/or disjunction) are part of the vocabulary as well, then there are additional requirement on the axiomatic system (e.g. that if it proves C and D, it would also prove their conjunction).
  4. If G is truth-like there is a G-Canonical valuation of the language: one that makes every sentence in G true and everything outside G false while still obeying the laws of semantic composition in the language. The requirement that it is truth-like is needed to guarantee that the laws of semantic composition in the language will be satisfied by this truth assignment.
  5. A G-canonical valuation will make our original set G all true, and make A false.
  6. If there is a valuation on which G are true and A is false, then G does not (semantically) imply A.

Thus every system that has modus ponens as an inference rule, and proves the following theorems (including substitutions thereof) is complete:

The first five are used for the satisfaction of the five conditions in stage III above, and the last three for proving the deduction theorem.

Example[edit]

As an example, it can be shown that as any other tautology, the three axioms of the classical propositional calculus system described earlier can be proven in any system that satisfies the above, namely that has modus ponens as an inference rule, and proves the above eight theorems (including substitutions thereof). Out of the eight theorems, the last two are two of the three axioms; the third axiom, , can be proven as well, as we now show.

For the proof we may use the hypothetical syllogism theorem (in the form relevant for this axiomatic system), since it only relies on the two axioms that are already in the above set of eight theorems. The proof then is as follows:

  1.       (instance of the 7th theorem)
  2.       (instance of the 7th theorem)
  3.       (from (1) and (2) by modus ponens)
  4.       (instance of the hypothetical syllogism theorem)
  5.       (instance of the 5th theorem)
  6.       (from (5) and (4) by modus ponens)
  7.       (instance of the 2nd theorem)
  8.       (instance of the 7th theorem)
  9.       (from (7) and (8) by modus ponens)
  10.       (instance of the 8th theorem)
  11.       (from (9) and (10) by modus ponens)
  12.       (from (3) and (11) by modus ponens)
  13.       (instance of the 8th theorem)
  14.       (from (12) and (13) by modus ponens)
  15.       (from (6) and (14) by modus ponens)
Verifying completeness for the classical propositional calculus system[edit]

We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. We use several lemmas proven here:

(DN1) - Double negation (one direction)
(DN2) - Double negation (another direction)
(HS1) - one form of Hypothetical syllogism
(HS2) - another form of Hypothetical syllogism
(TR1) - Transposition
(TR2) - another form of transposition.
(L1)
(L3)

We also use the method of the hypothetical syllogism metatheorem as a shorthand for several proof steps.

  • - proof:
    1.       (instance of (A1))
    2.       (instance of (TR1))
    3.       (from (1) and (2) using the hypothetical syllogism metatheorem)
    4.       (instance of (DN1))
    5.       (instance of (HS1))
    6.       (from (4) and (5) using modus ponens)
    7.       (from (3) and (6) using the hypothetical syllogism metatheorem)
  • - proof:
    1.       (instance of (HS1))
    2.       (instance of (L3))
    3.       (instance of (HS1))
    4.       (from (2) and (3) by modus ponens)
    5.       (from (1) and (4) using the hypothetical syllogism metatheorem)
    6.       (instance of (TR2))
    7.       (instance of (HS2))
    8.       (from (6) and (7) using modus ponens)
    9.       (from (5) and (8) using the hypothetical syllogism metatheorem)
  • - proof:
    1.       (instance of (A1))
    2.       (instance of (A1))
    3.       (from (1) and (2) using modus ponens)
  • - proof:
    1.       (instance of (L1))
    2.       (instance of (TR1))
    3.       (from (1) and (2) using the hypothetical syllogism metatheorem)
  • - proof:
    1.       (instance of (A1))
    2.       (instance of (A3))
    3.       (from (1) and (2) using the hypothetical syllogism metatheorem)
  • - proof given in the proof example above
  • - axiom (A1)
  • - axiom (A2)
Another outline for a completeness proof[edit]

If a formula is a tautology, then there is a truth table for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulas, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using "(P is true implies S) implies ((P is false implies S) implies S)". Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.

More complex axiomatic proof system example[edit]

It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.

Axioms[edit]

Let φ, χ, and ψ stand for well-formed formulas. (The well-formed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:

Axioms
Name Axiom Schema Description
THEN-1 Add hypothesis χ, implication introduction
THEN-2 Distribute hypothesis over implication
AND-1 Eliminate conjunction
AND-2  
AND-3 Introduce conjunction
OR-1 Introduce disjunction
OR-2  
OR-3 Eliminate disjunction
NOT-1 Introduce negation
NOT-2 Eliminate negation
NOT-3 Excluded middle, classical logic
IFF-1 Eliminate equivalence
IFF-2  
IFF-3 Introduce equivalence
  • Axiom THEN-2 may be considered to be a "distributive property of implication with respect to implication."
  • Axioms AND-1 and AND-2 correspond to "conjunction elimination". The relation between AND-1 and AND-2 reflects the commutativity of the conjunction operator.
  • Axiom AND-3 corresponds to "conjunction introduction."
  • Axioms OR-1 and OR-2 correspond to "disjunction introduction." The relation between OR-1 and OR-2 reflects the commutativity of the disjunction operator.
  • Axiom NOT-1 corresponds to "reductio ad absurdum."
  • Axiom NOT-2 says that "anything can be deduced from a contradiction."
  • Axiom NOT-3 is called "tertium non-datur" (Latin: "a third is not given") and reflects the semantic valuation of propositional formulas: a formula can have a truth-value of either true or false. There is no third truth-value, at least not in classical logic. Intuitionistic logicians do not accept the axiom NOT-3.
Inference rule[edit]

The inference rule is modus ponens:

.
Meta-inference rule[edit]

Let a demonstration be represented by a sequence, with hypotheses to the left of the turnstile and the conclusion to the right of the turnstile. Then the deduction theorem can be stated as follows:

If the sequence
has been demonstrated, then it is also possible to demonstrate the sequence
.

This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.

On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof inference rule which is part of the first version of propositional calculus introduced in this article.

The converse of DT is also valid:

If the sequence
has been demonstrated, then it is also possible to demonstrate the sequence

in fact, the validity of the converse of DT is almost trivial compared to that of DT:

If
then
1:
2:
and from (1) and (2) can be deduced
3:
by means of modus ponens, Q.E.D.

The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, by axiom AND-1 we have,

which can be transformed by means of the converse of the deduction theorem into

which tells us that the inference rule

is admissible. This inference rule is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.

Example of a proof in the more complex axiomatic system[edit]

The following is an example of a (syntactical) demonstration, involving only axioms THEN-1 and THEN-2:

Prove: (Reflexivity of implication).

Proof:

  1. Axiom THEN-2 with
  2. Axiom THEN-1 with
  3. From (1) and (2) by modus ponens.
  4. Axiom THEN-1 with
  5. From (3) and (4) by modus ponens.

Solvers[edit]

One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula is decidable.[84] 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.

See also[edit]

Higher logical levels[edit]

Related topics[edit]

Notes[edit]

  1. ^ Many sources write this with a definite article, as the propositional calculus, while others just call it propositional calculus with no article.
  2. ^ The "or both" makes it clear[29] that it's a logical disjunction, not an exclusive or, which is more common in English.
  3. ^ The turnstile (for syntactic consequence) is of a higher level than the comma (for premise combination) and the arrow (for material implication), so no parentheses are needed to interpret this formula.
  4. ^ Conventionally , with nothing to the left of the turnstile, is used to symbolize a tautology. It may be interpreted as saying that is a semantic consequence of the empty set of formulae, i.e., , but with the empty brackets omitted for simplicity;[44] 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.[44]
  5. ^ Formally, rule 2 obtains formulas in Polish notation, i.e. in this example. For convenience, we will use the common infix notation instead in this and all following examples.

References[edit]

  1. ^ a b c d e f g h i j k l m n o p q r s t u v "Propositional Logic | Internet Encyclopedia of Philosophy". Retrieved 22 March 2024.
  2. ^ a b c d e f g h i j k l m n o p q r s Franks, Curtis (2023), "Propositional Logic", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  3. ^ a b Weisstein, Eric W. "Propositional Calculus". mathworld.wolfram.com. Retrieved 22 March 2024.
  4. ^ a b Bělohlávek, Radim; Dauben, Joseph Warren; Klir, George J. (2017). Fuzzy logic and mathematics: a historical perspective. New York, NY, United States of America: Oxford University Press. p. 463. ISBN 978-0-19-020001-5.
  5. ^ a b Manzano, María (2005). Extensions of first order logic. Cambridge tracts in theoretical computer science (Digitally printed first paperback version ed.). Cambridge: Cambridge University Press. p. 180. ISBN 978-0-521-35435-6.
  6. ^ a b McGrath, Matthew; Frank, Devin (2023), "Propositions", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Winter 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  7. ^ "Predicate Logic". www3.cs.stonybrook.edu. Retrieved 22 March 2024.
  8. ^ "Philosophy 404: Lecture Five". www.webpages.uidaho.edu. Retrieved 22 March 2024.
  9. ^ a b c "3.1 Propositional Logic". www.teach.cs.toronto.edu. Retrieved 22 March 2024.
  10. ^ a b c d e f g Davis, Steven; Gillon, Brendan S., eds. (2004). Semantics: a reader. New York: Oxford University Press. ISBN 978-0-19-513697-5.
  11. ^ a b c d e Plato, Jan von (2013). Elements of logical reasoning (1. publ ed.). Cambridge: Cambridge University press. pp. 9, 32, 121. ISBN 978-1-107-03659-8.
  12. ^ a b "Propositional Logic". www.cs.miami.edu. Retrieved 22 March 2024.
  13. ^ Plato, Jan von (2013). Elements of logical reasoning (1. publ ed.). Cambridge: Cambridge University press. p. 9. ISBN 978-1-107-03659-8.
  14. ^ a b Weisstein, Eric W. "Connective". mathworld.wolfram.com. Retrieved 22 March 2024.
  15. ^ Bobzien, Susanne (1 January 2016). "Ancient Logic". In Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University – via Stanford Encyclopedia of Philosophy.
  16. ^ "Propositional Logic | Internet Encyclopedia of Philosophy". Retrieved 20 August 2020.
  17. ^ Bobzien, Susanne (2020), "Ancient Logic", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Summer 2020 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  18. ^ Peckhaus, Volker (1 January 2014). "Leibniz's Influence on 19th Century Logic". In Zalta, Edward N. (ed.). The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University – via Stanford Encyclopedia of Philosophy.
  19. ^ Hurley, Patrick (2007). A Concise Introduction to Logic 10th edition. Wadsworth Publishing. p. 392.
  20. ^ 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
  21. ^ a b Truth in Frege
  22. ^ a b c "Russell: the Journal of Bertrand Russell Studies".
  23. ^ Anellis, Irving H. (2012). "Peirce's Truth-functional Analysis and the Origin of the Truth Table". History and Philosophy of Logic. 33: 87–97. doi:10.1080/01445340.2011.621702. S2CID 170654885.
  24. ^ "Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables". www.math.fsu.edu. Retrieved 22 March 2024.
  25. ^ "Lecture Notes on Logical Organization and Critical Thinking". www2.hawaii.edu. Retrieved 22 March 2024.
  26. ^ "Logical Connectives". sites.millersville.edu. Retrieved 22 March 2024.
  27. ^ "Lecture1". www.cs.columbia.edu. Retrieved 22 March 2024.
  28. ^ a b c d "Introduction to Logic - Chapter 2". intrologic.stanford.edu. Retrieved 22 March 2024.
  29. ^ a b c d e f g h i j k l m n o p q r s t u v w x y z aa ab ac ad ae af ag ah ai aj ak al am an Beall, Jeffrey C. (2010). Logic: the basics. The basics (1. publ ed.). London: Routledge. pp. 14–16, 19–20, 45–48, 50–53, 56. ISBN 978-0-203-85155-5.
  30. ^ "Watson". watson.latech.edu. Retrieved 22 March 2024.
  31. ^ "Introduction to Theoretical Computer Science, Chapter 1". www.cs.odu.edu. Retrieved 22 March 2024.
  32. ^ "Rules of Inference and Logic Proofs". sites.millersville.edu. Retrieved 22 March 2024.
  33. ^ Pelletier, Francis Jeffry; Hazen, Allen (2024), "Natural Deduction Systems in Logic", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Spring 2024 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  34. ^ Restall, Greg (2018), "Substructural Logics", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  35. ^ a b c "Compactness | Internet Encyclopedia of Philosophy". Retrieved 22 March 2024.
  36. ^ a b "Lecture Topics for Discrete Math Students". math.colorado.edu. Retrieved 22 March 2024.
  37. ^ Paseau, Alexander; Pregel, Fabian (2023), "Deductivism in the Philosophy of Mathematics", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  38. ^ "Propositional Logic | Brilliant Math & Science Wiki". brilliant.org. Retrieved 20 August 2020.
  39. ^ "Compactness | Internet Encyclopedia of Philosophy". Retrieved 22 March 2024.
  40. ^ a b Demey, Lorenz; Kooi, Barteld; Sack, Joshua (2023), "Logic and Probability", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 22 March 2024
  41. ^ a b c d e f g h Kleene, Stephen Cole (2002). Mathematical logic (Dover ed.). Mineola, N.Y: Dover Publications. ISBN 978-0-486-42533-7.
  42. ^ Humberstone, Lloyd (2011). The connectives. Cambridge, Mass: MIT Press. p. 702. ISBN 978-0-262-01654-4. OCLC 694679197.
  43. ^ a b Lande, Nelson P. (2013). Classical logic and its rabbit holes: a first course. Indianapolis, Ind: Hackett Publishing Co., Inc. p. 20. ISBN 978-1-60384-948-7.
  44. ^ a b c d e f g Bostock, David (1997). Intermediate logic. Oxford : New York: Clarendon Press ; Oxford University Press. pp. 8, 11–12, 27, 29. ISBN 978-0-19-875141-0.
  45. ^ Goldrei, Derek (2005). Propositional and predicate calculus: a model of argument. London: Springer. p. 69. ISBN 978-1-85233-921-0.
  46. ^ "Propositional Logic". www.cs.rochester.edu. Retrieved 22 March 2024.
  47. ^ "Propositional calculus". www.cs.cornell.edu. Retrieved 22 March 2024.
  48. ^ a b Shramko, Yaroslav; Wansing, Heinrich (2021), "Truth Values", in Zalta, Edward N. (ed.), The Stanford Encyclopedia of Philosophy (Winter 2021 ed.), Metaphysics Research Lab, Stanford University, retrieved 23 March 2024
  49. ^ Metcalfe, David; Powell, John (2011). "Should doctors spurn Wikipedia?". Journal of the Royal Society of Medicine. 104 (12): 488–489. doi:10.1258/jrsm.2011.110227. ISSN 0141-0768. PMC 3241521. PMID 22179287.
  50. ^ Ayers, Phoebe; Matthews, Charles; Yates, Ben (2008). How Wikipedia works: and how you can be a part of it. San Francisco: No Starch Press. p. 22. ISBN 978-1-59327-176-3. OCLC 185698411.
  51. ^ Shapiro, Stewart; Kouri Kissel, Teresa (2024), Zalta, Edward N.; Nodelman, Uri (eds.), "Classical Logic", The Stanford Encyclopedia of Philosophy (Spring 2024 ed.), Metaphysics Research Lab, Stanford University, retrieved 25 March 2024
  52. ^ Bostock, David (1997). Intermediate logic. Oxford : New York: Clarendon Press ; Oxford University Press. p. 4. ISBN 978-0-19-875141-0.
  53. ^ a b c d Landman, Fred (1991). "Structures for Semantics". Studies in Linguistics and Philosophy. 45: 127. doi:10.1007/978-94-011-3212-1. ISBN 978-0-7923-1240-6. ISSN 0924-4662.
  54. ^ Nascimento, Marco Antonio Chaer (2015). Frontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013). Progress in theoretical chemistry and physics. International Workshop on Quantum Systems in Chemistry and Physics. Cham: Springer. p. 255. ISBN 978-3-319-14397-2.
  55. ^ a b c d e f g Chowdhary, K.R. (2020). "Fundamentals of Artificial Intelligence". SpringerLink: 31–34. doi:10.1007/978-81-322-3972-7. ISBN 978-81-322-3970-3.
  56. ^ a b c d e f g h i j k l m n o p q r s t Hunter, Geoffrey (1971). Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Press. ISBN 0-520-02356-0.
  57. ^ Aloni, Maria (2023), "Disjunction", in Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (Spring 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved 23 March 2024
  58. ^ Levin, Oscar. Propositional Logic.
  59. ^ a b c d e f g Rogers, Robert L. (1971). Mathematical Logic and Formalized Theories. Elsevier. pp. 38–39. doi:10.1016/c2013-0-11894-6. ISBN 978-0-7204-2098-2.
  60. ^ "6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation". leanprover.github.io. Retrieved 28 March 2024.
  61. ^ "Knowledge Representation and Reasoning: Basics of Logics". www.emse.fr. Retrieved 28 March 2024.
  62. ^ Awodey, Steve; Arnold, Greg Frost-, eds. (2024). Rudolf carnap: studies in semantics: the collected works of rudolf carnap, volume 7. New York: Oxford University Press. pp. xxvii. ISBN 978-0-19-289487-8.
  63. ^ Harel, Guershon; Stylianides, Andreas J., eds. (2018). Advances in Mathematics Education Research on Proof and Proving: An International Perspective. ICME-13 Monographs (1st ed. 2018 ed.). Cham: Springer International Publishing : Imprint: Springer. p. 181. ISBN 978-3-319-70996-3.
  64. ^ DeLancey, Craig (2017). "A Concise Introduction to Logic: §4. Proofs". Milne Publishing. Retrieved 23 March 2024.
  65. ^ Ferguson, Thomas Macaulay; Priest, Graham (23 June 2016), "semantic consequence", A Dictionary of Logic, Oxford University Press, doi:10.1093/acref/9780191816802.001.0001, ISBN 978-0-19-181680-2, retrieved 23 March 2024
  66. ^ Ferguson, Thomas Macaulay; Priest, Graham (23 June 2016), "syntactic consequence", A Dictionary of Logic, Oxford University Press, doi:10.1093/acref/9780191816802.001.0001, ISBN 978-0-19-181680-2, retrieved 23 March 2024
  67. ^ a b c Cook, Roy T. (2009). A dictionary of philosophical logic. Edinburgh: Edinburgh University Press. pp. 82, 176. ISBN 978-0-7486-2559-8.
  68. ^ "Truth table | Boolean, Operators, Rules | Britannica". www.britannica.com. 14 March 2024. Retrieved 23 March 2024.
  69. ^ a b c "MathematicalLogic". www.cs.yale.edu. Retrieved 23 March 2024.
  70. ^ "Analytic Tableaux". www3.cs.stonybrook.edu. Retrieved 23 March 2024.
  71. ^ "Formal logic - Semantic Tableaux, Proofs, Rules | Britannica". www.britannica.com. Retrieved 23 March 2024.
  72. ^ Howson, Colin (1997). Logic with trees: an introduction to symbolic logic. London ; New York: Routledge. pp. ix, x, 24–29, 47. ISBN 978-0-415-13342-5.
  73. ^ "Axiomatic method | Logic, Proofs & Foundations | Britannica". www.britannica.com. Retrieved 23 March 2024.
  74. ^ "Propositional Logic". mally.stanford.edu. Retrieved 23 March 2024.
  75. ^ a b "Natural Deduction | Internet Encyclopedia of Philosophy". Retrieved 23 March 2024.
  76. ^ a b Weisstein, Eric W. "Sequent Calculus". mathworld.wolfram.com. Retrieved 23 March 2024.
  77. ^ "Interactive Tutorial of the Sequent Calculus". logitext.mit.edu. Retrieved 23 March 2024.
  78. ^ "Tautology - New World Encyclopedia". www.newworldencyclopedia.org. Retrieved 28 March 2024.
  79. ^ Lucas, Peter; Gaag, Linda van der (1991). Principles of expert systems (PDF). International computer science series. Wokingham, England ; Reading, Mass: Addison-Wesley. p. 26. ISBN 978-0-201-41640-4.
  80. ^ Bachmair, Leo (2009). "CSE541 Logic in Computer Science" (PDF). Stony Brook University.{{cite web}}: CS1 maint: url-status (link)
  81. ^ a b c d e f g h i j k l m n o Hodges, Wilfrid (2001). Logic (2 ed.). London: Penguin Books. pp. 130–131. ISBN 978-0-14-100314-6.
  82. ^ Toida, Shunichi (2 August 2009). "Proof of Implications". CS381 Discrete Structures/Discrete Mathematics Web Course Material. Department of Computer Science, Old Dominion University. Retrieved 10 March 2010.
  83. ^ Wernick, William (1942) "Complete Sets of Logical Functions," Transactions of the American Mathematical Society 51, pp. 117–132.
  84. ^ W. V. O. Quine, Mathematical Logic (1980), p.81. Harvard University Press, 0-674-55451-5

Further reading[edit]

  • 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.

Related works[edit]

External links[edit]