Propositional calculus

From Wikipedia for FEVERv2
(Redirected from Propositional logic)
Jump to navigation Jump to search

Not to be confused with Propositional analysis. Propositional calculus_sentence_0

Propositional calculus is a branch of logic. Propositional calculus_sentence_1

It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Propositional calculus_sentence_2

It deals with propositions (which can be true or false) and relations between propositions, including the construction of arguments based on them. Propositional calculus_sentence_3

Compound propositions are formed by connecting propositions by logical connectives. Propositional calculus_sentence_4

Propositions that contain no logical connectives are called atomic propositions. Propositional calculus_sentence_5

Unlike first-order logic, propositional logic does not deal with non-logical objects, predicates about them, or quantifiers. Propositional calculus_sentence_6

However, all the machinery of propositional logic is included in first-order logic and higher-order logics. Propositional calculus_sentence_7

In this sense, propositional logic is the foundation of first-order logic and higher-order logic. Propositional calculus_sentence_8

Explanation Propositional calculus_section_0

Logical connectives are found in natural languages. Propositional calculus_sentence_9

In English for example, some examples are "and" (conjunction), "or" (disjunction), "not" (negation) and "if" (but only when used to denote material conditional). Propositional calculus_sentence_10

The following is an example of a very simple inference within the scope of propositional logic: Propositional calculus_sentence_11

Propositional calculus_description_list_0

  • Premise 1: If it's raining then it's cloudy.Propositional calculus_item_0_0
  • Premise 2: It's raining.Propositional calculus_item_0_1
  • Conclusion: It's cloudy.Propositional calculus_item_0_2

Both premises and the conclusion are propositions. Propositional calculus_sentence_12

The premises are taken for granted, and with the application of modus ponens (an inference rule), the conclusion follows. Propositional calculus_sentence_13

As propositional logic is not concerned with the structure of propositions beyond the point where they can't be decomposed any more by logical connectives, this inference can be restated replacing those atomic statements with statement letters, which are interpreted as variables representing statements: Propositional calculus_sentence_14

The same can be stated succinctly in the following way: Propositional calculus_sentence_15

When P is interpreted as "It's raining" and Q as "it's cloudy" the above symbolic expressions can be seen to correspond exactly with the original expression in natural language. Propositional calculus_sentence_16

Not only that, but they will also correspond with any other inference of this form, which will be valid on the same basis this inference is. Propositional calculus_sentence_17

Propositional logic may be studied through a formal system in which formulas of a formal language may be interpreted to represent propositions. Propositional calculus_sentence_18

A system of axioms and inference rules allows certain formulas to be derived. Propositional calculus_sentence_19

These derived formulas are called theorems and may be interpreted to be true propositions. Propositional calculus_sentence_20

A constructed sequence of such formulas is known as a derivation or proof and the last formula of the sequence is the theorem. Propositional calculus_sentence_21

The derivation may be interpreted as proof of the proposition represented by the theorem. Propositional calculus_sentence_22

In classical truth-functional propositional logic, formulas are interpreted as having precisely one of two possible truth values, the truth value of true or the truth value of false. Propositional calculus_sentence_23

The principle of bivalence and the law of excluded middle are upheld. Propositional calculus_sentence_24

Truth-functional propositional logic defined as such and systems isomorphic to it are considered to be zeroth-order logic. Propositional calculus_sentence_25

However, alternative propositional logics are also possible. Propositional calculus_sentence_26

For more, see Other logical calculi below. Propositional calculus_sentence_27

History Propositional calculus_section_1

Main article: History of logic Propositional calculus_sentence_28

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 and expanded by his successor Stoics. Propositional calculus_sentence_29

The logic was focused on propositions. Propositional calculus_sentence_30

This advancement was different from the traditional syllogistic logic, which was focused on terms. Propositional calculus_sentence_31

However, most of the original writings were lost and the propositional logic developed by the Stoics was no longer understood later in antiquity. Propositional calculus_sentence_32

Consequently, the system was essentially reinvented by Peter Abelard in the 12th century. Propositional calculus_sentence_33

Propositional logic was eventually refined using symbolic logic. Propositional calculus_sentence_34

