Movatterモバイル変換

[0]ホーム
URL:

Jump to content
WikipediaThe Free Encyclopedia
Search

Propositional logic

From Wikipedia, the free encyclopedia
(Redirected fromSentential logic)
Branch of logic
Not to be confused withPropositional analysis.

Propositional logic is a branch oflogic.[1][2] It is also calledstatement logic,[1]sentential calculus,[3]propositional calculus,[4][a]sentential logic,[5][1] or sometimeszeroth-order logic.[b][7][8][9] Sometimes, it is calledfirst-order propositional logic[10] to contrast it withSystem F, but it should not be confused withfirst-order logic. It deals withpropositions[1] (which can betrue or false)[11] and relations between propositions,[12] including the construction of arguments based on them.[13] Compound propositions are formed by connecting propositions bylogical connectives representing thetruth functions ofconjunction,disjunction,implication,biconditional, andnegation.[14][15][16][17] Some sources include other connectives, as in the table below.

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

Propositional logic is typically studied with aformal language,[c] in which propositions are represented by letters, which are calledpropositional variables. These are then used, together with symbols for connectives, to makepropositional formulas. Because of this, the propositional variables are calledatomic formulas of a formal propositional language.[15][2] While the atomic propositions are typically represented by letters of thealphabet,[d][15] there is a variety of notations to represent the logical connectives. For the benefit of readers who may only be used to a different variant notation for the logical connectives, the following table shows the main notational variants for each of the connectives in propositional logic. Other notations have been used historically, such asPolish notation. For the history of each of these symbols, see the respective articles as well as the article "Logical connective".

Notational variants of the connectives[e][18][19]
ConnectiveSymbol
ANDA∧B{\displaystyle A\land B},A⋅B{\displaystyle A\cdot B},AB{\displaystyle AB},A&B{\displaystyle A\&B},A&&B{\displaystyle A\&\&B}
equivalentA≡B{\displaystyle A\equiv B},A⇔B{\displaystyle A\Leftrightarrow B},A⇋B{\displaystyle A\leftrightharpoons B}
impliesA⇒B{\displaystyle A\Rightarrow B},A⊃B{\displaystyle A\supset B},A→B{\displaystyle A\rightarrow B}
NANDA∧¯B{\displaystyle A{\overline {\land }}B},A∣B{\displaystyle A\mid B},A⋅B¯{\displaystyle {\overline {A\cdot B}}}
nonequivalentA≢B{\displaystyle A\not \equiv B},A⇎B{\displaystyle A\not \Leftrightarrow B},A↮B{\displaystyle A\nleftrightarrow B}
NORA∨¯B{\displaystyle A{\overline {\lor }}B},A↓B{\displaystyle A\downarrow B},A+B¯{\displaystyle {\overline {A+B}}}
NOT¬A{\displaystyle \neg A},−A{\displaystyle -A},A¯{\displaystyle {\overline {A}}},∼A{\displaystyle \sim A}
ORA∨B{\displaystyle A\lor B},A+B{\displaystyle A+B},A∣B{\displaystyle A\mid B},A∥B{\displaystyle A\parallel B}
XNORA⊙B{\displaystyle A\odot B}
XORA∨_B{\displaystyle A{\underline {\lor }}B},A⊕B{\displaystyle A\oplus B}

The most thoroughly researched branch of propositional logic isclassical truth-functional propositional logic,[1] in which formulas are interpreted as having precisely one of two possibletruth values, the truth value oftrue or the truth value offalse.[20] Theprinciple of bivalence and thelaw of excluded middle are upheld. By comparison withfirst-order logic, truth-functional propositional logic is considered to bezeroth-order logic.[8][9]

History

[edit]
Main article:History of logic

Although propositional logic had been hinted by earlier philosophers,Chrysippus is often credited with development of a deductive system for propositional logic as his main achievement in the 3rd century BC[21] which was expanded by his successorStoics. The logic was focused onpropositions. This was different from the traditionalsyllogistic logic, which focused onterms. However, most of the original writings were lost[22] and, at some time between the 3rd and 6th century CE, Stoic logic faded into oblivion, to be resurrected only in the 20th century, in the wake of the (re)-discovery of propositional logic.[23]

Symbolic logic, which would come to be important to refine propositional logic, was first developed by the 17th/18th-century mathematicianGottfried Leibniz, whosecalculus ratiocinator was, however, unknown to the larger logical community. Consequently, many of the advances achieved by Leibniz were recreated by logicians likeGeorge Boole andAugustus De Morgan, completely independent of Leibniz.[24]

Gottlob Frege'spredicate logic builds upon propositional logic, and has been described as combining "the distinctive features of syllogistic logic and propositional logic."[25] Consequently, predicate logic ushered in a new era in logic's history; however, advances in propositional logic were still made after Frege, includingnatural deduction,truth trees andtruth tables. Natural deduction was invented byGerhard Gentzen andStanisław Jaśkowski. Truth trees were invented byEvert Willem Beth.[26] The invention of truth tables, however, is of uncertain attribution.

Within works by Frege[27] andBertrand Russell,[28] are ideas influential to the invention of truth tables. The actual tabular structure (being formatted as a table), itself, is generally credited to eitherLudwig Wittgenstein orEmil Post (or both, independently).[27] Besides Frege and Russell, others credited with having ideas preceding truth tables include Philo, Boole,Charles Sanders Peirce,[29] andErnst Schröder. Others credited with the tabular structure includeJan Łukasiewicz,Alfred North Whitehead,William Stanley Jevons,John Venn, andClarence Irving Lewis.[28] Ultimately, some have concluded, like John Shosky, that "It is far from clear that any one person should be given the title of 'inventor' of truth-tables".[28]

Sentences

[edit]
Main article:Proposition

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

Declarative sentences

[edit]

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

Declarative sentences are contrasted withquestions, such as "What is Wikipedia?", andimperative statements, such as "Please addcitations to support the claims in this article.".[31][32] Such non-declarative sentences have notruth value,[33] and are only dealt with innonclassical logics, callederotetic andimperative logics.

Compounding sentences with connectives

[edit]
See also:Atomic formula andAtomic sentence

In propositional logic, a statement can contain one or more other statements as parts.[1]Compound sentences are formed from simpler sentences and express relationships among the constituent sentences.[34] This is done by combining them withlogical connectives:[34][35] the main types of compound sentences arenegations,conjunctions,disjunctions,implications, andbiconditionals,[34] which are formed by using the corresponding connectives to connect propositions.[36][37] InEnglish, these connectives are expressed by the words "and" (conjunction), "or" (disjunction), "not" (negation), "if" (material conditional), and "if and only if" (biconditional).[1][14] Examples of such compound sentences might include:

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

If sentences lack any logical connectives, they are calledsimple sentences,[1] oratomic sentences;[35] if they contain one or more logical connectives, they are calledcompound sentences,[34] ormolecular sentences.[35]

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

Arguments

[edit]
Main article:Argument

Anargument is defined as apair of things, namely a set of sentences, called thepremises,[g] and a sentence, called theconclusion.[39][35][38] The conclusion is claimed tofollow from the premises,[38] and the premises are claimed tosupport the conclusion.[35]

Example argument

[edit]

The following is an example of an argument within the scope of propositional logic:

Premise 1:If it's raining,then it's cloudy.
Premise 2: It's raining.
Conclusion: It's cloudy.

Thelogical form of this argument is known asmodus ponens,[40] which is aclassicallyvalid form.[41] So, in classical logic, the argument isvalid, although it may or may not besound, depending on themeteorological facts in a given context. Thisexample argument will be reused when explaining§ Formalization.

Validity and soundness

[edit]
Main articles:Validity (logic) andSoundness

An argument isvalid if, and only if, it isnecessary that, if all its premises are true, its conclusion is true.[39][42][43] Alternatively, an argument is valid if, and only if, it isimpossible for all the premises to be true while the conclusion is false.[43][39]

Validity is contrasted withsoundness.[43] An argument issound if, and only if, it is valid and all its premises are true.[39][43] Otherwise, it isunsound.[43]

Logic, in general, aims to precisely specify valid arguments.[35] This is done by defining a valid argument as one in which its conclusion is alogical consequence of its premises,[35] which, when this is understood assemantic consequence, means that there is nocase in which the premises are true but the conclusion is not true[35] – see§ Semantics below.

Formalization

[edit]

Propositional logic is typically studied through aformal system in whichformulas of aformal language areinterpreted to representpropositions. This formal language is the basis forproof systems, which allow a conclusion to be derived from premises if, and only if, it is alogical consequence of them. This section will show how this works by formalizing the§ Example argument. The formal language for a propositional calculus will be fully specified in§ Language, and an overview of proof systems will be given in§ Proof systems.

Propositional variables

[edit]
Main article:Propositional variable

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

Premise 1:P→Q{\displaystyle P\to Q}
Premise 2:P{\displaystyle P}
Conclusion:Q{\displaystyle Q}

WhenP is interpreted as "It's raining" andQ as "it's cloudy" these symbolic expressions correspond exactly with the original expression in natural language. Not only that, but they will also correspond with any other inference with the samelogical form.

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

Gentzen notation

[edit]

If we assume that the validity ofmodus ponens has been accepted as anaxiom, then the same§ Example argument can also be depicted like this:

P→Q,PQ{\displaystyle {\frac {P\to Q,P}{Q}}}

This method of displaying it isGentzen's notation fornatural deduction andsequent calculus.[44] The premises are shown above a line, called theinference line,[16] separated by acomma, which indicatescombination of premises.[45] The conclusion is written below the inference line.[16] The inference line representssyntactic consequence,[16] sometimes calleddeductive consequence,[46] which is also symbolized with ⊢.[47][46] So the above can also be written in one line asP→Q,P⊢Q{\displaystyle P\to Q,P\vdash Q}.[h]

Syntactic consequence is contrasted withsemantic consequence,[48] which is symbolized with ⊧.[47][46] In this case, the conclusion followssyntactically because thenatural deductioninference rule ofmodus ponens has been assumed. For more on inference rules, see the sections on proof systems below.

Language

[edit]
Part ofa series on
Formal languages

