Propositional Logic

First published Thu May 18, 2023

Propositional logic is the study of the meanings of, and theinferential relationships that hold among, sentences based on the rolethat a specific class of logical operators called the propositionalconnectives have in determining those sentences’ truth orassertability conditions. As early as Aristotle it was observed thatpropositional connectives have a logical significance, and over manycenturies piecemeal observations about some of their properties weremade. But propositional logicper se did not emerge until thenineteenth century with the appreciation of the value of studying thebehavior of propositional connectives in isolation of otheroperators.

For example, a variation of the famous canonical syllogism where A isthe sentence “All men are mortal, and Socrates is a man”,and B is the sentence “Socrates is mortal” can give riseto a plurality of questions about the relationship between A and B.Whether B follows logically from A ought not depend, it is thought, onwhat words like “mortal” or “man” mean. Butone 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 asentence follows logically, we should attend to the role of all wordssuch as “and”, “is”, “are”,“all”, and “a”. Consider, however, if C is thesentence “All men are mortal” and D is the sentence“Socrates is a man”, that C also follows from A, but themeanings of the words “is”, “are”,“all”, and “a” play no role in the intuitiveverification of that fact. (Because A is just the sentence “Cand D”, nothing beyond an understanding of the meaning of theword “and” is needed to see that A cannot be true withoutC also being true.) It seems significant that B and C not only eachfollow from A, but that they do so in different ways. The inferencefrom A to C is not only simpler or more direct than the inference toB. In whatever sense B follows from A, so too does C, whereas there isa stricter sense in which C, but not B, follows from A: Although bothB and C follow “logically” from A, the logical bondbetween C and A is stronger than that between B and A. This highlightsthe importance, not just of determinations about whether one sentencefollows from another, but of what standard of logicality underwritesthat determination.

Propositional logic is the study of just such a specification of astandard of logicality, wherein only the meanings of the propositionalconnectives (e.g., “and” in the example above, but not“is”, “all”, etc.) are considered inevaluating things such as the cogency of a deduction or asentence’s truth conditions.

A sentential connective is a linguistic particle that binds sentencesto create a new compound sentence or that inflects a single sentenceto create a new sentence. Among the sentential connectives, apropositional connective has the characteristic feature that when theoriginal sentences it operates on are (or express) propositions, thenew sentence that results from its application also is (or expresses)a proposition. There are, as one would expect, many competing theoriesabout what a proposition is, and propositional logic originated as ascientific discipline independent of that debate. For this reason, theprecise demarcation of which linguistic particles qualify aspropositional connectives is somewhat vague and even contentious. Butthe general heuristic is that a propositional connective must createfrom some original sentences a new sentence that makes a claim of thesame order. Intuitively, because “A and B” is just anaffirmation of the content of A and the content of B, and “notA” is just a denial of the content of A, “and” and“not” are serving as propositional connectives. “Itis necessary that A”, on the other hand, is a claim not aboutthe content of A but about the sentence A itself. Similarly, “Aimplies B” is a claim about the sentences A and B, that theystand in an implication relationship with one another, rather than aclaim about the sort of thing that A and B themselves are claimsabout. For this reason, the necessity qualifier and the implicationrelation are typically not thought of as propositional connectives butas modal operators. The conditional operator in such expressions as“If A, then B” has not received a consensus: On someanalyses, this has been treated as a propositional connective, but onothers it cannot be.

In presenting propositional logic, we will not assume any particulartheory of propositions. As we will see, the development of andplurality of systems of propositional logic can only be appreciatedwhen no particular conception of proposition is in place. The onlystipulations are that the connectives operate always on wholesentences and never on sub-sentential items like predicates or terms,and that they create sentences in the same evaluation class as theones they operate on, never higher-order expressions about thesentences in that class.

1. Basic Framework

The formal language of propositional logic consists of“atomic” propositional variables, $p_1$, $p_2$,$p_3$, …, and propositional connectives, $c_1^1$,$c_2^1$, $c_3^1$, …, $c_1^2$, $c_2^2$, $c_3^2$,…, $c_1^3$, …. The expressions’ subscripts areused to distinguish them from one another; the fact that we usenatural numbers indicates the typical convention that the vocabularybe countable. The propositional connectives’ superscriptsindicate their “arity”, i.e., the number of propositionsthat they operate on in order to create a new proposition. Theformulas of propositional logic are defined recursively by

Atomic propositional variables are formulas.
If $c_n^m$ is a propositional connective, and $\langle$A, B, C,…$\rangle$ is a sequence ofm, possibly but notnecessarily atomic, possibly but not necessarily distinct, formulas,then the result of applying $c_n^m$ to $\langle$A, B, C,…$\rangle$ is a formula.

The result of applying $c_n^m$ to $\langle$A, B, C,…$\rangle$ is customarily written in functional notation:$c_n^m$(A, B, C, …). Examples of formulas are

$p_4$
$c_1^2(p_7, p_3)$
$c_2^2(c_1^1(p_1), c_1^1(c_1^2(p_2, p_3)))$
$c_5^3(p_2, c_3^2(c_4^1(c_6^2(p_3, p_3)), p_5),c_9^1(p_2))$

This recursive definition of the formulas of propositional logicjustifies the use of the label “atomic” for thepropositional variables: Every formula is built up stepwise from atomsthrough a finite application of propositional connectives. It can behelpful to think of the connectives as “propositionalfunctions” that take propositions (denoted by formulas) as inputand return propositions as output. The space of propositions is thengiven as the free algebra on the atomic formulas generated by thesefunctions, and the specification of a proposition is given by thestandard “composition of functions” notation. Thisterminology is not common, however, because the expression“propositional function” has a quite different use of highcurrency (see the entry onBertrand Russell).

It is customary to indicate the specific connectives one is studyingwith special characters, typically $\wedge$, $\vee$, $\supset$,$\neg$, to use infix notation for binary connectives, and to displayparentheses only when there would otherwise be ambiguity. It is alsocommon to investigate properties of propositional formulas that do notdepend on the occurrence of atoms fundamentally, in which caseformula variables A, B, C, etc. appear in the expression in place ofsentence letters. Thus if $c_1^1$ is relabeled $\neg$, $c_1^2$is relabeled $\wedge$, and $c_2^2$ is relabeled $\vee$, then inplace of thethird formula listed above one would write $\neg\rA\vee\neg(\rB\wedge\rC)$.

2. The Classical Interpretation

The logical analysis of propositional formulas proceeds from anassociation of some meaning with the connectives, and there areseveral ways of doing this. Because the original motivation forstudying propositional logic is the observation that some particles innatural language often behave like propositional connectives, anatural first move is to try to specify formal rules of inference orprecise assertability conditions that capture or approximate the rolethat these natural language predicates serve in informal reasoning.Two of the earliest specifications were in terms of truth functionsand in terms of axiomatic deduction systems. After considering thesein turn, we will compare the more sophisticated specifications givenby Gentzen’s calculi.

2.1 Truth-functionality

If $\calV$ is a set of truth values, a function$\calV^n\longrightarrow\calV$ mappingn-tuples of truthvalues to truth values is called ann-ary truth function. Thenumber of values in $\calV$ is called the valence of the functionspace. In the bivalent case, the truth values are denoted $\bT$ and$\bF$, and one has the classical theory of truth. Observe that inthis classical function space are two 0-ary truth functions which,following the conventions on indices for propositional connectives wecould denote $f_1^0$ and $f_2^0$, but are conventionally denoted$\top$ and $\bot$, defined by $\top=\bT$ and $\bot=\bF$, andfour unary truth functions defined by

\[\begin{aligned}f_1^1(\bT)&=f_1^1(\bF)=\bT,\\f_2^1(\bT) &=\bT, \\f_2^1(\bF) &=\bF, \\f_3^1(\bT) &=\bF, \\f_3^1(\bF) &=\bT, \\f_4^1(\bT) &=f_4^1(\bF)=\bF. \\\end{aligned}\]

One sees that $f_1^1$ performs no operation on its input and isessentially the same as $\top$. $f_4^1$ is similarly an impostor:$\bot$ dressed up as a unary function. One can quickly check thatthe number ofn-ary truth functions is $2^{2^n}$—therebeing 2 possible output values on each of the $2^n$ possiblen-tuples of input values, and that at each stage, a number oftruth functions are impostors from lower arity. A case of specialinterest are the sixteen binary truth functions, which one can fullyindividuate by specifying their range on the 4 possible inputvalues:

input	$\langle\bT, \bT\rangle$	$\langle\bT, \bF\rangle$	$\langle\bF, \bT\rangle$	$\langle\bF, \bF\rangle$
$f_1^2$	$\bT$	$\bT$	$\bT$	$\bT$
$f_2^2$	$\bT$	$\bT$	$\bT$	$\bF$
$f_3^2$	$\bT$	$\bT$	$\bF$	$\bT$
$f_4^2$	$\bT$	$\bT$	$\bF$	$\bF$
$f_5^2$	$\bT$	$\bF$	$\bT$	$\bT$
$f_6^2$	$\bT$	$\bF$	$\bT$	$\bF$
$f_7^2$	$\bT$	$\bF$	$\bF$	$\bT$
$f_8^2$	$\bT$	$\bF$	$\bF$	$\bF$
$f_9^2$	$\bF$	$\bT$	$\bT$	$\bT$
$f_{10}^2$	$\bF$	$\bT$	$\bT$	$\bF$
$f_{11}^2$	$\bF$	$\bT$	$\bF$	$\bT$
$f_{12}^2$	$\bF$	$\bT$	$\bF$	$\bF$
$f_{13}^2$	$\bF$	$\bF$	$\bT$	$\bT$
$f_{14}^2$	$\bF$	$\bF$	$\bT$	$\bF$
$f_{15}^2$	$\bF$	$\bF$	$\bF$	$\bT$
$f_{16}^2$	$\bF$	$\bF$	$\bF$	$\bF$

One immediately recognizes the impostors $f_1^2 = \top$, $f_4^2 =f_2^1$ acting on the first input value, $f_6^2 = f_2^1$ acting onthe second input value, $f_{11}^2 = f_3^1$ acting on the secondinput value, $f_{13}^2 = f_3^1$ action on the first value, and$f_{16}^2 = \bot$, leaving ten essentially new binary truthfunctions.

The truth-functional analysis of propositional logic proceeds byassociatingn-ary truth functions with then-arypropositional connectives. The classical case considered thus far,where the truth value space is bivalent, admits a strikingly simpleanalysis. Observe first that the functions $f_1^3$, $f_2^2$, and$f_2^8$ approximate the truth conditions of some uses of the naturallanguage particles “not”, “or”, and“and” (another use of the particle “or” isarguably approximated by $f_2^7$). Thus if we associate thesefunctions with the three connectives labeled earlier $\neg$,$\vee$, and $\wedge$, we could compute the truth value of complexformulas such as $\neg\rA\vee\neg(\rB\wedge\rC)$ given differentpossible assignments of truth values to the sentence letters A, B, andC, according to the composition of functions indicated in theformula’s propositional structure. One can check that thisformula takes the valueF precisely when each of A,B, and C is assignedT and takes the valueT otherwise. Under this interpretation, one candefine

A is aclassical propositional validity if itevaluates asT on every possible assignment of valuesto its atomic propositional variables;
A isclassically satisfiable if it evaluates asT on at least one possible assignment of values toits atomic propositional variables (and isclassicallyunsatisfiable otherwise);
A is aclassical propositional consequence of B if onno assignment of values to the atoms that occur in A and B on which B,evaluates asT does A evaluate asF;
A is aclassical propositional equivalent of B if Aand B evaluate asT on precisely the same assignmentsof values to atoms.

In this way, the language of propositional logic restricted to theconnectives $\neg$, $\vee$, and $\wedge$ corresponds with theformulas of the familiar two element Boolean algebra ofcomplementation, union, and intersection. The familiar Boolean lawsof

interchange:
If A and B are equivalent, and A occurs as a subformula of $\rC_1$,then the result of replacing an occurrence of A in $\rC_1$ with B isa formula $\rC_2$ that is equivalent to $\rC_1$.
substitution:
If A and $\rB_1$ and $\rC_1$ are any formulas whatsoever, then theresult of replacingeach occurrence of the propositionalvariable $p$ in $\rB_1$ and $\rC_1$ with A are formulas$\rB_2$ and $\rC_2$ with the properties: $\rB_2$ is valid if$\rB_1$ is; $\rB_2$ is unsatisfiable if $\rB_1$ is; $\rB_2$ isa consequence of $\rC_2$ if $\rB_1$ is a consequence of $\rC_1$;$\rB_2$ and $\rC_2$ are equivalent if $\rB_1$ and $\rC_1$are.
complementation:
$\rA\vee\neg\rA$ is a classical validity (called the “law ofexcluded middle” (lem) in propositionallogic).
double complementation:
$\neg\neg\rA$ is equivalent to A.
commutativity:
$\rA\wedge\rB$ is equivalent to $\rB\wedge\rA$, and $\rA\vee\rB$is equivalent to $\rB\vee\rA$.
associativity:
$(\rA\wedge\rB)\wedge\rC$ is equivalent to $\rA\wedge(\rB\wedge\rC)$, and $(\rA\vee\rB)\vee\rC$ is equivalent to$\rA\vee (\rB\vee\rC)$.
distribution:
$\rA\vee (\rB_1\wedge\rB_2\wedge \ldots \wedge\rB_n)$ is equivalentto $(\rA\vee\rB_1)\wedge (\rA\vee\rB_2)\wedge \ldots \wedge(\rA\vee\rB_n)$ and
$\rA\wedge (\rB_1\vee\rB_2\vee \ldots \vee\rB_n)$ is equivalent to$(\rA\wedge\rB_1)\vee (\rA\wedge\rB_2)\vee \ldots \vee(\rA\wedge\rB_n)$.
De Morgan equivalence:
$\neg(\rB_1\wedge\rB_2\wedge \ldots \wedge\rB_n)$ is equivalent to$\neg\rB_1\vee\neg\rB_2\vee \ldots \vee\neg\rB_n$ and
$\neg(\rB_1\vee\rB_2\vee \ldots \vee\rB_n)$ is equivalent to$\neg\rB_1\wedge\neg\rB_2\wedge \ldots \wedge\neg\rB_n$.