The 17th/18th-century mathematician Gottfried Leibniz has been credited with being the founder of symbolic logic for his work with the calculus ratiocinator. Propositional calculus_sentence_35

Although his work was the first of its kind, it was unknown to the larger logical community. Propositional calculus_sentence_36

Consequently, many of the advances achieved by Leibniz were recreated by logicians like George Boole and Augustus De Morgan—completely independent of Leibniz. Propositional calculus_sentence_37

Just as propositional logic can be considered an advancement from the earlier syllogistic logic, Gottlob Frege's predicate logic can be also considered an advancement from the earlier propositional logic. Propositional calculus_sentence_38

One author describes predicate logic as combining "the distinctive features of syllogistic logic and propositional logic." Propositional calculus_sentence_39

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. Propositional calculus_sentence_40

Natural deduction was invented by Gerhard Gentzen and Jan Łukasiewicz. Propositional calculus_sentence_41

Truth trees were invented by Evert Willem Beth. Propositional calculus_sentence_42

The invention of truth tables, however, is of uncertain attribution. Propositional calculus_sentence_43

Within works by Frege and Bertrand Russell, are ideas influential to the invention of truth tables. Propositional calculus_sentence_44

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

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

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

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. Propositional calculus_sentence_48

". Propositional calculus_sentence_49

Terminology Propositional calculus_section_2

In general terms, a calculus is a formal system that consists of a set of syntactic expressions (well-formed formulas), a distinguished subset of these expressions (axioms), plus a set of formal rules that define a specific binary relation, intended to be interpreted as logical equivalence, on the space of expressions. Propositional calculus_sentence_50

When the formal system is intended to be a logical system, the expressions are meant to be interpreted as statements, and the rules, known to be inference rules, are typically intended to be truth-preserving. Propositional calculus_sentence_51

In this setting, the rules, which may include axioms, can then be used to derive ("infer") formulas representing true statements—from given formulas representing true statements. Propositional calculus_sentence_52

The set of axioms may be empty, a nonempty finite set, or a countably infinite set (see axiom schema). Propositional calculus_sentence_53

A formal grammar recursively defines the expressions and well-formed formulas of the language. Propositional calculus_sentence_54

In addition a semantics may be given which defines truth and valuations (or interpretations). Propositional calculus_sentence_55

The language of a propositional calculus consists of Propositional calculus_sentence_56

Propositional calculus_ordered_list_1

  1. a set of primitive symbols, variously referred to as atomic formulas, placeholders, proposition letters, or variables, andPropositional calculus_item_1_3
  2. a set of operator symbols, variously interpreted as logical operators or logical connectives.Propositional calculus_item_1_4

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. Propositional calculus_sentence_57

Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional calculus_sentence_58

Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Propositional calculus_sentence_59

Schemata, however, range over all propositions. Propositional calculus_sentence_60

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 χ. Propositional calculus_sentence_61

Basic concepts Propositional calculus_section_3

The following outlines a standard propositional calculus. Propositional calculus_sentence_62

Many different formulations exist which are all more or less equivalent, but differ in the details of: Propositional calculus_sentence_63

Propositional calculus_ordered_list_2

  1. their language (i.e., the particular collection of primitive symbols and operator symbols),Propositional calculus_item_2_5
  2. the set of axioms, or distinguished formulas, andPropositional calculus_item_2_6
  3. the set of inference rules.Propositional calculus_item_2_7

Any given proposition may be represented with a letter called a 'propositional constant', analogous to representing a number by a letter in mathematics (e.g., a = 5). Propositional calculus_sentence_64

All propositions require exactly one of two truth-values: true or false. Propositional calculus_sentence_65

For example, let P be the proposition that it is raining outside. Propositional calculus_sentence_66

This will be true (P) if it is raining outside, and false otherwise (¬P). Propositional calculus_sentence_67

