Propositional Logic
Propositional logic is the study of the meanings of, and the inferential relationships that hold among, sentences based on the role that a specific class of logical operators called the propositional connectives have in determining those sentences’ truth or assertability conditions. As early as Aristotle it was observed that propositional connectives have a logical significance, and over many centuries piecemeal observations about some of their properties were made. But propositional logic per se did not emerge until the nineteenth century with the appreciation of the value of studying the behavior of propositional connectives in isolation of other operators.
For example, a variation of the famous canonical syllogism where A is the sentence “All men are mortal, and Socrates is a man”, and B is the sentence “Socrates is mortal” can give rise to a plurality of questions about the relationship between A and B. Whether B follows logically from A ought not depend, it is thought, on what words like “mortal” or “man” mean. But one could reasonably ask either of the questions,
Does B follow from A purely by virtue of the meaning of the words “and”, “is”, “are”, “all”, and “a”?
and
Does B follow from A purely by virtue of the meaning of the word “and”?
Intuitively, the answer to the first question is “yes”, and the answer to the second question is “no”.
The example suggests that there is a right way to ask the question, for surely B does follow logically from A. So when we want to ask if a sentence follows logically, we should attend to the role of all words such as “and”, “is”, “are”, “all”, and “a”. Consider, however, if C is the sentence “All men are mortal” and D is the sentence “Socrates is a man”, that C also follows from A, but the meanings of the words “is”, “are”, “all”, and “a” play no role in the intuitive verification of that fact. (Because A is just the sentence “C and D”, nothing beyond an understanding of the meaning of the word “and” is needed to see that A cannot be true without C also being true.) It seems significant that B and C not only each follow from A, but that they do so in different ways. The inference from A to C is not only simpler or more direct than the inference to B. In whatever sense B follows from A, so too does C, whereas there is a stricter sense in which C, but not B, follows from A: Although both B and C follow “logically” from A, the logical bond between C and A is stronger than that between B and A. This highlights the importance, not just of determinations about whether one sentence follows from another, but of what standard of logicality underwrites that determination.
Propositional logic is the study of just such a specification of a standard of logicality, wherein only the meanings of the propositional connectives (e.g., “and” in the example above, but not “is”, “all”, etc.) are considered in evaluating things such as the cogency of a deduction or a sentence’s truth conditions.
A sentential connective is a linguistic particle that binds sentences to create a new compound sentence or that inflects a single sentence to create a new sentence. Among the sentential connectives, a propositional connective has the characteristic feature that when the original sentences it operates on are (or express) propositions, the new sentence that results from its application also is (or expresses) a proposition. There are, as one would expect, many competing theories about what a proposition is, and propositional logic originated as a scientific discipline independent of that debate. For this reason, the precise demarcation of which linguistic particles qualify as propositional connectives is somewhat vague and even contentious. But the general heuristic is that a propositional connective must create from some original sentences a new sentence that makes a claim of the same order. Intuitively, because “A and B” is just an affirmation of the content of A and the content of B, and “not A” is just a denial of the content of A, “and” and “not” are serving as propositional connectives. “It is necessary that A”, on the other hand, is a claim not about the content of A but about the sentence A itself. Similarly, “A implies B” is a claim about the sentences A and B, that they stand in an implication relationship with one another, rather than a claim about the sort of thing that A and B themselves are claims about. For this reason, the necessity qualifier and the implication relation are typically not thought of as propositional connectives but as modal operators. The conditional operator in such expressions as “If A, then B” has not received a consensus: On some analyses, this has been treated as a propositional connective, but on others it cannot be.
In presenting propositional logic, we will not assume any particular theory of propositions. As we will see, the development of and plurality of systems of propositional logic can only be appreciated when no particular conception of proposition is in place. The only stipulations are that the connectives operate always on whole sentences and never on sub-sentential items like predicates or terms, and that they create sentences in the same evaluation class as the ones they operate on, never higher-order expressions about the sentences in that class.
- 1. Basic Framework
- 2. The Classical Interpretation
- 3. Non-Classical Interpretations
- Bibliography
- Academic Tools
- Other Internet Resources
- Related Entries
1. Basic Framework
The formal language of propositional logic consists of
“atomic” propositional variables,
-
Atomic propositional variables are formulas.
-
If
is a propositional connective, and A, B, C, … is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applying to A, B, C, … is a formula.
The result of applying
This recursive definition of the formulas of propositional logic justifies the use of the label “atomic” for the propositional variables: Every formula is built up stepwise from atoms through a finite application of propositional connectives. It can be helpful to think of the connectives as “propositional functions” that take propositions (denoted by formulas) as input and return propositions as output. The space of propositions is then given as the free algebra on the atomic formulas generated by these functions, and the specification of a proposition is given by the standard “composition of functions” notation. This terminology is not common, however, because the expression “propositional function” has a quite different use of high currency (see the entry on Bertrand Russell).
It is customary to indicate the specific connectives one is studying
with special characters, typically
2. The Classical Interpretation
The logical analysis of propositional formulas proceeds from an association of some meaning with the connectives, and there are several ways of doing this. Because the original motivation for studying propositional logic is the observation that some particles in natural language often behave like propositional connectives, a natural first move is to try to specify formal rules of inference or precise assertability conditions that capture or approximate the role that these natural language predicates serve in informal reasoning. Two of the earliest specifications were in terms of truth functions and in terms of axiomatic deduction systems. After considering these in turn, we will compare the more sophisticated specifications given by Gentzen’s calculi.
2.1 Truth-functionality
If
One sees that
input | ||||
---|---|---|---|---|
One immediately recognizes the impostors
The truth-functional analysis of propositional logic proceeds by
associating n-ary truth functions with the n-ary
propositional connectives. The classical case considered thus far,
where the truth value space is bivalent, admits a strikingly simple
analysis. Observe first that the functions
-
A is a classical propositional validity if it evaluates as T on every possible assignment of values to its atomic propositional variables;
-
A is classically satisfiable if it evaluates as T on at least one possible assignment of values to its atomic propositional variables (and is classically unsatisfiable otherwise);
-
A is a classical propositional consequence of B if on no assignment of values to the atoms that occur in A and B on which B, evaluates as T does A evaluate as F;
-
A is a classical propositional equivalent of B if A and B evaluate as T on precisely the same assignments of values to atoms.
In this way, the language of propositional logic restricted to the
connectives
-
interchange:
If A and B are equivalent, and A occurs as a subformula of , then the result of replacing an occurrence of A in with B is a formula that is equivalent to . -
substitution:
If A and and are any formulas whatsoever, then the result of replacing each occurrence of the propositional variable in and with A are formulas and with the properties: is valid if is; is unsatisfiable if is; is a consequence of if is a consequence of ; and are equivalent if and are. -
complementation:
is a classical validity (called the “law of excluded middle” (lem) in propositional logic). -
double complementation:
is equivalent to A. -
commutativity:
is equivalent to , and is equivalent to . -
associativity:
is equivalent to , and is equivalent to . -
distribution:
is equivalent to and
is equivalent to . -
De Morgan equivalence:
is equivalent to and
is equivalent to .
therefore apply to this language of “Boolean propositional formulas”.
2.1.1 Normal forms
Consider any other propositional connective denoted
input | |
---|---|
T | |
T | |
F | |
F | |
F | |
T | |
F | |
F |
There is a simple algorithm for constructing a Boolean formula that is
equivalent to
It is clear that this formula will evaluate as T on
all the rows that
Theorem 1. Any formula of propositional logic under the classical interpretation is equivalent to a disjunction of conjunctions of propositional variables and negated propositional variables.
Similar reasoning can be used to verify equivalence to a “conjunctive normal formula”, a conjunction of disjunctions of propositional variables and negated propositional variables.
2.1.2 Truth-functional completeness
One corollary of the DNF theorem is that Boolean logic—the
fragment of propositional logic with only the connectives
The idea of truth-functional completeness can be pressed further with
the simple observation that
2.1.3 Realization in switching circuits
More productive than reducing the number of connectives to the
smallest possible truth-functionally complete set, though, has been
the selection of connectives that convey the greatest perspicuity into
the structure of deductive inference. We have already indicated that
the Boolean connectives, by closely approximating the truth conditions
of the ordinary language particles “not”,
“and”, and “or”, provide a formal mechanism
for evaluating contentful human inference. Another merit of the
Boolean selection is its natural realization in the description of
relay and switching circuits. In 1940 Claude Shannon described an
interpretation of propositional logic in which sentence letters stand
for circuits: atomic circuits are nodes
Because of the simplicity of classical propositional logic,
Shannon’s thesis greatly facilitated circuit design.
Immediately, one sees that any circuit is equivalent to (i.e., opens
and closes under the same conditions as) a circuit described by a
disjunctive normal formula. Thus one could be given complex circuits
A, B, and C, connect A and B in series (
2.1.4 The material conditional
Another important feature of the classical interpretation is the
special role played by the binary truth function
What is more interesting is the thesis that
Of special interest is the suggestion, originally due to Frank Ramsey,
that expressions of the form “If A, then B” in the
indicative mood are best understood in terms of conditional
probabilities as “The probability of B given A is nearly certain
(
This example highlights again the delicacy of the problem of determining which connectives can be analyzed under the purview of propositional logic. On some interpretations (including the truth-functional one), indicative mood conditionals can be, but on Ramsey’s interpretation they cannot. In 1982, W. V. O. Quine anticipated Lewis’s result by expressing the caution, which he attributed to Philip Rhinelander, not to confuse the statement of a conditional “If A, then B” with the statement of B on condition A. The latter, he held, is typically the proper way of understanding an expression of the form “If A, then B”, which, because it is a non-statement in the absence of the condition A, cannot be understood as a proposition at all.
Gottlob Frege is often counted among the defenders of the material
conditional, but his attitude towards the connective is nuanced. His
systematization of propositional logic did feature a connective with
the truth conditions given by
Given the plurality of truth-functionally complete sets of
connectives, why would Frege or anyone else select the material
conditional as a primitive connective for classical logic? Frege saw
that the value of selecting the material conditional as a primitive
connective not from its approximation of ordinary language expression
but from its role internal to logical theory. Let us write
2.1.5 Decidability
A logic is said to be decidable if there is a reliable method for
determining whether a formula is satisfiable. Classical propositional
logic is readily seen to be decidable: Given an arbitrary formula,
simply enumerate in the tabular method used above each of the possible
sequences of truth values that can be input to its atomic
propositional variables, and compute the composition of functions on
each of these inputs. Because formulas are finite strings of symbols,
each contains only a finite number, say n, of atoms, so that
the truth-table will have exactly
2.1.6 NP-completeness
The problem of determining whether a formula of classical propositional logic is satisfiable is known as sat. Although decision procedures exists for sat, all known procedures for making this determination in a predetermined manner for every possible formula are in a precise sense tedious and inefficient: no procedure has been discovered which returns an answer after a number of computation steps polynomially bounded by the size of the formula one tests, i.e., it is unknown whether sat is in the complexity class P of problems solvable by a deterministic procedure in polynomial time. It is known that sat is in the complexity class NP—those questions that can be answered by a non-deterministic procedure in polynomial time. In 1971, Steven Cook proved that sat is “NP-complete”: any problem in the class NP is reducible in polynomial time to sat. A corollary of Cook’s theorem is that if sat is in the class P, then NP = P. It is generally believed that NP is a strictly larger class of problems than P and, for this reason, that no “efficient” procedure for solving sat in the sense of polynomial time computability exists. In the decades since Cook’s discovery, a wide range of problems have been shown to be NP-complete. But classical propositional logic figured prominently in the context of the discovery of NP-completeness. Its perspicuity was particularly suited to stage the concept’s formation.
2.1.7 Compactness
A fundamental fact about classical propositional logic is that it is
“compact”. To motivate the idea of compactness, consider
the set of formulas
The Compactness Theorem (Gödel 1930) tells us that this intuition is misleading:
Theorem 2. If each finite subset of
Notice that by “relaxing” the hypothesis from
“proper subset” to “finite subset”, the
Compactness Theorem is true and in fact trivial when
For a striking corollary of compactness, suppose that A is the
classical propositional consequence of the infinite set of formulas
2.2 Deduction
Formal deduction systems, introduced by Gottlob Frege in 1879, provide an alternative specification of the meanings of propositional connectives. Such systems are characterized by a finite set of formulas called axioms and a finite set of inference rules. The propositional axioms in Frege’s system are
The inference rules of are
-
modus ponens:
-
substitution: If
is an atomic variable in B, and C is any formula whatsoever, then let be the result of replacing every occurrence of with C, and from B infer .
A proof is defined as a finite sequence of formulas, each one of which
either is an axiom or follows from previous entries in the sequence by
an application of an inference rule. A theorem is a formula which
occurs as the final entry in a proof, and we denote the theoremhood of
a formula A by
and rules of inference
- Nicod’s inference:
- substitution: If
is an atomic variable in B, and C is any formula whatsoever, then let B’ be the result of replacing every occurrence of with C, and from B infer B’.
In parallel to the truth-functional framework for classical logic, one
can also introduce the notion of deduction from hypotheses: If
2.2.1 The Deduction Theorem
In 1910 Frege pointed out, but did not prove, that
The other direction is known as the Deduction Theorem. It’s
proof uses induction on the length of the
Theorem 3.
Proof. (base step) If there is a
one-line derivation of
is in the set is is an axiom
The following three
It is easy to check that each line of each derivation is either a
member of
(induction step) Assume that whenever there is
a
and
be examples of such derivations, and consider the sequence:
This is a
Because this verification of the Deduction Theorem depends only on the first two of Frege’s axioms, it applies also in many non-classical contexts including, importantly, a large class of constructive propositional logics.
2.2.2 Basic meta-theory
Another analogue to the evident facts from the truth-functional
framework, this time the DNF theorem, played a historical role in the
metatheoretical analysis of axiomatic systems. Hilbert showed how to
associate with every formula A a disjunctive normal formula
In particular, applying the Deduction Theorem, A and
Frege’s axiomatization obviously depends on the expressive
adequacy of the pair
The axiomatic framework with minimal signature (following Russell and
Whitehead, Hilbert used only
2.2.2.1 Consistency
An formal deductive system S is
consistent if for no formula A is
2.2.2.2 Maximality
A formal deductive system is maximal if any proper extension of it is inconsistent. Hilbert used the same interpretation from his consistency argument to show:
Theorem 4. cpc is maximal.
Proof. As above, a formula is provable only if it is constant
0 under the interpretation, which, in the case of a conjunctive normal
formula, occurs precisely when each of its conjuncts contains both a
negated and unnegated occurrence of some propositional variable. Now
let A be any unprovable formula. Its associated formula
Thus
Hilbert and others called this same property “completeness”, in analogy to the completeness axiom from Hilbert’s foundational studies of plane geometry and number theory. But as completeness has come to mean something else in the logical domain, this property is now commonly referred to as “Post-completeness” (after Post 1921 who rediscovered this property of cpc) or, as here, as “maximality”.
2.2.2.3 Completeness
The Completeness Theorem describes an exact correspondence between the truth-functional and deductive frameworks:
Theorem 5.
Proof. This result is often described as difficult to establish, but in Hilbert’s 1917 lectures, it is an immediate corollary of maximality. Already it was observed in the consistency argument that only formulas interpreted as constant 0 functions are provable. Suppose that some formula A were constant 0 but unprovable in cpc. Then the same consistency argument as before would carry through for cpc+A, contradicting the maximality result just proved. It follows that every formula interpreted as a constant 0 function is a theorem of cpc. The formulas interpreted as constant 0 functions are just the valid formulas on the classical truth-functional interpretation. ◻
A direct route to the Completeness Theorem is also possible. A famous proof from Kalmár 1935 begins with two observations:
- K1
-
- K2
- Let A be any formula with propositional variables
, , …, , and let be an assignment of truth values to propositional variables. Define if , if . Then if , .
Proof. Suppose now that T is a classical validity with
propositional variables
and
By the Deduction Theorem,
and
By K1,
Two applications of modus ponens yield
Repeating this same reasoning for
and after n repetitions
Proving completeness directly in this manner allows a different argument for maximality:
Proof. For suppose
2.2.2.4 Completeness as semi-decidability
The set of theorems of a formal deductive system can be seen to be
recursively enumerable. To construct a simple enumeration, let us add
to the language of propositional logic the symbol “;” as a
sequential location demarcator so that the language consists of
- Stage 1: list all strings of symbols of length 1 using only the
propositional variable
. - Stage 2: list all strings of symbols of length 1 or 2 using only
propositional variables
and . - ...
At each stage, the vocabulary is finite, so there are only finitely many strings of symbols to list. But every proof is a finite string of symbols and therefore gets listed at some stage or another. Therefore, given a formula A, one can begin searching for a proof one stage at a time, checking only finitely many strings at each stage. If A is valid, then by completeness it is provable, and one will discover a proof of it after examining some finite number of strings. On the other hand, if A is not valid, the search will never halt.
Completeness results are often described as valuable because they make evident the recursive enumerability of a logic’s validities. In the case of classical propositional logic, validity is already known to be recursively enumerable and even decidable by a much simpler and more efficient method of truth table evaluation. The Completeness Theorem’s value derives instead from the fact that two vastly different conceptions of logicality—formal provability and truth-functional validity—coincide. The situation is different with other logical systems. The most famous example is first-order classical quantification theory, which Church and Turing proved to be undecidable in 1936. Here, the Completeness Theorem of Gödel 1930 is especially insightful: the set of quantificational validities is not recursive, but it is at least recursively enumerable. In fact, the completeness results for classical propositional logic and quantification theory were the historical occasion for the clarification of the distinction between recursive and recursively enumerable sets—a distinction seen as elementary today but the source of considerable confusion in the first decades of the twentieth century.
Completeness results can play a role for many alternative systems of propositional logic similar to the one they play for classical quantification theory: Urquhart 1984 showed that the systems e and r of relevance logic are undecidable; Lincoln et al. 1992 showed that full propositional linear logic ll is undecidable. In these arenas, a complete formal derivation system can provide some concrete access to the space of valid formulas whose abstract definition is not otherwise readily navigable.
2.2.2.5 Independence
The style of reasoning exhibited in the consistency argument can be generalized to show independence results. The idea of the consistency argument was first to describe a property P such that
-
all the axioms have P, and
-
if an inference rule is applied to a formula with P, then the formula that results from its application also has P
and then to show that certain formulas do not have P. Because all theorems either are axioms or are generated from axioms by iterated applications of inference rules, those latter formulas cannot be theorems.
In the consistency proof, P is the property of being interpreted as a
constant 0 function, and the formulas that do not have P are the
negations of theorems. The reasoning can be generalized, though.
Suppose P were some other property that all but one of the axioms have
and that is similarly preserved by the inference rules. By verifying
this one could show that the one axiom is not derivable from the
others and therefore that the deductive system would have fewer
theorems without it. For example, the classical interpretation of
For a more interesting example, consider the interpretation of
A | B | |
---|---|---|
0 | 0 | 0 |
1 | 0 | 0 |
2 | 0 | 0 |
0 | 1 | 1 |
1 | 1 | 0 |
2 | 1 | 0 |
0 | 2 | 2 |
1 | 2 | 2 |
2 | 2 | 0 |
A | |
---|---|
0 | 2 |
1 | 2 |
2 | 0 |
If P is the property of being a constant 0 function on this interpretation, then one can verify that
-
axioms 1, 2, 3, and 4 each have P
-
P is preserved by modus ponens and substitution
-
axiom 5 evaluates as 1 on the input 1 and so does not have property P
and that axiom 5 is therefore independent of the first four axioms.
The use of non-classical (typically higher valence) truth-functional interpretations to define properties to be used in independence proofs dates back to Schröder 1890. It was pursued in full generality by Łukasiewicz, who also proved results about the scope of this technique.
2.3 Gentzen’s calculi
In 1934–35, Gerhard Gentzen introduced two alternative frameworks for presenting deductive inference that have led to particularly refined analyses of propositional logic. We will look first at Gentzen’s system of natural deduction and later consider his sequent calculus.
2.3.1 Natural deduction
In lectures from early 1920, David Hilbert remarked that a formal deduction system’s inference rules can be thought of as providing the meanings of the connectives they govern (Hilbert 2013: 323). Hilbert’s idea is given a profound realization in Gentzen’s natural deduction calculus. Natural deduction is an early and emblematic achievement in “proof-theoretic semantics”: the tradition of specifying definitions in inferential, rather than denotational, terms.
In systems like cpc the only inference rule
responsible specifically to a connective is modus ponens.
What would it mean for this rule not only to describe a deductively
valid pattern of inference but in fact to provide a definition of the
connective
Understood as a definition of
In Gentzen’s terminology, rules like modus ponens that describe the definitive way of reasoning from a sentence governed by a certain connective are called “elimination rules”. The Deduction Theorem, in describing the definitive pattern of reasoning whose conclusion is governed by a certain connective, is an example of an “introduction rule”. Gentzen wrote:
The introductions represent …the “definitions” of the symbols concerned, and the eliminations are no more, in the final analysis, than the consequences of these definitions. …By making these ideas more precise it should be possible to display the Elim-rules as unique functions of their corresponding Intro-rules. (1934–35: §II 5.13)
The precisification Gentzen foresaw is this: Elimination rules are not
“consequences” of their corresponding introduction rules;
neither are introduction rules “consequences” of their
corresponding elimination rules; but rules of the one type do follow
from the conception of their corresponding rules of the other type as
definitions. When conditionalization is understood as an operation
that maps
To take another example, consider the inferences
Gentzen’s system of natural deduction is a presentation of logic
in terms of an intro/elim pair of rules, related as are modus
ponens and the Deduction theorem, providing an inferential
definition of each logical particle. His natural deduction system of
propositional logic has such pairs of rules for the propositional
connectives
Notice the appearance of the arity-0 connective
Natural deduction proofs are trees constructed by iterating these
rules. When all the assumptions in such a proof are discharged by the
application of a rule, the formula in the tree’s single root
node is said to be proved; otherwise it is said to be derived from the
set of assumptions that remain open at leaf nodes. Let us write
Gentzen observed that the natural deduction calculus with intro/elim
pairs of rules for the connectives
This elementary inference that Chrysippus famously attributed to
hunting dogs cannot be justified by the inferential meaning of the
to derive the principle of excluded middle, one needs in addition the double negation rule
These rules can be used together with the introduction and elimination
rules for the propositional connectives to construct natural deduction
systems nd+
The distinction between classical and intuitionistic logic predates Gentzen’s work. But with its inferential definition of propositional connectives, natural deduction sheds new light on the distinction: classical, intuitionist, and other logicians can agree to the same definitions of the propositional connectives, the differences between their conceptions of logic having to do with the acceptability of principles like the law of excluded middle that are independent of the connectives’ meanings.
2.3.2 Sequent calculus
This same point is brought out in a different way in Gentzen’s
propositional sequent calculi. These calculi present logical inference
in the form of sequents: expressions of the form “
In the sequent calculi, these left/right rules for the propositional connectives function alongside another set of rules of structural reasoning. The classical calculus pk has seven:
A proof in pk is a finite branching tree built
from iterations of these logical and structural rules, each leaf node
of which is an basic sequent of the form
-
if, and only if, if, and only if, -
If one modifies pk by requiring the righthand side of the sequent arrow to have at most one formula and accordingly rewrites the
rule asthe resulting calculus pi is such that
if, and only if, if, and only if, , where ipc stands for Heyting’s formal deduction system for propositional intuitionistic logic and its equivalents. (Obviously the rules exchange(R) and contraction(R) play no role in pi and can be omitted.) -
Cut Elimination Theorem: If one modifies pk and pi simply by removing the rule “cut”, the resulting calculi pk- and pi- are such that
if, and only if, , and if, and only if, . -
All the formulas that appear anywhere in a pk- or pi- proof are subformulas of the formulas that appear in the endsequent. (This “subformula property” clearly does not hold of pk and pi proofs.)
Observation 2 provides yet another perspective on the way logicians
could disagree about the validity of principles like the law of
excluded middle without disagreeing about the meanings of the
propositional connectives. The treatment of
Observation 1 allows one immediately to conclude that pk is complete with respect to the classical truth functional interpretation of propositional logic. Gentzen did not draw this conclusion because he had a different understanding of completeness made possible by the sequent calculus: Because the rule “cut” can be shown to fully capture the general concept of logical consequence—something Gentzen took himself to have demonstrated in 1932—, observation 3, that “cut” is eliminable from pk, shows that the left/right rules for the propositional connectives are complete in the sense that no logical consequence of formulas provable with them is itself unprovable with them (see Franks 2010). This way of framing completeness has the further advantage that pi can be said to be complete in the same sense.
2.3.3 Constructive completeness of pk and of pi
Because of observation 4, however, it is possible to prove the completeness of pk in the usual sense very simply.
Proof. Let us call a sequent
Because of the invertibility of
As was mentioned, Gentzen did not present this very simple version of
the completeness theorem. Because he was interested in cut-elimination
as an expression of the completeness of his rules, he pursued that
instead, providing an elaborate proof transformation technique.
Knowledge of the completeness of pk-, though,
leads to an alternate verification of cut-elimination: Suppose
Reflection on the construction implicit in this completeness argument
in fact shows that an arbitrary formula can in this way be tested for
validity and therefore provides a new decision procedure for classical
logic: The end result of the construction will either be a proof or
will be a tree whose leaf nodes indicate how to construct a falsifying
interpretation for
A version of the same argument applies also to pi, not—of course—to show that it is complete with respect to its classical truth-functional interpretation, but to show that it is complete with respect to another sort of interpretation based on Kripke frames. The interesting thing about this approach to an analysis of intuitionistic logic is that one need not have in mind in advance what sort of interpretation one wants to show pi complete with respect to. Just setting out algorithmically to build a cut-free pi proof will either succeed or will indicate the sort of falsifying interpretation that applies in the intuitionistic case (see Takeuti 1987 [2013]).
3. Non-Classical Interpretations
Classical propositional logic is evidently a valuable framework not only for organizing principles of reasoning but for providing a fairly simple setting for showcasing basic theoretical phenomena such as completeness, formal consistency, axiomatic independence, and the like. But a considerable measure of the value of its systematic development lies in the indications, along the way, of ways to deviate from the classical framework and devise alternative interpretations of the propositional connectives. We have touched on a few indications already: the independence of the principle of excluded middle from the other axioms in Frege’s formal deduction system, the implausibility of the material conditional as an analysis of the truth conditions of ordinary indicative mood “if …then” statements, etc. Here we survey some of the most prevalent alternative systems of propositional logic.
3.1 Multi-valued logics
Already we indicated how truth-functional interpretations with valence
greater than 2 can be utilized to provide independence proofs for
axiom systems. Gödel (1932) defined a sequence
with
Beyond such utilitarian roles, multi-valued logics have attracted interest in their own right. Important examples are the (strong and weak) Kleene 3-valued logics, which are meant to assign truth values to propositions about partial recursive functions. Other 3-valued logics have been proposed as improvements on the material conditional as interpretations of indicative mood conditionals (see Cobreros et al 2014). 4-valued logics have been used to model computation on databases containing conflicting information—here the values correspond with the information states “true”, “false”, “both”, and “neither” (see Belnap 1977). Graham Priest 1992 has applied the same framework in the development of a system of relevance logic, again offering an improved formalization of conditional language.
Another important class of multi-valued logics are the infinitely-valued “fuzzy logics”. These have been used in order to provide an analysis of propositions with vague terms, which can be thought of as admitting degrees of truth.
3.2 Constructive logics
We have already noted that simply rejecting the lem leads to a subtle deviation from the classical interpretation: The classical truth functional interpretation falls away, but the inferential definition of the connectives evident in natural deduction can be preserved. The intuitionistic propositional calculus ipc has been studied in great depth. Among its prominent features are:
1. The “disjunction property”: the fact that
At one time it was conjectured that ipc can be characterized as the strongest propositional logic with the disjunction property (an example of a weaker logic is Johansson’s mpc, corresponding to the pure system of natural deduction nd). In 1957, Kreisel and Putnam studied the “independence of premises (IndPrem)” inference
and observed that
although the logic kp = ipc+IndPrem also has the disjunction property. Today it is known that there are infinitely many distinct logical systems intermediate in strength between ipc and cpc, and that infinitely many of them have the disjunction property.
2. The failure of truth-functionality: The intuitive understanding of intuitionism is to replace the idealistic concept of truth with the notion of having been constructively verified. Some authors suggested that in the propositional case, this might lead to a 3-valued logic: one value indicating that a statement was constructively verified, another value indicating that it had been constructively refuted, and a third value indicating that neither of these is the case. This seems at least to accord with ipc’s rejection of lem. However, because there are only a small number of 3-valued semantic environments, others were able to rule out this possibility case-by case. This led to speculation that the right semantics might have valence 4 or possibly 5. Gödel’s 1932 proof rules out all truth-functional interpretations of any finite valence.
Because of the failure of truth-functionality, a new framework for understanding ipc validity is needed. Adequate topological, algebraic, and Kripke-frame semantics have been introduced, and completeness results demonstrating a correspondence between these frameworks and various proof systems abound. We have already indicated that the completeness argument for the intuitionistic sequent calculus pi with respect to Kripke frames is a variation of the simple constructive completeness theorem for pk with respect to the classical theory of truth. Again, the argument shows that pi is decidable: Given a formula A, the algorithm either returns a pi-proof of A or a falsifying Kripke frame.
There is also an informal, intuitive understanding of ipc
theoremhood called the BHK interpretation.
According to this interpretation, the disjunction property is a formal
analogue of the definition of the
Because the BHK interpretation specifies, not what expressions like
3. A striking feature of ipc is the presence of inference rules like IndPrem that are not derivable
but that nevertheless preserve the property of ipc-provability. Other examples of such rules are
Is it right to say that such rules are valid patterns of intuitionistic inference? The question is ambiguous in a way that experience with classical logic desensitizes one to. For it can be shown that any rule that preserves the property of being a classical validity is also derivable in cpc itself. The fact that the rules under whose application the set of ipc theorems is closed properly extends the ipc-derivable rules leads to a new concept: the former rules are called “admissible”. The intuitionsitic study of propositional logic thereby reveals a fundamental distinction in the basic concept of deductive validity, between a rule licensing legitimate inferences from theorems and it applying also to arbitrary hypotheses.
Because the primitive understanding of logical connectives from the intuitionist perspective is in terms of the conditions of the provability of statements containing them, one might, and many authors have, maintained that admissibility is the proper precisification of the concept of deductive validity for ipc. On the other hand, what distinguishes ipc from mpc is the derivability of the rule ex falso quodlibet. That rule (as well as the disjunctive syllogism) is admissible already in mpc, so the decision to include it explicitly as a derivable inference in ipc indicates some recognition of the importance of derivability. What can be said definitely is that the distinction between derivability and admissibility is important in constructive logics in a way that it is not in cpc.
4. Three of the De Morgan inferences are derivable in ipc,
but the inference
5. We have observed how the Gentzen calculi highlight certain relationships between ipc and cpc. Translation schemes of Kolmogorov, Glivenko, Gödel, and Gentzen make evident other relationships between these and other systems. We begin with a result of Valérii Glivenko (1929):
Theorem 6. If
Proof. First observe three simple facts about nd+
For the proof of the main theorem, suppose
By
V1,
there exist nd+
From these pieces one can construct a nd+
That completes the proof of the main theorem. ◻
We observe two corollaries:
- V4
- If
, then .This follows immediately from the main theorem and V3.
- V5
- cpc is inconsistent only if ipc
is.
For if cpc is inconsistent, then there is a formula
such that and . But then and .
Glivenko’s theorem provides a simple translation
-
is , for all propositional variables -
is -
is -
is -
is
The Gödel/Gentzen (1933) translation
-
is , for all propositional variables -
is -
is -
is -
is
It is easy to show that
In 1933b, Gödel provided similar translation from ipc
to the modal logic S4.
S4 is cpc
supplemented with a new primitive symbol
and three new axioms
Gödel defined a translation
and stated, without proof:
Gödel further declared both that “the translation of
(*) and (**) together obviously entail the disjunction property for ipc.
3.3 Relevance and connexive logics
Returning to the problem of approximating natural language
expressions, some writers have proposed overcoming the apparent
inadequacies of the material conditional by stipulating stronger
conditions on the truth of propositions of the form
Connexive logicians aim instead to make good of the intuition that for
a conditional statement to be true, the negation of its consequent
should be incompatible with its antecedent. This requirement on the
truth of conditional statements has a formidable history, appearing in
logical manuscripts of the Stoic philosophers Chrysippus and Sextus
Empiricus and evidently garnering more support at the time than the
contrary opinion of Philo of Melaga. A related idea appears already in
the Prior Analytics, where Aristotle claimed that it is
impossible that if not A, then A. This, “Aristotle’s
thesis”, can be formalized as
By including as theorems principles that are classically invalid, such
logics risk trivialization because of the maximality of cpc.
Some approaches address this problem by
rejecting classical principles such as the
3.4 Linear logic
If many departures from the classical framework are motivated by wanting to study connectives that more closely approximate the truth conditions of ordinary language expressions, linear logic (introduced in Girard 1987) can be thought of as a push in the opposite direction. Just as Frege saw logical significance in the material conditional despite (maybe even because of) its lack of correspondence with ordinary “if …then” statements for reasons internal to logical theory, linear logic can be thought of as an attempt to discover in the fine structure of formal logic those propositional connectives that play specific inference-tracking roles that ordinary expressions might be too crude to articulate.
We saw earlier how in the sequent calculus classical and intuitionistic logic differ not in the inference rules governing the propositional connectives but in the background structure of reasoning—specifically, in the presence or absence of multiple formulas in succedents. Linear logic analyzes this relationship further through adjustments to other structural aspects of reasoning. It is well known that the operational rules of pk can be written either in a “context-sharing” or “context-independent” form. The operational rules were given a context-sharing presentation above, but for example the rule
could instead be given a context-independent presentation:
The equivalence of these presentations is easy to verify:
but we see that their equivalence depends on the presence of the structural rules thinning and contraction.
In propositional linear logic, there are two conjunction-like
operators,
Disambiguating the logical conjunction and disjunction into additive
and multiplicative versions lends great perspicuity to the
relationship between classical and intuitionistic logic. For example,
there are two versions of lem. The additive
version
In the absence of contraction and weakening, formulas of linear logic
stand for something more like resources than permanent statements or
constructions. Just as intuitionistic logic replaced the classical
understanding of a conditional
The fragment of linear logic presented so far is called mall (for multiplicative/additive linear logic). In order to preserve its distinctive properties but also be able to express claims interpretable as, for example, the intuitionistic implication, the linear modalities are introduced. These are unary connectives for which restricted forms of weakening and contraction apply. They are called “modalities” for a reason, though: They are governed by the same left and right rules as the necessity and possibility operators of modal logic S4. This makes it unclear whether full linear logic ll with their inclusion qualifies as a propositional logic.
This is no fault of linear logic, but rather one of its main contributions to the study of propositions. As stressed in the introduction to this article, a helpful attitude for the development of propositional logic is to bracket questions about the nature of propositions and simply require that the propositional connectives return expressions of the same order as those they operate on. From this perspective, the idea of “persistent factual truth” or “reusable construction”, which is the basic starting point of classical and intuitionistic logic, is related to linear logic’s basic unit of “limited resource” just as the modalities “necessary truth” and “possible truth” are related to the category of “persistent factual truth” or “reusable construction”.
Bibliography
References
- Belnap, Nuel D., 1977, “A Useful Four-Valued Logic”, in Modern Uses of Multiple-Valued Logic, J. Michael Dunn and George Epstein (eds.), Dordrecht/Boston: D. Reidel, 5–37. doi:10.1007/978-94-010-1161-7_2
- Bernays, Paul, 1926, “Axiomatische Untersuchung des Aussagen-Kalkuls der Principia Mathematica”, Mathematische Zeitschrift, 25: 305–320. doi:10.1007/BF01283841
- Cook, Stephen A., 1971, “The Complexity of Theorem-Proving Procedures”, in Proceedings of the Third Annual ACM Symposium on Theory of Computing, New York: ACM Press, 151–158. doi:10.1145/800157.805047
- Cobreros, Pablo, Paul Égré, David Ripley, and Robert van Rooij, 2014, “Foreword: Three-Valued Logics and Their Applications”, Journal of Applied Non-Classical Logics, 24(1–2): 1–11. doi:10.1080/11663081.2014.909631
- Church, Alonzo, 1936, “An Unsolvable Problem of Elementary Number Theory”, American Journal of Mathematics, 58(2): 345–353. doi:10.2307/2371045
- Edgington, Dorothy, 1995, “On Conditionals”, Mind, 104(414): 235–329. doi:10.1093/mind/104.414.235
- Franks, Curtis, 2010, “Cut as Consequence”, History and Philosophy of Logic, 31(4): 349–379. doi:10.1080/01445340.2010.522365
- –––, 2021, “The Deduction Theorem (Before and After Herbrand)”, History and Philosophy of Logic, 42(2): 129–159. doi:10.1080/01445340.2021.1889117
- Frege, Gottlob, 1879, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Halle: L. Nebert. Translated as Conceptual Notation: a formula language of pure thought modeled upon the formula language of arithmetic in Frege 1972:: 101–208.
- –––, 1910 [1980], “Letter to Jourdain”, translated and reprinted in his Philosophical and Mathematical Correspondence, G. Gabriel, et al. (eds.), Chicago: University of Chicago Press, 1980.
- –––, 1972, Conceptual Notation, and Related Articles, Terrell Ward Bynum (trans.), Oxford: Clarendon Press.
- Gentzen, Gerhard, 1932, “Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen”, Mathematische Annalen 107: 329–50. Translated as “On the Existence of Independent Axiomsystems for Infinite Sentence Systems”, in Gentzen 1969: 29–52. doi:10.1007/BF01448897 (de)
- –––, 1934–35, “Untersuchungen über das logische Schließen”, Gentzen’s doctoral thesis at the University of Göttingen, translated as “Investigations into Logical Deduction”, in Gentzen 1969: 68–131.
- –––, 1969, The Collected Papers of Gerhard Gentzen, M. E. Szabo (ed.), (Studies in Logic and the Foundations of Mathematics 55), Amsterdam: North-Holland.
- Girard, Jean-Yves, 1987, “Linear Logic”, Theoretical Computer Science, 50(1): 1–101. doi:10.1016/0304-3975(87)90045-4
- Glivenko, Valéry, 1929, “Sur quelques points de la logique de M. Brouwer”, Académie royale de Belgique, Bulletin de la classe des sciences, series 5, 15: 183–188.
- Gödel, Kurt, 1930 [1986], “Die Vollständigkeit der Axiome des logischen Funktionenkalküls”, Monatshefte für Mathematik und Physik, 37: 349–360. Translated by S. Bauer-Mengelberg as “The completeness of the axioms of the functional calculus of logic” reprinted in Gödel 1986: 102–23. doi:10.1007/BF01696781
- –––, 1932 [1986], “Zum intuitionistischen Aussagenkalkül”, Anzeiger der Akademie der Wissenschaftischen in Wien, 69: 65–66. Translated by J. Dawson as “On the intuitionistic propositional calculus”, in Gödel 1986: 223–25.
- –––, 1933a [1986], “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse eines mathematischen Kolloquiums, 4: 39–40. Translated as “An Interpretation of the Intuitionistic Propositional Calculus”, in Gödel 1986: 301–302.
- –––, 1933b [1986], “Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38. Translated as “On Intuitionistic Arithmetic and Number Theory”, in Gödel 1986: 287–295.
- –––, 1986, Collected Works, Volume I: Publications 1929–1936, Solomon Feferman, John W. Dawson Jr, Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jean van Heijenoort (eds.), Oxford/New York: Clarendon Press.
- Herbrand, Jacques, 1930, Recherches sur la théorie de la démonstration, Herbrand’s doctoral thesis at the University of Paris. Translated by W. Goldfarb, except pp. 133–88 translated by B. Dreben and J. van Heijenoort, as “Investigations in proof theory” in Herbrand 1968 [1971: 44–202].
- –––, 1968 [1971], Écrits Logigues, Jean van Heijenoort (ed.), (Bibliothèque de Philosophie Contemporaine. Logique et Philosophie Des Sciences), Paris: Presses universitaires de France. Translated as Logical Writings, Warren D. Goldfarb (trans.), Dordrecht, Holland: D. Reidel, 1971.
- Hilbert, David, 2013, David Hilbert’s Lectures on the Foundations of Arithmetic and Logic 1917–1933 (David Hilbert’s Lectures on the Foundations of Mathematics and Physics, 1891–1933, vol. 3), William Ewald and Wilfried Sieg (eds.), Berlin, Heidelberg: Springer Berlin Heidelberg. doi:10.1007/978-3-540-69444-1
- Hilbert, David and W. Ackermann, 1928, Grundzüge der theoretischen Logik, (Die Grundlehren der mathematischen Wissenschaften 27), Berlin: J. Springer.
- Johansson, Ingebrigt, 1937, “Der Minimalkalkül, ein reduzierter Intuitionistischer Formalismus”, Compositio Mathematica, 4: 119–136. [Johansson 1937 available online]
- Kalmár, László, 1935, “Über die Axiomatisierbarkeit des Aussagenkalküls”, Acta Scientiarum Mathematicarum, 7(4): 222–43.
- Kolmogorov [Kolmogoroff], Andrey N., 1925 [1967], “О принцип tertium non datur”, Matematicheskii Sbornik, 32(4): 646–667. Translated as “On the Principle of Excluded Middle”, in From Frege to Gödel A Source Book in Mathematical Logic, 1879–1931, Jean van Heijenoort (ed.), Cambridge, MA: Harvard University Press, 1967, 416–437.
- Kreisel, Georg and Hilary Putnam, 1957, “Eine Unableitbarkeitsbeweismethode für den Intuitionistischen Aussagenkalkül”, Archiv für Mathematische Logik und Grundlagenforschung, 3(3–4): 74–78. doi:10.1007/BF01988049
- Lewis, David, 1976, “Probabilities of Conditionals and Conditional Probabilities”, The Philosophical Review, 85(3): 297–315. doi:10.2307/2184045
- Lincoln, Patrick, John Mitchell, Andre Scedrov, and Natarajan Shankar, 1992, “Decision Problems for Propositional Linear Logic”, Annals of Pure and Applied Logic, 56(1–3): 239–311. doi:10.1016/0168-0072(92)90075-B
- Nicod, J. G. P., 1917, “A Reduction in the Number of Primitive Propositions of Logic”, Proceedings of the Cambridge Philosophical Society, 19: 32–41.
- Post, Emil L., 1921, “Introduction to a General Theory of Elementary Propositions”, American Journal of Mathematics, 43(3): 163–185. doi:10.2307/2370324
- Priest, Graham, 1992, “What is a non-normal world?”, Logique & Analyse, 139–140: 291–302.
- Prucnal, Tadeusz, 1976, “Structural Completeness of Medvedev’s Propositional Calculus”, Reports on Mathematical Logic, 6: 103–105.
- Quine, W. V. O., 1955, “A Way to Simplify Truth Functions”, The American Mathematical Monthly, 62(9): 627–631. doi:10.1080/00029890.1955.11988710
- –––, 1982, Methods of Logic, fourth edition, Cambridge, MA: Harvard University Press.
- Samson, E. and B. Mills, 1954, “Circuit minimization: algebra and algorithms for new Boolean canonical expressions”, Technical Report 54–21, Air Force Cambridge Research Center.
- Schröder, Ernst, 1890, Vorlesungen über die Algebra der Logik (exakte Logik), volume 1, Leipzig: B. G. Teubner. Reprinted 1966, New York: Chelsea.
- Shannon, Claude Elwood, 1940, “A Symbolic Analysis of Relay and Switching Circuits”, Thesis (M.S.), Massachusetts Institute of Technology, Dept. of Electrical Engineering. [Shannon 1940 available online]
- Sheffer, Henry Maurice, 1913, “A Set of Five Independent Postulates for Boolean Algebras, with Application to Logical Constants”, Transactions of the American Mathematical Society, 14(4): 481–488. doi:10.1090/S0002-9947-1913-1500960-1
- Sorbi, Andrea, 1991, “Some Quotient Lattices of the Medvedev Lattice”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 37(9–12): 167–182. doi:10.1002/malq.19910370905
- Takeuti, Gaisi, 1987 [2013], Proof Theory, second edition, (Studies in Logic and the Foundations of Mathematics 81), Amsterdam/New York: North-Holland. Reprinted New York: Dover, 2013.
- Tarski, Alfred, 1933, “Einige Betrachtungen über die Begriffe der ω-Widerspruchsfreiheit und der ω-Vollständigkeit”, Monatshefte für Mathematik und Physik, 40(1): 97–112. doi:10.1007/BF01708855
- Troelstra, A. S. and D. van Dalen, 1988, Constructivism in Mathematics, Volume 1: An Introduction, (Studies in Logic and the Foundations of Mathematics 121), Amsterdam: North-Holland.
- Turing, A. M., 1936, “On Computable Numbers, with an Application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society, series 2, 42(1): 230–265. doi:10.1112/plms/s2-42.1.230
- Urquhart, Alasdair, 1984, “The Undecidability of Entailment and Relevant Implication”, Journal of Symbolic Logic, 49(4): 1059–1073. doi:10.2307/2274261
- Whitehead, Alfred North and Bertrand Russell, 1925–27, Principia Mathematica, Volumes 1, 2 and 3, 2nd Edition, Cambridge: Cambridge University Press.
More Readings
Most textbooks treat propositional logic as an elementary step en route to quantification theory or another more general topic. A notable exception is:
- Schechter, Eric, 2005, Classical and Nonclassical Logics: An Introduction to the Mathematics of Propositions, N.J: Princeton University Press.
Another sensitive treatment of propositional logic with attention to non-classical interpretations is:
- Gamut, L. T. F., 1990, Logic, Language, and Meaning, Volume 1: Introduction to Logic, Chicago, IL: University of Chicago Press. Translation of Logica, taal en betekenis I: inleiding in de logica, Utrecht: Het Spectrum, 1982. (L. T. F. Gamut is a collective name for Johan van Benthem, J. A. G. Groenendijk, D. H. J. de Jongh, M. J. B. Stokhof, and H. J. Verkuyl.)
Among standard textbook treatments, standout presentations of propositional logic can be found in Quine 1982 and in:
- Buss, Samuel R., 1998, “An Introduction to Proof Theory”, in Handbook of Proof Theory, Samuel R. Buss (ed.), (Studies in Logic and the Foundations of Mathematics 137), Amsterdam: Elsevier, 1–78. doi:10.1016/S0049-237X(98)80016-5
- Kleene, Stephen Cole, 1952, Introduction to Metamathematics, (The University Series in Higher Mathematics), New York: Van Nostrand.
- Mendelson, Elliott, 2015, Introduction to Mathematical Logic, sixth edition, (Textbooks in Mathematics), Boca Raton, FL: CRC Press.
- Von Plato, Jan, 2013, Elements of Logical Reasoning, Cambridge/New York: Cambridge University Press. doi:10.1017/CBO9781139567862
An excellent presentation of the rapid historical development of the subject in the early twentieth century is:
- Mancosu, Paolo, Richard Zach, and Calixto Badesa, 2009, “The Development of Mathematical Logic from Russell to Tarski, 1900–1935”, in The Development of Modern Logic, Leila Haaparanta (ed.), Oxford/New York: Oxford University Press, 318–470. doi:10.1093/acprof:oso/9780195137316.003.0029
Academic Tools
How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.
Other Internet Resources
[Please contact the author with suggestions.]