therefore apply to this language of “Boolean propositionalformulas”.

2.1.1 Normal forms

Consider any other propositional connective denoted $\star$, of anyarity, say 3, and suppose that with it too is associated an arity-3truth function. As before let us specify this truth function byindicating its output on each of the $2^3$ possible inputvalues.

input	$\star$
$\langle$T,T,T$\rangle$	T
$\langle$T,T,F$\rangle$	T
$\langle$T,F,T$\rangle$	F
$\langle$T,F,F$\rangle$	F
$\langle$F,T,T$\rangle$	F
$\langle$F,T,F$\rangle$	T
$\langle$F,F,T$\rangle$	F
$\langle$F,F,F$\rangle$	F

There is a simple algorithm for constructing a Boolean formula that isequivalent to $\star$(A, B, C): For each row of the defining tablefor $\star$ in which the output value isT,construct a conjunction of each propositional variable that isassignedT and the negation of each propositionalvariable that is assignedF in that row’sinput: in our case, $\rA\wedge\rB\wedge\rC$ from row 1,$\rA\wedge\rB\wedge\neg\rC$ from row 2, and$\neg\rA\wedge\rB\wedge\neg\rC$ from row 3. Then disjoin theseconjunctions. In our case the final formula is

\[(\rA\wedge \rB\wedge\rC)\vee (\rA\wedge\rB\wedge\neg\rC)\vee (\neg \rA\wedge \rB\wedge\neg\rC).\]

It is clear that this formula will evaluate asT onall the rows that $\star$(A, B, C) did and as false on all the otherrows. Suppose, now, that one is given a propositional formula with anyarbitrary composition of connectives, and that under the classicalinterpretation these connectives are associated with truth-functionalconnectives of the appropriate arity. This formula will be equivalentto some simple formula with a single connective whose arity is equalto the total number of propositional variables in the originalformula. By the construction just rehearsed, that simple formula isagain equivalent to a Boolean formula of a certain form. Thus we haveverified the Disjunctive Normal Form (DNF) theorem:

Theorem 1.Any formula of propositional logicunder the classical interpretation is equivalent to a disjunction ofconjunctions of propositional variables and negated propositionalvariables.

Similar reasoning can be used to verify equivalence to a“conjunctive normal formula”, a conjunction ofdisjunctions of propositional variables and negated propositionalvariables.

2.1.2 Truth-functional completeness

One corollary of the DNF theorem is that Boolean logic—thefragment of propositional logic with only the connectives $\neg$,$\wedge$, and $\vee$—is in a sense just as expressive asfull classical propositional logic with infinitely many connectives ofinfinitely many arities. This fact is often expressed by saying thatthe set of connectives $\{\neg, \wedge, \vee\}$ on the classicalinterpretation is “truth-functionally complete”: the otherconnectives aren’t all exactly impostors in the above usedsense, but they can each be viewed as an abbreviation of somecombination of Boolean connectives. Algebraically, one can think ofthe infinite function space as being fully spanned by the Booleanfunctions.

The idea of truth-functional completeness can be pressed further withthe simple observation that $\rA\wedge\rB$ is the classicalequivalent of $\neg (\neg\rA\vee\neg\rB)$, so that it too can beviewed as an abbreviation. So the pair $\{\vee, \neg\}$ istruth-functionally complete. Likewise, $\rA\vee\rB$ abbreviates$\neg (\neg\rA\wedge\neg\rB)$: $\{\wedge, \neg\}$ istruth-functionally complete. In 1913, Henry Sheffer rediscovered anunpublished observation of Charles Sanders Peirce that the functions$f_9^2$ and $f_{15}^2$ approximating the truth conditions of thenatural language expressions “not both …and…” and “neither …nor …” eachindividually span the entire space of bivalent truth-functions.

2.1.3 Realization in switching circuits

More productive than reducing the number of connectives to thesmallest possible truth-functionally complete set, though, has beenthe selection of connectives that convey the greatest perspicuity intothe structure of deductive inference. We have already indicated thatthe Boolean connectives, by closely approximating the truth conditionsof the ordinary language particles “not”,“and”, and “or”, provide a formal mechanismfor evaluating contentful human inference. Another merit of theBoolean selection is its natural realization in the description ofrelay and switching circuits. In 1940 Claude Shannon described aninterpretation of propositional logic in which sentence letters standfor circuits: atomic circuits are nodes $n_1$ and $n_2$ connectedby a gated path which, when closed, allows a current to pass between$n_1$ to $n_2$ and, when open, does not. $\rA\wedge\rB$represents the serial connection of circuits A and B, $\rA\vee\rB$represents their parallel connection, and $\neg\rA$ represents acircuit that is closed if A is open and open if A is closed (this is atheoretical posit: the interpretation alone provides no predeterminedway to construct such a circuit). Letting the value 0 represent acircuit being closed and the value 1 represent a circuit being open,one sees that the formulas of propositional logic represent all thepossible ways of constructing electrical circuits, and their classicaltruth functional analysis determines exactly whether a circuit sorepresented is open: open circuits evaluate asT,closed circuits asF.

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., opensand closes under the same conditions as) a circuit described by adisjunctive normal formula. Thus one could be given complex circuitsA, B, and C, connect A and B in series ($\rA\vee\rB$), then connectthis in parallel to C ($(\rA\vee\rB)\wedge\rC$), and finally desirea circuit that is closed when this is open: $\neg((\rA\vee\rB)\wedge\rC)$. This formula describes the conditions underwhich the circuit you are after will be closed, but it does notspecify a way of constructing it. The DNF theorem tells us that thereis a “normal” circuit with the same closure conditions.Because all switches in such normal circuits apply at the atomiclevel, there is a known way to construct them. More, there aresystematic methods for simplifying disjunctive normal formulas toequivalent formulas with the fewest number of occurrences of atoms(Quine 1955 presents an algorithm originally discovered by Samson andMills 1954). Combined with Shannon’s result, this shows not onlythat symbolic manipulation provides a guide for how to construct acircuit with desired closure conditions but that it can be used todesign the least complicated and resource demanding one.

2.1.4 The material conditional

Another important feature of the classical interpretation is thespecial role played by the binary truth function $f_5^2$, whichalways returns the valueT unless given the input$\langle$T,F$\rangle$. Thistruth function is often described, controversially, as giving thetruth conditions for the indicative mood conditional connective“if …, then …”, or even, erroneously, forthe relation “implies”. It is important to underscore theerror in attributing truth functionality to the implication relation.To say that one proposition implies another is to say that under anyconditions in which the first is true, the second is also true. Tosuggest that this relation is truth-functional is to suggest thatsimply knowing whether A and B are true is enough to determine whetherA implies B. This suggestion is untenable because the truth or falsityof A and B indicate nothing about other conditions. B could be truebut, for all that, not be implied by A because under some othersituation A could be true while B is false. As emphasized above, theimplication relation is not ordinarily thought of as a propositionalconnective at all, but a relation that two propositions might bear toone another.

What is more interesting is the thesis that $f_5^2$ captures thetruth conditions of, at least some uses of, conditional expressions inthe indicative mood. The binary connective given this truth-functionalinterpretation is known as the “material conditional” andis often denoted $\supset$. One can readily check that$\rA\supset\rB$ is equivalent to the Boolean expression$\neg\rA\vee\rB$. There is a vast literature about the tenability ofthe claim that ordinary language conditional expressions aretruth-functional. The claim itself is apparently ancient, attributedto Philo of Melaga and referenced in Chrysippus’s earlysystematization of propositional logic. It has been defended in amodern context by Charles Peirce, H. P. Grice, and Frank Jackson. Butits detractors have been many (see the entry onindicative conditionals).

Of special interest is the suggestion, originally due to Frank Ramsey,that expressions of the form “If A, then B” in theindicative mood are best understood in terms of conditionalprobabilities as “The probability of B given A is nearly certain($\bP_\rA (\rB) > 0.95$)”. In 1976 David Lewis proved thatthe conditional expressions, so understood, not only fail to betruth-functional but in fact are not even propositions. DorothyEdgington (1995: 280) provided the following simple argument forLewis’s result: Suppose $\bP_\rA (\rB)$ measured theprobability of some (not necessarily truth functional) proposition$\rA\cdot\rB$. If $\rA\supset\rB$ implies $\rA\cdot\rB$, then$\rA\cdot\rB$ is true whenever A is false. Therefore,$\rA\cdot\rB$ cannot be unlikely when A is unlikely. But theunlikelihood of A certainly does not prevent $\bP_\rA (\rB)$ frombeing very low. If, on the other hand, $\rA\supset\rB$ does notimply $\rA\cdot\rB$, then $\rA\cdot\rB$ could be false when$\neg(\rA\wedge\neg \rB)$ is true, and certainty about$\neg(\rA\wedge\neg \rB)$ would still leave room for doubt about$\rA\cdot\rB$. But being certain of $\neg(\rA\wedge\neg\rB)$suffices for $\bP_A (\rB)=1$. It follows that $\rA\supset\rB$neither implies nor doesn’t imply $\rA\cdot\rB$, and the onlyway this could happen is for $\rA\cdot\rB$ not to havetruth-conditions at all, for $\bP_\rA (\rB)$ not to measure theprobability of any proposition.

This example highlights again the delicacy of the problem ofdetermining which connectives can be analyzed under the purview ofpropositional logic. On some interpretations (including thetruth-functional one), indicative mood conditionals can be, but onRamsey’s interpretation they cannot. In 1982, W. V. O. Quineanticipated Lewis’s result by expressing the caution, which heattributed to Philip Rhinelander, not to confuse the statement of aconditional “If A, then B” with the statement of B oncondition A. The latter, he held, is typically the proper way ofunderstanding an expression of the form “If A, then B”,which, because it is a non-statement in the absence of the conditionA, cannot be understood as a proposition at all.

Gottlob Frege is often counted among the defenders of the materialconditional, but his attitude towards the connective is nuanced. Hissystematization of propositional logic did feature a connective withthe truth conditions given by $f_5^2$, but Frege rejected the ideathat this connective expressed the indicative conditional of naturallanguage. He wrote, “the causal connection implicit in the word‘if’ …is not expressed by our symbols” (1972:116). It is a matter of ongoing debate whether Frege believed that thematerial conditional failed even to capture the truth conditions ofordinary language indicative conditionals or if he meant only thatalthough it captures those conditionals’ truth conditions, thematerial conditional fails to capture other, non truth-conditionalaspects of meaning. What is clear is that whatever mismatch hedetected between ordinary conditional statements and the materialconditional did not dissuade him from placing the latter in the centerof his logical investigations.

Given the plurality of truth-functionally complete sets ofconnectives, why would Frege or anyone else select the materialconditional as a primitive connective for classical logic? Frege sawthat the value of selecting the material conditional as a primitiveconnective not from its approximation of ordinary language expressionbut from its role internal to logical theory. Let us write$\dturnstile{\CTT} \rB$ to indicate that the formula B is valid inthe classical theory of truth. Generalizing this turnstile notation,one also writes $\rA \dturnstile{\CTT} \rB$ to indicate that B is aclassical propositional consequence of A, and where $\calS$ is a setof propositional formulas, $\calS \dturnstile{\CTT} \rB$ to indicatethat B is a classical propositional consequence of all the formulas in$\calS$. A fundamental fact, readily verifiable with a truth table,is that $\calS\cup\{\rA\}\dturnstile{\CTT} \rB$ if, and only if,$\calS\dturnstile{\CTT} \rA\supset\rB$. In the case that $\calS$is empty, $\rA\dturnstile{\CTT} \rB$ exactly when$\dturnstile{\CTT} \rA\supset\rB$. Earlier we emphasized that thematerial conditional cannot be understood as an expression of logicalimplication. The relation of classical logical consequence, on theother hand, is in fact a (particularly strict sort of) logicalimplication relation, one to which the material conditional is in factdirectly related: $\rA\supset\rB$ does not express any implicationrelation between A and B, but the claim that $\rA\supset\rB$ is aclassical propositional validity is such an expression ofimplication.

2.1.5 Decidability

A logic is said to be decidable if there is a reliable method fordetermining whether a formula is satisfiable. Classical propositionallogic is readily seen to be decidable: Given an arbitrary formula,simply enumerate in the tabular method used above each of the possiblesequences of truth values that can be input to its atomicpropositional variables, and compute the composition of functions oneach of these inputs. Because formulas are finite strings of symbols,each contains only a finite number, sayn, of atoms, so thatthe truth-table will have exactly $2^n$ rows. Completing the truthtable is therefore a finite determinate task, at the end of which onewill have discovered whether or not the formula is satisfiable.

2.1.6 NP-completeness