Propositional calculus_unordered_list_3

  • We then define truth-functional operators, beginning with negation. ¬P represents the negation of P, which can be thought of as the denial of P. In the example above, ¬P expresses that it is not raining outside, or by a more standard reading: "It is not the case that it is raining outside." When P is true, ¬P is false; and when P is false, ¬P is true. As a result, ¬ ¬P always has the same truth-value as P.Propositional calculus_item_3_8
  • Conjunction is a truth-functional connective which forms a proposition out of two simpler propositions, for example, P and Q. The conjunction of P and Q is written P ∧ Q, and expresses that each are true. We read P ∧ Q as "P and Q". For any two propositions, there are four possible assignments of truth values:Propositional calculus_item_3_9
    1. P is true and Q is truePropositional calculus_item_3_10
    2. P is true and Q is falsePropositional calculus_item_3_11
    3. P is false and Q is truePropositional calculus_item_3_12
    4. P is false and Q is falsePropositional calculus_item_3_13

Propositional calculus_description_list_4

  • The conjunction of P and Q is true in case 1, and is false otherwise. Where P is the proposition that it is raining outside and Q is the proposition that a cold-front is over Kansas, P ∧ Q is true when it is raining outside and there is a cold-front over Kansas. If it is not raining outside, then P ∧ Q is false; and if there is no cold-front over Kansas, then P ∧ Q is also false.Propositional calculus_item_4_14

Propositional calculus_unordered_list_5

  • Disjunction resembles conjunction in that it forms a proposition out of two simpler propositions. We write it P ∨ Q, and it is read "P or Q". It expresses that either P or Q is true. Thus, in the cases listed above, the disjunction of P with Q is true in all cases—except case 4. Using the example above, the disjunction expresses that it is either raining outside, or there is a cold front over Kansas. (Note, this use of disjunction is supposed to resemble the use of the English word "or". However, it is most like the English inclusive "or", which can be used to express the truth of at least one of two propositions. It is not like the English exclusive "or", which expresses the truth of exactly one of two propositions. In other words, the exclusive "or" is false when both P and Q are true (case 1). An example of the exclusive or is: You may have a bagel or a pastry, but not both. Often in natural language, given the appropriate context, the addendum "but not both" is omitted—but implied. In mathematics, however, "or" is always inclusive or; if exclusive or is meant it will be specified, possibly by "xor".)Propositional calculus_item_5_15
  • Material conditional also joins two simpler propositions, and we write P → Q, which is read "if P then Q". The proposition to the left of the arrow is called the antecedent, and the proposition to the right is called the consequent. (There is no such designation for conjunction or disjunction, since they are commutative operations.) It expresses that Q is true whenever P is true. Thus P → Q is true in every case above except case 2, because this is the only case when P is true but Q is not. Using the example, if P then Q expresses that if it is raining outside, then there is a cold-front over Kansas. The material conditional is often confused with physical causation. The material conditional, however, only relates two propositions by their truth-values—which is not the relation of cause and effect. It is contentious in the literature whether the material implication represents logical causation.Propositional calculus_item_5_16
  • Biconditional joins two simpler propositions, and we write P ↔ Q, which is read "P if and only if Q". It expresses that P and Q have the same truth-value, and in cases 1 and 4. 'P is true if and only if Q' is true, and is false otherwise.Propositional calculus_item_5_17

It is very helpful to look at the truth tables for these different operators, as well as the method of analytic tableaux. Propositional calculus_sentence_68

Closure under operations Propositional calculus_section_4

Propositional logic is closed under truth-functional connectives. Propositional calculus_sentence_69

That is to say, for any proposition φ, ¬φ is also a proposition. Propositional calculus_sentence_70

Likewise, for any propositions φ and ψ, φ ∧ ψ is a proposition, and similarly for disjunction, conditional, and biconditional. Propositional calculus_sentence_71

This implies that, for instance, φ ∧ ψ is a proposition, and so it can be conjoined with another proposition. Propositional calculus_sentence_72

In order to represent this, we need to use parentheses to indicate which proposition is conjoined with which. Propositional calculus_sentence_73

For instance, P ∧ Q ∧ R is not a well-formed formula, because we do not know if we are conjoining P ∧ Q with R or if we are conjoining P with Q ∧ R. Thus we must write either (P ∧ Q) ∧ R to represent the former, or P ∧ (Q ∧ R) to represent the latter. Propositional calculus_sentence_74

By evaluating the truth conditions, we see that both expressions have the same truth conditions (will be true in the same cases), and moreover that any proposition formed by arbitrary conjunctions will have the same truth conditions, regardless of the location of the parentheses. Propositional calculus_sentence_75