Thelanguage (commonly calledL{\displaystyle {\mathcal {L}}})[46][49][35] of a propositional calculus is defined in terms of:[2][15]

  1. a set of primitive symbols, calledatomic formulas,atomic sentences,[40][35]atoms,[50]placeholders,prime formulas,[50]proposition letters,sentence letters,[40] orvariables, and
  2. a set of operator symbols, calledconnectives,[19][1][51]logical connectives,[1]logical operators,[1]truth-functional connectives,[1]truth-functors,[38] orpropositional connectives.[2]

Awell-formed formula is any atomic formula, or any formula that can be built up from atomic formulas by means of operator symbols according to the rules of the grammar. The languageL{\displaystyle {\mathcal {L}}}, then, is defined either as beingidentical to its set of well-formed formulas,[49] or ascontaining that set (together with, for instance, its set of connectives and variables).[15][35]

Usually the syntax ofL{\displaystyle {\mathcal {L}}} is defined recursively by just a few definitions, as seen next; some authors explicitly includeparentheses as punctuation marks when defining their language's syntax,[35][52] while others use them without comment.[2][15]

Syntax

[edit]

Given a set of atomic propositional variablesp1{\displaystyle p_{1}},p2{\displaystyle p_{2}},p3{\displaystyle p_{3}}, ..., and a set of propositional connectivesc11{\displaystyle c_{1}^{1}},c21{\displaystyle c_{2}^{1}},c31{\displaystyle c_{3}^{1}}, ...,c12{\displaystyle c_{1}^{2}},c22{\displaystyle c_{2}^{2}},c32{\displaystyle c_{3}^{2}}, ...,c13{\displaystyle c_{1}^{3}},c23{\displaystyle c_{2}^{3}},c33{\displaystyle c_{3}^{3}}, ..., a formula of propositional logic isdefined recursively by these definitions:[2][15][51][i]

Definition 1: Atomic propositional variables are formulas.
Definition 2: Ifcnm{\displaystyle c_{n}^{m}} is a propositional connective, and⟨{\displaystyle \langle }A, B, C, …⟩{\displaystyle \rangle } is a sequence of m, possibly but not necessarily atomic, possibly but not necessarily distinct, formulas, then the result of applyingcnm{\displaystyle c_{n}^{m}} to⟨{\displaystyle \langle }A, B, C, …⟩{\displaystyle \rangle } is a formula.
Definition 3: Nothing else is a formula.

Writing the result of applyingcnm{\displaystyle c_{n}^{m}} to⟨{\displaystyle \langle }A, B, C, ...⟩{\displaystyle \rangle } in functional notation, ascnm{\displaystyle c_{n}^{m}}(A, B, C, ...), we have the following as examples of well-formed formulas:

What was given asDefinition 2 above, which is responsible for the composition of formulas, is referred to byColin Howson as theprinciple of composition.[40][j] It is thisrecursionin the definition of a language's syntax which justifies the use of the word "atomic" to refer to propositional variables, since all formulas in the languageL{\displaystyle {\mathcal {L}}} are built up from the atoms as ultimate building blocks.[2] Composite formulas (all formulas besides atoms) are calledmolecules,[50] ormolecular sentences.[35] (This is an imperfect analogy withchemistry, since a chemical molecule may sometimes have only one atom, as inmonatomic gases.)[50]

The definition that "nothing else is a formula", given above asDefinition 3, excludes any formula from the language which is not specifically required by the other definitions in the syntax.[38] In particular, it excludesinfinitely long formulas from beingwell-formed.[38] It is sometimes called theClosure Clause.[54]

CF grammar in BNF

[edit]

An alternative to the syntax definitions given above is to write acontext-free (CF) grammar for the languageL{\displaystyle {\mathcal {L}}} inBackus-Naur form (BNF).[55][56] This is more common incomputer science than inphilosophy.[56] It can be done in many ways,[55] of which a particularly brief one, for the common set of five connectives, is this single clause:[56][57]

ϕ::=a1,a2,… | ¬ϕ | ϕ & ψ | ϕ∨ψ | ϕ→ψ | ϕ↔ψ{\displaystyle \phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\&~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi }

This clause, due to itsself-referential nature (sinceϕ{\displaystyle \phi } is in some branches of the definition ofϕ{\displaystyle \phi }), also acts as arecursive definition, and therefore specifies the entire language. To expand it to addmodal operators, one need only add ... | ◻ϕ | ◊ϕ{\displaystyle |~\Box \phi ~|~\Diamond \phi } to the end of the clause.[56]

Constants and schemata

[edit]

Mathematicians sometimes distinguish between propositional constants,propositional variables, and schemata.Propositional constants represent some particular proposition,[58] whilepropositional variables range over the set of all atomic propositions.[58] Schemata, orschematic letters, however, range over all formulas.[38][1] (Schematic letters are also calledmetavariables.)[39] It is common to represent propositional constants byA,B, andC, propositional variables byP,Q, andR, and schematic letters are often Greek letters, most oftenφ,ψ, andχ.[38][1]

However, some authors recognize only two "propositional constants" in their formal system: the special symbol⊤{\displaystyle \top }, called "truth", which always evaluates toTrue, and the special symbol⊥{\displaystyle \bot }, called "falsity", which always evaluates toFalse.[59][60][61] Other authors also include these symbols, with the same meaning, but consider them to be "zero-place truth-functors",[38] or equivalently, "nullary connectives".[51]

Semantics

[edit]
Main articles:Semantics of logic andModel theory

To serve as a model of the logic of a givennatural language, a formal language must be semantically interpreted.[35] Inclassical logic, all propositions evaluate to exactly one of twotruth-values:True orFalse.[1][62] For example, "Wikipedia is afreeonline encyclopedia that anyone can edit"evaluates toTrue,[63] while "Wikipedia is apaperencyclopedia"evaluates toFalse.[64]

In other respects, the following formal semantics can apply to the language of any propositional logic, but the assumptions that there are only two semantic values (bivalence), that only one of the two is assigned to each formula in the language (noncontradiction), and that every formula gets assigned a value (excluded middle), are distinctive features of classical logic.[62][65][38] To learn aboutnonclassical logics with more than two truth-values, and their unique semantics, one may consult the articles on "Many-valued logic", "Three-valued logic", "Finite-valued logic", and "Infinite-valued logic".

Interpretation (case) and argument

[edit]
Main article:Interpretation (logic)

For a given languageL{\displaystyle {\mathcal {L}}}, aninterpretation,[66]valuation,[52]Boolean valuation,[67] orcase,[35][k] is anassignment ofsemantic values to each formula ofL{\displaystyle {\mathcal {L}}}.[35] For a formal language of classical logic, a case is defined as anassignment, to each formula ofL{\displaystyle {\mathcal {L}}}, of one or the other, but not both, of thetruth values, namelytruth (T, or 1) andfalsity (F, or 0).[68][69] An interpretation that follows the rules of classical logic is sometimes called aBoolean valuation.[52][70] An interpretation of a formal language for classical logic is often expressed in terms oftruth tables.[71][1] Since each formula is only assigned a single truth-value, an interpretation may be viewed as afunction, whosedomain isL{\displaystyle {\mathcal {L}}}, and whoserange is its set of semantic valuesV={T,F}{\displaystyle {\mathcal {V}}=\{{\mathsf {T}},{\mathsf {F}}\}},[2] orV={1,0}{\displaystyle {\mathcal {V}}=\{1,0\}}.[35]

Forn{\displaystyle n} distinct propositional symbols there are2n{\displaystyle 2^{n}} distinct possible interpretations. For any particular symbola{\displaystyle a}, for example, there are21=2{\displaystyle 2^{1}=2} possible interpretations: eithera{\displaystyle a} is assignedT, ora{\displaystyle a} is assignedF. And for the paira{\displaystyle a},b{\displaystyle b} there are22=4{\displaystyle 2^{2}=4} possible interpretations: either both are assignedT, or both are assignedF, ora{\displaystyle a} is assignedT andb{\displaystyle b} is assignedF, ora{\displaystyle a} is assignedF andb{\displaystyle b} is assignedT.[71] SinceL{\displaystyle {\mathcal {L}}} hasℵ0{\displaystyle \aleph _{0}}, that is,denumerably many propositional symbols, there are2ℵ0=c{\displaystyle 2^{\aleph _{0}}={\mathfrak {c}}}, and thereforeuncountably many distinct possible interpretations ofL{\displaystyle {\mathcal {L}}} as a whole.[71]

WhereI{\displaystyle {\mathcal {I}}} is an interpretation andφ{\displaystyle \varphi } andψ{\displaystyle \psi } represent formulas, the definition of anargument, given in§ Arguments, may then be stated as a pair⟨{φ1,φ2,φ3,...,φn},ψ⟩{\displaystyle \langle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\},\psi \rangle }, where{φ1,φ2,φ3,...,φn}{\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}} is the set of premises andψ{\displaystyle \psi } is the conclusion. The definition of an argument'svalidity, i.e. its property that{φ1,φ2,φ3,...,φn}⊨ψ{\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}\models \psi }, can then be stated as itsabsence of a counterexample, where acounterexample is defined as a caseI{\displaystyle {\mathcal {I}}} in which the argument's premises{φ1,φ2,φ3,...,φn}{\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}} are all true but the conclusionψ{\displaystyle \psi } is not true.[35][40] As will be seen in§ Semantic truth, validity, consequence, this is the same as to say that the conclusion is asemantic consequence of the premises.

Propositional connective semantics

[edit]
Main articles:Logical connective andTruth function

An interpretation assigns semantic values toatomic formulas directly.[66][35] Molecular formulas are assigned afunction of the value of their constituent atoms, according to the connective used;[66][35] the connectives are defined in such a way that thetruth-value of a sentence formed from atoms with connectives depends on the truth-values of the atoms that they're applied to, andonly on those.[66][35] This assumption is referred to byColin Howson as the assumption of thetruth-functionality of theconnectives.[40]

Semantics via truth tables