The problem of determining whether a formula of classicalpropositional logic is satisfiable is known assat.Although decision procedures exists forsat,all known procedures for making thisdetermination in a predetermined manner for every possible formula arein a precise sense tedious and inefficient: no procedure has beendiscovered which returns an answer after a number of computation stepspolynomially bounded by the size of the formula one tests, i.e., it isunknown whethersat is in the complexity classP of problems solvable by a deterministic procedurein polynomial time. It is known thatsat is inthe complexity classNP—those questions thatcan be answered by a non-deterministic procedure in polynomial time.In 1971, Steven Cook proved thatsat is“NP-complete”: any problem in the classNP is reducible in polynomial time tosat.A corollary of Cook’s theorem is that ifsat is in the classP, thenNP =P. It is generally believedthatNP is a strictly larger class of problems thanP and, for this reason, that no“efficient” procedure for solvingsatin the sense of polynomial time computabilityexists. In the decades since Cook’s discovery, a wide range ofproblems have been shown to beNP-complete. Butclassical propositional logic figured prominently in the context ofthe discovery ofNP-completeness. Its perspicuity wasparticularly 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, considerthe set of formulas $\calS = \{p_1, p_2, p_3, \neg (p_1\wedgep_2\wedge p_3) \}$. Every proper subset of $\calS$ is“simultaneously satisfiable”, i.e., given any such propersubset, there is a single assignment of truth values to atoms underwhich each of the subset’s formulas are true. However, $\calS$itself is not simultaneously satisfiable: Making each of $p_1$,$p_2$, and $p_3$ true guarantees the falsity of $\neg (p_1\wedgep_2\wedge p_3)$. What if another set $\calT$ contains infinitelymany formulas? Our observation about $\calS$ might well foster theintuition that every proper subset of $\calT$ could besimultaneously satisfiable despite there being no assignment of truthvalues to atoms that satisfies every formula in $\calT$. What if,instead of knowing that everyproper subset of $\calT$ issimultaneously satisfiable, one were told only that eachfinite subset of $\calT$ is? Because most proper subsets of$\calT$ are infinite, the intuition that $\calT$ couldnevertheless fail to be simultaneously satisfiable is onlystrengthened.

The Compactness Theorem (Gödel 1930) tells us that this intuitionis misleading:

Theorem 2.If each finite subset of $\calT$ issimultaneously satisfiable, then so is $\calT$.

Notice that by “relaxing” the hypothesis from“proper subset” to “finite subset”, theCompactness Theorem is true and in fact trivial when $\calT$ isfinite: $\calT$ is one of its own finite subsets. When $\calT$ isinfinite, though, relaxing the hypothesis dramatically increases thetheorem’s strength (In the language of quantification theory,the theorem involves a strong quantifier switch: From the fact that,given any finite subset of $\calT$, one can always find aninterpretation that satisfies it (potentially a differentinterpretation for each finite subset), one may infer the existence ofa single interpretation that satisfies every possible finite subset of$\calT$ one might ever be given).

For a striking corollary of compactness, suppose that A is theclassical propositional consequence of the infinite set of formulas$\calU$ ($\calU \dturnstile{\CTT} \rA$). If every finite subset of$\calU\cup\{\neg\rA\}$ were simultaneously satisfiable, then bycompactness, $\calU\cup \{\neg\rA\}$ would be simultaneouslysatisfiable, contrary to the our supposition. Therefore, some finitesubset of $\calU\cup\{\neg\rA\}$ is not simultaneouslysatisfiable—for some finite subset $\calV$ of $\calU$, thereis no assignment of truth values to atoms that makes every formula in$\calV$ true and A false. Classical propositional consequence isalways “finitely determined”: If $\calU \dturnstile{\CTT}\rA$, then for some finite subset $\calV$ of $\calU$, $\calV\dturnstile{\CTT} \rA$.

2.2 Deduction

Formal deduction systems, introduced by Gottlob Frege in 1879, providean alternative specification of the meanings of propositionalconnectives. Such systems are characterized by a finite set offormulas called axioms and a finite set of inference rules. Thepropositional axioms in Frege’s system are

\[\begin{align}\rA&\supset (\rB\supset\rA) \tag*{axiom 1}\\(\rC\supset (\rB\supset\rA))&\supset ((\rC\supset\rB)\supset (\rC\supset\rA)) \tag*{axiom 2}\\(\rB\supset\rA)&\supset (\neg\rA\supset \neg\rB) \tag*{axiom 3}\\\rA&\supset \neg\neg\rA \tag*{axiom 4}\\\neg\neg\rA&\supset\rA \tag*{axiom 5}\\\end{align}\]

The inference rules of are

modus ponens: $\begin{prooftree}\AxiomC{\(\rA\supset\rB$}\AxiomC{$\rA$}\BinaryInfC{$\rB$}\end{prooftree}\)
substitution: If $p$ is an atomic variable in B, and C is anyformula whatsoever, then let $\rB'$ be the result of replacing everyoccurrence of $p$ with C, and from B infer $\rB'$.

A proof is defined as a finite sequence of formulas, each one of whicheither is an axiom or follows from previous entries in the sequence byan application of an inference rule. A theorem is a formula whichoccurs as the final entry in a proof, and we denote the theoremhood ofa formula A by $\turnstile{\CPC} \rA$—herecpcstands for “the classical propositionalcalculus”. We have presented the formal deduction system foundin Frege 1879, butcpc is meant to label anyequivalent system. Frege’s system is in two senses adequate forrepresenting classical propositional logic: Because the pair $\{\neg,\supset\}$ is truth-functionally complete, any formula expressiblewith any combination of bivalent truth-functional connectiveswhatsoever can be translated into a formula in Frege’s system.Moreover, the system is complete in the sense that all and only theclassical propositional tautologies are theorems. The verification ofthis propositional completeness theorem below uses a differentdeductive system forcpc due to Hilbert andBernays. As Jean Nicod (1917) was the first to observe, there are evenpresentations ofcpc using only the single“not both …and …” connective $|$, e.g.,with the lone axiom

\[((\rA | (\rB | \rC)) | ((\rE | (\rE | \rE)) | ((\rD | \rB) | ((\rA | \rD) | (\rA | \rD)))))\]

and rules of inference

Nicod’s inference: $\begin{prooftree}\AxiomC{\(\rA$} \AxiomC{$\rA|(\rB|\rC)$} \BinaryInfC{$\rC$}\end{prooftree}\)
substitution: If $p$ is an atomic variable in B, and C is anyformula whatsoever, then let B’ be the result of replacing everyoccurrence of $p$ with C, and from B infer B’.

In parallel to the truth-functional framework for classical logic, onecan also introduce the notion of deduction from hypotheses: If$\calS$ is a set of formulas, then a sequence of formulas whose lastentry is A and in which every entry either is an axiom, a member of$\calS$, or the result of an application of a inference rule fromearlier entries is called a derivation of A from $\calS$. Informulating this notion forcpc, however, somecare is needed. One does not want, for example, every formula to bededucible from a propositional variable, and yet the substitution ruleallows one to infer anything from $p_1$. In moving from pureaxiomatic provability to the idea of deduction from arbitraryhypotheses, therefore, the substitution rule is restricted to beapplicable only to axioms. One can easily show that this restrictiondoes not affect the set of theorems. With this restriction in place,we can denote the derivability of A from the set $\calS$ by $\calS\turnstile{\CPC} \rA$.

2.2.1 The Deduction Theorem

In 1910 Frege pointed out, but did not prove, that$\calS\cup\{\rA\}\turnstile{\CPC} \rB$ if, and only if,$\calS\turnstile{\CPC} \rA\supset\rB$. The first recorded proofs arein Herbrand 1930 and Tarski 1933. Whereas the analogous observation inthe case of the truth-functional interpretation is trivial, thisresult of Herbrand and Tarski is more complex. One direction isreadily verified: Any $\calS$-derivation $\calD$ of$\rA\supset\rB$ is obviously also a $\calS\cup\{\rA\}$-derivation.To construct a $\calS\cup\{\rA\}$-derivation of $\rB$, simplyappend the two formulas $\rA$ and $\rB$ to the end of$\calD$.

The other direction is known as the Deduction Theorem. It’sproof uses induction on the length of the $\calS\cup\{\rA\}$-derivation of $\rB$:

Theorem 3.$\calS\cup\{\rA\}\turnstile{\CPC}\rB$ only if $\calS\turnstile{\CPC}\rA\supset\rB$

Proof. (base step) If there is aone-line derivation of $\rB$ from $\calS\cup\{ \rA\}$, then it ispossible to construct a $\calS$-derivation of $\rA\supset\rB$. Tosee this, notice that there are only three types of one-linederivations:

$\rB$ is in the set $\calS$
$\rB$ is $\rA$
$\rB$ is an axiom

The following three $\calS$-derivations exhibit the fact that$\calS \turnstile{\CPC}\rA\supset\rB$ in case 1, 2, and 3,respectively:

\[\begin{array}{c|c|c}\rB & (\rB\supset((\rC\supset\rB)\supset\rB))\supset((\rB\supset(\rC\supset\rB))\supset(\rB\supset\rB)) &\rB \\\rB\supset (\rA\supset\rB) & \rB\supset((\rC\supset\rB)\supset\rB) & \rB\supset(\rA\supset\rB) \\\rA\supset\rB & (\rB\supset(\rC\supset\rB))\supset(\rB\supset\rB)) &\rA\supset\rB \\& \rB\supset (\rC\supset\rB) & \\& \rB\supset\rB & \end{array}\]

It is easy to check that each line of each derivation is either amember of $\calS,$ an axiom, or the result of an application ofmodus ponens. (The middle sequence qualifies as a$\calS$-derivation of $\rA\supset\rB$ because of the assumptionthat $\rA$ is $\rB$.)

(induction step) Assume that whenever there isa $\calS\cup\{ \rA\}$-derivation of $\rB$ that isn orfewer lines long, there is a $\calS$-derivation of$\rA\supset\rB$. Now suppose there is an $n+1$ line long$\calS\cup\{ \rA\}$-derivation $\calD$ of $\rB$. It is possiblethat the justification for line $n+1$ is one of the possibilitiesfrom the base case—that $\rB$ is an axiom, is from the set$\calS$, or is identical to $\rA$. In any of those cases, the$\calS$-derivation of $\rA\supset\rB$ would be constructed as inthe base case. In the novel case that the last line is the result ofan application ofmodus ponens, the formulas$\rC\supset\rB$ and $\rC$ occur as earlier lines in $\calD$.Therefore $\calS\cup\{ \rA\}$-derivations that aren lineslong or shorter of $\rC\supset\rB$ and $\rC$ appear assubsequences of $\calD$. The induction hypothesis then guaranteesthe existence of $\calS$-derivations of $\rA\supset(\rC\supset\rB)$ and of $\rA\supset\rC$. Let

\[\calD_1 = \langle\rS_1, \rS_2, \ldots, \rA\supset (\rC\supset\rB)\rangle\]

and

\[\calD_2 = \langle\rT_1, \rT_2, \ldots, \rA\supset\rC\rangle\]

be examples of such derivations, and consider the sequence:

\[\begin{array}{c} \calD_1\\ \calD_2\\ (\rA\supset (\rC\supset\rB))\supset ((\rA\supset\rC)\supset (\rA\supset\rB))\\ (\rA\supset\rC)\supset (\rA\supset\rB)\\ \rA\supset\rB\end{array}\]

This is a $\calS$-derivation of $\rA\supset\rB$. ◻

Because this verification of the Deduction Theorem depends only on thefirst two of Frege’s axioms, it applies also in manynon-classical contexts including, importantly, a large class ofconstructive propositional logics.

2.2.2 Basic meta-theory

Another analogue to the evident facts from the truth-functionalframework, this time the DNF theorem, played a historical role in themetatheoretical analysis of axiomatic systems. Hilbert showed how toassociate with every formula A a disjunctive normal formula$\rA_{\dnf}$ and a conjunctive normal formula $\rA_{\cnf}$ suchthat

\[\begin{aligned}&\turnstile{\CPC} \rA \supset\rA_{\dnf},\\ &\turnstile{\CPC} \rA_{\dnf} \supset\rA, \\&\turnstile{\CPC} \rA \supset\rA_{\cnf}, \text{ and }\\ &\turnstile{\CPC} \rA_{\cnf} \supset\rA.\end{aligned}\]

In particular, applying the Deduction Theorem, A and $\rA_{\cnf}$are inter-derivable.

Frege’s axiomatization obviously depends on the expressiveadequacy of the pair $\{\supset, \neg\}$, about which one cannotreally be certain unless one has in mind some account of the meaningof the connectives other than that provided by the deduction systemitself. Russell and Whitehead inPrincipia Mathematica andHilbert and Ackermann in 1928 followed Frege in working with a smallset of basic connectives and using others as abbreviations. In 1926,Bernays questioned “the predominant tendency …to reducethe number of basic connectives and therewith the number ofaxioms”, observing that “one can, on the other hand,sharply distinguish the various connectives” and thereby notpresuppose equivalences such as $\neg\rA\vee\rB = \rA\supset\rB$that do not appear in the axiomatic framework itself. Such an approachallows one to explore modifications of an axiom system in whichcertain equivalences do not hold, and to compare them with oneanother. The axiomatic framework is generally a crude device for suchcomparative studies; the spirit of Bernays’s insight reached itsmaturation in the natural deduction and sequent calculi of Gentzen(1934–35) wherein the meaning of each connective is fullyspecified, in terms of characterizing inference rules, in isolation ofthe other connectives.

The axiomatic framework with minimal signature (following Russell andWhitehead, Hilbert used only $\{\vee, \neg\}$) neverthelesssubmitted to the Hilbert school’s profound metatheoreticalanalysis in terms of consistency, independence, maximality, andcompleteness proofs. In order to preserve the context of discovery,the following retraces the original proofs provided in Hilbert’slectures “Prinzipien der Mathematik” from 1917.

2.2.2.1 Consistency