This means that conjunction is associative, however, one should not assume that parentheses never serve a purpose. Propositional calculus_sentence_76

For instance, the sentence P ∧ (Q ∨ R) does not have the same truth conditions of (P ∧ Q) ∨ R, so they are different sentences distinguished only by the parentheses. Propositional calculus_sentence_77

One can verify this by the truth-table method referenced above. Propositional calculus_sentence_78

Note: For any arbitrary number of propositional constants, we can form a finite number of cases which list their possible truth-values. Propositional calculus_sentence_79

A simple way to generate this is by truth-tables, in which one writes P, Q, ..., Z, for any list of k propositional constants—that is to say, any list of propositional constants with k entries. Propositional calculus_sentence_80

Below this list, one writes 2 rows, and below P one fills in the first half of the rows with true (or T) and the second half with false (or F). Propositional calculus_sentence_81

Below Q one fills in one-quarter of the rows with T, then one-quarter with F, then one-quarter with T and the last quarter with F. The next column alternates between true and false for each eighth of the rows, then sixteenths, and so on, until the last propositional constant varies between T and F for each row. Propositional calculus_sentence_82

This will give a complete listing of cases or truth-value assignments possible for those propositional constants. Propositional calculus_sentence_83

Argument Propositional calculus_section_5

The propositional calculus then defines an argument to be a list of propositions. Propositional calculus_sentence_84

A valid argument is a list of propositions, the last of which follows from—or is implied by—the rest. Propositional calculus_sentence_85

All other arguments are invalid. Propositional calculus_sentence_86

The simplest valid argument is modus ponens, one instance of which is the following list of propositions: Propositional calculus_sentence_87

This generalizes schematically. Propositional calculus_sentence_88

Thus, where φ and ψ may be any propositions at all, Propositional calculus_sentence_89

Other argument forms are convenient, but not necessary. Propositional calculus_sentence_90

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. Propositional calculus_sentence_91

Note, this is not true of the extension of propositional logic to other logics like first-order logic. Propositional calculus_sentence_92

First-order logic requires at least one additional rule of inference in order to obtain completeness. Propositional calculus_sentence_93

Generic description of a propositional calculus Propositional calculus_section_6

Example 1. Simple axiom system Propositional calculus_section_7

Example 2. Natural deduction system Propositional calculus_section_8

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. Propositional calculus_sentence_94

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. Propositional calculus_sentence_95

Our propositional calculus has eleven inference rules. Propositional calculus_sentence_96

These rules allow us to derive other true formulas given a set of formulas that are assumed to be true. Propositional calculus_sentence_97

The first ten simply state that we can infer certain well-formed formulas from other well-formed formulas. Propositional calculus_sentence_98

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. Propositional calculus_sentence_99

Since the first ten rules don't do this they are usually described as non-hypothetical rules, and the last one as a hypothetical rule. Propositional calculus_sentence_100

Basic and derived argument forms Propositional calculus_section_9

Proofs in propositional calculus Propositional calculus_section_10

One of the main uses of a propositional calculus, when interpreted for logical applications, is to determine relations of logical equivalence between propositional formulas. Propositional calculus_sentence_101

These relationships are determined by means of the available transformation rules, sequences of which are called derivations or proofs. Propositional calculus_sentence_102

In the discussion to follow, 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. Propositional calculus_sentence_103

Each premise of the argument, that is, an assumption introduced as an hypothesis of the argument, is listed at the beginning of the sequence and is marked as a "premise" in lieu of other justification. Propositional calculus_sentence_104

The conclusion is listed on the last line. Propositional calculus_sentence_105

A proof is complete if every line follows from the previous ones by the correct application of a transformation rule. Propositional calculus_sentence_106

(For a contrasting approach, see proof-trees). Propositional calculus_sentence_107

Example of a proof in natural deduction system Propositional calculus_section_11

Propositional calculus_unordered_list_6

  • To be shown that A → A.Propositional calculus_item_6_18
  • One possible proof of this (which, though valid, happens to contain more steps than are necessary) may be arranged as follows:Propositional calculus_item_6_19