[edit]
Logical connectives
NOT¬A,−A,A¯,∼A{\displaystyle \neg A,-A,{\overline {A}},{\sim }A}
ANDA∧B,A⋅B,AB,A&⁡B,A&&⁡B{\displaystyle A\land B,A\cdot B,AB,A\mathop {\&} B,A\mathop {\&\&} B}
NANDA∧¯B,A↑B,A∣B,A⋅B¯{\displaystyle A\mathrel {\overline {\land }} B,A\uparrow B,A\mid B,{\overline {A\cdot B}}}
ORA∨B,A+B,A∣B,A∥B{\displaystyle A\lor B,A+B,A\mid B,A\parallel B}
NORA∨¯B,A↓B,A+B¯{\displaystyle A\mathrel {\overline {\lor }} B,A\downarrow B,{\overline {A+B}}}
XNORA⊙B,A∨¯B¯{\displaystyle A\odot B,{\overline {A\mathrel {\overline {\lor }} B}}}
└equivalentA≡B,A⇔B,A⇋B{\displaystyle A\equiv B,A\Leftrightarrow B,A\leftrightharpoons B}
XORA∨_B,A⊕B{\displaystyle A\mathrel {\underline {\lor }} B,A\oplus B}
└ nonequivalentA≢B,A⇎B,A↮B{\displaystyle A\not \equiv B,A\not \Leftrightarrow B,A\nleftrightarrow B}
impliesA⇒B,A⊃B,A→B{\displaystyle A\Rightarrow B,A\supset B,A\rightarrow B}
nonimplication (NIMPLY)A⇏B,A⊅B,A↛B{\displaystyle A\not \Rightarrow B,A\not \supset B,A\nrightarrow B}
converseA⇐B,A⊂B,A←B{\displaystyle A\Leftarrow B,A\subset B,A\leftarrow B}
converse nonimplicationA⇍B,A⊄B,A↚B{\displaystyle A\not \Leftarrow B,A\not \subset B,A\nleftarrow B}
Related concepts
Applications
Category

Since logical connectives are defined semantically only in terms of thetruth values that they take when thepropositional variables that they're applied to take either of thetwo possible truth values,[1][35] the semantic definition of the connectives is usually represented as atruth table for each of the connectives,[1][35][72] as seen below:

p{\displaystyle p}q{\displaystyle q}p∧q{\displaystyle p\land q}p∨q{\displaystyle p\lor q}p→q{\displaystyle p\rightarrow q}p⇔q{\displaystyle p\Leftrightarrow q}¬p{\displaystyle \neg p}¬q{\displaystyle \neg q}
TTTTTTFF
TFFTFFFT
FTFTTFTF
FFFFTTTT

This table covers each of the main fivelogical connectives:[14][15][16][17]conjunction (here notatedp∧q{\displaystyle p\land q}),disjunction (p ∨q),implication (p →q),biconditional (p ↔q) andnegation, (¬p, or ¬q, as the case may be). It is sufficient for determining the semantics of each of these operators.[1][73][35] For more truth tables for more different kinds of connectives, see the article "Truth table".

Semantics via assignment expressions

[edit]

Some authors write out the connective semantics using a list of statements instead of a table. In this format, whereI(φ){\displaystyle {\mathcal {I}}(\varphi )} is the interpretation ofφ{\displaystyle \varphi }, the five connectives are defined as:[38][52]

Instead ofI(φ){\displaystyle {\mathcal {I}}(\varphi )}, the interpretation ofφ{\displaystyle \varphi } may be written out as|φ|{\displaystyle |\varphi |},[38][74] or, for definitions such as the above,I(φ)=T{\displaystyle {\mathcal {I}}(\varphi )={\mathsf {T}}} may be written simply as the English sentence "φ{\displaystyle \varphi } is given the valueT{\displaystyle {\mathsf {T}}}".[52] Yet other authors[75][76] may prefer to speak of aTarskian modelM{\displaystyle {\mathfrak {M}}} for the language, so that instead they'll use the notationM⊨φ{\displaystyle {\mathfrak {M}}\models \varphi }, which is equivalent to sayingI(φ)=T{\displaystyle {\mathcal {I}}(\varphi )={\mathsf {T}}}, whereI{\displaystyle {\mathcal {I}}} is the interpretation function forM{\displaystyle {\mathfrak {M}}}.[76]

Connective definition methods

[edit]

Some of these connectives may be defined in terms of others: for instance, implication,p→q{\displaystyle p\rightarrow q}, may be defined in terms of disjunction and negation, as¬p∨q{\displaystyle \neg p\lor q};[77] and disjunction may be defined in terms of negation and conjunction, as¬(¬p∧¬q{\displaystyle \neg (\neg p\land \neg q}).[52] In fact, atruth-functionally complete system,[l] in the sense that all and only the classical propositional tautologies are theorems, may be derived using only disjunction and negation (asRussell,Whitehead, andHilbert did), or using only implication and negation (asFrege did), or using only conjunction and negation, or even using only a single connective for "not and" (theSheffer stroke),[3] asJean Nicod did.[2] Ajoint denial connective (logical NOR) will also suffice, by itself, to define all other connectives. Besides NOR and NAND, no other connectives have this property.[52][m]

Some authors, namelyHowson[40] and Cunningham,[79] distinguish equivalence from the biconditional. (As to equivalence, Howson calls it "truth-functional equivalence", while Cunningham calls it "logical equivalence".) Equivalence is symbolized with ⇔ and is a metalanguage symbol, while a biconditional is symbolized with ↔ and is a logical connective in the object languageL{\displaystyle {\mathcal {L}}}. Regardless, an equivalence or biconditional is true if, and only if, the formulas connected by it are assigned the same semantic value under every interpretation. Other authors often do not make this distinction, and may use the word "equivalence",[16] and/or the symbol ⇔,[80] to denote their object language's biconditional connective.

Semantic truth, validity, consequence

[edit]

Givenφ{\displaystyle \varphi } andψ{\displaystyle \psi } asformulas (or sentences) of a languageL{\displaystyle {\mathcal {L}}}, andI{\displaystyle {\mathcal {I}}} as an interpretation (or case)[n] ofL{\displaystyle {\mathcal {L}}}, then the following definitions apply:[71][69]

For interpretations (cases)I{\displaystyle {\mathcal {I}}} ofL{\displaystyle {\mathcal {L}}}, these definitions are sometimes given:

Forclassical logic, which assumes that all cases are complete and consistent,[35] the following theorems apply:

Proof systems

[edit]
See also:Proof theory andProof calculus

Proof systems in propositional logic can be broadly classified intosemantic proof systems andsyntactic proof systems,[89][90][91] according to the kind oflogical consequence that they rely on: semantic proof systems rely on semantic consequence (φ⊨ψ{\displaystyle \varphi \models \psi }),[92] whereas syntactic proof systems rely on syntactic consequence (φ⊢ψ{\displaystyle \varphi \vdash \psi }).[93] Semantic consequence deals with the truth values of propositions in all possible interpretations, whereas syntactic consequence concerns the derivation of conclusions from premises based on rules and axioms within a formal system.[94] This section gives a very brief overview of the kinds of proof systems, withanchors to the relevant sections of this article on each one, as well as to the separate Wikipedia articles on each one.

Semantic proof systems

[edit]
Example of atruth table
A graphical representation of a partially builtpropositional tableau

Semantic proof systems rely on the concept of semantic consequence, symbolized asφ⊨ψ{\displaystyle \varphi \models \psi }, which indicates that ifφ{\displaystyle \varphi } is true, thenψ{\displaystyle \psi } must also be true in every possible interpretation.[94]

Truth tables

[edit]
Main article:Truth table

Atruth table is a semantic proof method used to determine the truth value of a propositional logic expression in every possible scenario.[95] By exhaustively listing the truth values of its constituent atoms, a truth table can show whether a proposition is true, false, tautological, or contradictory.[96] See§ Semantic proof via truth tables.

Semantic tableaux

[edit]
Main article:Method of analytic tableaux

Asemantic tableau is another semantic proof technique that systematically explores the truth of a proposition.[97] It constructs a tree where each branch represents a possible interpretation of the propositions involved.[98] If every branch leads to a contradiction, the original proposition is considered to be a contradiction, and its negation is considered atautology.[40] See§ Semantic proof via tableaux.

Syntactic proof systems

[edit]
Rules for the propositionalsequent calculus LK, inGentzen notation

Syntactic proof systems, in contrast, focus on the formal manipulation of symbols according to specific rules. The notion of syntactic consequence,φ⊢ψ{\displaystyle \varphi \vdash \psi }, signifies thatψ{\displaystyle \psi } can be derived fromφ{\displaystyle \varphi } using the rules of the formal system.[94]

Axiomatic systems

[edit]
Main article:Axiomatic system (logic)

Anaxiomatic system is a set of axioms or assumptions from which other statements (theorems) are logically derived.[99] In propositional logic, axiomatic systems define a base set of propositions considered to be self-evidently true, and theorems are proved by applying deduction rules to these axioms.[100] See§ Syntactic proof via axioms.

Natural deduction

[edit]
Main article:Natural deduction

Natural deduction is a syntactic method of proof that emphasizes the derivation of conclusions from premises through the use of intuitive rules reflecting ordinary reasoning.[101] Each rule reflects a particular logical connective and shows how it can be introduced or eliminated.[101] See§ Syntactic proof via natural deduction.

Sequent calculus

[edit]
Main article:Sequent calculus

Thesequent calculus is a formal system that represents logical deductions as sequences or "sequents" of formulas.[102] Developed byGerhard Gentzen, this approach focuses on the structural properties of logical deductions and provides a powerful framework for proving statements within propositional logic.[102][103]

Semantic proof via truth tables

[edit]
See also:Truth table

Taking advantage of the semantic concept of validity (truth in every interpretation), it is possible to prove a formula's validity by using atruth table, which gives every possible interpretation (assignment of truth values to variables) of a formula.[96][50][38] If, and only if, all the lines of a truth table come out true, the formula is semantically valid (true in every interpretation).[96][50] Further, if (and only if)¬φ{\displaystyle \neg \varphi } is valid, thenφ{\displaystyle \varphi } is inconsistent.[84][85][86]

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

pqrq ∨rr → ¬pq ∨r → (r → ¬p)p → (q ∨r → (r → ¬p))
TTTTFFF
TTFTTTT
TFTTFFF
TFFFTTT
FTTTTTT
FTFTTTT
FFTTTTT
FFFFTTT

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

p→(q∨r→(r→¬p))
T→(F∨T→(T→¬T))
T→(T→(T→F))
T→(T→F)
T→F
F
TFFTTFTFFT

Further, using the theorem thatφ⊨ψ{\displaystyle \varphi \models \psi } if, and only if,(φ→ψ){\displaystyle (\varphi \to \psi )} is valid,[71][81] we can use a truth table to prove that a formula is a semantic consequence of a set of formulas:{φ1,φ2,φ3,...,φn}⊨ψ{\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}\models \psi } if, and only if, we can produce a truth table that comes out all true for the formula((⋀i=1nφi)→ψ){\displaystyle \left(\left(\bigwedge _{i=1}^{n}\varphi _{i}\right)\rightarrow \psi \right)} (that is, if⊨((⋀i=1nφi)→ψ){\displaystyle \models \left(\left(\bigwedge _{i=1}^{n}\varphi _{i}\right)\rightarrow \psi \right)}).[104][105]