An formal deductive systemS isconsistent if for no formula A is $\turnstile{\rS} \rA$ and$\turnstile{\rS} \neg\rA$. To prove consistency ofcpc,Hilbert reasoned as follows: Let the sentenceletters range over the numbers 1 and 0, interpret the disjunctionsymbol as multiplication and the negation symbol as the function $1 -x$. In this interpretation, every formula is a function on 0 and 1composed of multiplication and $1 - x$. Hilbert observed that theaxioms are each interpreted as functions that return the value 0 onevery input, and that the rules of inference each preserve thisproperty (so that every theorem is constant 0). Furthermore, thenegation of any theorem is constant 1 and therefore unprovable. Thus,no formula is provable if its negation also is, so the system isconsistent.

2.2.2.2 Maximality

A formal deductive system ismaximal if any proper extensionof it is inconsistent. Hilbert used the same interpretation from hisconsistency argument to show:

Theorem 4.cpc ismaximal.

Proof. As above, a formula is provable only if it is constant0 under the interpretation, which, in the case of a conjunctive normalformula, occurs precisely when each of its conjuncts contains both anegated and unnegated occurrence of some propositional variable. Nowlet A be any unprovable formula. Its associated formula $\rA_{\cnf}$must also be unprovable and therefore must contain a conjunct C withno propositional variable appearing both negated and unnegated. Toshow thatcpc+A (cpcaugmented with A as an additional axiom) is inconsistent, let B be anyformula whatsoever, and label D the result of substituting, into$\rA_{\cnf}$, B for every propositional variable that occursunnegated in C and $\neg\rB$ for every propositional variable thatoccurs negated in C. It is easy to show that

\[\begin{aligned}&\turnstile{\CPC+\rA} \rA, \\&\turnstile{\CPC} \rA\supset\rA_{\cnf},\\&\turnstile{\CPC} \rA_{\cnf}\supset\rD, \text{ and}\\&\turnstile{\CPC} \rD\supset\rB.\\\end{aligned}\]

Thus $\turnstile{\CPC+\rA} \rB$ for any formula B. ◻

Hilbert and others called this same property“completeness”, in analogy to the completeness axiom fromHilbert’s foundational studies of plane geometry and numbertheory. But as completeness has come to mean something else in thelogical domain, this property is now commonly referred to as“Post-completeness” (after Post 1921 who rediscovered thisproperty ofcpc) or, as here, as“maximality”.

2.2.2.3 Completeness

The Completeness Theorem describes an exact correspondence between thetruth-functional and deductive frameworks:

Theorem 5.$\turnstile{\CPC} \rA$ if, and onlyif, $\dturnstile{\CTT} \rA$.

Proof. This result is often described as difficult toestablish, but in Hilbert’s 1917 lectures, it is an immediatecorollary of maximality. Already it was observed in the consistencyargument that only formulas interpreted as constant 0 functions areprovable. Suppose that some formula A were constant 0 but unprovableincpc. Then the same consistency argument asbefore would carry through forcpc+A,contradicting the maximality result just proved. It follows that everyformula interpreted as a constant 0 function is a theorem ofcpc.The formulas interpreted as constant 0functions are just the valid formulas on the classicaltruth-functional interpretation. ◻

A direct route to the Completeness Theorem is also possible. A famousproof from Kalmár 1935 begins with two observations:

K1: $\turnstile{\CPC} (\rA\supset \rB)\supset ((\neg \rA\supset\rB)\supset \rB)$
K2: Let A be any formula with propositional variables $p_1$,$p_2$, …, $p_n$, and let $\mathit{v}$ be an assignment oftruth values to propositional variables. Define $\rC_k = p_1$ if$\mathit{v}(p_1) = \mathbf{T}$, $\neg p_1$ if $\mathit{v}(p_k) =\mathbf{F}$. Then if $\mathit{v}(\rA) = \mathbf{T}$, $\rC_1,\rC_2, \ldots, \rC_n \turnstile{\CPC} \rA$.

Proof. Suppose now that T is a classical validity withpropositional variables $p_1$, $p_2$, …, $p_n$. Then byK2, for every assignment $\mathit{v}$ of truth values to propositionalvariables, $\mathit{v}(\rT) = \mathbf{T}$ and $\rC_1, \rC_2,\ldots, \rC_n \turnstile{\CPC} \rT$. Let $\mathit{u}$ and$\mathit{w}$ be assignments of truth values that differ only in that$\mathit{u}(p_n) = \mathbf{T}$ whereas $\mathit{w}(p_n) =\mathbf{F}.$

\[\rC_1, \rC_2, \ldots, \rC_{n-1}, p_n \turnstile{\CPC} \rT\]

and

\[\rC_1, \rC_2, \ldots, \rC_{n-1}, \neg p_n \turnstile{\CPC} \rT.\]

By the Deduction Theorem,

\[\rC_1, \rC_2, \ldots, \rC_{n-1} \turnstile{\CPC} p_n\supset \rT,\]

and

\[\rC_1, \rC_2, \ldots, \rC_{n-1} \turnstile{\CPC} \neg p_n\supset \rT.\]

ByK1,

\[\rC_1, \rC_2, \ldots, \rC_{n-1} \turnstile{\CPC} (p_n\supset \rT)\supset ((\neg p_n\supset \rT)\supset \rT).\]

Two applications ofmodus ponens yield

\[\rC_1, \rC_2, \ldots, \rC_{n-1} \turnstile{\CPC} \rT.\]

Repeating this same reasoning for $p_{n-1}$ yields

\[\rC_1, \rC_2, \ldots, \rC_{n-2} \turnstile{\CPC} \rT,\]

and aftern repetitions $\turnstile{\CPC} \rT$ isestablished. ◻

Proving completeness directly in this manner allows a differentargument for maximality:

Proof. For suppose $\centernot{\turnstile{\CPC}} \rA$. Thenby completeness, $\centernot{\dturnstile{\CTT}} \rA$. So there issome assignment $\mathit{v}$ of truth values to propositionalvariables on which A evaluates asF. Let $\rA'$ bethe result of replacing every propositional variable assignedT by $\mathit{v}$ with $p_1\supset p_1$ and everypropositional variable assignedF by $\mathit{v}$with $p_1\supset\neg p_1$. $\rA'$ is unsatisfiable. Therefore$\neg \rA'$ is valid. So $\turnstile{\CPC+\rA} \neg\rA'$. But$\turnstile{\CPC+\rA} \rA$ and, by substitution,$\turnstile{\CPC+\rA} \rA'$. Socpc+A isinconsistent. ◻

2.2.2.4 Completeness as semi-decidability

The set of theorems of a formal deductive system can be seen to berecursively enumerable. To construct a simple enumeration, let us addto the language of propositional logic the symbol “;” as asequential location demarcator so that the language consists of $p_1,p_2, \ldots, (, ), \supset, \neg, \hbox{and} ;$. Then we can list allpossible sequences of symbols in stages:

Stage 1: list all strings of symbols of length 1 using only thepropositional variable $p_1$.
Stage 2: list all strings of symbols of length 1 or 2 using onlypropositional variables $p_1$ and $p_2$.
...

At each stage, the vocabulary is finite, so there are only finitelymany strings of symbols to list. But every proof is a finite string ofsymbols and therefore gets listed at some stage or another. Therefore,given a formula A, one can begin searching for a proof one stage at atime, checking only finitely many strings at each stage. If A isvalid, then by completeness it is provable, and one will discover aproof of it after examining some finite number of strings. On theother hand, if A is not valid, the search will never halt.

Completeness results are often described as valuable because they makeevident the recursive enumerability of a logic’s validities. Inthe case of classical propositional logic, validity is already knownto be recursively enumerable and even decidable by a much simpler andmore efficient method of truth table evaluation. The CompletenessTheorem’s value derives instead from the fact that two vastlydifferent conceptions of logicality—formal provability andtruth-functional validity—coincide. The situation is differentwith other logical systems. The most famous example is first-orderclassical quantification theory, which Church and Turing proved to beundecidable in 1936. Here, the Completeness Theorem of Gödel 1930is especially insightful: the set of quantificational validities isnot recursive, but it is at least recursively enumerable. In fact, thecompleteness results for classical propositional logic andquantification theory were the historical occasion for theclarification of the distinction between recursive and recursivelyenumerable sets—a distinction seen as elementary today but thesource of considerable confusion in the first decades of the twentiethcentury.

Completeness results can play a role for many alternative systems ofpropositional logic similar to the one they play for classicalquantification theory: Urquhart 1984 showed that the systemseandr of relevance logicare undecidable; Lincoln et al. 1992 showed that full propositionallinear logicll is undecidable. In thesearenas, a complete formal derivation system can provide some concreteaccess to the space of valid formulas whose abstract definition is nototherwise readily navigable.

2.2.2.5 Independence

The style of reasoning exhibited in the consistency argument can begeneralized to show independence results. The idea of the consistencyargument 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 formulathat results from its application also has P

and then to show that certain formulas do not have P. Because alltheorems either are axioms or are generated from axioms by iteratedapplications of inference rules, those latter formulas cannot betheorems.

In the consistency proof, P is the property of being interpreted as aconstant 0 function, and the formulas that do not have P are thenegations of theorems. The reasoning can be generalized, though.Suppose P were some other property that all but one of the axioms haveand that is similarly preserved by the inference rules. By verifyingthis one could show that the one axiom is not derivable from theothers and therefore that the deductive system would have fewertheorems without it. For example, the classical interpretation of$\supset$ is a function that returns 1 on the input $\langle 0,1\rangle$ and 0 otherwise, and the classical interpretation of$\neg$ is the function that returns 1 on the input 0 and returns 0on the input 1. All five of Frege’s axioms are constant 0 onthis interpretation. If we modify the interpretation so that$\supset$ is unchanged but $\neg$ returns 1 on the input 1 andreturns 0 on the input 0, thenaxioms 1, 2, 4, and 5 are still interpreted as constant 0 functions, whereas axiom 3returns 1 on the input $\langle 0, 1\rangle$. The inference rulesstill preserve the property of being constant 0 on this modifiedinterpretation, so we know that axiom 3 cannot be proved using onlyaxioms 1, 2, 4, and 5 and that without axiom 3 Frege’s systemwould not be complete.

For a more interesting example, consider the interpretation of$\supset$ and $\neg$ in terms of trivalent functions given by thefollowing tables:

A	B	$\rA\supset\rB$
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	$\neg\rA$
0	2
1	2
2	0

If P is the property of being a constant 0 function on thisinterpretation, then one can verify that

axioms 1, 2, 3, and 4 each have P
P is preserved bymodus ponens and substitution
axiom 5 evaluates as 1 on the input 1 and so does not have propertyP

and that axiom 5 is therefore independent of the first fouraxioms.

The use of non-classical (typically higher valence) truth-functionalinterpretations to define properties to be used in independence proofsdates back to Schröder 1890. It was pursued in full generality byŁukasiewicz, who also proved results about the scope of thistechnique.

2.3 Gentzen’s calculi

In 1934–35, Gerhard Gentzen introduced two alternativeframeworks for presenting deductive inference that have led toparticularly refined analyses of propositional logic. We will lookfirst at Gentzen’s system of natural deduction and laterconsider his sequent calculus.

2.3.1 Natural deduction

In lectures from early 1920, David Hilbert remarked that a formaldeduction system’s inference rules can be thought of asproviding the meanings of the connectives they govern (Hilbert 2013:323). Hilbert’s idea is given a profound realization inGentzen’s natural deduction calculus. Natural deduction is anearly and emblematic achievement in “proof-theoreticsemantics”: the tradition of specifying definitions ininferential, rather than denotational, terms.

In systems likecpc the only inference ruleresponsible specifically to a connective ismodus ponens.What would it mean for this rule not only to describe a deductivelyvalid pattern of inference but in fact to provide a definition of theconnective $\supset$? If one understandsmodus ponens notjust as one among many patterns of valid inference but as saying thatit isdefinitive of the conditional $\rA\supset\rB$ that itlicenses the inference from $\rA$ to $\rB$, then part of what onemeans is that any sentence that, together with $\rA$, allows theinference to $\rB$ expresses something equivalent to or strongerthan $\rA\supset\rB$. To illustrate this, let us rewritemodusponens in the turnstile notation as

\[\begin{aligned}\rA\supset\rB, \rA\vdash \rB\end{aligned}\]

Understood as a definition of $\supset$, this determines thefollowing form of the Deduction Theorem, stating that$\rA\supset\rB$ can be inferred from any other formula thatsimilarly licenses the inference from A to B:

\[\hbox{for all }\rC, \hbox{if } \rC, \rA\vdash \rB, \hbox{then }\rC\vdash \rA\supset\rB\]

In Gentzen’s terminology, rules likemodus ponens thatdescribe the definitive way of reasoning from a sentence governed by acertain connective are called “elimination rules”. TheDeduction Theorem, in describing the definitive pattern of reasoningwhose conclusion is governed by a certain connective, is an example ofan “introduction rule”. Gentzen wrote:

The introductions represent …the “definitions” ofthe symbols concerned, and the eliminations are no more, in the finalanalysis, than the consequences of these definitions. …Bymaking these ideas more precise it should be possible to display theElim-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 theircorresponding elimination rules; but rules of the one type do followfrom the conception of their corresponding rules of the other type asdefinitions. When conditionalization is understood as an operationthat maps $\rA$ and $\rB$ to the proposition that together with$\rA$ licenses an inference to $\rB$,modus ponenscaptures the part about licensing this inference, and the DeductionTheorem captures the part about beingthe thing that solicenses it, so that any other proposition that allows an inferencefrom $\rA$ to $\rB$ only does sovia $\rA\supset\rB$(see Franks 2021).