Example of a proof in a classical propositional calculus system Propositional calculus_section_12

The axioms are: Propositional calculus_sentence_108

And the proof is as follows: Propositional calculus_sentence_109

Soundness and completeness of the rules Propositional calculus_section_13

The crucial properties of this set of rules are that they are sound and complete. Propositional calculus_sentence_110

Informally this means that the rules are correct and that no other rules are required. Propositional calculus_sentence_111

These claims can be made more formal as follows. Propositional calculus_sentence_112

Note that 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. Propositional calculus_sentence_113

We define a truth assignment as a function that maps propositional variables to true or false. Propositional calculus_sentence_114

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. Propositional calculus_sentence_115

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. Propositional calculus_sentence_116

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

Propositional calculus_unordered_list_7

  • A satisfies the propositional variable P if and only if A(P) = truePropositional calculus_item_7_20
  • A satisfies ¬φ if and only if A does not satisfy φPropositional calculus_item_7_21
  • A satisfies (φ ∧ ψ) if and only if A satisfies both φ and ψPropositional calculus_item_7_22
  • A satisfies (φ ∨ ψ) if and only if A satisfies at least one of either φ or ψPropositional calculus_item_7_23
  • A satisfies (φ → ψ) if and only if it is not the case that A satisfies φ but not ψPropositional calculus_item_7_24
  • A satisfies (φ ↔ ψ) if and only if A satisfies both φ and ψ or satisfies neither one of themPropositional calculus_item_7_25

With this definition we can now formalize what it means for a formula φ to be implied by a certain set S of formulas. Propositional calculus_sentence_118

Informally this is true if in all worlds that are possible given the set of formulas S the formula φ also holds. Propositional calculus_sentence_119

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 φ. Propositional calculus_sentence_120

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. Propositional calculus_sentence_121

This allows us to formulate exactly what it means for the set of inference rules to be sound and complete: Propositional calculus_sentence_122

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

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

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

Sketch of a soundness proof Propositional calculus_section_14

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

Notational conventions: Let G be a variable ranging over sets of sentences. Propositional calculus_sentence_127

Let A, B and C range over sentences. Propositional calculus_sentence_128

For "G syntactically entails A" we write "G proves A". Propositional calculus_sentence_129

For "G semantically entails A" we write "G implies A". Propositional calculus_sentence_130

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

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 ...". Propositional calculus_sentence_132

So our proof proceeds by induction. Propositional calculus_sentence_133

Notice that Basis Step II can be omitted for natural deduction systems because they have no axioms. Propositional calculus_sentence_134

When used, Step II involves showing that each of the axioms is a (semantic) logical truth. Propositional calculus_sentence_135

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.) Propositional calculus_sentence_136

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. Propositional calculus_sentence_137

(For example, we might have a rule telling us that from "A" we can derive "A or B". Propositional calculus_sentence_138

In III.a We assume that if A is provable it is implied. Propositional calculus_sentence_139

We also know that if A is provable then "A or B" is provable. Propositional calculus_sentence_140

We have to show that then "A or B" too is implied. Propositional calculus_sentence_141

We do so by appeal to the semantic definition and the assumption we just made. Propositional calculus_sentence_142

A is provable from G, we assume. Propositional calculus_sentence_143

So it is also implied by G. So any semantic valuation making all of G true makes A true. Propositional calculus_sentence_144

But any valuation making A true makes "A or B" true, by the defined semantics for "or". Propositional calculus_sentence_145

So any valuation which makes all of G true makes "A or B" true. Propositional calculus_sentence_146

So "A or B" is implied.) Propositional calculus_sentence_147

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. Propositional calculus_sentence_148

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. Propositional calculus_sentence_149

Sketch of completeness proof Propositional calculus_section_15

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

We adopt the same notational conventions as above. Propositional calculus_sentence_151

We want to show: If G implies A, then G proves A. Propositional calculus_sentence_152

We proceed by contraposition: We show instead that if G does not prove A then G does not imply A. Propositional calculus_sentence_153

If we show that there is a model where A does not hold despite G being true, then obviously G does not imply A. Propositional calculus_sentence_154

The idea is to build such a model out of our very assumption that G does not prove A. Propositional calculus_sentence_155

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