Semantic proof via tableaux

[edit]
Main article:Method of analytic tableaux

Since truth tables have 2n lines for n variables, they can be tiresomely long for large values of n.[40] Analytic tableaux are a more efficient, but nevertheless mechanical,[72] semantic proof method; they take advantage of the fact that "we learn nothing about the validity of the inference from examining the truth-value distributions which make either the premises false or the conclusion true: the only relevant distributions when considering deductive validity are clearly just those which make the premises true or the conclusion false."[40]

Analytic tableaux for propositional logic are fully specified by the rules that are stated in schematic form below.[52] These rules use "signed formulas", where a signed formula is an expressionTX{\displaystyle TX} orFX{\displaystyle FX}, whereX{\displaystyle X} is a (unsigned) formula of the languageL{\displaystyle {\mathcal {L}}}.[52] (Informally,TX{\displaystyle TX} is read "X{\displaystyle X} is true", andFX{\displaystyle FX} is read "X{\displaystyle X} is false".)[52] Their formal semantic definition is that "under any interpretation, a signed formulaTX{\displaystyle TX} is called true ifX{\displaystyle X} is true, and false ifX{\displaystyle X} is false, whereas a signed formulaFX{\displaystyle FX} is called false ifX{\displaystyle X} is true, and true ifX{\displaystyle X} is false."[52]

1)T∼XFXF∼XTXspacer2)T(X∧Y)TXTYF(X∧Y)FX|FYspacer3)T(X∨Y)TX|TYF(X∨Y)FXFYspacer4)T(X⊃Y)FX|TYF(X⊃Y)TXFY{\displaystyle {\begin{aligned}&1)\quad {\frac {T\sim X}{FX}}\quad &&{\frac {F\sim X}{TX}}\\{\phantom {spacer}}\\&2)\quad {\frac {T(X\land Y)}{\begin{matrix}TX\\TY\end{matrix}}}\quad &&{\frac {F(X\land Y)}{FX|FY}}\\{\phantom {spacer}}\\&3)\quad {\frac {T(X\lor Y)}{TX|TY}}\quad &&{\frac {F(X\lor Y)}{\begin{matrix}FX\\FY\end{matrix}}}\\{\phantom {spacer}}\\&4)\quad {\frac {T(X\supset Y)}{FX|TY}}\quad &&{\frac {F(X\supset Y)}{\begin{matrix}TX\\FY\end{matrix}}}\end{aligned}}}

In this notation, rule 2 means thatT(X∧Y){\displaystyle T(X\land Y)} yields bothTX,TY{\displaystyle TX,TY}, whereasF(X∧Y){\displaystyle F(X\land Y)}branches intoFX,FY{\displaystyle FX,FY}. The notation is to be understood analogously for rules 3 and 4.[52] Often, in tableaux forclassical logic, thesigned formula notation is simplified so thatTφ{\displaystyle T\varphi } is written simply asφ{\displaystyle \varphi }, andFφ{\displaystyle F\varphi } as¬φ{\displaystyle \neg \varphi }, which accounts for naming rule 1 the "Rule of Double Negation".[40][72]

One constructs a tableau for a set of formulas by applying the rules to produce more lines and tree branches until every line has been used, producing acomplete tableau. In some cases, a branch can come to contain bothTX{\displaystyle TX} andFX{\displaystyle FX} for someX{\displaystyle X}, which is to say, a contradiction. In that case, the branch is said toclose.[40] If every branch in a tree closes, the tree itself is said to close.[40] In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself self-contradictory, and therefore false.[40] Conversely, a tableau can also prove that a logical formula istautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.[40]

To construct a tableau for an argument⟨{φ1,φ2,φ3,...,φn},ψ⟩{\displaystyle \langle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\},\psi \rangle }, one first writes out the set of premise formulas,{φ1,φ2,φ3,...,φn}{\displaystyle \{\varphi _{1},\varphi _{2},\varphi _{3},...,\varphi _{n}\}}, with one formula on each line, signed withT{\displaystyle T} (that is,Tφ{\displaystyle T\varphi } for eachTφ{\displaystyle T\varphi } in the set);[72] and together with those formulas (the order is unimportant), one also writes out the conclusion,ψ{\displaystyle \psi }, signed withF{\displaystyle F} (that is,Fψ{\displaystyle F\psi }).[72] One then produces a truth tree (analytic tableau) by using all those lines according to the rules.[72] A closed tree will be proof that the argument was valid, in virtue of the fact thatφ⊨ψ{\displaystyle \varphi \models \psi } if, and only if,{φ,∼ψ}{\displaystyle \{\varphi ,\sim \psi \}} is inconsistent (also written asφ,∼ψ⊨{\displaystyle \varphi ,\sim \psi \models }).[72]

List of classically valid argument forms

[edit]

Using semantic checking methods, such as truth tables or semantic tableaux, to check for tautologies and semantic consequences, it can be shown that, in classical logic, the following classical argument forms are semantically valid, i.e., these tautologies and semantic consequences hold.[38] We useφ{\displaystyle \varphi } ⟚ψ{\displaystyle \psi } to denote equivalence ofφ{\displaystyle \varphi } andψ{\displaystyle \psi }, that is, as an abbreviation for bothφ⊨ψ{\displaystyle \varphi \models \psi } andψ⊨φ{\displaystyle \psi \models \varphi };[38] as an aid to reading the symbols, a description of each formula is given. The description reads the symbol ⊧ (called the "double turnstile") as "therefore", which is a common reading of it,[38][106] although many authors prefer to read it as "entails",[38][107] or as "models".[108]

NameSequentDescription
Modus Ponens((p→q)∧p)⊨q{\displaystyle ((p\to q)\land p)\models q}[35]Ifp thenq;p; thereforeq
Modus Tollens((p→q)∧¬q)⊨¬p{\displaystyle ((p\to q)\land \neg q)\models \neg p}[35]Ifp thenq; notq; therefore notp
Hypothetical Syllogism((p→q)∧(q→r))⊨(p→r){\displaystyle ((p\to q)\land (q\to r))\models (p\to r)}[39]Ifp thenq; ifq thenr; therefore, ifp thenr
Disjunctive Syllogism((p∨q)∧¬p)⊨q{\displaystyle ((p\lor q)\land \neg p)\models q}[109]Eitherp orq, or both; notp; therefore,q
Constructive Dilemma((p→q)∧(r→s)∧(p∨r))⊨(q∨s){\displaystyle ((p\to q)\land (r\to s)\land (p\lor r))\models (q\lor s)}[39]Ifp thenq; and ifr thens; butp orr; thereforeq ors
Destructive Dilemma((p→q)∧(r→s)∧(¬q∨¬s))⊨(¬p∨¬r){\displaystyle ((p\to q)\land (r\to s)\land (\neg q\lor \neg s))\models (\neg p\lor \neg r)}Ifp thenq; and ifr thens; but notq or nots; therefore notp or notr
Bidirectional Dilemma((p→q)∧(r→s)∧(p∨¬s))⊨(q∨¬r){\displaystyle ((p\to q)\land (r\to s)\land (p\lor \neg s))\models (q\lor \neg r)}Ifp thenq; and ifr thens; butp or nots; thereforeq or notr
Simplification(p∧q)⊨p{\displaystyle (p\land q)\models p}[35]p andq are true; thereforep is true
Conjunctionp,q⊨(p∧q){\displaystyle p,q\models (p\land q)}[35]p andq are true separately; therefore they are true conjointly
Additionp⊨(p∨q){\displaystyle p\models (p\lor q)}[35][109]p is true; therefore the disjunction (p orq) is true
Composition of conjunction((p→q)∧(p→r)){\displaystyle ((p\to q)\land (p\to r))} ⟚(p→(q∧r)){\displaystyle (p\to (q\land r))}Ifp thenq; and ifp thenr; therefore ifp is true thenq andr are true
Composition of disjunction((p→q)∨(p→r)){\displaystyle ((p\to q)\lor (p\to r))} ⟚(p→(q∨r)){\displaystyle (p\to (q\lor r))}Ifp thenq; or ifp thenr; therefore ifp is true thenq orr is true
De Morgan's Theorem (1)¬(p∧q){\displaystyle \neg (p\land q)} ⟚(¬p∨¬q){\displaystyle (\neg p\lor \neg q)}[35]The negation of (p andq) is equiv. to (notp or notq)
De Morgan's Theorem (2)¬(p∨q){\displaystyle \neg (p\lor q)} ⟚(¬p∧¬q){\displaystyle (\neg p\land \neg q)}[35]The negation of (p orq) is equiv. to (notp and notq)
Commutation (1)(p∨q){\displaystyle (p\lor q)} ⟚(q∨p){\displaystyle (q\lor p)}[109](p orq) is equiv. to (q orp)
Commutation (2)(p∧q){\displaystyle (p\land q)} ⟚(q∧p){\displaystyle (q\land p)}[109](p andq) is equiv. to (q andp)
Commutation (3)(p↔q){\displaystyle (p\leftrightarrow q)} ⟚(q↔p){\displaystyle (q\leftrightarrow p)}[109](p iffq) is equiv. to (q iffp)
Association (1)(p∨(q∨r)){\displaystyle (p\lor (q\lor r))} ⟚((p∨q)∨r){\displaystyle ((p\lor q)\lor r)}[40]p or (q orr) is equiv. to (p orq) orr
Association (2)(p∧(q∧r)){\displaystyle (p\land (q\land r))} ⟚((p∧q)∧r){\displaystyle ((p\land q)\land r)}[40]p and (q andr) is equiv. to (p andq) andr
Distribution (1)(p∧(q∨r)){\displaystyle (p\land (q\lor r))} ⟚((p∧q)∨(p∧r)){\displaystyle ((p\land q)\lor (p\land r))}[109]p and (q orr) is equiv. to (p andq) or (p andr)
Distribution (2)(p∨(q∧r)){\displaystyle (p\lor (q\land r))} ⟚((p∨q)∧(p∨r)){\displaystyle ((p\lor q)\land (p\lor r))}[109]p or (q andr) is equiv. to (p orq) and (p orr)
Double Negationp{\displaystyle p} ⟚¬¬p{\displaystyle \neg \neg p}[35][109]p is equivalent to the negation of notp
Transposition(p→q){\displaystyle (p\to q)} ⟚(¬q→¬p){\displaystyle (\neg q\to \neg p)}[35]Ifp thenq is equiv. to if notq then notp
Material Implication(p→q){\displaystyle (p\to q)} ⟚(¬p∨q){\displaystyle (\neg p\lor q)}[109]Ifp thenq is equiv. to notp orq
Material Equivalence (1)(p↔q){\displaystyle (p\leftrightarrow q)} ⟚((p→q)∧(q→p)){\displaystyle ((p\to q)\land (q\to p))}[109](p iffq) is equiv. to (ifp is true thenq is true) and (ifq is true thenp is true)
Material Equivalence (2)(p↔q){\displaystyle (p\leftrightarrow q)} ⟚((p∧q)∨(¬p∧¬q)){\displaystyle ((p\land q)\lor (\neg p\land \neg q))}[109](p iffq) is equiv. to either (p andq are true) or (bothp andq are false)
Material Equivalence (3)(p↔q){\displaystyle (p\leftrightarrow q)} ⟚((p∨¬q)∧(¬p∨q)){\displaystyle ((p\lor \neg q)\land (\neg p\lor q))}(p iffq) is equiv to., both (p or notq is true) and (notp orq is true)
Exportation((p∧q)→r)⊨(p→(q→r)){\displaystyle ((p\land q)\to r)\models (p\to (q\to r))}[110]from (ifp andq are true thenr is true) we can prove (ifq is true thenr is true, ifp is true)
Importation(p→(q→r))⊨((p∧q)→r){\displaystyle (p\to (q\to r))\models ((p\land q)\to r)}[39]Ifp then (ifq thenr) is equivalent to ifp andq thenr
Idempotence of disjunctionp{\displaystyle p} ⟚(p∨p){\displaystyle (p\lor p)}[109]p is true is equiv. top is true orp is true
Idempotence of conjunctionp{\displaystyle p} ⟚(p∧p){\displaystyle (p\land p)}[109]p is true is equiv. top is true andp is true
Tertium non datur (Law of Excluded Middle)⊨(p∨¬p){\displaystyle \models (p\lor \neg p)}[35][109]p or notp is true
Law of Non-Contradiction⊨¬(p∧¬p){\displaystyle \models \neg (p\land \neg p)}[35][109]p and notp is false, is a true statement
Explosion(p∧¬p)⊨q{\displaystyle (p\land \neg p)\models q}[35]p and notp; thereforeq