To take another example, consider the inferences $\rA\wedge\rB\vdash\rA$ and $\rA\wedge\rB\vdash \rB$. One might think of these asdefinitive of the logical conjunction: To know $\rA\wedge\rB$ is tobe in a position to immediately infer both A and B. If so, then simplybeing in the position to immediately infer both A and B should sufficeto allow one to conclude $\rA\wedge\rB$: For all $\rC$, if$\rC\vdash \rA$ and $\rC\vdash \rB$, then $\rC\vdash\rA\wedge\rB$. Here again, Gentzen labeled the first pair ofinferences the elimination rule for $\wedge$ and the latterinference its introduction rule.

Gentzen’s system of natural deduction is a presentation of logicin terms of an intro/elim pair of rules, related as aremodusponens and the Deduction theorem, providing an inferentialdefinition of each logical particle. His natural deduction system ofpropositional logic has such pairs of rules for the propositionalconnectives $\supset$, $\wedge$, $\vee$, and $\neg$, which hepresented in two-dimensional inference figures:

\[\hspace{-10em}\begin{prooftree} \AxiomC{$\rA\supset\rB$} \AxiomC{$\rA$}\RightLabel{${\supset}\text{elim}$} \BinaryInfC{$\rB$}\end{prooftree}\hspace{4em}\begin{prooftree} \AxiomC{$[\rA]$} \noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$\rB$} \RightLabel{${\supset}\text{intro}$}\UnaryInfC{$\rA\supset\rB$} \end{prooftree}\]\[\hspace{-4em}\begin{prooftree} \AxiomC{$\rA\wedge\rB$} \UnaryInfC{$\rA$}\end{prooftree} \quad \begin{prooftree} \AxiomC{$\rA\wedge\rB$}\RightLabel{${\wedge}\text{elim}$} \UnaryInfC{$\rB$}\end{prooftree}\hspace{4em}\begin{prooftree} \AxiomC{$\rA$} \AxiomC{$\rB$}\RightLabel{${\wedge}\text{intro}$} \BinaryInfC{$\rA\wedge\rB$}\end{prooftree}\] \[\hspace{-3em}\begin{prooftree} \AxiomC{$\rA\vee\rB$} \AxiomC{[$\rA$]}\noLine\UnaryInfC{$\vdots$} \noLine\UnaryInfC{$\rC$}\AxiomC{[$\rB$]} \noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$\rC$} \RightLabel{${\vee}\text{elim}$}\TrinaryInfC{$\rC$} \end{prooftree}\hspace{7em}\begin{prooftree} \AxiomC{$\rA$} \UnaryInfC{$\rA\vee\rB$}\end{prooftree} \quad \begin{prooftree} \AxiomC{$\rB$}\RightLabel{${\vee}\text{intro}$} \UnaryInfC{$\rA\vee\rB$}\end{prooftree}\] \[\hspace{-10em}\begin{prooftree} \AxiomC{$\neg\rA$} \AxiomC{$\rA$}\RightLabel{${\neg}\text{elim}$} \BinaryInfC{$\bot$}\end{prooftree}\hspace{6em}\begin{prooftree} \AxiomC{$[\rA]$} \noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{$\bot$} \RightLabel{${\neg}\text{intro}$}\UnaryInfC{$\neg A$} \end{prooftree}\]

Notice the appearance of the arity-0 connective $\bot$ in the$\neg$ rules, which has no inferential definition of its own.

Natural deduction proofs are trees constructed by iterating theserules. When all the assumptions in such a proof are discharged by theapplication of a rule, the formula in the tree’s single rootnode is said to be proved; otherwise it is said to be derived from theset of assumptions that remain open at leaf nodes. Let us write$\turnstile{\ND} \rA$ when there is a natural deduction proof ofA.

Gentzen observed that the natural deduction calculus with intro/elimpairs of rules for the connectives $\supset$, $\wedge$, $\vee$,and $\neg$ isnot equivalent to classical propositionallogic: $\turnstile{\ND} \rA$ only if $\dturnstile{\CTT} \rA$, but,for example, $\dturnstile{\CTT} \rA\vee\neg\rA$ whereas$\centernot{\turnstile{\ND}} \rA\vee\neg\rA$. “The law ofexcluded middle, which the intuitionists reject”, Gentzen wrote,“occupies a special position” in natural deduction.Gentzen’s framework revealed that the specification of themeanings of the propositional connectives in terms of binary truthfunctions does not correspond with the “inferential”specification of their meanings in terms of the intro/elim rulescheme. In fact, Johansson pointed out in 1937 that the introductionand elimination rules of Gentzen’s natural deduction cannot evenderive the rule of disjunctive syllogism

\[ \begin{prooftree}\AxiomC{$\rA\vee\rB$}\AxiomC{$\neg\rB$}\BinaryInfC{$\rA$} \end{prooftree}\]

This elementary inference that Chrysippus famously attributed tohunting dogs cannot be justified by the inferential meaning of the$\neg$ and $\vee$ connectives alone. To derive the disjunctivesyllogism rule, one needs the additional primitive inference figure

\[ \begin{prooftree}\AxiomC{$\bot$}\UnaryInfC{A} \end{prooftree}\qquad(\textit{ex falso quodlibet});\]

to derive the principle of excluded middle, one needs in addition thedouble negation rule

\[ \begin{prooftree}\AxiomC{$\neg\neg\rA$}\UnaryInfC{$\rA$} \end{prooftree}.\]

These rules can be used together with the introduction and eliminationrules for the propositional connectives to construct natural deductionsystemsnd+$\frac{\bot}{\rA}$ forintuitionistic propositional logic andnd+$\frac{\neg\neg\rA}{\rA}$for classicalpropositional logic, but Gentzen observed, such inference schemata“fall outside the intro/elim framework …”.(Classical propositional logic is often given a natural deductionpresentationnd+$\frac{\bot}{\rA}$+$\frac{\neg\neg\rA}{\rA}$,but theex falso quodlibet rule is redundant in that systembecause $\bot \turnstile{\ND+({\neg\neg\rA}/{\rA})} \rB$.)

The distinction between classical and intuitionistic logic predatesGentzen’s work. But with its inferential definition ofpropositional connectives, natural deduction sheds new light on thedistinction: classical, intuitionist, and other logicians can agree tothe same definitions of the propositional connectives, the differencesbetween their conceptions of logic having to do with the acceptabilityof principles like the law of excluded middle that are independent ofthe connectives’ meanings.

2.3.2 Sequent calculus

This same point is brought out in a different way in Gentzen’spropositional sequent calculi. These calculi present logical inferencein the form of sequents: expressions of the form “$\Gamma\Lrightarrow \Delta$” in which Greek letters stand for(possibly empty) finite sequences of formula. The sequences to theleft and to the right of the coordinating “sequent arrow”$\Lrightarrow$ are called the antecedent and succedent. The sequentcalculus again associates with each propositional connective a pair ofrules, this time “left” and “right” rules:

\[\hspace{1em} \begin{prooftree} \def\fCenter{\Lrightarrow} \Axiom$\rA, \rB, \Gamma \fCenter \Delta$ \RightLabel{ $\wedge$(L)} \UnaryInf$\rA \wedge \rB, \Gamma\fCenter \Delta$ \end{prooftree}\hspace{2em} \begin{prooftree} \AxiomC{$\Gamma\Lrightarrow\Theta, \rA$} \AxiomC{$\Gamma\Lrightarrow\Theta, \rB$} \RightLabel{ $\wedge$(R)} \BinaryInfC{$\Gamma\Lrightarrow\Theta, \rA \wedge \rB$} \end{prooftree}\] \[\hspace{-3em} \begin{prooftree} \AxiomC{$\rA, \Gamma\Lrightarrow\Theta$} \AxiomC{$\rB, \Gamma\Lrightarrow\Theta$} \RightLabel{ $\vee$(L)} \BinaryInfC{$\rA \vee \rB, \Gamma\Lrightarrow\Theta$} \end{prooftree}\hspace{2em} \begin{prooftree} \def\fCenter{\Lrightarrow} \Axiom$\Gamma \fCenter \Delta, \rA, \rB$ \RightLabel{ $\vee$(R)} \UnaryInf$\Gamma \fCenter \Delta, \rA \vee \rB$ \end{prooftree}\] \[\hspace{-2em}\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rA$\RightLabel{$\neg\text{(L)}$}\UnaryInf$\neg\rA, \Gamma\fCenter \Theta$\end{prooftree}\hspace{6em}\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\rA, \Gamma\fCenter \Theta$\RightLabel{$\neg\text{(R)}$}\UnaryInf$\Gamma\fCenter \Theta, \neg\rA$\end{prooftree}\] \[\hspace{-3em}\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rA$\Axiom$\rB, \Gamma\fCenter \Theta$\RightLabel{${\supset}\text{(L)}$}\BinaryInf$\rA \supset \rB, \Gamma\fCenter \Theta$\end{prooftree}\hspace{2em}\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\rA, \Gamma\fCenter \Theta, \rB$\RightLabel{${\supset}\text{(R)}$}\UnaryInf$\Gamma\fCenter \Theta, \rA \supset \rB$\end{prooftree}\]

In the sequent calculi, these left/right rules for the propositionalconnectives function alongside another set of rules of structuralreasoning. The classical calculuspk hasseven:

\[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta$\RightLabel{$\text{thinning(L)}$}\UnaryInf$\rD,\Gamma\fCenter \Theta$\end{prooftree}\qquad\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta$\RightLabel{$\text{thinning(R)}$}\UnaryInf$\Gamma\fCenter \Theta, \rD$\end{prooftree}\] \[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\rD, \rD, \Gamma\fCenter \Theta$\RightLabel{$\text{contraction(L)}$}\UnaryInf$\rD, \Gamma\fCenter \Theta$\end{prooftree}\qquad\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rD, \rD$\RightLabel{$\text{contraction(R)}$}\UnaryInf$\Gamma\fCenter \Theta, \rD$\end{prooftree}\] \[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Delta, \rD, \rE, \Gamma\fCenter \Theta$\RightLabel{$\text{exchange(L)}$}\UnaryInf$\Delta, \rE, \rD, \Gamma\fCenter \Theta$\end{prooftree}\qquad\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rE, \rD, \Delta$\RightLabel{$\text{exchange(R)}$}\UnaryInf$\Gamma\fCenter \Theta, \rD, \rE, \Delta$\end{prooftree}\] \[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rD$\Axiom$\rD, \Delta\fCenter \Lambda$\RightLabel{$\text{cut}$}\BinaryInf$\Gamma, \Delta\fCenter \Theta, \Lambda$\end{prooftree}\]

A proof inpk is a finite branching tree builtfrom iterations of these logical and structural rules, each leaf nodeof which is an basic sequent of the form $p_i\Lrightarrow p_i$. Thesequent with which the root node is labeled is called the endsequent.When the endsequent of apk proof has the form$\Lrightarrow \rA$, we write $\turnstile{\PK} \rA$. Gentzen madeseveral observations aboutpk:

$\turnstile{\PK} \rA$ if, and only if, $\turnstile{\CPC} \rA$ if,and only if, $\turnstile{\ND+\sfrac{\neg\neg\rA}{\rA}} \rA$
If one modifiespk by requiring the righthandside of the sequent arrow to have at most one formula and accordinglyrewrites the $\vee(\rR)$ rule as
\[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \rA$\RightLabel{$\vee\text{(R)}$}\UnaryInf$\Gamma\fCenter \rB \vee \rA$\end{prooftree}\qquad\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \rA$\RightLabel{$\vee\text{(R)}$}\UnaryInf$\Gamma\fCenter \rA \vee \rB$\end{prooftree}\]
the resulting calculuspi is such that$\turnstile{\text{PI}} \rA$ if, and only if, $\turnstile{\IPC}\rA$ if, and only if, $\turnstile{\ND+\sfrac{\bot}{\rA}} \rA$,whereipc stands for Heyting’s formaldeduction system for propositional intuitionistic logic and itsequivalents. (Obviously the rules exchange(R) and contraction(R) playno role inpi and can be omitted.)
Cut Elimination Theorem: If one modifiespkandpi simply by removing the rule“cut”, the resulting calculi pk-andpi- are such that $\turnstile{\PK} \rA$if, and only if, $\turnstile{\text{PK-}} \rA$, and$\turnstile{\text{PI}} \rA$ if, and only if,$\turnstile{\text{PI-}} \rA$.
All the formulas that appear anywhere in apk-orpi- proof are subformulas of the formulasthat appear in the endsequent. (This “subformula property”clearly does not hold ofpk andpiproofs.)

Observation 2 provides yet another perspective on the way logicianscould disagree about the validity of principles like the law ofexcluded middle without disagreeing about the meanings of thepropositional connectives. The treatment of $\vee$ and $\neg$ isidentical inpk andpi;the only difference between them is in thebackground structure of reasoning.

Observation 1 allows one immediately to conclude thatpkis complete with respect to the classical truthfunctional interpretation of propositional logic. Gentzen did not drawthis conclusion because he had a different understanding ofcompleteness made possible by the sequent calculus: Because the rule“cut” can be shown to fully capture the general concept oflogical consequence—something Gentzen took himself to havedemonstrated in 1932—, observation 3, that “cut” iseliminable frompk, shows that the left/rightrules for the propositional connectives are complete in the sense thatno logical consequence of formulas provable with them is itselfunprovable with them (see Franks 2010). This way of framingcompleteness has the further advantage thatpican be said to be complete in the same sense.

2.3.3 Constructive completeness ofpk and ofpi

Because of observation 4, however, it is possible to prove thecompleteness ofpk in the usual sense verysimply.