Propositional calculus_unordered_list_8

  • p → (¬p → q)Propositional calculus_item_8_26
  • (p → q) → ((¬p → q) → q)Propositional calculus_item_8_27
  • p → (q → (p → q))Propositional calculus_item_8_28
  • p → (¬q → ¬(p → q))Propositional calculus_item_8_29
  • ¬p → (p → q)Propositional calculus_item_8_30
  • p → pPropositional calculus_item_8_31
  • p → (q → p)Propositional calculus_item_8_32
  • (p → (q → r)) → ((p → q) → (p → r))Propositional calculus_item_8_33

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. Propositional calculus_sentence_157

Example Propositional calculus_section_16

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. Propositional calculus_sentence_158

The proof then is as follows: Propositional calculus_sentence_159

Verifying completeness for the classical propositional calculus system Propositional calculus_section_17

We now verify that the classical propositional calculus system described earlier can indeed prove the required eight theorems mentioned above. Propositional calculus_sentence_160

We use several lemmas proven here: Propositional calculus_sentence_161

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

Another outline for a completeness proof Propositional calculus_section_18

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. Propositional calculus_sentence_163

Consider such a valuation. Propositional calculus_sentence_164

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. Propositional calculus_sentence_165

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)". Propositional calculus_sentence_166

Keep repeating this until all dependencies on propositional variables have been eliminated. Propositional calculus_sentence_167

The result is that we have proved the given tautology. Propositional calculus_sentence_168

Since every tautology is provable, the logic is complete. Propositional calculus_sentence_169

Interpretation of a truth-functional propositional calculus Propositional calculus_section_19

Interpretation of a sentence of truth-functional propositional logic Propositional calculus_section_20

Main article: Interpretation (logic) Propositional calculus_sentence_170

Some consequences of these definitions: Propositional calculus_sentence_171

Alternative calculus Propositional calculus_section_21

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. Propositional calculus_sentence_172

Axioms Propositional calculus_section_22

Let φ, χ, and ψ stand for well-formed formulas. Propositional calculus_sentence_173