Syntactic proof via natural deduction

[edit]
Main article:Natural deduction
Transformation rules
Propositional calculus
Rules of inference (List)
Rules of replacement
Predicate logic
Rules of inference

Natural deduction, since it is a method of syntactical proof, is specified by providinginference rules (also calledrules of proof)[39] for a language with the typical set of connectives{−,&,∨,→,↔}{\displaystyle \{-,\&,\lor ,\to ,\leftrightarrow \}}; no axioms are used other than these rules.[111] The rules are covered below, and a proof example is given afterwards.

Notation styles

[edit]

Different authors vary to some extent regarding which inference rules they give, which will be noted. More striking to the look and feel of a proof, however, is the variation in notation styles. The§ Gentzen notation, which was covered earlier for a short argument, can actually be stacked to produce large tree-shaped natural deduction proofs[44][16]—not to be confused with "truth trees", which is another name foranalytic tableaux.[72] There is also a style due toStanisław Jaśkowski, where the formulas in the proof are written inside various nested boxes,[44] and there is a simplification of Jaśkowski's style due toFredric Fitch (Fitch notation), where the boxes are simplified to simple horizontal lines beneath the introductions of suppositions, and vertical lines to the left of the lines that are under the supposition.[44] Lastly, there is the only notation style which will actually be used in this article, which is due toPatrick Suppes,[44] but was much popularized byE.J. Lemmon andBenson Mates.[112] This method has the advantage that, graphically, it is the least intensive to produce and display, which made it a natural choice for theeditor who wrote this part of the article, who did not understand the complexLaTeX commands that would be required to produce proofs in the other methods.

Aproof, then, laid out in accordance with theSuppes–Lemmon notation style,[44] is a sequence of lines containing sentences,[39] where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence.[39] Eachline of proof is made up of asentence of proof, together with itsannotation, itsassumption set, and the currentline number.[39] The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers.[39] The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.[39] See the§ Natural deduction proof example.

Inference rules

[edit]

Natural deduction inference rules, due ultimately toGentzen, are given below.[111] There are ten primitive rules of proof, which are the ruleassumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rulereductio ad adbsurdum.[39] Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,[39] and MTT and DN are commonly given rules,[111] although they are not primitive.[39]

List of Inference Rules
Rule NameAlternative namesAnnotationAssumption setStatement
Rule of Assumptions[111]Assumption[39]A[111][39]The current line number.[39]At any stage of the argument, introduce a proposition as an assumption of the argument.[111][39]
Conjunction introductionAmpersand introduction,[111][39] conjunction (CONJ)[39][113]m, n &I[39][111]The union of the assumption sets at linesm andn.[39]Fromφ{\displaystyle \varphi } andψ{\displaystyle \psi } at linesm andn, inferφ & ψ{\displaystyle \varphi ~\&~\psi }.[111][39]
Conjunction eliminationSimplification (S),[39] ampersand elimination[111][39]m &E[39][111]The same as at linem.[39]Fromφ & ψ{\displaystyle \varphi ~\&~\psi } at linem, inferφ{\displaystyle \varphi } andψ{\displaystyle \psi }.[39][111]
Disjunction introduction[111]Addition (ADD)[39]m ∨I[39][111]The same as at linem.[39]Fromφ{\displaystyle \varphi } at linem, inferφ∨ψ{\displaystyle \varphi \lor \psi }, whateverψ{\displaystyle \psi } may be.[39][111]
Disjunction eliminationWedge elimination,[111] dilemma (DL)[113]j,k,l,m,n ∨E[111]The linesj,k,l,m,n.[111]Fromφ∨ψ{\displaystyle \varphi \lor \psi } at linej, and an assumption ofφ{\displaystyle \varphi } at linek, and a derivation ofχ{\displaystyle \chi } fromφ{\displaystyle \varphi } at linel, and an assumption ofψ{\displaystyle \psi } at linem, and a derivation ofχ{\displaystyle \chi } fromψ{\displaystyle \psi } at linen, inferχ{\displaystyle \chi }.[111]
Disjunctive SyllogismWedge elimination (∨E),[39] modus tollendo ponens (MTP)[39]m,n DS[39]The union of the assumption sets at linesm andn.[39]Fromφ∨ψ{\displaystyle \varphi \lor \psi } at linem and−φ{\displaystyle -\varphi } at linen, inferψ{\displaystyle \psi }; fromφ∨ψ{\displaystyle \varphi \lor \psi } at linem and−ψ{\displaystyle -\psi } at linen, inferφ{\displaystyle \varphi }.[39]
Arrow elimination[39]Modus ponendo ponens (MPP),[111][39] modus ponens (MP),[113][39] conditional eliminationm, n →E[39][111]The union of the assumption sets at linesm andn.[39]Fromφ→ψ{\displaystyle \varphi \to \psi } at linem, andφ{\displaystyle \varphi } at linen, inferψ{\displaystyle \psi }.[39]
Arrow introduction[39]Conditional proof (CP),[113][111][39] conditional introductionn, →I (m)[39][111]Everything in the assumption set at linen, exceptingm, the line where the antecedent was assumed.[39]Fromψ{\displaystyle \psi } at linen, following from the assumption ofφ{\displaystyle \varphi } at linem, inferφ→ψ{\displaystyle \varphi \to \psi }.[39]
Reductio ad absurdum[111]Indirect Proof (IP),[39] negation introduction (−I),[39] negation elimination (−E)[39]m, n RAA (k)[39]The union of the assumption sets at linesm andn, excludingk (the denied assumption).[39]From a sentence and its denial[p] at linesm andn, infer the denial of any assumption appearing in the proof (at linek).[39]
Double arrow introduction[39]Biconditional definition (Df ↔),[111] biconditional introductionm, n ↔ I[39]The union of the assumption sets at linesm andn.[39]Fromφ→ψ{\displaystyle \varphi \to \psi } andψ→φ{\displaystyle \psi \to \varphi } at linesm andn, inferφ↔ψ{\displaystyle \varphi \leftrightarrow \psi }.[39]
Double arrow elimination[39]Biconditional definition (Df ↔),[111] biconditional eliminationm ↔ E[39]The same as at linem.[39]Fromφ↔ψ{\displaystyle \varphi \leftrightarrow \psi } at linem, infer eitherφ→ψ{\displaystyle \varphi \to \psi } orψ→φ{\displaystyle \psi \to \varphi }.[39]
Double negation[111][113]Double negation eliminationm DN[111]The same as at linem.[111]From−−φ{\displaystyle --\varphi } at linem, inferφ{\displaystyle \varphi }.[111]
Modus tollendo tollens[111]Modus tollens (MT)[113]m, n MTT[111]The union of the assumption sets at linesm andn.[111]Fromφ→ψ{\displaystyle \varphi \to \psi } at linem, and−ψ{\displaystyle -\psi } at linen, infer−φ{\displaystyle -\varphi }.[111]

Natural deduction proof example

[edit]

The proof below[39] derives−P{\displaystyle -P} fromP→Q{\displaystyle P\to Q} and−Q{\displaystyle -Q} using onlyMPP andRAA, which shows thatMTT is not a primitive rule, since it can be derived from those two other rules.

Derivation of MTT from MPP and RAA
Assumption setLine numberSentence of proofAnnotation
11P→Q{\displaystyle P\to Q}A
22−Q{\displaystyle -Q}A
33P{\displaystyle P}A
1,34Q{\displaystyle Q}1,3 →E
1,25−P{\displaystyle -P}2,4 RAA

Syntactic proof via axioms

[edit]
Main article:Hilbert system