Proof. Let us call a sequent $\Gamma\Lrightarrow \Delta$valid if the formula $\bigwedge\Gamma\supset\bigvee\Delta$ is validon the classical truth-functional interpretation. As one expects, itis easy to check that all the rules ofpkpreserve validity. More surprisingly, the same rules, except forthinning, preserve validity when read backwards. Call such inferencefigures “invertible”. Suppose now that one is given asequent $\Gamma\Lrightarrow \Delta$ containingn logicalconnectives. A straightforward mathematical induction demonstratesthat, if $\Gamma\Lrightarrow \Delta$ is valid, then there is apk-proofof it. Suppose first that $n=0(\Gamma\Lrightarrow \Delta$ contains no logical connectives). Thenthere must be some atom $p_i$ that appears in both its antecedentand its succedent. Obviously $\Gamma\Lrightarrow \Delta$ can beproved from $p_i \rightarrow p_i$ by a series of thinning andexchange inferences. Now with the induction hypothesis that$\Gamma\Lrightarrow \Delta$ is provable when $n=k$, suppose$n=k+1$. Select any formula in $\Gamma\Lrightarrow \Delta$ that isnot atomic and identify its main connective. Suppose, for example,that it is in $\Gamma$ and its main connective is $\supset$. Thenwe can begin building a proof from the bottom up, using$\rA\supset\rB$ as our selected formula and $\Theta$ to stand for$\Gamma$ with the selected occurrence of the formula$\rA\supset\rB$ deleted:

\[\begin{prooftree} \AxiomC{$\Theta \Lrightarrow \Delta, \rA$} \AxiomC{$\rB, \Theta \Lrightarrow \Delta$} \RightLabel{ $\supset$(L)} \BinaryInfC{$\dfrac{\rA \supset \rB, \Theta\Lrightarrow \Delta} {\phantom{\rA \supset \rB,\,}\Gamma\Lrightarrow \Delta}$}\end{prooftree}\kern-5em\lower 1.5em \text{exchange(L)}\]

Because of the invertibility of $\supset$(L) both leafnodes of this tree are labeled with valid sequents containing kconnectives. The induction hypothesis guarantees that they havepk-proofs.Therefore $\Gamma\Lrightarrow \Delta$has apk-proof. An analogous argument appliesfor each connective. In the special case that $\Gamma$ is empty and$\Delta$ contains a single (valid) formula, this construction showsthat $\turnstile{\text{PK-}} \rA$ if$\dturnstile{\CTT}\rA.$ ◻

As was mentioned, Gentzen did not present this very simple version ofthe completeness theorem. Because he was interested in cut-eliminationas an expression of the completeness of his rules, he pursued thatinstead, providing an elaborate proof transformation technique.Knowledge of the completeness ofpk-, though,leads to an alternate verification of cut-elimination: Suppose$\turnstile{\PK} \rA$. Because all basic sequents are valid and allpk rules preserve validity,$\dturnstile{\CTT} \rA$. Butpk- iscomplete, so $\turnstile{\PK\text{-}} \rA$ .

Reflection on the construction implicit in this completeness argumentin fact shows that an arbitrary formula can in this way be tested forvalidity and therefore provides a new decision procedure for classicallogic: The end result of the construction will either be a proof orwill be a tree whose leaf nodes indicate how to construct a falsifyinginterpretation for $\Gamma\Lrightarrow \Delta.$

A version of the same argument applies also topi,not—of course—to show that it iscomplete with respect to its classical truth-functionalinterpretation, but to show that it is complete with respect toanother sort of interpretation based on Kripke frames. The interestingthing about this approach to an analysis of intuitionistic logic isthat one need not have in mind in advance what sort of interpretationone wants to showpi complete with respect to.Just setting out algorithmically to build a cut-freepiproof will either succeed or will indicate thesort of falsifying interpretation that applies in the intuitionisticcase (see Takeuti 1987 [2013]).

3. Non-Classical Interpretations

Classical propositional logic is evidently a valuable framework notonly for organizing principles of reasoning but for providing a fairlysimple setting for showcasing basic theoretical phenomena such ascompleteness, formal consistency, axiomatic independence, and thelike. But a considerable measure of the value of its systematicdevelopment lies in the indications, along the way, of ways to deviatefrom the classical framework and devise alternative interpretations ofthe propositional connectives. We have touched on a few indicationsalready: the independence of the principle of excluded middle from theother axioms in Frege’s formal deduction system, theimplausibility of the material conditional as an analysis of the truthconditions of ordinary indicative mood “if …then”statements, etc. Here we survey some of the most prevalent alternativesystems of propositional logic.

3.1 Multi-valued logics

Already we indicated how truth-functional interpretations with valencegreater than 2 can be utilized to provide independence proofs foraxiom systems. Gödel (1932) defined a sequence$\{S_n\}_{n=2}^\infty$ ofn-valued logics that generalize theclassical interpretation:

\[\begin{align} v(\neg\rA) &= \begin{cases} 0 & v(\rA) = n-1\\ n-1 & \text{otherwise} \end{cases}\\ v(\rA\wedge\rB) &= \mathbf{max}\{v(\rA),v(\rB)\}\\ v(\rA\vee\rB) &= \mathbf{min}\{v(\rA),v(\rB)\}\\ v(\rA\supset\rB) &= \begin{cases} v(\rB) & v(\rA) <v(\rB)\\ 0 & \text{otherwise} \end{cases}\\ v(\bot) &= n-1\end{align}\]

with $\dturnstile{S_n}\rA$ if $v(\rA) = 0$ for all assignments ofvalues from $\{0, 1, \ldots, n-1\}$ to atomic formulas.

$S_2$ is just the classical theory of truth. $S_3$ was used aboveto demonstrate the independence of Frege’s fifth axiom.Gödel used the whole sequence in a demonstration thatintuitionistic logic is not complete with respect to any finite-valuedtruth-functional interpretation.

Beyond such utilitarian roles, multi-valued logics have attractedinterest in their own right. Important examples are the (strong andweak) Kleene 3-valued logics, which are meant to assign truth valuesto propositions about partial recursive functions. Other 3-valuedlogics have been proposed as improvements on the material conditionalas interpretations of indicative mood conditionals (see Cobreros et al2014). 4-valued logics have been used to model computation ondatabases containing conflicting information—here the valuescorrespond with the information states “true”,“false”, “both”, and “neither”(see Belnap 1977). Graham Priest 1992 has applied the same frameworkin the development of a system of relevance logic, again offering animproved formalization of conditional language.

Another important class of multi-valued logics are theinfinitely-valued “fuzzy logics”. These have been used inorder to provide an analysis of propositions with vague terms, whichcan be thought of as admitting degrees of truth.

3.2 Constructive logics

We have already noted that simply rejecting thelemleads to a subtle deviation from the classicalinterpretation: The classical truth functional interpretation fallsaway, but the inferential definition of the connectives evident innatural deduction can be preserved. The intuitionistic propositionalcalculusipc has been studied in great depth.Among its prominent features are:

1. The “disjunction property”: the fact that$\turnstile{\IPC} \rA\vee\rB$ only if either $\turnstile{\IPC}\rA$ or $\turnstile{\IPC} \rB$. Gödel (1932, 1933a) containthe first observations thatipc has thedisjunction property. The first recorded proof is in Gentzen1934–35, where it is a trivial consequence of cut eliminationforpi: The only way api-proof can have the endsequent $\Lrightarrow\rA\vee\rB$ is for the last inference to be a thinning(R) or$\vee(\rR)$. If the inference were thinning(R), then the previoussequent would be $\Lrightarrow$. Becausepiis consistent, that is impossible. Therefore, the previous sequentmust either be $\Lrightarrow \rA$ or $\Lrightarrow \rB$.

At one time it was conjectured thatipc can becharacterized as the strongest propositional logic with thedisjunction property (an example of a weaker logic isJohansson’smpc, corresponding to thepure system of natural deductionnd). In 1957,Kreisel and Putnam studied the “independence of premises(IndPrem)” inference

\[\begin{prooftree}\AxiomC{$\neg\rA\supset(\rB\vee\rC)$}\UnaryInfC{($\neg\rA\supset\rB)\vee(\neg\rA\supset\rC)$}\end{prooftree}\]

and observed that

\[\neg\rA\supset(\rB\vee\rC)\centernot{\turnstile{\IPC}} (\neg\rA\supset\rB)\vee(\neg\rA\supset\rC)\]

although the logickp =ipc+IndPremalso has the disjunction property. Todayit is known that there are infinitely many distinct logical systemsintermediate in strength betweenipc andcpc,and that infinitely many of them have thedisjunction property.

2. The failure of truth-functionality: The intuitive understanding ofintuitionism is to replace the idealistic concept of truth with thenotion of having been constructively verified. Some authors suggestedthat 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, anda third value indicating that neither of these is the case. This seemsat least to accord withipc’s rejectionoflem. However, because there are only asmall number of 3-valued semantic environments, others were able torule out this possibility case-by case. This led to speculation thatthe right semantics might have valence 4 or possibly 5.Gödel’s 1932 proof rules out all truth-functionalinterpretations of any finite valence.

Because of the failure of truth-functionality, a new framework forunderstandingipc validity is needed. Adequatetopological, algebraic, and Kripke-frame semantics have beenintroduced, and completeness results demonstrating a correspondencebetween these frameworks and various proof systems abound. We havealready indicated that the completeness argument for theintuitionistic sequent calculuspi withrespect to Kripke frames is a variation of the simple constructivecompleteness theorem forpk with respect tothe classical theory of truth. Again, the argument shows thatpiis decidable: Given a formula A, the algorithmeither returns api-proof of A or a falsifyingKripke frame.

There is also an informal, intuitive understanding ofipctheoremhood called the BHK interpretation.According to this interpretation, the disjunction property is a formalanalogue of the definition of the $\vee$ symbol: To have a proof of$\rA\vee\rB$ just means that either $\rA$ or $\rB$ has beenproved. In a similar fashion, to have a proof of $\rA\wedge\rB$means that both $\rA$ and $\rB$ have been proved; a proof of$\rA\supset\rB$ is a construction that allows any proof of A to betransformed into a proof of B; a proof of $\neg\rA$ is aconstruction that allows any proof of A to be transformed into a proofof $\bot$. In this specification of the meanings of the connectives,“provability” refers to informal provability by any meanswhatsoever, rather than to formal provability within a specificsystem.

Because the BHK interpretation specifies, not what expressions like$\rA\vee\rB$ and $\rA\supset\rB$ mean, but what it means to saythat such expressions are provable, the $\supset$ connective istypically referred to in the intuitionistic setting as the“implication” operator. This is sometimes misread as adisagreement with the classical distinction between the conditionalconnective and the implication relation. But as we have seen, on theclassical conception, too, the expression $\vdash \rA\supset\rB$represents implication, i.e., truth of the conditional claim on everyassignment. On the intuitionistic conception, however, the connectivesare understood primitively in terms of what it means for expressionsgoverned by them to be provable. The same conception figures into theunderstanding of connectives in relevance logic, where again$\supset$ is typically described as an implication operator (and itsclassical treatment is faulted for engendering the “paradoxes ofmaterial implication”, not the “paradoxes of materialconditionalization”.)

3. A striking feature ofipc is the presenceof inference rules like IndPrem that are not derivable

\[\neg\rA\supset(\rB\vee\rC) \centernot{\turnstile{\IPC}} (\neg\rA\supset\rB)\vee(\neg\rA\supset\rC)\]

but that nevertheless preserve the property ofipc-provability.Other examples of such rulesare

\[ \begin{prooftree} \AxiomC{$(\rA\supset\rB)\supset (\rA\vee\rC)$} \RightLabel{ Mints’s rule} \UnaryInfC{(($\rA\supset\rB)\supset\rA)\vee((\rA\supset\rB)\supset\rC)$}\end{prooftree}\] \[\begin{prooftree} \AxiomC{$(\neg\neg\rA\supset\rA)\supset (\neg\neg\rA\vee\neg\rA)$} \RightLabel{ Rose’s rule} \UnaryInfC{$\neg\neg\rA\vee\neg\rA$}\end{prooftree}\]

Is it right to say that such rules are valid patterns ofintuitionistic inference? The question is ambiguous in a way thatexperience with classical logic desensitizes one to. For it can beshown that any rule that preserves the property of being a classicalvalidity is also derivable incpc itself. Thefact that the rules under whose application the set ofipctheorems is closed properly extends theipc-derivablerules leads to a new concept: theformer rules are called “admissible”. The intuitionsiticstudy of propositional logic thereby reveals a fundamental distinctionin the basic concept of deductive validity, between a rule licensinglegitimate inferences from theorems and it applying also to arbitraryhypotheses.

Because the primitive understanding of logical connectives from theintuitionist perspective is in terms of the conditions of theprovability of statements containing them, one might, and many authorshave, maintained that admissibility is the proper precisification ofthe concept of deductive validity foripc. Onthe other hand, what distinguishesipc frommpc is the derivability of the ruleexfalso quodlibet. That rule (as well as the disjunctive syllogism)is admissible already inmpc, so the decisionto include it explicitly as a derivable inference inipcindicates some recognition of the importance ofderivability. What can be said definitely is that the distinctionbetween derivability and admissibility is important in constructivelogics in a way that it is not incpc.