(The well-formed formulas themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Propositional calculus_sentence_174

Then the axioms are as follows: Propositional calculus_sentence_175

Propositional calculus_unordered_list_9

  • Axiom THEN-2 may be considered to be a "distributive property of implication with respect to implication."Propositional calculus_item_9_34
  • 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.Propositional calculus_item_9_35
  • Axiom AND-3 corresponds to "conjunction introduction."Propositional calculus_item_9_36
  • 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.Propositional calculus_item_9_37
  • Axiom NOT-1 corresponds to "reductio ad absurdum."Propositional calculus_item_9_38
  • Axiom NOT-2 says that "anything can be deduced from a contradiction."Propositional calculus_item_9_39
  • 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.Propositional calculus_item_9_40

Inference rule Propositional calculus_section_23

The inference rule is modus ponens: Propositional calculus_sentence_176

Meta-inference rule Propositional calculus_section_24

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. Propositional calculus_sentence_177

Then the deduction theorem can be stated as follows: Propositional calculus_sentence_178

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. Propositional calculus_sentence_179

In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus. Propositional calculus_sentence_180

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. Propositional calculus_sentence_181

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. Propositional calculus_sentence_182

The converse of DT is also valid: Propositional calculus_sentence_183

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

The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. Propositional calculus_sentence_185

For example, the axiom AND-1, Propositional calculus_sentence_186

can be transformed by means of the converse of the deduction theorem into the inference rule Propositional calculus_sentence_187

which is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus. Propositional calculus_sentence_188

Example of a proof Propositional calculus_section_25

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

Proof: Propositional calculus_sentence_190

Equivalence to equational logics Propositional calculus_section_26

The preceding alternative calculus is an example of a Hilbert-style deduction system. Propositional calculus_sentence_191

In the case of propositional systems the axioms are terms built with logical connectives and the only inference rule is modus ponens. Propositional calculus_sentence_192

Equational logic as standardly used informally in high school algebra is a different kind of calculus from Hilbert systems. Propositional calculus_sentence_193

Its theorems are equations and its inference rules express the properties of equality, namely that it is a congruence on terms that admits substitution. Propositional calculus_sentence_194

is translated in the inequality version of the algebraic framework as Propositional calculus_sentence_195

Similar but more complex translations to and from algebraic logics are possible for natural deduction systems as described above and for the sequent calculus. Propositional calculus_sentence_196

The entailments of the latter can be interpreted as two-valued, but a more insightful interpretation is as a set, the elements of which can be understood as abstract proofs organized as the morphisms of a category. Propositional calculus_sentence_197

In this interpretation the cut rule of the sequent calculus corresponds to composition in the category. Propositional calculus_sentence_198

Boolean and Heyting algebras enter this picture as special categories having at most one morphism per homset, i.e., one proof per entailment, corresponding to the idea that existence of proofs is all that matters: any proof will do and there is no point in distinguishing them. Propositional calculus_sentence_199

Graphical calculi Propositional calculus_section_27

Other logical calculi Propositional calculus_section_28

Propositional calculus is about the simplest kind of logical calculus in current use. Propositional calculus_sentence_200

It can be extended in several ways. Propositional calculus_sentence_201

(Aristotelian "syllogistic" calculus, which is largely supplanted in modern logic, is in some ways simpler – but in other ways more complex – than propositional calculus.) Propositional calculus_sentence_202

The most immediate way to develop a more complex logical calculus is to introduce rules that are sensitive to more fine-grained details of the sentences being used. Propositional calculus_sentence_203

First-order logic (a.k.a. first-order predicate logic) results when the "atomic sentences" of propositional logic are broken up into terms, variables, predicates, and quantifiers, all keeping the rules of propositional logic with some new ones introduced. Propositional calculus_sentence_204

(For example, from "All dogs are mammals" we may infer "If Rover is a dog then Rover is a mammal".) Propositional calculus_sentence_205

With the tools of first-order logic it is possible to formulate a number of theories, either with explicit axioms or by rules of inference, that can themselves be treated as logical calculi. Propositional calculus_sentence_206

Arithmetic is the best known of these; others include set theory and mereology. Propositional calculus_sentence_207

Second-order logic and other higher-order logics are formal extensions of first-order logic. Propositional calculus_sentence_208

Thus, it makes sense to refer to propositional logic as "zeroth-order logic", when comparing it with these logics. Propositional calculus_sentence_209

Modal logic also offers a variety of inferences that cannot be captured in propositional calculus. Propositional calculus_sentence_210

For example, from "Necessarily p" we may infer that p. From p we may infer "It is possible that p". Propositional calculus_sentence_211

The translation between modal logics and algebraic logics concerns classical and intuitionistic logics but with the introduction of a unary operator on Boolean or Heyting algebras, different from the Boolean operations, interpreting the possibility modality, and in the case of Heyting algebra a second operator interpreting necessity (for Boolean algebra this is redundant since necessity is the De Morgan dual of possibility). Propositional calculus_sentence_212

The first operator preserves 0 and disjunction while the second preserves 1 and conjunction. Propositional calculus_sentence_213

Many-valued logics are those allowing sentences to have values other than true and false. Propositional calculus_sentence_214

(For example, neither and both are standard "extra values"; "continuum logic" allows each sentence to have any of an infinite number of "degrees of truth" between true and false.) Propositional calculus_sentence_215

These logics often require calculational devices quite distinct from propositional calculus. Propositional calculus_sentence_216

When the values form a Boolean algebra (which may have more than two or even infinitely many values), many-valued logic reduces to classical logic; many-valued logics are therefore only of independent interest when the values form an algebra that is not Boolean. Propositional calculus_sentence_217

Solvers Propositional calculus_section_29

Finding solutions to propositional logic formulas is an NP-complete problem. Propositional calculus_sentence_218

However, practical methods exist (e.g., DPLL algorithm, 1962; Chaff algorithm, 2001) that are very fast for many useful cases. Propositional calculus_sentence_219

Recent work has extended the SAT solver algorithms to work with propositions containing arithmetic expressions; these are the SMT solvers. Propositional calculus_sentence_220

See also Propositional calculus_section_30

Higher logical levels Propositional calculus_section_31

Propositional calculus_unordered_list_10

Related topics Propositional calculus_section_32

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: calculus.