It is possible to perform proofs axiomatically, which means that certaintautologies are taken as self-evident and various others are deduced from them usingmodus ponens as aninference rule, as well as arule ofsubstitution, which permits replacing anywell-formed formula with anysubstitution-instance of it.[114] Alternatively, one usesaxiom schemas instead of axioms, and no rule of substitution is used.[114]

This section gives the axioms of some historically notable axiomatic systems for propositional logic. For more examples, as well as metalogical theorems that are specific to such axiomatic systems (such as their completeness and consistency), see the articleAxiomatic system (logic).

Frege'sBegriffsschrift

[edit]

Although axiomatic proof has been used since the famousAncient Greek textbook,Euclid'sElements of Geometry, in propositional logic it dates back toGottlob Frege's1879Begriffsschrift.[38][114] Frege's system used onlyimplication andnegation as connectives.[2] It had six axioms:[114][115][116]

These were used by Frege together with modus ponens and a rule of substitution (which was used but never precisely stated) to yield a complete and consistent axiomatization of classical truth-functional propositional logic.[115]

Łukasiewicz's P2

[edit]

Jan Łukasiewicz showed that, in Frege's system, "the third axiom is superfluous since it can be derived from the preceding two axioms, and that the last three axioms can be replaced by the single sentenceCCNpNqCqp{\displaystyle CCNpNqCqp}".[116] Which, taken out of Łukasiewicz'sPolish notation into modern notation, means(¬p→¬q)→(q→p){\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)}. Hence, Łukasiewicz is credited[114] with this system of three axioms:

Just like Frege's system, this system uses a substitution rule and uses modus ponens as an inference rule.[114] The exact same system was given (with an explicit substitution rule) byAlonzo Church,[117] who referred to it as the system P2[117][118] and helped popularize it.[118]

Schematic form of P2

[edit]

One may avoid using the rule of substitution by giving the axioms in schematic form, using them to generate an infinite set of axioms. Hence, using Greek letters to represent schemata (metalogical variables that may stand for anywell-formed formulas), the axioms are given as:[38][118]

The schematic version of P2 is attributed toJohn von Neumann,[114] and is used in theMetamath "set.mm" formal proof database.[118] It has also been attributed toHilbert,[119] and namedH{\displaystyle {\mathcal {H}}} in this context.[119]

Proof example in P2

[edit]

As an example, a proof ofA→A{\displaystyle A\to A} in P2 is given below. First, the axioms are given names:

(A1)(p→(q→p)){\displaystyle (p\to (q\to p))}
(A2)((p→(q→r))→((p→q)→(p→r))){\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}
(A3)((¬p→¬q)→(q→p)){\displaystyle ((\neg p\to \neg q)\to (q\to p))}

And the proof is as follows:

  1. A→((B→A)→A){\displaystyle A\to ((B\to A)\to A)}       (instance of (A1))
  2. (A→((B→A)→A))→((A→(B→A))→(A→A)){\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}       (instance of (A2))
  3. (A→(B→A))→(A→A){\displaystyle (A\to (B\to A))\to (A\to A)}       (from (1) and (2) bymodus ponens)
  4. A→(B→A){\displaystyle A\to (B\to A)}       (instance of (A1))
  5. A→A{\displaystyle A\to A}       (from (4) and (3) by modus ponens)

Solvers

[edit]

One notable difference between propositional calculus and predicate calculus is that satisfiability of a propositional formula isdecidable.[120]: 81  Deciding satisfiability of propositional logic formulas is anNP-complete problem. However, practical methods exist (e.g.,DPLL algorithm, 1962;Chaff algorithm, 2001) that are very fast for many useful cases. Recent work has extended theSAT solver algorithms to work with propositions containingarithmetic expressions; these are theSMT solvers.

See also

[edit]

Higher logical levels

[edit]

Related topics

[edit]

Notes

[edit]
  1. ^Many sources write this with a definite article, asthe propositional calculus, while others just call it propositional calculus with no article.
  2. ^Zeroth-order logic is sometimes used to denote aquantifier-free predicate logic. That is, propositional logic extended with functions, relations, and constants.[6]
  3. ^For propositional logic, the formal language used is apropositional language.
  4. ^Not to be confused with the formal language'salphabet.
  5. ^See all possibleconnectives on truth-functional propositional logic with some of their properties.
  6. ^The "or both" makes it clear[35] that it's alogical disjunction, not anexclusive or, which is more common in English.
  7. ^The set of premises may be theempty set;[38][39] an argument from an empty set of premises isvalid if, and only if, the conclusion is atautology.[38][39]
  8. ^The turnstile, for syntactic consequence, is of lowerprecedence than the comma, which represents premise combination, which in turn is of lower precedence than the arrow, used for material implication; so no parentheses are needed to interpret this formula.[45]
  9. ^A very general and abstract syntax is given here, following the notation in the SEP,[2] but including the third definition, which is very commonly given explicitly by other sources, such as Gillon,[15] Bostock,[38] Allen & Hand,[39] and many others. As noted elsewhere in the article, languages variously compose their set of atomic propositional variables from uppercase or lowercase letters (often focusing on P/p, Q/q, and R/r), with or without subscript numerals; and in their set of connectives, they may include either the full set of five typical connectives,{¬,∧,∨,→,↔}{\displaystyle \{\neg ,\land ,\lor ,\to ,\leftrightarrow \}}, or any of the truth-functionally complete subsets of it. (And, of course, they may also use any of the notational variants of these connectives.)
  10. ^Note that the phrase "principle of composition" has referred to other things in other contexts, and even in the context of logic, sinceBertrand Russell used it to refer to the principle that "a proposition which implies each of two propositions implies them both."[53]
  11. ^The name "interpretation" is used by some authors and the name "case" by other authors. This article will be indifferent and use either, since it is collaboratively edited and there is no consensus about which terminology to adopt.
  12. ^A truth-functionally complete set of connectives[2] is also called simplyfunctionally complete, oradequate for truth-functional logic,[40] orexpressively adequate,[78] or simplyadequate.[40][78]
  13. ^See a table of all 16 bivalent truth functions.
  14. ^Some of these definitions use the word "interpretation", and speak of sentences/formulas being true or false "under" it, and some will use the word "case", and speak of sentences/formulas being true or false "in" it. Publishedreliable sources (WP:RS) have used both kinds of terminological convention, although usually a given author will use only one of them. Since this article is collaboratively edited and there is no consensus about which convention to use, these variations in terminology have been left standing.
  15. ^Conventionally⊨φ{\displaystyle \models \varphi }, with nothing to the left of the turnstile, is used to symbolize a tautology. It may be interpreted as saying thatφ{\displaystyle \varphi } is a semantic consequence of the empty set of formulae, i.e.,{}⊨φ{\displaystyle \{\}\models \varphi }, but with the empty brackets omitted for simplicity;[38] which is just the same as to say that it is a tautology, i.e., that there is no interpretation under which it is false.[38]
  16. ^To simplify the statement of the rule, the word "denial" here is used in this way: thedenial of a formulaφ{\displaystyle \varphi } that is not anegation is−φ{\displaystyle -\varphi }, whereas anegation,−φ{\displaystyle -\varphi }, has twodenials, viz.,φ{\displaystyle \varphi } and−−φ{\displaystyle --\varphi }.[39]

References