4. Three of the De Morgan inferences are derivable inipc,but the inference$\frac{\neg(\rA\wedge\rB)}{\neg\rA\vee\neg\rB}$ is not.ipctherefore serves as a background theory fromwhich the strength of this inference can be measured. One mightconjecture thatipc+$\frac{\neg(\rA\wedge\rB)}{\neg\rA\vee\neg\rB}$is fully classical, but in fact this system still does not provelem.It does, however, prove the so-called weak lawof excluded middle (wlem):$\neg\rA\vee\neg\neg\rA$. Moreover, all De Morgan’s inferencesare derivable inipc+wlem,so thatwlem and$\frac{\neg(\rA\wedge\rB)}{\neg\rA\vee\neg\rB}$ can be said to beequivalent over the base theoryipc. The logicipc+$\frac{\neg(\rA\wedge\rB)}{\neg\rA\vee\neg\rB}$,sometimes called De Morgan logic or Jankov’s logic, occupies aunique place in the hierarchy of systems intermediate in strengthbetweenipc andcpc.It has a natural realization in the Medvedev lattice of degrees ofsolvability. The setting is Baire space $\omega^\omega$ (the set offunctions from $\omega$ to $\omega$) and the problem of producingan element of a given subset of this space. Subsets of Baire space arecalled mass problems, and their elements are called solutions. Onemass problem is said to reduce to another if there is an effectiveprocedure for transforming solutions of the second into solutions ofthe first. If one defines the lattice $\calM$ of degrees ofreducibility of mass problems, the set of identities of $\calM$corresponds to the set of theorems De Morgan logic (Sorbi 1991), sothat the theory of mass problems provides a constructiveinterpretation of this logic. (This is like a constructive analogue tothe way switching circuits are a realization ofcpc.)Unlikeipc, however,no rule admissible in De Morgan logic is underivable (Prucnal 1976).Thus one sees thatwlem, standing in the placeof fulllem, allows for a constructiveinterpretation without exhibiting underivable admissible rules.

5. We have observed how the Gentzen calculi highlight certainrelationships betweenipc andcpc.Translation schemes of Kolmogorov, Glivenko,Gödel, and Gentzen make evident other relationships between theseand other systems. We begin with a result of Valérii Glivenko(1929):

Theorem 6.If $\turnstile{\CPC}\rA$, then$\turnstile{\IPC}\neg\neg\rA$.

Proof. First observe three simple facts aboutnd+$\frac{\bot}{\rA}$,the natural deductionequivalent ofipc:

\[\tag*{V1}\turnstile{\ND+\sfrac{\bot}{\rA}}\neg\neg(\rB\vee\neg\rB) \]

\[\tag*{V2}\neg\neg\rB\turnstile{\ND+\sfrac{\bot}{\rA}+ (\rC\vee\neg\rC)}\rB \]

\[\tag*{V3}\neg\neg\neg\rB\turnstile{\ND+\sfrac{\bot}{\rA}}\neg\rB \]

For the proof of the main theorem, suppose $\turnstile{\CPC}\rA$.Then byV2 we have $\turnstile{\ND+\sfrac{\bot}{\rA}+ (\rC\vee\neg\rC)}\rA$,hence a proof innd+$\frac{\bot}{\rA}$+$(\rC\vee\neg\rC)$:

\[\begin{prooftree} \AxiomC{$\text{P}_{1}\vee\neg\text{P}_{1}$} \noLine \UnaryInfC{$\ddots$} \AxiomC{$\text{P}_{2}\vee\neg\text{P}_{2}$} \noLine \UnaryInfC{$\ddots$} \AxiomC{$\cdots$} \noLine \UnaryInfC{$\iddots$} \AxiomC{$\text{P}_{k}\vee\neg\text{P}_{k}$} \noLine \UnaryInfC{$\iddots$} \noLine \QuaternaryInfC{$\rA$}\end{prooftree} \]

ByV1, there existnd+$\frac{\bot}{\rA}$proofs:

\[\begin{prooftree} \AxiomC{$\ddots$} \AxiomC{$\iddots$} \noLine \BinaryInfC{$\neg\neg (\text{P}_{1}\vee\text{P}_{1}$)}\end{prooftree}\qquad\begin{prooftree} \AxiomC{$\ddots$} \AxiomC{$\iddots$} \noLine \BinaryInfC{$\neg\neg (\text{P}_{2}\vee\text{P}_{2}$)}\end{prooftree} \ldots\begin{prooftree} \AxiomC{$\ddots$} \AxiomC{$\iddots$} \noLine \BinaryInfC{$\neg\neg (\text{P}_{k}\vee\text{P}_{k}$)}\end{prooftree}\]

From these pieces one can construct and+$\frac{\bot}{\rA}$proof:

This proof is built by placing each of the proof figures indicated above on the left side of each of the binary inferences. Each binary inference is a negation elimination, and each subsequent unary inference is a negation introduction.

That completes the proof of the main theorem. ◻

We observe two corollaries:

V4: If $\turnstile{\CPC}\neg\rA$, then $\turnstile{\IPC}\neg\rA$.
This follows immediately from the main theorem andV3.
V5: cpc is inconsistent only ifipcis.
For ifcpc is inconsistent, then there is aformula $\rA$ such that $\turnstile{\CPC}\rA$ and$\turnstile{\CPC}\neg\rA$. But then $\turnstile{\IPC}\neg\neg\rA$and $\turnstile{\IPC}\neg\rA$.

Glivenko’s theorem provides a simple translation $t_\rV$ ofclassical logic into intuitionistic logic defined by $t_\rV (\rA) =\neg\neg\rA$ for all formulas A. It is a translation in the sensethat $\turnstile{\CPC}\rA$ if, and only if,$\turnstile{\IPC}t_\rV(\rA$). This translation is limited in that itdoes not extend to quantification theory. Kolmogorov (1925) provided avariation $t_\rK$ as follows:

$t_\rK(p)$ is $\neg\neg p$, for all propositionalvariables
$t_\rK(\neg\rA)$ is $\neg t_\rK(\rA)$
$t_\rK(\rB\wedge\rC)$ is $\neg\neg(t_\rK(\rB)\wedget_\rK(\rC))$
$t_\rK (\rB\vee\rC)$ is $\neg\neg (t_\rK(\rB)\vee\t_\rK(\rC))$
$t_\rK(\rB\supset\rC)$ is $\neg\neg (t_\rK(\rB)\supsett_\rK(\rC)$

The Gödel/Gentzen (1933) translation $t_\rG$ is defined by:

$t_\rG(p)$ is $\neg\neg p$, for all propositionalvariables
$t_\rG(\neg\rA)$ is $\neg t_\rG(\rA)$
$t_\rG(\rB\wedge\rC)$ is $t_\rG(\rB)\wedge t_\rG(\rC)$
$t_\rG (\rB\vee\rC)$ is $\neg (\neg t_\rG(\rB)\wedge\negt_\rG(\rC))$
$t_\rG(\rB\supset\rC)$ is $t_\rG(\rB)\supset t_\rG(\rC)$

It is easy to show that $\turnstile{\CPC}\rA$ if, and only if,$\turnstile{\IPC}t_\rK(\rA$) if, and only if,$\turnstile{\IPC}t_\rG(\rA$). Unlike $t_\rV$, the schemes ofKolmogorov and of Gödel/Gentzen can be extended to quantifiers.The latter can be further extended to theories of arithmetic and toset theory (see Troelstra & van Dalen 1988).

In 1933b, Gödel provided similar translation fromipcto the modal logicS4.S4 iscpcsupplemented with a new primitive symbol$\Box$ so that, if A is a formula, then $\Box\rA$ is a formula, anew rule of inference

$\dfrac{\rA}{\Box\rA}$

and three new axioms

$\Box\rA\supset\rA$
$\Box\rA\supset (\Box (\rA\supset\rB)\supset\Box\rB)$
$\Box\rA\supset\Box\Box\rA$

Gödel defined a translation $t_\Box$ of formulas fromipcinto the language ofS4by:

$t_\Box(\neg\rA) \text{ is } \Box\neg\Box t_\Box(\rA)$
$t_\Box(\rA\supset\rB) \text{ is } \Box t_\Box(\rA)\supset\Boxt_\Box(\rB)$
$t_\Box(\rA\vee\rB) \text{ is } \Box t_\Box(\rA)\vee\Boxt_\Box(\rB)$
$t_\Box(\rA\wedge\rB) \text{ is } \Box t_\Box(\rA)\wedge\Boxt_\Box(\rB)$

and stated, without proof:

\[\turnstile{\IPC}\rA \text{ if, and only if, }\turnstile{\text{S4}} t_\Box(\rA).\tag{*}\]

Gödel further declared both that “the translation of$\rA\vee\neg\rA$ is not derivable inS4”and also that “neither ingeneral is any formula of the form $\Box\rA\vee\Box\rB$ for whichneither $\Box\rA$ nor $\Box\rB$ is already provable inS4”:

\[\turnstile{\text{S4}}\Box\rA\vee\Box\rB\text{ only if either }\turnstile{\text{S4}}\Box\rA\text{ or }\turnstile{\text{S4}}\Box\rB\tag{**}\]

(*) and (**) together obviously entail the disjunction property foripc.

3.3 Relevance and connexive logics

Returning to the problem of approximating natural languageexpressions, some writers have proposed overcoming the apparentinadequacies of the material conditional by stipulating strongerconditions on the truth of propositions of the form $\rA\supset\rB$.Relevance logicians suggest that many of the features exhibited by thematerial conditional that seem like departures from speakers’intuitions about the truth of conditional expressions stem fromascriptions of truth to conditionals whose antecedents are irrelevantto their consequents. As a formal measure to ensure relevance, theypropose a “variable sharing condition”. Variable sharingis generally thought to be only a necessary condition for relevance,however, and the project of describing sufficient formal conditions isongoing.

Connexive logicians aim instead to make good of the intuition that fora conditional statement to be true, the negation of its consequentshould be incompatible with its antecedent. This requirement on thetruth of conditional statements has a formidable history, appearing inlogical manuscripts of the Stoic philosophers Chrysippus and SextusEmpiricus and evidently garnering more support at the time than thecontrary opinion of Philo of Melaga. A related idea appears already inthePrior Analytics, where Aristotle claimed that it isimpossible that if not A, then A. This, “Aristotle’sthesis”, can be formalized as $\neg (\neg\rA\supset\rA)$,which is obviously invalid both classically and intuitionistically.Sometimes instead the formula $\neg (\rA\supset\neg\rA)$ is calledAristotle’s thesis. Systems of connexive logic accept both asaxioms, as well as the principles$(\rA\supset\rB)\supset\neg(\rA\supset\neg\rB)$ and$(\rA\supset\neg\rB)\supset\neg(\rA\supset\rB)$, which purport toformalize the original idea attributed to Chrysippus above. (Theselatter two principles are interderivable, over the base theoryipc,with Aristotle’s theses).

By including as theorems principles that are classically invalid, suchlogics risk trivialization because of the maximality ofcpc.Some approaches address this problem byrejecting classical principles such as the $\wedge$-elimination ruleof natural deduction, avoiding thereby any formula and its negationbeing theorems. Other approaches are “paraconsistent”,i.e., they allow theorems A and $\neg\rA$ but do not allow thederivation of arbitrary formulas from this contradiction.Paraconsistent approaches are often interpretable with the 4-valuedtruth-assignment mentioned above.

3.4 Linear logic

If many departures from the classical framework are motivated bywanting to study connectives that more closely approximate the truthconditions of ordinary language expressions, linear logic (introducedin Girard 1987) can be thought of as a push in the opposite direction.Just as Frege saw logical significance in the material conditionaldespite (maybe even because of) its lack of correspondence withordinary “if …then” statements for reasons internalto logical theory, linear logic can be thought of as an attempt todiscover in the fine structure of formal logic those propositionalconnectives that play specific inference-tracking roles that ordinaryexpressions might be too crude to articulate.

We saw earlier how in the sequent calculus classical andintuitionistic logic differ not in the inference rules governing thepropositional connectives but in the background structure ofreasoning—specifically, in the presence or absence of multipleformulas in succedents. Linear logic analyzes this relationshipfurther through adjustments to other structural aspects of reasoning.It is well known that the operational rules ofpkcan be written either in a“context-sharing” or “context-independent”form. The operational rules were given a context-sharing presentationabove, but for example the rule

\[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rA$\Axiom$\rB, \Gamma\fCenter \Theta$\RightLabel{${{\supset}\text{(L)-cs}}$}\BinaryInf$\rA \supset \rB, \Gamma\fCenter \Theta$\end{prooftree}\]

could instead be given a context-independent presentation:

\[\begin{prooftree} \def\fCenter{\Lrightarrow}\Axiom$\Gamma\fCenter \Theta, \rA$\Axiom$\rB, \Delta\fCenter \Lambda$\RightLabel{${\supset}\text{(L)-ci}$}\BinaryInf$\rA \supset \rB, \Gamma, \Delta\fCenter \Lambda, \Theta$\end{prooftree}\]

The equivalence of these presentations is easy to verify:

\[\xlongequal[{\Large \rA \,\supset\, \rB, \Gamma \,\Lrightarrow\, \Theta}]{\Large \begin{prooftree} \def\fCenter{\Lrightarrow} \Axiom$\Gamma\fCenter \Theta, \rA$ \Axiom$\rB, \Gamma\fCenter \Theta$ \BinaryInf$\rA \,\supset\, \rB, \Gamma, \Gamma \fCenter \Theta, \Theta$ \end{prooftree} }\raise 1.6em {{\supset}\text{(L)-ci}}\kern -3.5em \text{\}exchanges and contractions}\] \[\frac{ \xlongequal[{\Large \Gamma,\Delta \,\Lrightarrow\, \Lambda,\Theta,\rA}]{{\Large \Gamma \,\Lrightarrow\, \Theta,\rA}} \text{\}thinnings and exchanges\{} \xlongequal[{\Large\rB,\Gamma, \Delta \,\Lrightarrow\, \Lambda,\Theta}]{{\Large \rB, \Delta \,\Lrightarrow\, \Lambda}} }{ \rA \supset \rB, \Gamma, \Delta \,\Lrightarrow\, \Lambda, \Theta}{\supset}\text{(L)-cs}\]

but we see that their equivalence depends on the presence of thestructural rules thinning and contraction.

