In mathematical logic, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true propositions. The series of formulas which is constructed within such a system is called a derivation and the last formula of the series is a theorem, whose derivation may be interpreted as a proof of the truth of the proposition represented by the theorem.
Truth-functional propositional logic is a propositional logic whose interpretation limits the truth values of its propositions to two, usually true and false. Truth-functional propositional logic and systems isomorphic to it are considered to be zeroth-order logic.
Although propositional logic (which is interchangeable with propositional calculus) had been hinted by earlier philosophers, it was developed into a formal logic by Chrysippus[1] and expanded by the Stoics. The logic was focused on propositions. This advancement was different from the traditional syllogistic logic which was focused on terms. However, later in antiquity, the propositional logic developed by the stoics was no longer understood. As a result, the system was essentially reinvented by Peter Abelard.[2]
Propositional logic was eventually refined using symbolic logic. Gottfried Leibniz has been credited with being the founder of symbolic logic for his work with the calculus ratiocinator. Although his work was the first of its kind, it was unknown to the larger logical community. As a result, many of the advances achieved by Leibniz were reachieved by logicians like George Boole and Augustus De Morgan completely independent of Leibniz.[3]
Just as propositional logic can be seen as an advancement from the earlier syllogistic logic, Gottlob Frege's predicate logic was an advancement from the earlier propositional logic. Predicate logic has been described as combining "the distinctive features of syllogistic logic and propositional logic."[4] As a result, It ushered a new era in the history of logic. However, advances in propositional logic were still made after Frege. These include Natural Deduction, Truth-Trees and Truth-Tables. Natural deduction was invented by Jan Łukasiewicz. Truth-Trees were invented by Evert Willem Beth.[5] The invention of truth-tables, however, is of controversial attribution.
The ideas preceding truth tables have been found in both Frege[6] and Bertrand Russell[7] whereas the actual 'tabular structure' (i.e. being formed as a table) is generally credited to either Ludwig Wittgenstein, Emil Post or both (independently of one another).[6] Besides Frege and Russell, others credited for having preceding ideas of truth-tables include Philo, Boole, Charles Sanders Peirce, and Ernst Schröder. And besides Post and Wittgenstein, others credited with the tabular structure include Łukasiewicz, Schröder, Alfred North Whitehead, William Stanley Jevons, John Venn, and Clarence Irving Lewis.[7] Ultimately, some, like John Shosky, have concluded "It is far from clear that any one person should be given the title of 'inventor' of truth-tables.".[7]
In general terms, a calculus is a formal system that consists of a set of syntactic expressions (well-formed formulæ or wffs), 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.
When the formal system is intended to be a logical system, the expressions are meant to be interpreted as statements, and the rules, known as inference rules, are typically intended to be truth-preserving. In this setting, the rules (which may include axioms) can then be used to derive ("infer") formulæ representing true statements from given formulæ representing true statements.
The set of axioms may be empty, a nonempty finite set, a countably infinite set, or be given by axiom schemata. A formal grammar recursively defines the expressions and well-formed formulæ (wffs) of the language. In addition a semantics may be given which defines truth and valuations (or interpretations).
The language of a propositional calculus consists of
- a set of primitive symbols, variously referred to as atomic formulae, placeholders, proposition letters, or variables, and
- a set of operator symbols, variously interpreted as logical operators or logical connectives.
A well-formed formula (wff) is any atomic formula, or any formula that can be built up from atomic formulæ by means of operator symbols according to the rules of the grammar.
Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schemata, however, range over all propositions. It is common to represent propositional constants by Failed to parse (Missing texvc executable; please see math/README to configure.): A , Failed to parse (Missing texvc executable; please see math/README to configure.): B , and Failed to parse (Missing texvc executable; please see math/README to configure.): C , propositional variables by Failed to parse (Missing texvc executable; please see math/README to configure.): P , Failed to parse (Missing texvc executable; please see math/README to configure.): Q , and Failed to parse (Missing texvc executable; please see math/README to configure.): R , and schematic letters are often Greek letters, most often Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \,\! , Failed to parse (Missing texvc executable; please see math/README to configure.): \psi , and Failed to parse (Missing texvc executable; please see math/README to configure.): \chi .
The following outlines a standard propositional calculus. Many different formulations exist which are all more or less equivalent but differ in the details of
- their language, that is, the particular collection of primitive symbols and operator symbols,
- the set of axioms, or distinguished formulæ, and
- the set of inference rules.
We may represent any given proposition with a letter which we call a propositional constant, analogous to representing a number by a letter in mathematics, for instance, Failed to parse (Missing texvc executable; please see math/README to configure.): a = 5 . We require that all propositions have exactly one of two truth-values: true or false. To take an example, let Failed to parse (Missing texvc executable; please see math/README to configure.): P
be the proposition that it is raining outside. This will be true if it is raining outside and false otherwise.
- We then define truth-functional operators, beginning with negation. We write Failed to parse (Missing texvc executable; please see math/README to configure.): \neg P
to represent the negation of Failed to parse (Missing texvc executable; please see math/README to configure.): P
, which can be thought of as the denial of Failed to parse (Missing texvc executable; please see math/README to configure.): P . In the example above, Failed to parse (Missing texvc executable; please see math/README to configure.): \neg 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 Failed to parse (Missing texvc executable; please see math/README to configure.): P
is true, Failed to parse (Missing texvc executable; please see math/README to configure.): \neg P
is false; and when Failed to parse (Missing texvc executable; please see math/README to configure.): P
is false, Failed to parse (Missing texvc executable; please see math/README to configure.): \neg P
is true. Failed to parse (Missing texvc executable; please see math/README to configure.): \neg \neg P
always has the same truth-value as Failed to parse (Missing texvc executable; please see math/README to configure.): P
.
- Conjunction is a truth-functional connective which forms a proposition out of two simpler propositions, for example, Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
. The conjunction of Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is written Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
, and expresses that each are true. We read Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
as "Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
". For any two propositions, there are four possible assignments of truth values:
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): P
is true and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): P
is true and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is false
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): P
is false and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): P
is false and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is false
- The conjunction of Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true in case 1 and is false otherwise. Where Failed to parse (Missing texvc executable; please see math/README to configure.): P
is the proposition that it is raining outside and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is the proposition that a cold-front is over Kansas, Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
is true when it is raining outside and there is a cold-front over Kansas. If it is not raining outside, then Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
is false; and if there is no cold-front over Kansas, then Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
is false.
- Disjunction resembles conjunction in that it forms a proposition out of two simpler propositions. We write it Failed to parse (Missing texvc executable; please see math/README to configure.): P \vee Q
, and it is read "Failed to parse (Missing texvc executable; please see math/README to configure.): P
or Failed to parse (Missing texvc executable; please see math/README to configure.): Q
". It expresses that either Failed to parse (Missing texvc executable; please see math/README to configure.): P
or Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true. Thus, in the cases listed above, the disjunction of Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true in all cases except 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. That is to say, the exclusive "or" is false when both Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
are true (case 1). An example of the exclusive or is: You may have a bagel or a pastry, but not both. Sometimes, given the appropriate context, the addendum "but not both" is omitted but implied.)
- Material conditional also joins two simpler propositions, and we write Failed to parse (Missing texvc executable; please see math/README to configure.): P \rightarrow Q
, which is read "if Failed to parse (Missing texvc executable; please see math/README to configure.): P
then Failed to parse (Missing texvc executable; please see math/README to configure.): 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 Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true whenever Failed to parse (Missing texvc executable; please see math/README to configure.): P
is true. Thus it is true in every case above except case 2, because this is the only case when Failed to parse (Missing texvc executable; please see math/README to configure.): P
is true but Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is not. Using the example, if Failed to parse (Missing texvc executable; please see math/README to configure.): P
then Failed to parse (Missing texvc executable; please see math/README to configure.): 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.
- Biconditional joins two simpler propositions, and we write Failed to parse (Missing texvc executable; please see math/README to configure.): P \leftrightarrow Q
, which is read "Failed to parse (Missing texvc executable; please see math/README to configure.): P
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): Q
". It expresses that Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
have the same truth-value, thus Failed to parse (Missing texvc executable; please see math/README to configure.): P
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true in cases 1 and 4, and false otherwise.
It is extremely helpful to look at the truth tables for these different operators, as well as the method of analytic tableaux.
Propositional logic is closed under truth-functional connectives. That is to say, for any proposition Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \,\! , Failed to parse (Missing texvc executable; please see math/README to configure.): \neg \varphi \,\!
is also a proposition. Likewise, for any propositions Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \,\!
and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \,\!
, Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \and \psi \,\!
is a proposition, and similarly for disjunction, conditional, and biconditional. This implies that, for instance, Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
is a proposition, and so it can be conjoined with another proposition. In order to represent this, we need to use parentheses to indicate which proposition is conjoined with which. For instance, Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q \and R
is not a well-formed formula, because we do not know if we are conjoining Failed to parse (Missing texvc executable; please see math/README to configure.): P \and Q
with Failed to parse (Missing texvc executable; please see math/README to configure.): R
or if we are conjoining Failed to parse (Missing texvc executable; please see math/README to configure.): P
with Failed to parse (Missing texvc executable; please see math/README to configure.): Q \and R
. Thus we must write either Failed to parse (Missing texvc executable; please see math/README to configure.): (P \and Q) \and R
to represent the former, or Failed to parse (Missing texvc executable; please see math/README to configure.): P \and (Q \and R)
to represent the latter. 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. This means that conjunction is associative, however, one should not assume that parentheses never serve a purpose. For instance, the sentence Failed to parse (Missing texvc executable; please see math/README to configure.): P \and (Q \vee R)
does not have the same truth conditions as Failed to parse (Missing texvc executable; please see math/README to configure.): (P \and Q) \vee R
, so they are different sentences distinguished only by the parentheses. One can verify this by the truth-table method referenced above.
Note: For any arbitrary number of propositional constants, we can form a finite number of cases which list their possible truth-values. A simple way to generate this is by truth-tables, in which one writes Failed to parse (Missing texvc executable; please see math/README to configure.): P , Failed to parse (Missing texvc executable; please see math/README to configure.): Q , …, Failed to parse (Missing texvc executable; please see math/README to configure.): Z
for any list of Failed to parse (Missing texvc executable; please see math/README to configure.): k
propositional constants—that is to say, any list of propositional constants with Failed to parse (Missing texvc executable; please see math/README to configure.): k
entries. Below this list, one writes Failed to parse (Missing texvc executable; please see math/README to configure.): 2^k
rows, and below Failed to parse (Missing texvc executable; please see math/README to configure.): P
one fills in the first half of the rows with true (or T) and the second half with false (or F). Below Failed to parse (Missing texvc executable; please see math/README to configure.): 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. This will give a complete listing of cases or truth-value assignments possible for those propositional constants.
The propositional calculus then defines an argument as a set of propositions. A valid argument is a set 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 set of propositions:
- Failed to parse (Missing texvc executable; please see math/README to configure.): \begin{array}{rl} 1. & P \rightarrow Q \\ 2. & P \\ \hline \therefore & Q \end{array}
This is a set 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 Failed to parse (Missing texvc executable; please see math/README to configure.): C
follows from any set of propositions Failed to parse (Missing texvc executable; please see math/README to configure.): (P_1, ..., P_n)
, if Failed to parse (Missing texvc executable; please see math/README to configure.): C
must be true whenever every member of the set Failed to parse (Missing texvc executable; please see math/README to configure.): (P_1, ..., P_n)
is true. In the argument above, for any Failed to parse (Missing texvc executable; please see math/README to configure.): P
and Failed to parse (Missing texvc executable; please see math/README to configure.): Q
, whenever Failed to parse (Missing texvc executable; please see math/README to configure.): P \rightarrow Q
and Failed to parse (Missing texvc executable; please see math/README to configure.): P
are true, necessarily Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is true. Notice that, when Failed to parse (Missing texvc executable; please see math/README to configure.): P
is true, we cannot consider cases 3 and 4 (from the truth table). When Failed to parse (Missing texvc executable; please see math/README to configure.): P \rightarrow Q
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 Failed to parse (Missing texvc executable; please see math/README to configure.): \varphi \,\!
and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
may be any propositions at all,
- Failed to parse (Missing texvc executable; please see math/README to configure.): \begin{array}{rl} 1. & \varphi \rightarrow \psi \\ 2. & \varphi \\ \hline \therefore & \psi \end{array}
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, and so we may think of them as 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 Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is not yet known or stated. After the argument is made, Failed to parse (Missing texvc executable; please see math/README to configure.): Q
is deduced. In this way, we define a deduction system as a set of all propositions that may be deduced from another set of propositions. For instance, given the set of propositions Failed to parse (Missing texvc executable; please see math/README to configure.): A = \{ P \or Q, \neg Q \and R, (P \or Q) \rightarrow R \}
, we can define a deduction system, Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma , which is the set of all propositions which follow from Failed to parse (Missing texvc executable; please see math/README to configure.): A . Reiteration is always assumed, so Failed to parse (Missing texvc executable; please see math/README to configure.): P \or Q, \neg Q \and R, (P \or Q) \rightarrow R \in \Gamma . Also, from the first element of Failed to parse (Missing texvc executable; please see math/README to configure.): A , last element, as well as modus ponens, Failed to parse (Missing texvc executable; please see math/README to configure.): R
is a consequence, and so Failed to parse (Missing texvc executable; please see math/README to configure.): R \in \Gamma
. 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 Failed to parse (Missing texvc executable; please see math/README to configure.): (P \or Q) \leftrightarrow (\neg P \rightarrow Q) , this one is too weak to prove such a proposition.
A propositional calculus is a formal system Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L} = \mathcal{L} \left( \Alpha,\ \Omega,\ \Zeta,\ \Iota \right) , where:
- The alpha set Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha
is a finite set of elements called proposition symbols or propositional variables. Syntactically speaking, these are the most basic elements of the formal language Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L}
, otherwise referred to as atomic formulæ or terminal elements. In the examples to follow, the elements of Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha
are typically the letters Failed to parse (Missing texvc executable; please see math/README to configure.): p
, Failed to parse (Missing texvc executable; please see math/README to configure.): q , Failed to parse (Missing texvc executable; please see math/README to configure.): r , and so on.
- The omega set Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega
is a finite set of elements called operator symbols or logical connectives. The set Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega
is partitioned into disjoint subsets as follows:
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega = \Omega_0 \cup \Omega_1 \cup \ldots \cup \Omega_j \cup \ldots \cup \Omega_m.
- In this partition, Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_j
is the set of operator symbols of arity Failed to parse (Missing texvc executable; please see math/README to configure.): j
.
- In the more familiar propositional calculi, Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega
is typically partitioned as follows:
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_1 = \{ \lnot \},
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_2 \subseteq \{ \land, \lor, \rightarrow, \leftrightarrow \}.
- A frequently adopted convention treats the constant logical values as operators of arity zero, thus:
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_0 = \{ 0, 1 \}.\,\!
- Some writers use the tilde (~), or N, instead of Failed to parse (Missing texvc executable; please see math/README to configure.): \neg
- and some use the ampersand (&), the prefixed K, or Failed to parse (Missing texvc executable; please see math/README to configure.): \cdot
instead of Failed to parse (Missing texvc executable; please see math/README to configure.): \wedge
. Notation varies even more for the set of logical values, with symbols like {false, true}, {F, T}, or Failed to parse (Missing texvc executable; please see math/README to configure.): \{ \bot, \top \}
all being seen in various contexts instead of {0, 1}.
- The zeta set Failed to parse (Missing texvc executable; please see math/README to configure.): \Zeta
is a finite set of transformation rules that are called inference rules when they acquire logical applications.
- The iota set Failed to parse (Missing texvc executable; please see math/README to configure.): \Iota
is a finite set of initial points that are called axioms when they receive logical interpretations.
The language of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L} , also known as its set of formulæ, well-formed formulas or wffs, is inductively defined by the following rules:
- Base: Any element of the alpha set Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha
is a formula of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L}
.
- If Failed to parse (Missing texvc executable; please see math/README to configure.): p_1, p_2, \ldots, p_j
are formulæ and Failed to parse (Missing texvc executable; please see math/README to configure.): f
is in Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_j
, then Failed to parse (Missing texvc executable; please see math/README to configure.): \left( f(p_1, p_2, \ldots, p_j) \right)
is a formula.
- Closed: Nothing else is a formula of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L}
.
Repeated applications of these rules permits the construction of complex formulæ. For example:
- By rule 1, Failed to parse (Missing texvc executable; please see math/README to configure.): p
is a formula.
- By rule 2, Failed to parse (Missing texvc executable; please see math/README to configure.): \neg p
is a formula.
- By rule 1, Failed to parse (Missing texvc executable; please see math/README to configure.): q
is a formula.
- By rule 2, Failed to parse (Missing texvc executable; please see math/README to configure.): ( \neg p \lor q )
is a formula.
Let Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L}_1 = \mathcal{L}(\Alpha,\Omega,\Zeta,\Iota) , where Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha , Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega , Failed to parse (Missing texvc executable; please see math/README to configure.): \Zeta , Failed to parse (Missing texvc executable; please see math/README to configure.): \Iota
are defined as follows:
- The alpha set Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha
, is a finite set of symbols that is large enough to supply the needs of a given discussion, for example:
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha = \{p, q, r, s, t, u \}.\,\!
- Of the three connectives for conjunction, disjunction, and implication (Failed to parse (Missing texvc executable; please see math/README to configure.): \wedge
, Failed to parse (Missing texvc executable; please see math/README to configure.): \lor , and Failed to parse (Missing texvc executable; please see math/README to configure.): \rightarrow ), one can be taken as primitive and the other two can be defined in terms of it and negation (Failed to parse (Missing texvc executable; please see math/README to configure.): \neg ). Indeed, all of the logical connectives can be defined in terms of a sole sufficient operator. The biconditional (Failed to parse (Missing texvc executable; please see math/README to configure.): \leftrightarrow ) can of course be defined in terms of conjunction and implication, with Failed to parse (Missing texvc executable; please see math/README to configure.): a \leftrightarrow b
defined as Failed to parse (Missing texvc executable; please see math/README to configure.): (a \to b) \land (b \to a)
.
Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega = \Omega_1 \cup \Omega_2
partition as follows:
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_1 = \{ \lnot \},
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_2 = \{ \rightarrow \}.
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to (q \to p))
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to (q \to r)) \to ((p \to q) \to (p \to r)))
-
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): ((\neg p \to \neg q) \to (q \to p))
- The rule of inference is modus ponens (i.e., from Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): q ). Then Failed to parse (Missing texvc executable; please see math/README to configure.): a \lor b
is defined as Failed to parse (Missing texvc executable; please see math/README to configure.): \neg a \to b
, and Failed to parse (Missing texvc executable; please see math/README to configure.): a \land b
is defined as Failed to parse (Missing texvc executable; please see math/README to configure.): \neg(a \to \neg b)
.
Let Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{L}_2 = \mathcal{L}(\Alpha, \Omega, \Zeta, \Iota) , where Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha , Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega , Failed to parse (Missing texvc executable; please see math/README to configure.): \Zeta , Failed to parse (Missing texvc executable; please see math/README to configure.): \Iota
are defined as follows:
- The alpha set Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha
, is a finite set of symbols that is large enough to supply the needs of a given discussion, for example:
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Alpha = \{p, q, r, s, t, u \}.\,\!
- The omega set Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega = \Omega_1 \cup \Omega_2
partitions as follows:
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_1 = \{ \lnot \},
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \Omega_2 = \{ \land, \lor, \rightarrow, \leftrightarrow \}.
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, Failed to parse (Missing texvc executable; please see math/README to configure.): \Iota = \varnothing
.
- The set of transformation rules, Failed to parse (Missing texvc executable; please see math/README to configure.): \Zeta
, is described as follows:
Our propositional calculus has ten inference rules. These rules allow us to derive other true formulae given a set of formulae that are assumed to be true. The first nine simply state that we can infer certain wffs from other wffs. 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 formulae to see if we can infer a certain other formula. Since the first nine rules don't 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 Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash . It is basically a convenient shorthand for saying "infer that". The format is Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma \vdash \psi , in which Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma
is a (possibly empty) set of formulae called premises, and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
is a formula called conclusion. The transformation rule Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma \vdash \psi
means that if every proposition in Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma
is a theorem (or has the same truth value as the axioms), then Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
is also a theorem. Note that considering the following rule Conjunction introduction, we will know whenever Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma
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 Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma
as one formula instead of a set. Another omission for convenience is when Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma
is an empty set, in which case Failed to parse (Missing texvc executable; please see math/README to configure.): \Gamma
may not appear.
- Reductio ad absurdum (negation introduction)
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q)
and Failed to parse (Missing texvc executable; please see math/README to configure.): \neg q
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): \neg p .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): \{ p \to q, \neg q \} \vdash \neg p
.
- Double negative elimination
- From Failed to parse (Missing texvc executable; please see math/README to configure.): \neg \neg p
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): p .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): \neg \neg p \vdash p
.
- Conjunction introduction
- From Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q) .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): \{ p, q \} \vdash (p \land q)
.
- Conjunction elimination
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): p .
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): q .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q) \vdash p
and Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q) \vdash q
.
- Disjunction introduction
- From Failed to parse (Missing texvc executable; please see math/README to configure.): p
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): (p \lor q) .
- From Failed to parse (Missing texvc executable; please see math/README to configure.): q
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): (p \lor q) .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): p \vdash (p \lor q)
and Failed to parse (Missing texvc executable; please see math/README to configure.): q \vdash (p \lor q)
.
- Disjunction elimination
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \lor q)
and Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to r)
and Failed to parse (Missing texvc executable; please see math/README to configure.): (q \to r)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): r .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): \{p \lor q, p \to r, q \to r\} \vdash r
.
- Biconditional introduction
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q)
and Failed to parse (Missing texvc executable; please see math/README to configure.): (q \to p)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): \{p \to q, q \to p\} \vdash (p \leftrightarrow q)
.
- Biconditional elimination
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q) .
- From Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): (q \to p) .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) \vdash (p \to q)
and Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) \vdash (q \to p)
.
- Modus ponens (conditional elimination)
- From Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q)
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): q .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): \{ p, p \to q\} \vdash q
.
- Conditional proof (conditional introduction)
- From [accepting Failed to parse (Missing texvc executable; please see math/README to configure.): p
allows a proof of Failed to parse (Missing texvc executable; please see math/README to configure.): q
], infer Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q) .
- That is, Failed to parse (Missing texvc executable; please see math/README to configure.): (p \vdash q) \vdash (\vdash (p \to q))
.
| Basic and Derived Argument Forms |
| Name |
Sequent |
Description |
| Modus Ponens |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land p) \vdash q |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- Failed to parse (Missing texvc executable; please see math/README to configure.): p
- therefore Failed to parse (Missing texvc executable; please see math/README to configure.): q
|
| Modus Tollens |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land \neg q) \vdash \neg p |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- not Failed to parse (Missing texvc executable; please see math/README to configure.): q
- therefore not Failed to parse (Missing texvc executable; please see math/README to configure.): p
|
| Hypothetical Syllogism |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land (q \to r)) \vdash (p \to r) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- if Failed to parse (Missing texvc executable; please see math/README to configure.): q
then Failed to parse (Missing texvc executable; please see math/README to configure.): r
- therefore, if Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): r
|
| Disjunctive Syllogism |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \lor q) \land \neg p) \vdash q |
Either Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
, or both; not Failed to parse (Missing texvc executable; please see math/README to configure.): p
- therefore, Failed to parse (Missing texvc executable; please see math/README to configure.): q
|
| Constructive Dilemma |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land (r \to s) \land (p \lor r)) \vdash (q \lor s) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- and if Failed to parse (Missing texvc executable; please see math/README to configure.): r
then Failed to parse (Missing texvc executable; please see math/README to configure.): s
- but Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): r
- therefore Failed to parse (Missing texvc executable; please see math/README to configure.): q
or Failed to parse (Missing texvc executable; please see math/README to configure.): s
|
| Destructive Dilemma |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land (r \to s) \land(\neg q \lor \neg s)) \vdash (\neg p \lor \neg r) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- and if Failed to parse (Missing texvc executable; please see math/README to configure.): r
then Failed to parse (Missing texvc executable; please see math/README to configure.): s
- but not Failed to parse (Missing texvc executable; please see math/README to configure.): q
or not Failed to parse (Missing texvc executable; please see math/README to configure.): s
- therefore not Failed to parse (Missing texvc executable; please see math/README to configure.): p
or not Failed to parse (Missing texvc executable; please see math/README to configure.): r
|
| Bidirectional Dilemma |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land (r \to s) \land(p \lor \neg s)) \vdash (q \lor \neg r) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- and if Failed to parse (Missing texvc executable; please see math/README to configure.): r
then Failed to parse (Missing texvc executable; please see math/README to configure.): s
- but Failed to parse (Missing texvc executable; please see math/README to configure.): p
or not Failed to parse (Missing texvc executable; please see math/README to configure.): s
- therefore Failed to parse (Missing texvc executable; please see math/README to configure.): q
or not Failed to parse (Missing texvc executable; please see math/README to configure.): r
|
| Simplification |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q) \vdash p |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
are true; therefore Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true
|
| Conjunction |
Failed to parse (Missing texvc executable; please see math/README to configure.): p, q \vdash (p \land q) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
are true separately; therefore they are true conjointly
|
| Addition |
Failed to parse (Missing texvc executable; please see math/README to configure.): p \vdash (p \lor q) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true; therefore the disjunction (Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
) is true
|
| Composition |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \to q) \land (p \to r)) \vdash (p \to (q \land r)) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
- and if Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): r
- therefore if Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true then Failed to parse (Missing texvc executable; please see math/README to configure.): q
and Failed to parse (Missing texvc executable; please see math/README to configure.): r
are true
|
| De Morgan's Theorem (1) |
Failed to parse (Missing texvc executable; please see math/README to configure.): \neg (p \land q) \vdash (\neg p \lor \neg q) |
The negation of (Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
) is equiv. to (not Failed to parse (Missing texvc executable; please see math/README to configure.): p
or not Failed to parse (Missing texvc executable; please see math/README to configure.): q
)
|
| De Morgan's Theorem (2) |
Failed to parse (Missing texvc executable; please see math/README to configure.): \neg (p \lor q) \vdash (\neg p \land \neg q) |
The negation of (Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
) is equiv. to (not Failed to parse (Missing texvc executable; please see math/README to configure.): p
and not Failed to parse (Missing texvc executable; please see math/README to configure.): q
)
|
| Commutation (1) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \lor q) \vdash (q \lor p) |
(Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): q
or Failed to parse (Missing texvc executable; please see math/README to configure.): p
)
|
| Commutation (2) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land q) \vdash (q \land p) |
(Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): q
and Failed to parse (Missing texvc executable; please see math/README to configure.): p
)
|
| Commutation (3) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) \vdash (q \leftrightarrow p) |
(Failed to parse (Missing texvc executable; please see math/README to configure.): p
is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): q
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): q
is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): p
)
|
| Association (1) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \lor (q \lor r)) \vdash ((p \lor q) \lor r) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
or (Failed to parse (Missing texvc executable; please see math/README to configure.): q
or Failed to parse (Missing texvc executable; please see math/README to configure.): r
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
) or Failed to parse (Missing texvc executable; please see math/README to configure.): r
|
| Association (2) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land (q \land r)) \vdash ((p \land q) \land r) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
and (Failed to parse (Missing texvc executable; please see math/README to configure.): q
and Failed to parse (Missing texvc executable; please see math/README to configure.): r
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
) and Failed to parse (Missing texvc executable; please see math/README to configure.): r
|
| Distribution (1) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \land (q \lor r)) \vdash ((p \land q) \lor (p \land r)) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
and (Failed to parse (Missing texvc executable; please see math/README to configure.): q
or Failed to parse (Missing texvc executable; please see math/README to configure.): r
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
) or (Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): r
)
|
| Distribution (2) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \lor (q \land r)) \vdash ((p \lor q) \land (p \lor r)) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
or (Failed to parse (Missing texvc executable; please see math/README to configure.): q
and Failed to parse (Missing texvc executable; please see math/README to configure.): r
) is equiv. to (Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
) and (Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): r
)
|
| Double Negation |
Failed to parse (Missing texvc executable; please see math/README to configure.): p \vdash \neg \neg p |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
is equivalent to the negation of not Failed to parse (Missing texvc executable; please see math/README to configure.): p
|
| Transposition |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q) \vdash (\neg q \to \neg p) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
is equiv. to if not Failed to parse (Missing texvc executable; please see math/README to configure.): q
then not Failed to parse (Missing texvc executable; please see math/README to configure.): p
|
| Material Implication |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to q) \vdash (\neg p \lor q) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then Failed to parse (Missing texvc executable; please see math/README to configure.): q
is equiv. to not Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
|
| Material Equivalence (1) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) \vdash ((p \to q) \land (q \to p)) |
(Failed to parse (Missing texvc executable; please see math/README to configure.): p
is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): q
) means (if Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true then Failed to parse (Missing texvc executable; please see math/README to configure.): q
is true) and (if Failed to parse (Missing texvc executable; please see math/README to configure.): q
is true then Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true)
|
| Material Equivalence (2) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) \vdash ((p \land q) \lor (\neg p \land \neg q)) |
(Failed to parse (Missing texvc executable; please see math/README to configure.): p
is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): q
) means either (Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
are true) or (both Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
are false)
|
| Material Equivalence (3) |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \leftrightarrow q) \vdash ((p \lor \neg q) \land (\neg p \lor q)) |
(Failed to parse (Missing texvc executable; please see math/README to configure.): p
is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): q
) means, both (Failed to parse (Missing texvc executable; please see math/README to configure.): p
or not Failed to parse (Missing texvc executable; please see math/README to configure.): q
is true) and (not Failed to parse (Missing texvc executable; please see math/README to configure.): p
or Failed to parse (Missing texvc executable; please see math/README to configure.): q
is true)
|
| Exportation[8] |
Failed to parse (Missing texvc executable; please see math/README to configure.): ((p \land q) \to r) \vdash (p \to (q \to r)) |
from (if Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
are true then Failed to parse (Missing texvc executable; please see math/README to configure.): r
is true) we can prove (if Failed to parse (Missing texvc executable; please see math/README to configure.): q
is true then Failed to parse (Missing texvc executable; please see math/README to configure.): r
is true, if Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true)
|
| Importation |
Failed to parse (Missing texvc executable; please see math/README to configure.): (p \to (q \to r)) \vdash ((p \land q) \to r) |
If Failed to parse (Missing texvc executable; please see math/README to configure.): p
then (if Failed to parse (Missing texvc executable; please see math/README to configure.): q
then Failed to parse (Missing texvc executable; please see math/README to configure.): r
) is equivalent to if Failed to parse (Missing texvc executable; please see math/README to configure.): p
and Failed to parse (Missing texvc executable; please see math/README to configure.): q
then Failed to parse (Missing texvc executable; please see math/README to configure.): r
|
| Tautology (1) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p \vdash (p \lor p) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true or Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true
|
| Tautology (2) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p \vdash (p \land p) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true is equiv. to Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true and Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true
|
| Tertium non datur (Law of Excluded Middle) |
Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash (p \lor \neg p) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
or not Failed to parse (Missing texvc executable; please see math/README to configure.): p
is true
|
| Law of Non-Contradiction |
Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash \neg (p \land \neg p) |
Failed to parse (Missing texvc executable; please see math/README to configure.): p
and not Failed to parse (Missing texvc executable; please see math/README to configure.): p
is false, is a true statement
|
One of the main uses of a propositional calculus, when interpreted for logical applications, is to determine relations of logical equivalence between propositional formulæ. These relationships are determined by means of the available transformation rules, sequences of which are called derivations or proofs.
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. 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. 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).
- To be shown that Failed to parse (Missing texvc executable; please see math/README to configure.): A \to A
.
- 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 |
Failed to parse (Missing texvc executable; please see math/README to configure.): A\,\! |
premise |
| 2 |
Failed to parse (Missing texvc executable; please see math/README to configure.): A \lor A |
From (1) by disjunction introduction |
| 3 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (A \lor A) \land A |
From (1) and (2) by conjunction introduction |
| 4 |
Failed to parse (Missing texvc executable; please see math/README to configure.): A\,\! |
From (3) by conjunction elimination |
| 5 |
Failed to parse (Missing texvc executable; please see math/README to configure.): A \vdash A |
Summary of (1) through (4) |
| 6 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash A \to A |
From (5) by conditional proof |
Interpret Failed to parse (Missing texvc executable; please see math/README to configure.): A \vdash A
as "Assuming Failed to parse (Missing texvc executable; please see math/README to configure.): A
, infer Failed to parse (Missing texvc executable; please see math/README to configure.): A ". Read Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash A \to A
as "Assuming nothing, infer that Failed to parse (Missing texvc executable; please see math/README to configure.): A
implies Failed to parse (Missing texvc executable; please see math/README to configure.): A
", or "It is a tautology that Failed to parse (Missing texvc executable; please see math/README to configure.): A
implies Failed to parse (Missing texvc executable; please see math/README to configure.): A
", or "It is always true that Failed to parse (Missing texvc executable; please see math/README to configure.): A
implies Failed to parse (Missing texvc executable; please see math/README to configure.): A
".
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.
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 formulae 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 Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies a certain wff with the following rules:
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies the propositional variable Failed to parse (Missing texvc executable; please see math/README to configure.): P \,
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): A(P) = \text{true} \,
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): \neg \phi \,
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
does not satisfy Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \land \psi) \,
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies both Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \,
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \lor \psi) \,
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies at least one of either Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
or Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \,
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \to \psi) \,
if and only if it is not the case that Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
but not Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \,
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \leftrightarrow \psi) \,
if and only if Failed to parse (Missing texvc executable; please see math/README to configure.): A \,
satisfies both Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi \,
or satisfies neither one of them
With this definition we can now formalize what it means for a formula Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
to be implied by a certain set Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
of formulae. Informally this is true if in all worlds that are possible given the set of formulae Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
the formula Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
also holds. This leads to the following formal definition: We say that a set Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
of wffs semantically entails (or implies) a certain wff Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
if all truth assignments that satisfy all the formulae in Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
also satisfy Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,.
Finally we define syntactical entailment such that Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
is syntactically entailed by Failed to parse (Missing texvc executable; please see math/README to configure.): 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 wffs Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
syntactically entails wff Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
then Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
semantically entails Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
- Completeness
- If the set of wffs Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
semantically entails wff Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
then Failed to parse (Missing texvc executable; please see math/README to configure.): S \,
syntactically entails Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \,
For the above set of rules this is indeed the case.
(For most logical systems, this is the comparatively "simple" direction of proof)
Notational conventions: Let Failed to parse (Missing texvc executable; please see math/README to configure.): G
be a variable ranging over sets of sentences. Let Failed to parse (Missing texvc executable; please see math/README to configure.): A
, Failed to parse (Missing texvc executable; please see math/README to configure.): B , and Failed to parse (Missing texvc executable; please see math/README to configure.): C
range over sentences. For "Failed to parse (Missing texvc executable; please see math/README to configure.): G
syntactically entails Failed to parse (Missing texvc executable; please see math/README to configure.): A
" we write "Failed to parse (Missing texvc executable; please see math/README to configure.): G
proves Failed to parse (Missing texvc executable; please see math/README to configure.): A
". For "Failed to parse (Missing texvc executable; please see math/README to configure.): G
semantically entails Failed to parse (Missing texvc executable; please see math/README to configure.): A
" we write "Failed to parse (Missing texvc executable; please see math/README to configure.): G
implies Failed to parse (Missing texvc executable; please see math/README to configure.): A
".
We want to show: (Failed to parse (Missing texvc executable; please see math/README to configure.): A )(Failed to parse (Missing texvc executable; please see math/README to configure.): G )(if Failed to parse (Missing texvc executable; please see math/README to configure.): G
proves Failed to parse (Missing texvc executable; please see math/README to configure.): A
, then Failed to parse (Missing texvc executable; please see math/README to configure.): G
implies Failed to parse (Missing texvc executable; please see math/README to configure.): A
).
We note that "Failed to parse (Missing texvc executable; please see math/README to configure.): G
proves Failed to parse (Missing texvc executable; please see math/README to configure.): A
" has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If Failed to parse (Missing texvc executable; please see math/README to configure.): G
proves Failed to parse (Missing texvc executable; please see math/README to configure.): A
, then ...". So our proof proceeds by induction.
- Basis. Show: If Failed to parse (Missing texvc executable; please see math/README to configure.): A is a member of Failed to parse (Missing texvc executable; please see math/README to configure.): G , then Failed to parse (Missing texvc executable; please see math/README to configure.): G implies Failed to parse (Missing texvc executable; please see math/README to configure.): A .
- Basis. Show: If Failed to parse (Missing texvc executable; please see math/README to configure.): A is an axiom, then Failed to parse (Missing texvc executable; please see math/README to configure.): G implies Failed to parse (Missing texvc executable; please see math/README to configure.): A .
- Inductive step (induction on Failed to parse (Missing texvc executable; please see math/README to configure.): n , the length of the proof):
- Assume for arbitrary Failed to parse (Missing texvc executable; please see math/README to configure.): G and Failed to parse (Missing texvc executable; please see math/README to configure.): A that if Failed to parse (Missing texvc executable; please see math/README to configure.): G proves Failed to parse (Missing texvc executable; please see math/README to configure.): A in Failed to parse (Missing texvc executable; please see math/README to configure.): n or fewer steps, then Failed to parse (Missing texvc executable; please see math/README to configure.): G implies Failed to parse (Missing texvc executable; please see math/README to configure.): A .
- For each possible application of a rule of inference at step Failed to parse (Missing texvc executable; please see math/README to configure.): n+1 , leading to a new theorem Failed to parse (Missing texvc executable; please see math/README to configure.): B , show that Failed to parse (Missing texvc executable; please see math/README to configure.): G implies Failed to parse (Missing texvc executable; please see math/README to configure.): 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 step(s) demonstrate(s) that the simplest provable sentences from Failed to parse (Missing texvc executable; please see math/README to configure.): G
are also implied by Failed to parse (Missing texvc executable; please see math/README to configure.): G
, for any Failed to parse (Missing texvc executable; please see math/README to configure.): G . (The 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 "Failed to parse (Missing texvc executable; please see math/README to configure.): A " we can derive "Failed to parse (Missing texvc executable; please see math/README to configure.): A
or Failed to parse (Missing texvc executable; please see math/README to configure.): B
". In III.a We assume that if Failed to parse (Missing texvc executable; please see math/README to configure.): A
is provable it is implied. We also know that if Failed to parse (Missing texvc executable; please see math/README to configure.): A
is provable then "Failed to parse (Missing texvc executable; please see math/README to configure.): A
or Failed to parse (Missing texvc executable; please see math/README to configure.): B
" is provable. We have to show that then "Failed to parse (Missing texvc executable; please see math/README to configure.): A
or Failed to parse (Missing texvc executable; please see math/README to configure.): B
" too is implied. We do so by appeal to the semantic definition and the assumption we just made. Failed to parse (Missing texvc executable; please see math/README to configure.): A
is provable from Failed to parse (Missing texvc executable; please see math/README to configure.): G
, we assume. So it is also implied by Failed to parse (Missing texvc executable; please see math/README to configure.): G . So any semantic valuation making all of Failed to parse (Missing texvc executable; please see math/README to configure.): G
true makes Failed to parse (Missing texvc executable; please see math/README to configure.): A
true. But any valuation making Failed to parse (Missing texvc executable; please see math/README to configure.): A
true makes "Failed to parse (Missing texvc executable; please see math/README to configure.): A
or Failed to parse (Missing texvc executable; please see math/README to configure.): B
" true, by the defined semantics for "or". So any valuation which makes all of Failed to parse (Missing texvc executable; please see math/README to configure.): G
true makes "Failed to parse (Missing texvc executable; please see math/README to configure.): A
or Failed to parse (Missing texvc executable; please see math/README to configure.): B
" true. So "Failed to parse (Missing texvc executable; please see math/README to configure.): A
or Failed to parse (Missing texvc executable; please see math/README to configure.): 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 Failed to parse (Missing texvc executable; please see math/README to configure.): G , an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.
(This is usually the much harder direction of proof.)
We adopt the same notational conventions as above.
We want to show: If Failed to parse (Missing texvc executable; please see math/README to configure.): G
implies Failed to parse (Missing texvc executable; please see math/README to configure.): A
, then Failed to parse (Missing texvc executable; please see math/README to configure.): G
proves Failed to parse (Missing texvc executable; please see math/README to configure.): A
. We proceed by contraposition: We show instead that if Failed to parse (Missing texvc executable; please see math/README to configure.): G
does not prove Failed to parse (Missing texvc executable; please see math/README to configure.): A
then Failed to parse (Missing texvc executable; please see math/README to configure.): G
does not imply Failed to parse (Missing texvc executable; please see math/README to configure.): A
.
- Failed to parse (Missing texvc executable; please see math/README to configure.): G does not prove Failed to parse (Missing texvc executable; please see math/README to configure.): A . (Assumption)
- If Failed to parse (Missing texvc executable; please see math/README to configure.): G does not prove Failed to parse (Missing texvc executable; please see math/README to configure.): A , then we can construct an (infinite) "Maximal Set", Failed to parse (Missing texvc executable; please see math/README to configure.): G^* , which is a superset of Failed to parse (Missing texvc executable; please see math/README to configure.): G and which also does not prove Failed to parse (Missing texvc executable; please see math/README to configure.): A .
- Place an "ordering" on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them Failed to parse (Missing texvc executable; please see math/README to configure.): E_1 , Failed to parse (Missing texvc executable; please see math/README to configure.): E_2 , …
- Define a series Failed to parse (Missing texvc executable; please see math/README to configure.): G_n of sets (Failed to parse (Missing texvc executable; please see math/README to configure.): G_0 , Failed to parse (Missing texvc executable; please see math/README to configure.): G_1 , …) inductively:
- Failed to parse (Missing texvc executable; please see math/README to configure.): G_0 = G
- If Failed to parse (Missing texvc executable; please see math/README to configure.): G_k \cup \{ E_{k+1} \} proves Failed to parse (Missing texvc executable; please see math/README to configure.): A , then Failed to parse (Missing texvc executable; please see math/README to configure.): G_{k+1} = G_k
- If Failed to parse (Missing texvc executable; please see math/README to configure.): G_k \cup \{ E_{k+1} \} does not prove Failed to parse (Missing texvc executable; please see math/README to configure.): A , then Failed to parse (Missing texvc executable; please see math/README to configure.): G_{k+1} = G_k \cup \{ E_{k+1} \}
- Define Failed to parse (Missing texvc executable; please see math/README to configure.): G^* as the union of all the Failed to parse (Missing texvc executable; please see math/README to configure.): G_n . (That is, Failed to parse (Missing texvc executable; please see math/README to configure.): G^* is the set of all the sentences that are in any Failed to parse (Missing texvc executable; please see math/README to configure.): G_n .)
- It can be easily shown that
- Failed to parse (Missing texvc executable; please see math/README to configure.): G^* contains (is a superset of) Failed to parse (Missing texvc executable; please see math/README to configure.): G (by (b.i));
- Failed to parse (Missing texvc executable; please see math/README to configure.): G^* does not prove Failed to parse (Missing texvc executable; please see math/README to configure.): A (because if it proves Failed to parse (Missing texvc executable; please see math/README to configure.): A then some sentence was added to some Failed to parse (Missing texvc executable; please see math/README to configure.): G_n which caused it to prove 'Failed to parse (Missing texvc executable; please see math/README to configure.): A
- but this was ruled out by definition); and
- Failed to parse (Missing texvc executable; please see math/README to configure.): G^* is a "Maximal Set" (with respect to Failed to parse (Missing texvc executable; please see math/README to configure.): A ): If any more sentences whatever were added to Failed to parse (Missing texvc executable; please see math/README to configure.): G^* , it would prove Failed to parse (Missing texvc executable; please see math/README to configure.): 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 Failed to parse (Missing texvc executable; please see math/README to configure.): G_n , again by definition)
- If Failed to parse (Missing texvc executable; please see math/README to configure.): G^* is a Maximal Set (wrt Failed to parse (Missing texvc executable; please see math/README to configure.): A ), then it is "truth-like". This means that it contains the sentence "Failed to parse (Missing texvc executable; please see math/README to configure.): C " only if it does not contain the sentence not-Failed to parse (Missing texvc executable; please see math/README to configure.): C
- If it contains "Failed to parse (Missing texvc executable; please see math/README to configure.): C
" and contains "If Failed to parse (Missing texvc executable; please see math/README to configure.): C then Failed to parse (Missing texvc executable; please see math/README to configure.): B " then it also contains "Failed to parse (Missing texvc executable; please see math/README to configure.): B "; and so forth.
- If Failed to parse (Missing texvc executable; please see math/README to configure.): G^* is truth-like there is a "Failed to parse (Missing texvc executable; please see math/README to configure.): G^* -Canonical" valuation of the language: one that makes every sentence in Failed to parse (Missing texvc executable; please see math/README to configure.): G^* true and everything outside Failed to parse (Missing texvc executable; please see math/README to configure.): G^* false while still obeying the laws of semantic composition in the language.
- A Failed to parse (Missing texvc executable; please see math/README to configure.): G^* -canonical valuation will make our original set Failed to parse (Missing texvc executable; please see math/README to configure.): G all true, and make Failed to parse (Missing texvc executable; please see math/README to configure.): A false.
- If there is a valuation on which Failed to parse (Missing texvc executable; please see math/README to configure.): G are true and Failed to parse (Missing texvc executable; please see math/README to configure.): A is false, then Failed to parse (Missing texvc executable; please see math/README to configure.): G does not (semantically) imply Failed to parse (Missing texvc executable; please see math/README to configure.): A .
QED
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 subformulae, 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.
An interpretation of a truth-functional propositional calculus Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P}
is an assignment to each propositional symbol of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P}
of one or the other (but not both) of the truth values truth (T) and falsity (F), and an assignment to the connective symbols of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P}
of their usual truth-functional meanings. An interpretation of a truth-functional propositional calculus may also be expressed in terms of truth tables.[9]
For Failed to parse (Missing texvc executable; please see math/README to configure.): n
distinct propositional symbols there are Failed to parse (Missing texvc executable; please see math/README to configure.): 2^n
distinct possible interpretations. For any particular symbol Failed to parse (Missing texvc executable; please see math/README to configure.): a
, for example, there are Failed to parse (Missing texvc executable; please see math/README to configure.): 2^1=2
possible interpretations:
- Failed to parse (Missing texvc executable; please see math/README to configure.): a
is assigned T, or
- Failed to parse (Missing texvc executable; please see math/README to configure.): a
is assigned F.
For the pair Failed to parse (Missing texvc executable; please see math/README to configure.): a , Failed to parse (Missing texvc executable; please see math/README to configure.): b
there are Failed to parse (Missing texvc executable; please see math/README to configure.): 2^2=4
possible interpretations:
- both are assigned T,
- both are assigned F,
- Failed to parse (Missing texvc executable; please see math/README to configure.): a
is assigned T and Failed to parse (Missing texvc executable; please see math/README to configure.): b
is assigned F, or
- Failed to parse (Missing texvc executable; please see math/README to configure.): a
is assigned F and Failed to parse (Missing texvc executable; please see math/README to configure.): b
is assigned T.[9]
Since Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P}
has Failed to parse (Missing texvc executable; please see math/README to configure.): \aleph_0
, that is, denumerably many propositional symbols, there are Failed to parse (Missing texvc executable; please see math/README to configure.): 2^{\aleph_0}=\mathfrak c , and therefore uncountably many distinct possible interpretations of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P} .[9]
If Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
are formulas of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P}
and Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
is an interpretation of Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{P}
then:
- A sentence of propositional logic is true under an interpretation Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
iff Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
assigns the truth value T to that sentence. If a sentence is true under an interpretation, then that interpretation is called a model of that sentence.
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is false under an interpretation Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
iff Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is not true under Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
.[9]
- A sentence of propositional logic is logically valid iff it is true under every interpretation
- Failed to parse (Missing texvc executable; please see math/README to configure.): \models\phi
means that Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is logically valid
- A sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
of propositional logic is a semantic consequence of a sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
iff there is no interpretation under which Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is true and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
is false.
- A sentence of propositional logic is consistent iff it is true under at least one interpretation. It is inconsistent if it is not consistent.
Some consequences of these definitions:
- For any given interpretation a given formula is either true or false.[9]
- No formula is both true and false under the same interpretation.[9]
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is false for a given interpretation iff Failed to parse (Missing texvc executable; please see math/README to configure.): \neg\phi
is true for that interpretation; and Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is true under an interpretation iff Failed to parse (Missing texvc executable; please see math/README to configure.): \neg\phi
is false under that interpretation.[9]
- If Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
and Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \rightarrow \psi)
are both true under a given interpretation, then Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
is true under that interpretation.[9]
- If Failed to parse (Missing texvc executable; please see math/README to configure.): \models_{\mathrm P}\phi
and Failed to parse (Missing texvc executable; please see math/README to configure.): \models_{\mathrm P}(\phi \rightarrow \psi)
, then Failed to parse (Missing texvc executable; please see math/README to configure.): \models_{\mathrm P}\psi .[9]
- Failed to parse (Missing texvc executable; please see math/README to configure.): \neg\phi
is true under Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
iff Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is not true under Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
.
- Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \rightarrow \psi)
is true under Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
iff either Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
is not true under Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
or Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
is true under Failed to parse (Missing texvc executable; please see math/README to configure.): \mathcal{I}
.[9]
- A sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
of propositional logic is a semantic consequence of a sentence Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
iff Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \rightarrow \psi)
is logically valid, that is, Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \models_{\mathrm P} \psi
iff Failed to parse (Missing texvc executable; please see math/README to configure.): \models_{\mathrm P}(\phi \rightarrow \psi)
.[9]
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.
Let Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\! , Failed to parse (Missing texvc executable; please see math/README to configure.): \chi
and Failed to parse (Missing texvc executable; please see math/README to configure.): \psi
stand for well-formed formulæ. (The wffs 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 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \to (\chi \to \phi) |
Add hypothesis Failed to parse (Missing texvc executable; please see math/README to configure.): \chi
, implication introduction
|
| THEN-2 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \to (\chi \to \psi)) \to ((\phi \to \chi) \to (\phi \to \psi)) |
Distribute hypothesis Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
over implication
|
| AND-1 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \land \chi \to \phi |
Eliminate conjunction |
| AND-2 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \land \chi \to \chi |
|
| AND-3 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \to (\chi \to (\phi \land \chi)) |
Introduce conjunction |
| OR-1 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \to \phi \lor \chi |
Introduce disjunction |
| OR-2 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \chi \to \phi \lor \chi |
|
| OR-3 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \to \psi) \to ((\chi \to \psi) \to (\phi \lor \chi \to \psi)) |
Eliminate disjunction |
| NOT-1 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \to \chi) \to ((\phi \to \neg \chi) \to \neg \phi) |
Introduce negation |
| NOT-2 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \to (\neg \phi \to \chi) |
Eliminate negation |
| NOT-3 |
Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \lor \neg \phi |
Excluded middle, classical logic |
| IFF-1 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \leftrightarrow \chi) \to (\phi \to \chi) |
Eliminate equivalence |
| IFF-2 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \leftrightarrow \chi) \to (\chi \to \phi) |
|
| IFF-3 |
Failed to parse (Missing texvc executable; please see math/README to configure.): (\phi \to \chi) \to ((\chi \to \phi) \to (\phi \leftrightarrow \chi)) |
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 formulae: 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.
The inference rule is modus ponens:
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi, \ \phi \rightarrow \chi \vdash \chi
.
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
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ \phi_2, \ ... , \ \phi_n, \ \chi \vdash \psi
- has been demonstrated, then it is also possible to demonstrate the sequence
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ \phi_2, \ ..., \ \phi_n \vdash \chi \rightarrow \psi
.
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
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ \phi_2, \ ..., \ \phi_n \vdash \chi \rightarrow \psi
- has been demonstrated, then it is also possible to demonstrate the sequence
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ \phi_2, \ ... , \ \phi_n, \ \chi \vdash \psi
in fact, the validity of the converse of DT is almost trivial compared to that of DT:
- If
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ ... , \ \phi_n \vdash \chi \rightarrow \psi
- then
- 1: Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ ... , \ \phi_n, \ \chi \vdash \chi \rightarrow \psi
-
- 2: Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ ... , \ \phi_n, \ \chi \vdash \chi
- and from (1) and (2) can be deduced
- 3: Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ ... , \ \phi_n, \ \chi \vdash \psi
- 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, the axiom AND-1,
- Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash \phi \wedge \chi \rightarrow \phi
can be transformed by means of the converse of the deduction theorem into the inference rule
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi \wedge \chi \vdash \phi
which is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.
The following is an example of a (syntactical) demonstration, involving only axioms THEN-1 and THEN-2:
Prove: Failed to parse (Missing texvc executable; please see math/README to configure.): A \rightarrow A
(Reflexivity of implication).
Proof:
- Failed to parse (Missing texvc executable; please see math/README to configure.): (A \rightarrow ((B \rightarrow A) \rightarrow A)) \rightarrow ((A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A))
-
- Axiom THEN-2 with Failed to parse (Missing texvc executable; please see math/README to configure.): \phi = A\,\!
, Failed to parse (Missing texvc executable; please see math/README to configure.): \chi = B \rightarrow A , Failed to parse (Missing texvc executable; please see math/README to configure.): \psi = A
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \rightarrow ((B \rightarrow A) \rightarrow A)
-
- Axiom THEN-1 with Failed to parse (Missing texvc executable; please see math/README to configure.): \phi = A\,\!
, Failed to parse (Missing texvc executable; please see math/README to configure.): \chi = B \rightarrow A
- Failed to parse (Missing texvc executable; please see math/README to configure.): (A \rightarrow (B \rightarrow A)) \rightarrow (A \rightarrow A)
-
- From (1) and (2) by modus ponens.
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \rightarrow (B \rightarrow A)
-
- Axiom THEN-1 with Failed to parse (Missing texvc executable; please see math/README to configure.): \phi = A\,\!
, Failed to parse (Missing texvc executable; please see math/README to configure.): \chi = B
- Failed to parse (Missing texvc executable; please see math/README to configure.): A \rightarrow A
-
- From (3) and (4) by modus ponens.
The preceding alternative calculus is an example of a Hilbert-style deduction system. In the case of propositional systems the axioms are terms built with logical connectives and the only inference rule is modus ponens. Equational logic as standardly used informally in high school algebra is a different kind of calculus from Hilbert systems. Its theorems are equations and its inference rules express the properties of equality, namely that it is a congruence on terms that admits substitution.
Classical propositional calculus as described above is equivalent to Boolean algebra, while intuitionistic propositional calculus is equivalent to Heyting algebra. The equivalence is shown by translation in each direction of the theorems of the respective systems. Theorems Failed to parse (Missing texvc executable; please see math/README to configure.): \phi\,\!
of classical or intuitionistic propositional calculus are translated as equations Failed to parse (Missing texvc executable; please see math/README to configure.): \phi = 1\,\!
of Boolean or Heyting algebra respectively. Conversely theorems Failed to parse (Missing texvc executable; please see math/README to configure.): x = y
of Boolean or Heyting algebra are translated as theorems Failed to parse (Missing texvc executable; please see math/README to configure.): (x \to y) \land (y \to x)
of classical or propositional calculus respectively, for which Failed to parse (Missing texvc executable; please see math/README to configure.): x \equiv y
is a standard abbreviation. In the case of Boolean algebra Failed to parse (Missing texvc executable; please see math/README to configure.): x = y
can also be translated as Failed to parse (Missing texvc executable; please see math/README to configure.): (x \land y) \lor (\neg x \land \neg y)
, but this translation is incorrect intuitionistically.
In both Boolean and Heyting algebra, inequality Failed to parse (Missing texvc executable; please see math/README to configure.): x \le y
can be used in place of equality. The equality Failed to parse (Missing texvc executable; please see math/README to configure.): x = y
is expressible as a pair of inequalities Failed to parse (Missing texvc executable; please see math/README to configure.): x \le y
and Failed to parse (Missing texvc executable; please see math/README to configure.): y \le x
. Conversely the inequality Failed to parse (Missing texvc executable; please see math/README to configure.): x \le y
is expressible as the equality Failed to parse (Missing texvc executable; please see math/README to configure.): x \land y = x
, or as Failed to parse (Missing texvc executable; please see math/README to configure.): x \lor y = y . The significance of inequality for Hilbert-style systems is that it corresponds to the latter's deduction or entailment symbol Failed to parse (Missing texvc executable; please see math/README to configure.): \vdash . An entailment
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1, \ \phi_2, \ \dots, \ \phi_n \vdash \psi
is translated in the inequality version of the algebraic framework as
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): \phi_1\ \land\ \phi_2\ \land\ \dots\ \land \ \phi_n\ \ \le\ \ \psi
Conversely the algebraic inequality Failed to parse (Missing texvc executable; please see math/README to configure.): x \le y
is translated as the entailment
-
- Failed to parse (Missing texvc executable; please see math/README to configure.): x\ \vdash\ y
.
The difference between implication Failed to parse (Missing texvc executable; please see math/README to configure.): x \to y
and inequality or entailment Failed to parse (Missing texvc executable; please see math/README to configure.): x \le y
or Failed to parse (Missing texvc executable; please see math/README to configure.): x\ \vdash\ y
is that the former is internal to the logic while the latter is external. Internal implication between two terms is another term of the same kind. Entailment as external implication between two terms expresses a metatruth outside the language of the logic, and is considered part of the metalanguage. Even when the logic under study is intuitionistic, entailment is ordinarily understood classically as two-valued: either the left side entails, or is less-or-equal to, the right side, or it is not.
Similar but more complex translations to and from algebraic logics are possible for natural deduction systems as described above and for the sequent calculus. 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. In this interpretation the cut rule of the sequent calculus corresponds to composition in the category. 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.
It is possible to generalize the definition of a formal language from a set of finite sequences over a finite basis to include many other sets of mathematical structures, so long as they are built up by finitary means from finite materials. What's more, many of these families of formal structures are especially well-suited for use in logic.
For example, there are many families of graphs that are close enough analogues of formal languages that the concept of a calculus is quite easily and naturally extended to them. Indeed, many species of graphs arise as parse graphs in the syntactic analysis of the corresponding families of text structures. The exigencies of practical computation on formal languages frequently demand that text strings be converted into pointer structure renditions of parse graphs, simply as a matter of checking whether strings are wffs or not. Once this is done, there are many advantages to be gained from developing the graphical analogue of the calculus on strings. The mapping from strings to parse graphs is called parsing and the inverse mapping from parse graphs to strings is achieved by an operation that is called traversing the graph.
Propositional calculus is about the simplest kind of logical calculus in current use. It can be extended in several ways. (Aristotelian "syllogistic" calculus, which is largely supplanted in modern logic, is in some ways simpler – but in other ways more complex – than propositional calculus.) 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.
First-order logic (aka 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. (For example, from "All dogs are mammals" we may infer "If Rover is a dog then Rover is a mammal".) 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. Arithmetic is the best known of these; others include set theory and mereology. Second-order logic and other higher-order logics are formal extensions of first-order logic. Thus, it makes sense to refer to propositional logic as "zeroth-order logic", when comparing it with these logics.
Modal logic also offers a variety of inferences that cannot be captured in propositional calculus. For example, from "Necessarily Failed to parse (Missing texvc executable; please see math/README to configure.): p " we may infer that Failed to parse (Missing texvc executable; please see math/README to configure.): p . From Failed to parse (Missing texvc executable; please see math/README to configure.): p
we may infer "It is possible that Failed to parse (Missing texvc executable; please see math/README to configure.): p
". The translation between modal logics and algebraic logics is as for 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). The first operator preserves 0 and disjunction while the second preserves 1 and conjunction.
Many-valued logics are those allowing sentences to have values other than true and false. (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.) These logics often require calculational devices quite distinct from propositional calculus. 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.
Finding solutions to 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.
- ^ Ancient Logic (Stanford Encyclopedia of Philosophy)
- ^ Marenbon, John (2007). Medieval philosophy: an historical and philosophical introduction. Routledge. p. 137.
- ^ Leibniz's Influence on 19th Century Logic
- ^ Hurley, Patrick (2007). A Concise Introduction to Logic 10th edition. Wadsworth Publishing. p. 392.
- ^ Beth, Evert W.; "Semantic entailment and formal derivability", series: Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, Nieuwe Reeks, vol. 18, no. 13, Noord-Hollandsche Uitg. Mij., Amsterdam, 1955, pp. 309–42. Reprinted in Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969
- ^ a b Truth in Frege
- ^ a b c Russell's Use of Truth-Tables
- ^ Toida, Shunichi (2 August 2009). "Proof of Implications". CS381 Discrete Structures/Discrete Mathematics Web Course Material. Department Of Computer Science, Old Dominion University. http://www.cs.odu.edu/~toida/nerzic/content/logic/prop_logic/implications/implication_proof.html. Retrieved 10 March 2010.
- ^ a b c d e f g h i j k Hunter, Geoffrey (1971). Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Pres. ISBN 0-520-02356-0.
- 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.
|
|
|
|
Overview
|
|
Academic
areas |
|
|
Foundational
concepts |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Tautology Failed to parse (Missing texvc executable; please see math/README to configure.): \top
|
|
|
NAND Failed to parse (Missing texvc executable; please see math/README to configure.): \uparrow · Converse implication Failed to parse (Missing texvc executable; please see math/README to configure.): \leftarrow · Implication Failed to parse (Missing texvc executable; please see math/README to configure.): \rightarrow · OR Failed to parse (Missing texvc executable; please see math/README to configure.): \or
|
|
Negation Failed to parse (Missing texvc executable; please see math/README to configure.): \neg · XOR Failed to parse (Missing texvc executable; please see math/README to configure.): \oplus
· Biconditional Failed to parse (Missing texvc executable; please see math/README to configure.): \leftrightarrow
· Statement
|
|
NOR Failed to parse (Missing texvc executable; please see math/README to configure.): \downarrow · Nonimplication Failed to parse (Missing texvc executable; please see math/README to configure.): \nrightarrow · Converse nonimplication Failed to parse (Missing texvc executable; please see math/README to configure.): \nleftarrow · AND Failed to parse (Missing texvc executable; please see math/README to configure.): \and
|
|
Contradiction Failed to parse (Missing texvc executable; please see math/README to configure.): \bot
|
|