[edit]
  1. ^abcdefghijklmnopqrstuvwxyKlement, Kevin C."Propositional Logic". In Fieser, James; Dowden, Bradley (eds.).Internet Encyclopedia of Philosophy. Retrieved7 April 2025.
  2. ^abcdefghijklmnopqrsFranks, Curtis (2024)."Propositional Logic". In Zalta, Edward N.; Nodelman, Uri (eds.).Stanford Encyclopedia of Philosophy (Winter 2024 ed.). Metaphysics Research Lab, Stanford University. Retrieved7 April 2025.
  3. ^abWeisstein, Eric W."Propositional Calculus".Wolfram MathWorld. Retrieved9 August 2025.
  4. ^Lemmon, E. J. (30 September 1971).Beginning Logic. CRC Press. pp. ix.ISBN 978-0-412-38090-7.
  5. ^Hilbert, D.; Ackermann, W. (1950).Principles of Mathematical Logic. Chelsea Publishing Company.OCLC 372927.
  6. ^Tao, Terence (2010),"The completeness and compactness theorems of first-order logic",An epsilon of room, II, American Mathematical Society, pp. 27–31,doi:10.1090/mbk/077,ISBN 978-0-8218-5280-4,MR 2780010
  7. ^Andrews, Peter B. (2002),An introduction to mathematical logic and type theory: to truth through proof, Applied Logic Series, vol. 27 (Second ed.), Kluwer Academic Publishers, Dordrecht, p. 201,doi:10.1007/978-94-015-9934-4,ISBN 1-4020-0763-9,MR 1932484
  8. ^abBělohlávek, Radim; Dauben, Joseph Warren; Klir, George J. (2017).Fuzzy logic and mathematics: a historical perspective. New York, NY, United States of America: Oxford University Press. p. 463.ISBN 978-0-19-020001-5.
  9. ^abManzano, María (2005).Extensions of first order logic. Cambridge tracts in theoretical computer science (Digitally printed first paperback version ed.). Cambridge: Cambridge University Press. p. 180.ISBN 978-0-521-35435-6.
  10. ^Matthes, Ralph (1999).Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Herbert Utz Verlag. p. 23.ISBN 978-3-89675-578-0.
  11. ^abMcGrath, Matthew; Frank, Devin (2023),"Propositions", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Winter 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved22 March 2024
  12. ^"Predicate Logic".www3.cs.stonybrook.edu. Retrieved22 March 2024.
  13. ^"Philosophy 404: Lecture Five".www.webpages.uidaho.edu. Retrieved22 March 2024.
  14. ^abc"3.1 Propositional Logic".www.teach.cs.toronto.edu. Retrieved22 March 2024.
  15. ^abcdefghiDavis, Steven; Gillon, Brendan S., eds. (2004).Semantics: a reader. New York: Oxford University Press.ISBN 978-0-19-513697-5.
  16. ^abcdefgPlato, Jan von (2013).Elements of logical reasoning (1. publ ed.). Cambridge: Cambridge University press. pp. 9, 32, 121.ISBN 978-1-107-03659-8.
  17. ^ab"Propositional Logic".www.cs.miami.edu. Retrieved22 March 2024.
  18. ^Plato, Jan von (2013).Elements of logical reasoning (1. publ ed.). Cambridge: Cambridge University press. p. 9.ISBN 978-1-107-03659-8.
  19. ^abWeisstein, Eric W."Connective".Wolfram MathWorld. Retrieved9 August 2025.
  20. ^"Propositional Logic | Brilliant Math & Science Wiki".brilliant.org. Retrieved20 August 2020.
  21. ^Bobzien, Susanne (1 January 2016). "Ancient Logic". In Zalta, Edward N. (ed.).The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University – via Stanford Encyclopedia of Philosophy.
  22. ^"Propositional Logic | Internet Encyclopedia of Philosophy". Retrieved20 August 2020.
  23. ^Bobzien, Susanne (2020),"Ancient Logic", in Zalta, Edward N. (ed.),The Stanford Encyclopedia of Philosophy (Summer 2020 ed.), Metaphysics Research Lab, Stanford University, retrieved22 March 2024
  24. ^Peckhaus, Volker (1 January 2014). "Leibniz's Influence on 19th Century Logic". In Zalta, Edward N. (ed.).The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University – via Stanford Encyclopedia of Philosophy.
  25. ^Hurley, Patrick (2007).A Concise Introduction to Logic 10th edition. Wadsworth Publishing. p. 392.
  26. ^Beth, Evert W.; "Semantic entailment and formal derivability", series: Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, Nieuwe Reeks, vol. 18, no. 13, Noord-Hollandsche Uitg. Mij., Amsterdam, 1955, pp. 309–42. Reprinted in Jaakko Intikka (ed.)The Philosophy of Mathematics, Oxford University Press, 1969
  27. ^abTruth in Frege
  28. ^abc"Russell: the Journal of Bertrand Russell Studies". Archived fromthe original on 3 November 2013. Retrieved6 January 2012.
  29. ^Anellis, Irving H. (2012). "Peirce's Truth-functional Analysis and the Origin of the Truth Table".History and Philosophy of Logic.33:87–97.doi:10.1080/01445340.2011.621702.S2CID 170654885.
  30. ^"Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables".www.math.fsu.edu. Retrieved22 March 2024.
  31. ^"Lecture Notes on Logical Organization and Critical Thinking".www2.hawaii.edu. Retrieved22 March 2024.
  32. ^"Logical Connectives".sites.millersville.edu. Retrieved22 March 2024.
  33. ^"Lecture1".www.cs.columbia.edu. Retrieved22 March 2024.
  34. ^abcd"Introduction to Logic - Chapter 2".intrologic.stanford.edu. Retrieved22 March 2024.
  35. ^abcdefghijklmnopqrstuvwxyzaaabacadaeafagahaiajakalamanaoapaqarasatauavawaxBeall, Jeffrey C. (2010).Logic: the basics (1. publ ed.). London: Routledge. pp. 6, 8,14–16,19–20,44–48,50–53, 56.ISBN 978-0-203-85155-5.
  36. ^"Watson".watson.latech.edu. Retrieved22 March 2024.
  37. ^"Introduction to Theoretical Computer Science, Chapter 1".www.cs.odu.edu. Retrieved22 March 2024.
  38. ^abcdefghijklmnopqrstuvwxyBostock, David (1997).Intermediate logic. Oxford : New York: Clarendon Press; Oxford University Press. pp. 4–5,8–13,18–19, 22, 27, 29, 191, 194.ISBN 978-0-19-875141-0.
  39. ^abcdefghijklmnopqrstuvwxyzaaabacadaeafagahaiajakalamanaoapaqarasatauavawaxayazbabbbcbdbebfbgbhbibjbkblbmbnbobpbqbrAllen, Colin; Hand, Michael (2022).Logic primer (3rd ed.). Cambridge, Massachusetts: The MIT Press.ISBN 978-0-262-54364-4.
  40. ^abcdefghijklmnopqrstHowson, Colin (1997).Logic with trees: an introduction to symbolic logic. London; New York: Routledge. pp. ix, x,5–6,15–16, 20,24–29, 38,42–43, 47.ISBN 978-0-415-13342-5.
  41. ^Stojnić, Una (2017)."One's Modus Ponens: Modality, Coherence and Logic".Philosophy and Phenomenological Research.95 (1):167–214.doi:10.1111/phpr.12307.ISSN 0031-8205.JSTOR 48578954.
  42. ^Dutilh Novaes, Catarina (2022),"Argument and Argumentation", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Fall 2022 ed.), Metaphysics Research Lab, Stanford University, retrieved5 April 2024
  43. ^abcde"Validity and Soundness | Internet Encyclopedia of Philosophy". Retrieved5 April 2024.
  44. ^abcdefPelletier, Francis Jeffry; Hazen, Allen (2024),"Natural Deduction Systems in Logic", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Spring 2024 ed.), Metaphysics Research Lab, Stanford University, retrieved22 March 2024
  45. ^abRestall, Greg (2018),"Substructural Logics", in Zalta, Edward N. (ed.),The Stanford Encyclopedia of Philosophy (Spring 2018 ed.), Metaphysics Research Lab, Stanford University, retrieved22 March 2024
  46. ^abcd"Compactness | Internet Encyclopedia of Philosophy". Retrieved22 March 2024.
  47. ^ab"Lecture Topics for Discrete Math Students".math.colorado.edu. Retrieved22 March 2024.
  48. ^Paseau, Alexander; Pregel, Fabian (2023),"Deductivism in the Philosophy of Mathematics", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved22 March 2024
  49. ^abDemey, Lorenz; Kooi, Barteld; Sack, Joshua (2023),"Logic and Probability", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Fall 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved22 March 2024
  50. ^abcdefghKleene, Stephen Cole (2002).Mathematical logic (Dover ed.). Mineola, N.Y: Dover Publications.ISBN 978-0-486-42533-7.
  51. ^abcHumberstone, Lloyd (2011).The connectives. Cambridge, Mass: MIT Press. pp. 118, 702.ISBN 978-0-262-01654-4.OCLC 694679197.
  52. ^abcdefghijklmSmullyan, Raymond M. (1995) [1968].First-Order Logic. New York:Dover Publications. pp. 5,10–11, 14.ISBN 978-0-486-68370-6.
  53. ^Russell, Bertrand (2010).Principles of mathematics. Routledge classics. London: Routledge. p. 17.ISBN 978-0-415-48741-2.
  54. ^Makridis, Odysseus (2022).Symbolic Logic. Palgrave Philosophy Today. p. 87.doi:10.1007/978-3-030-67396-3.ISBN 978-3-030-67395-6.ISSN 2947-9339.
  55. ^abHodges, Wilfrid (1977).Logic. Harmondsworth; New York: Penguin. pp. 80–85.ISBN 978-0-14-021985-2.
  56. ^abcdHansson, Sven Ove; Hendricks, Vincent F. (2018).Introduction to formal philosophy. Springer undergraduate texts in philosophy. Cham: Springer. p. 38.ISBN 978-3-030-08454-7.
  57. ^Ayala-Rincón, Mauricio; de Moura, Flávio L.C. (2017).Applied Logic for Computer Scientists. Undergraduate Topics in Computer Science. Springer. p. 2.doi:10.1007/978-3-319-51653-0.ISBN 978-3-319-51651-6.
  58. ^abLande, Nelson P. (2013).Classical logic and its rabbit holes: a first course. Indianapolis, Ind: Hackett Publishing Co., Inc. p. 20.ISBN 978-1-60384-948-7.
  59. ^Goldrei, Derek (2005).Propositional and predicate calculus: a model of argument. London: Springer. p. 69.ISBN 978-1-85233-921-0.
  60. ^"Propositional Logic".www.cs.rochester.edu. Retrieved22 March 2024.
  61. ^"Propositional calculus".www.cs.cornell.edu. Retrieved22 March 2024.
  62. ^abShramko, Yaroslav; Wansing, Heinrich (2021),"Truth Values", in Zalta, Edward N. (ed.),The Stanford Encyclopedia of Philosophy (Winter 2021 ed.), Metaphysics Research Lab, Stanford University, retrieved23 March 2024
  63. ^Metcalfe, David; Powell, John (2011)."Should doctors spurn Wikipedia?".Journal of the Royal Society of Medicine.104 (12):488–489.doi:10.1258/jrsm.2011.110227.ISSN 0141-0768.PMC 3241521.PMID 22179287.
  64. ^Ayers, Phoebe; Matthews, Charles; Yates, Ben (2008).How Wikipedia works: and how you can be a part of it. San Francisco: No Starch Press. p. 22.ISBN 978-1-59327-176-3.OCLC 185698411.
  65. ^Shapiro, Stewart; Kouri Kissel, Teresa (2024),"Classical Logic", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Spring 2024 ed.), Metaphysics Research Lab, Stanford University, retrieved25 March 2024
  66. ^abcdLandman, Fred (1991).Structures for Semantics. Studies in Linguistics and Philosophy. Vol. 45. p. 127.doi:10.1007/978-94-011-3212-1.ISBN 978-0-7923-1240-6.ISSN 0924-4662.
  67. ^Fitting, Melvin (6 December 2012).First-Order Logic and Automated Theorem Proving. Springer Science & Business Media. p. 16.ISBN 978-1-4612-2360-3.
  68. ^Nascimento, Marco Antonio Chaer (2015).Frontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013). Progress in theoretical chemistry and physics. International Workshop on Quantum Systems in Chemistry and Physics. Cham: Springer. p. 255.ISBN 978-3-319-14397-2.
  69. ^abcdefgChowdhary, K.R. (2020).Fundamentals of Artificial Intelligence. pp. 31–34.doi:10.1007/978-81-322-3972-7.ISBN 978-81-322-3970-3.
  70. ^Restall, Greg; Standefer, Shawn (3 January 2023).Logical Methods. MIT Press. p. 76.ISBN 978-0-262-54484-9.
  71. ^abcdefghijklmnopqrstHunter, Geoffrey (1971).Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Press.ISBN 0-520-02356-0.
  72. ^abcdefghRestall, Greg (2010).Logic: an introduction. Fundamentals of philosophy. London: Routledge. pp. 5,36–41,55–60, 69.ISBN 978-0-415-40068-8.
  73. ^Aloni, Maria (2023),"Disjunction", in Zalta, Edward N.; Nodelman, Uri (eds.),The Stanford Encyclopedia of Philosophy (Spring 2023 ed.), Metaphysics Research Lab, Stanford University, retrieved23 March 2024
  74. ^Makridis, Odysseus (2022).Symbolic logic. Palgrave philosophy today. Cham, Switzerland: Palgrave Macmillan. p. 119.ISBN 978-3-030-67395-6.
  75. ^Burgess, John P. (2009).Philosophical logic. Princeton foundations of contemporary philosophy. Princeton: Princeton University Press. p. 5.ISBN 978-0-691-13789-6.OCLC 276141382.
  76. ^abBeall, J. C.; Restall, Greg (2006).Logical Pluralism. Clarendon Press. p. 38.ISBN 978-0-19-928840-3.
  77. ^Levin, Oscar.Propositional Logic.
  78. ^abSmith, Peter (2003),An introduction to formal logic,Cambridge University Press,ISBN 978-0-521-00804-4. (Defines "expressively adequate", shortened to "adequate set of connectives" in a section heading.)
  79. ^Cunningham, Daniel W. (2016).Set theory: a first course. Cambridge mathematical textbooks. New York, NY: Cambridge University Press.ISBN 978-1-107-12032-7.
  80. ^abGenesereth, Michael; Kao, Eric J. (2017).Introduction to Logic. Synthesis Lectures on Computer Science. Cham: Springer International Publishing. p. 18.doi:10.1007/978-3-031-01801-5.ISBN 978-3-031-00673-9.
  81. ^abcdefgRogers, Robert L. (1971).Mathematical Logic and Formalized Theories. Elsevier. pp. 38–39.doi:10.1016/c2013-0-11894-6.ISBN 978-0-7204-2098-2.
  82. ^"6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation".leanprover.github.io. Retrieved28 March 2024.
  83. ^"Knowledge Representation and Reasoning: Basics of Logics".www.emse.fr. Retrieved28 March 2024.
  84. ^ab"1.4: Tautologies and contradictions".Mathematics LibreTexts. 9 September 2021. Retrieved29 March 2024.
  85. ^abSylvestre, Jeremy.EF Tautologies and contradictions.
  86. ^abDeLancey, Craig; Woodrow, Jenna (2017).Elementary Formal Logic (1 ed.). Pressbooks.
  87. ^Dix, J.; Fisher, Michael; Novak, Peter, eds. (2010).Computational logic in multi-agent systems: 10th international workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009: revised selected and invited papers. Lecture notes in computer science. Berlin; New York: Springer. p. 49.ISBN 978-3-642-16866-6.OCLC 681481210.
  88. ^Prakken, Henry; Bistarelli, Stefano; Santini, Francesco; Taticchi, Carlo, eds. (2020).Computational models of argument: proceedings of comma 2020. Frontiers in artificial intelligence and applications. Washington: IOS Press. p. 252.ISBN 978-1-64368-106-1.
  89. ^Awodey, Steve; Arnold, Greg Frost-, eds. (2024).Rudolf Carnap: studies in semantics: the collected works of rudolf carnap, volume 7. New York: Oxford University Press. pp. xxvii.ISBN 978-0-19-289487-8.
  90. ^Harel, Guershon; Stylianides, Andreas J., eds. (2018).Advances in Mathematics Education Research on Proof and Proving: An International Perspective. ICME-13 Monographs (1st ed. 2018 ed.). Cham: Springer International Publishing : Imprint: Springer. p. 181.ISBN 978-3-319-70996-3.
  91. ^DeLancey, Craig (2017)."A Concise Introduction to Logic: §4. Proofs".Milne Publishing. Retrieved23 March 2024.
  92. ^Ferguson, Thomas Macaulay; Priest, Graham (23 June 2016),"semantic consequence",A Dictionary of Logic, Oxford University Press,doi:10.1093/acref/9780191816802.001.0001,ISBN 978-0-19-181680-2, retrieved23 March 2024
  93. ^Ferguson, Thomas Macaulay; Priest, Graham (23 June 2016),"syntactic consequence",A Dictionary of Logic, Oxford University Press,doi:10.1093/acref/9780191816802.001.0001,ISBN 978-0-19-181680-2, retrieved23 March 2024
  94. ^abcCook, Roy T. (2009).A dictionary of philosophical logic. Edinburgh: Edinburgh University Press. pp. 82, 176.ISBN 978-0-7486-2559-8.
  95. ^"Truth table | Boolean, Operators, Rules | Britannica".www.britannica.com. 14 March 2024. Retrieved23 March 2024.
  96. ^abc"MathematicalLogic".www.cs.yale.edu. Retrieved23 March 2024.
  97. ^"Analytic Tableaux".www3.cs.stonybrook.edu. Retrieved23 March 2024.
  98. ^"Formal logic - Semantic Tableaux, Proofs, Rules | Britannica".www.britannica.com. Retrieved23 March 2024.
  99. ^"Axiomatic method | Logic, Proofs & Foundations | Britannica".www.britannica.com. Retrieved23 March 2024.
  100. ^"Propositional Logic".mally.stanford.edu. Retrieved23 March 2024.
  101. ^ab"Natural Deduction | Internet Encyclopedia of Philosophy". Retrieved23 March 2024.
  102. ^abWeisstein, Eric W."Sequent Calculus".Wolfram MathWorld. Retrieved9 August 2025.
  103. ^"Interactive Tutorial of the Sequent Calculus".logitext.mit.edu. Retrieved23 March 2024.
  104. ^Lucas, Peter; Gaag, Linda van der (1991).Principles of expert systems(PDF). International computer science series. Wokingham, England; Reading, Mass: Addison-Wesley. p. 26.ISBN 978-0-201-41640-4.
  105. ^Bachmair, Leo (2009)."CSE541 Logic in Computer Science"(PDF).Stony Brook University.
  106. ^Lawson, Mark V. (2019).A first course in logic. Boca Raton: CRC Press, Taylor & Francis Group. pp. example 1.58.ISBN 978-0-8153-8664-3.
  107. ^Dean, Neville (2003).Logic and language. Basingstoke: Palgrave Macmillan. p. 66.ISBN 978-0-333-91977-4.
  108. ^Chiswell, Ian; Hodges, Wilfrid (2007).Mathematical logic. Oxford texts in logic. Oxford: Oxford university press. p. 3.ISBN 978-0-19-857100-1.
  109. ^abcdefghijklmnoHodges, Wilfrid (2001).Logic (2 ed.). London: Penguin Books. pp. 130–131.ISBN 978-0-14-100314-6.
  110. ^Toida, Shunichi (2 August 2009)."Proof of Implications".CS381 Discrete Structures/Discrete Mathematics Web Course Material. Department of Computer Science,Old Dominion University. Retrieved10 March 2010.
  111. ^abcdefghijklmnopqrstuvwxyzaaabacadaeafagahLemmon, Edward John (1998).Beginning logic. Boca Raton, FL: Chapman & Hall/CRC. pp. passim, especially 39–40.ISBN 978-0-412-38090-7.
  112. ^"Natural Deduction Systems in Logic > Notes (Stanford Encyclopedia of Philosophy)".plato.stanford.edu. Retrieved19 April 2024.
  113. ^abcdefArthur, Richard T. W. (2017).An introduction to logic: using natural deduction, real arguments, a little history, and some humour (2nd ed.). Peterborough, Ontario: Broadview Press.ISBN 978-1-55481-332-2.OCLC 962129086.
  114. ^abcdefgSmullyan, Raymond M. (23 July 2014).A Beginner's Guide to Mathematical Logic. Courier Corporation. pp. 102–103.ISBN 978-0-486-49237-7.
  115. ^abMendelsohn, Richard L. (10 January 2005).The Philosophy of Gottlob Frege. Cambridge University Press. p. 185.ISBN 978-1-139-44403-3.
  116. ^abŁukasiewicz, Jan (1970).Jan Lukasiewicz: Selected Works. North-Holland. p. 136.
  117. ^abChurch, Alonzo (1996).Introduction to Mathematical Logic. Princeton University Press. p. 119.ISBN 978-0-691-02906-1.
  118. ^abcd"Proof Explorer - Home Page - Metamath".us.metamath.org. Retrieved2 July 2024.
  119. ^abWalicki, Michał (2017).Introduction to mathematical logic (Extended ed.). New Jersey: World Scientific. p. 126.ISBN 978-981-4719-95-7.
  120. ^Quine, W. V. O. (1980).Mathematical Logic.Harvard University Press.ISBN 0-674-55451-5.