In propositional linear logic, there are two conjunction-likeoperators, $\otimes$ and $\amp$, and two disjunction-likeoperators $\oplus$ and $\parr$. $\oplus$ is given acontext-sharing left rule and a right rule with “built-inthinning” like the intuitionistic version of $\vee(\rR)$.$\parr$ is its structural dual: its left rule is context-independentand its right rule is just like the classical $\vee(\rR)$.Similarly, $\otimes(\rR)$ is context-independent and $\otimes$(L)is just like the classical $\wedge$(L), whereas $\&(\rR)$ iscontext-sharing and $\&$(L) has built in thinning. Theconnectives $\&$ and $\oplus$ with context-sharing rules arecalled “additives”; $\otimes$ and $\parr$ withcontext-independent rules are called “multiplicatives”.But there are no structural rules for thinning and contraction, so theadditive and multiplicative rules are not equivalent.

Disambiguating the logical conjunction and disjunction into additiveand multiplicative versions lends great perspicuity to therelationship between classical and intuitionistic logic. For example,there are two versions oflem. The additiveversion $\rA\oplus\neg\rA$ can be thought of as based on theintuitionsitic disjunction: Since neither of its disjuncts isprovable, neither is it. The multiplicative version$\rA\parr\neg\rA$, on the other hand, corresponds to the classicalunderstanding and is readily provable (“linearimplication” $\rA\multimap\rB$ is defined as$\neg\rA\parr\rB$, so the multiplicativelemcorresponds with the linear identity $\rA\multimap\rA$).

In the absence of contraction and weakening, formulas of linear logicstand for something more like resources than permanent statements orconstructions. Just as intuitionistic logic replaced the classicalunderstanding of a conditional $\rA\supset\rB$ “either A isfalse or B is true” with a procedural claim “Given A, Ican produce B”, linear logic is able to distinguish claims“Given one copy of A, I can produce one copy of B” from“Given three copies of A, I can produce one copy of B”.This allows modeling of propositions about resource use incomputation, and much of the attention directed towards linear logichas arisen because of its natural realization in computational modelssuch as Petri nets.

The fragment of linear logic presented so far is calledmall(for multiplicative/additive linear logic). Inorder to preserve its distinctive properties but also be able toexpress claims interpretable as, for example, the intuitionisticimplication, the linear modalities are introduced. These are unaryconnectives for which restricted forms of weakening and contractionapply. They are called “modalities” for a reason, though:They are governed by the same left and right rules as the necessityand possibility operators of modal logicS4.This makes it unclear whether full linearlogicll with their inclusion qualifies as apropositional logic.

This is no fault of linear logic, but rather one of its maincontributions to the study of propositions. As stressed in theintroduction to this article, a helpful attitude for the developmentof propositional logic is to bracket questions about the nature ofpropositions and simply require that the propositional connectivesreturn expressions of the same order as those they operate on. Fromthis perspective, the idea of “persistent factual truth”or “reusable construction”, which is the basic startingpoint of classical and intuitionistic logic, is related to linearlogic’s basic unit of “limited resource” just as themodalities “necessary truth” and “possibletruth” are related to the category of “persistent factualtruth” or “reusable construction”.

Bibliography

References

Belnap, Nuel D., 1977, “A Useful Four-Valued Logic”,inModern Uses of Multiple-Valued Logic, J. Michael Dunn andGeorge Epstein (eds.), Dordrecht/Boston: D. Reidel, 5–37.doi:10.1007/978-94-010-1161-7_2
Bernays, Paul, 1926, “Axiomatische Untersuchung desAussagen-Kalkuls derPrincipia Mathematica”,Mathematische Zeitschrift, 25: 305–320.doi:10.1007/BF01283841
Cook, Stephen A., 1971, “The Complexity of Theorem-ProvingProcedures”, inProceedings of the Third Annual ACMSymposium on Theory of Computing, New York: ACM Press,151–158. doi:10.1145/800157.805047
Cobreros, Pablo, Paul Égré, David Ripley, and Robertvan Rooij, 2014, “Foreword: Three-Valued Logics and TheirApplications”,Journal of Applied Non-Classical Logics,24(1–2): 1–11. doi:10.1080/11663081.2014.909631
Church, Alonzo, 1936, “An Unsolvable Problem of ElementaryNumber 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 (Beforeand After Herbrand)”,History and Philosophy of Logic,42(2): 129–159. doi:10.1080/01445340.2021.1889117
Frege, Gottlob, 1879,Begriffsschrift, eine der arithmetischennachgebildete Formelsprache des reinen Denkens, Halle: L. Nebert.Translated asConceptual Notation: a formula language of purethought modeled upon the formula language of arithmetic in Frege1972:: 101–208.
–––, 1910 [1980], “Letter toJourdain”, translated and reprinted in hisPhilosophical andMathematical Correspondence, G. Gabriel, et al. (eds.), Chicago:University of Chicago Press, 1980.
–––, 1972,Conceptual Notation, and RelatedArticles, Terrell Ward Bynum (trans.), Oxford: ClarendonPress.
Gentzen, Gerhard, 1932, “Über die Existenzunabhängiger Axiomensysteme zu unendlichen Satzsystemen”,Mathematische Annalen 107: 329–50. Translated as“On the Existence of Independent Axiomsystems for InfiniteSentence Systems”, in Gentzen 1969: 29–52.doi:10.1007/BF01448897 (de)
–––, 1934–35, “Untersuchungenüber das logische Schließen”, Gentzen’sdoctoral thesis at the University of Göttingen, translated as“Investigations into Logical Deduction”, in Gentzen 1969:68–131.
–––, 1969,The Collected Papers of GerhardGentzen, M. E. Szabo (ed.), (Studies in Logic and the Foundationsof 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 lalogique 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 derAxiome des logischen Funktionenkalküls”,Monatsheftefür Mathematik und Physik, 37: 349–360. Translated byS. Bauer-Mengelberg as “The completeness of the axioms of thefunctional calculus of logic” reprinted in Gödel 1986:102–23. doi:10.1007/BF01696781
–––, 1932 [1986], “Zum intuitionistischenAussagenkalkül”,Anzeiger der Akademie derWissenschaftischen in Wien, 69: 65–66. Translated by J.Dawson as “On the intuitionistic propositional calculus”,in Gödel 1986: 223–25.
–––, 1933a [1986], “Eine Interpretationdes intuitionistischen Aussagenkalküls”,Ergebnisseeines mathematischen Kolloquiums, 4: 39–40. Translated as“An Interpretation of the Intuitionistic PropositionalCalculus”, in Gödel 1986: 301–302.
–––, 1933b [1986], “Zur intuitionistischenArithmetik und Zahlentheorie”,Ergebnisse einesmathematischen Kolloquiums, 4: 34–38. Translated as“On Intuitionistic Arithmetic and Number Theory”, inGödel 1986: 287–295.
–––, 1986,Collected Works, Volume I:Publications 1929–1936, Solomon Feferman, John W. DawsonJr, Stephen C. Kleene, Gregory H. Moore, Robert M. Solovay, and Jeanvan Heijenoort (eds.), Oxford/New York: Clarendon Press.
Herbrand, Jacques, 1930,Recherches sur la théorie dela démonstration, Herbrand’s doctoral thesis at theUniversity 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],ÉcritsLogigues, Jean van Heijenoort (ed.), (Bibliothèque dePhilosophie Contemporaine. Logique et Philosophie Des Sciences),Paris: Presses universitaires de France. Translated asLogicalWritings, Warren D. Goldfarb (trans.), Dordrecht, Holland: D.Reidel, 1971.
Hilbert, David, 2013,David Hilbert’s Lectures on theFoundations of Arithmetic and Logic 1917–1933 (DavidHilbert’s Lectures on the Foundations of Mathematics andPhysics, 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 dertheoretischen Logik, (Die Grundlehren der mathematischenWissenschaften 27), Berlin: J. Springer.
Johansson, Ingebrigt, 1937, “Der Minimalkalkül, einreduzierter Intuitionistischer Formalismus”,CompositioMathematica, 4: 119–136. [Johansson 1937 available online]
Kalmár, László, 1935, “Über dieAxiomatisierbarkeit des Aussagenkalküls”,ActaScientiarum Mathematicarum, 7(4): 222–43.
Kolmogorov [Kolmogoroff], Andrey N., 1925 [1967], “Опринцип tertium nondatur”,Matematicheskii Sbornik, 32(4): 646–667.Translated as “On the Principle of Excluded Middle”, inFrom Frege to Gödel A Source Book in Mathematical Logic,1879–1931, Jean van Heijenoort (ed.), Cambridge, MA: HarvardUniversity Press, 1967, 416–437.
Kreisel, Georg and Hilary Putnam, 1957, “EineUnableitbarkeitsbeweismethode für den IntuitionistischenAussagenkalkül”,Archiv für Mathematische Logikund Grundlagenforschung, 3(3–4): 74–78.doi:10.1007/BF01988049
Lewis, David, 1976, “Probabilities of Conditionals andConditional Probabilities”,The Philosophical Review,85(3): 297–315. doi:10.2307/2184045
Lincoln, Patrick, John Mitchell, Andre Scedrov, and NatarajanShankar, 1992, “Decision Problems for Propositional LinearLogic”,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 ofPrimitive Propositions of Logic”,Proceedings of theCambridge Philosophical Society, 19: 32–41.
Post, Emil L., 1921, “Introduction to a General Theory ofElementary Propositions”,American Journal ofMathematics, 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 ofMedvedev’s Propositional Calculus”,Reports onMathematical Logic, 6: 103–105.
Quine, W. V. O., 1955, “A Way to Simplify TruthFunctions”,The American Mathematical Monthly, 62(9):627–631. doi:10.1080/00029890.1955.11988710
–––, 1982,Methods of Logic, fourthedition, 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 ResearchCenter.
Schröder, Ernst, 1890,Vorlesungen über die Algebrader Logik (exakte Logik), volume 1, Leipzig: B. G. Teubner.Reprinted 1966, New York: Chelsea.
Shannon, Claude Elwood, 1940, “A Symbolic Analysis of Relayand Switching Circuits”, Thesis (M.S.), Massachusetts Instituteof Technology, Dept. of Electrical Engineering. [Shannon 1940 available online]
Sheffer, Henry Maurice, 1913, “A Set of Five IndependentPostulates for Boolean Algebras, with Application to LogicalConstants”,Transactions of the American MathematicalSociety, 14(4): 481–488.doi:10.1090/S0002-9947-1913-1500960-1
Sorbi, Andrea, 1991, “Some Quotient Lattices of the MedvedevLattice”,Zeitschrift für Mathematische Logik undGrundlagen der Mathematik, 37(9–12): 167–182.doi:10.1002/malq.19910370905
Takeuti, Gaisi, 1987 [2013],Proof Theory, secondedition, (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 dieBegriffe der ω-Widerspruchsfreiheit und derω-Vollständigkeit”,Monatshefte fürMathematik und Physik, 40(1): 97–112.doi:10.1007/BF01708855
Troelstra, A. S. and D. van Dalen, 1988,Constructivism inMathematics, Volume 1: An Introduction, (Studies in Logic and theFoundations of Mathematics 121), Amsterdam: North-Holland.
Turing, A. M., 1936, “On Computable Numbers, with anApplication to the Entscheidungsproblem”,Proceedings of theLondon Mathematical Society, series 2, 42(1): 230–265.doi:10.1112/plms/s2-42.1.230
Urquhart, Alasdair, 1984, “The Undecidability of Entailmentand 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.

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

[Please contact the author with suggestions.]

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

input	\(\langle\bT, \bT\rangle\)	\(\langle\bT, \bF\rangle\)	\(\langle\bF, \bT\rangle\)	\(\langle\bF, \bF\rangle\)
\(f_1^2\)	\(\bT\)	\(\bT\)	\(\bT\)	\(\bT\)
\(f_2^2\)	\(\bT\)	\(\bT\)	\(\bT\)	\(\bF\)
\(f_3^2\)	\(\bT\)	\(\bT\)	\(\bF\)	\(\bT\)
\(f_4^2\)	\(\bT\)	\(\bT\)	\(\bF\)	\(\bF\)
\(f_5^2\)	\(\bT\)	\(\bF\)	\(\bT\)	\(\bT\)
\(f_6^2\)	\(\bT\)	\(\bF\)	\(\bT\)	\(\bF\)
\(f_7^2\)	\(\bT\)	\(\bF\)	\(\bF\)	\(\bT\)
\(f_8^2\)	\(\bT\)	\(\bF\)	\(\bF\)	\(\bF\)
\(f_9^2\)	\(\bF\)	\(\bT\)	\(\bT\)	\(\bT\)
\(f_{10}^2\)	\(\bF\)	\(\bT\)	\(\bT\)	\(\bF\)
\(f_{11}^2\)	\(\bF\)	\(\bT\)	\(\bF\)	\(\bT\)
\(f_{12}^2\)	\(\bF\)	\(\bT\)	\(\bF\)	\(\bF\)
\(f_{13}^2\)	\(\bF\)	\(\bF\)	\(\bT\)	\(\bT\)
\(f_{14}^2\)	\(\bF\)	\(\bF\)	\(\bT\)	\(\bF\)
\(f_{15}^2\)	\(\bF\)	\(\bF\)	\(\bF\)	\(\bT\)
\(f_{16}^2\)	\(\bF\)	\(\bF\)	\(\bF\)	\(\bF\)

input	\(\star\)
\(\langle\)T,T,T\(\rangle\)	T
\(\langle\)T,T,F\(\rangle\)	T
\(\langle\)T,F,T\(\rangle\)	F
\(\langle\)T,F,F\(\rangle\)	F
\(\langle\)F,T,T\(\rangle\)	F
\(\langle\)F,T,F\(\rangle\)	T
\(\langle\)F,F,T\(\rangle\)	F
\(\langle\)F,F,F\(\rangle\)	F

Movatterモバイル変換