Further reading

[edit]
  • Brown, Frank Markham (2003),Boolean Reasoning: The Logic of Boolean Equations, 1st edition, Kluwer Academic Publishers, Norwell, MA. 2nd edition, Dover Publications, Mineola, NY.
  • Chang, C.C. andKeisler, H.J. (1973),Model Theory, North-Holland, Amsterdam, Netherlands.
  • Kohavi, Zvi (1978),Switching and Finite Automata Theory, 1st edition, McGraw–Hill, 1970. 2nd edition, McGraw–Hill, 1978.
  • Korfhage, Robert R. (1974),Discrete Computational Structures, Academic Press, New York, NY.
  • Lambek, J. and Scott, P.J. (1986),Introduction to Higher Order Categorical Logic, Cambridge University Press, Cambridge, UK.
  • Mendelson, Elliot (1964),Introduction to Mathematical Logic, D. Van Nostrand Company.

Related works

[edit]

External links

[edit]
Wikimedia Commons has media related toPropositional logic.
General
Law of noncontradiction
Classical logics
Principles
Rules
Introduction
Elimination
People
Works
Commonfallacies (list)
Formal
Inpropositional logic
Inquantificational logic
Syllogistic fallacy
Informal
Equivocation
Question-begging
Correlative-based
Illicit transference
Secundum quid
Faulty generalization
Ambiguity
Questionable cause
Appeals
Consequences
Emotion
Genetic fallacy
Ad hominem
Otherfallacies
of relevance
Arguments
General
Theorems (list)
 and paradoxes
Logics
Traditional
Propositional
Predicate
Set theory
Types ofsets
Maps and cardinality
Set theories
Formal systems (list),
language and syntax
Example axiomatic
systems (list)
Proof theory
Model theory
Computability theory
Related
International
National
Retrieved from "https://en.wikipedia.org/w/index.php?title=Propositional_logic&oldid=1316791515"
Categories:
Hidden categories:
[8]ページ先頭
©2009-2025 Movatter.jp