Propositional calculus
Encyclopedia
In mathematical logic
, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system
in which formulas
of a formal language
may be interpreted
as representing propositions. A system
of inference rules
and axiom
s allows certain formulas to be derived, called theorem
s; which may be interpreted as true propositions. The series of formulas which is constructed within such a system is called a derivation
and the last formula of the series is a theorem, whose derivation may be interpreted as a proof of the truth of the proposition represented by the theorem.
Truth-functional propositional logic is a propositional logic whose interpretation limits the truth values of its propositions to two, usually true and false. Truth-functional propositional logic and systems isomorphic to it are considered to be zeroth-order logic
.
that consists of a set of syntactic expressions (well-formed formulæ
or wffs), a distinguished subset of these expressions (axioms), plus a set of formal rules that define a specific binary relation
, intended to be interpreted as logical equivalence
, on the space of expressions.
When the formal system is intended to be a logical system, the expressions are meant to be interpreted as statements, and the rules, known as inference rules, are typically intended to be truth-preserving. In this setting, the rules (which may include axioms) can then be used to derive ("infer") formulæ representing true statements from given formulæ representing true statements.
The set of axioms may be empty, a nonempty finite set, a countably infinite set, or be given by axiom schema
ta. A formal grammar
recursively defines the expressions and well-formed formulæ (wffs) of the language
. In addition a semantics
may be given which defines truth and valuation
s (or interpretations
).
The language
of a propositional calculus consists of
A well-formed formula
(wff) is any atomic formula, or any formula that can be built up from atomic formulæ by means of operator symbols according to the rules of the grammar.
Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schemata, however, range over all propositions. It is common to represent propositional constants by
, 
, and 
, propositional variables by 
, 
, and 
, and schematic letters are often Greek letters, most often 
, 
, and 
.
We may represent any given proposition with a letter which we call a propositional constant, analogous to representing a number by a letter in mathematics, for instance,
. We require that all propositions have exactly one of two truth-values: true or false. To take an example, let 
be the proposition that it is raining outside. This will be true if it is raining outside and false otherwise.
It is extremely helpful to look at the truth table
s for these different operators, as well as the method of analytic tableaux
.
, 
is also a proposition. Likewise, for any propositions 
and 
, 
is a proposition, and similarly for disjunction, conditional, and biconditional. This implies that, for instance, 
is a proposition, and so it can be conjoined with another proposition. In order to represent this, we need to use parentheses to indicate which proposition is conjoined with which. For instance, 
is not a well-formed formula, because we do not know if we are conjoining 
with 
or if we are conjoining 
with 
. Thus we must write either 
to represent the former, or 
to represent the latter. By evaluating the truth conditions, we see that both expressions have the same truth conditions (will be true in the same cases), and moreover that any proposition formed by arbitrary conjunctions will have the same truth conditions, regardless of the location of the parentheses. This means that conjunction is associative, however, one should not assume that parentheses never serve a purpose. For instance, the sentence 
does not have the same truth conditions as 
, so they are different sentences distinguished only by the parentheses. One can verify this by the truth-table method referenced above.
Note: For any arbitrary number of propositional constants, we can form a finite number of cases which list their possible truth-values. A simple way to generate this is by truth-tables, in which one writes
, 
, …, 
for any list of 
propositional constants—that is to say, any list of propositional constants with 
entries. Below this list, one writes 
rows, and below 
one fills in the first half of the rows with true (or T) and the second half with false (or F). Below 
one fills in one-quarter of the rows with T, then one-quarter with F, then one-quarter with T and the last quarter with F. The next column alternates between true and false for each eighth of the rows, then sixteenths, and so on, until the last propositional constant varies between T and F for each row. This will give a complete listing of cases or truth-value assignments possible for those propositional constants.
as a set of propositions. A valid argument is a set of propositions, the last of which follows from—or is implied by—the rest. All other arguments are invalid. The simplest valid argument is modus ponens
, one instance of which is the following set of propositions:
This is a set of three propositions, each line is a proposition, and the last follows from the rest. The first two lines are called premises, and the last line the conclusion. We say that any proposition
follows from any set of propositions 
, if 
must be true whenever every member of the set 
is true. In the argument above, for any 
and 
, whenever 
and 
are true, necessarily 
is true. Notice that, when 
is true, we cannot consider cases 3 and 4 (from the truth table). When 
is true, we cannot consider case 2. This leaves only case 1, in which Q is also true. Thus Q is implied by the premises.
This generalizes schematically. Thus, where
and 
may be any propositions at all,
Other argument forms are convenient, but not necessary. Given a complete set of axioms (see below for one such set), modus ponens is sufficient to prove all other argument forms in propositional logic, and so we may think of them as derivative. Note, this is not true of the extension of propositional logic to other logics like first-order logic
. First-order logic requires at least one additional rule of inference in order to obtain completeness
.
The significance of argument in formal logic is that one may obtain new truths from established truths. In the first example above, given the two premises, the truth of
is not yet known or stated. After the argument is made, 
is deduced. In this way, we define a deduction system as a set of all propositions that may be deduced from another set of propositions. For instance, given the set of propositions 
, we can define a deduction system, 
, which is the set of all propositions which follow from 
. Reiteration is always assumed, so 
. Also, from the first element of 
, last element, as well as modus ponens, 
is a consequence, and so 
. Because we have not included sufficiently complete axioms, though, nothing else may be deduced. Thus, even though most deduction systems studied in propositional logic are able to deduce 
, this one is too weak to prove such a proposition.
, where:
The language of
, also known as its set of formulæ, well-formed formula
s or wffs, is inductively defined by the following rules:
Repeated applications of these rules permits the construction of complex formulæ. For example:
, where 
, 
, 
, 
are defined as follows:
/>Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set
partition as follows:
, where 
, 
, 
, 
are defined as follows:
In the following example of a propositional calculus, the transformation rules are intended to be interpreted as the inference rules of a so-called natural deduction system. The particular system presented here has no initial points, which means that its interpretation for logical applications derives its theorem
s from an empty axiom set.
Our propositional calculus has ten inference rules. These rules allow us to derive other true formulae given a set of formulae that are assumed to be true. The first nine simply state that we can infer certain wffs from other wffs. The last rule however uses hypothetical reasoning in the sense that in the premise of the rule we temporarily assume an (unproven) hypothesis to be part of the set of inferred formulae to see if we can infer a certain other formula. Since the first nine rules don't do this they are usually described as non-hypothetical rules, and the last one as a hypothetical rule.
Reductio ad absurdum
(negation introduction) : From
and [accepting 
leads to a proof that 
], infer 
.
Double negative elimination
: From
, infer 
.
Conjunction introduction
: From
and 
, infer 
.
Conjunction elimination: From
, infer 
.
Disjunction introduction
: From
, infer 
.
Disjunction elimination
: From
and 
and 
, infer 
.
Biconditional introduction
: From
and 
, infer 
.
Biconditional elimination
: From
, infer 
.
Modus ponens
(conditional elimination) : From
and 
, infer 
.
Conditional proof
(conditional introduction) : From [accepting
allows a proof of 
], infer 
.
In the discussion to follow, a proof is presented as a sequence of numbered lines, with each line consisting of a single formula followed by a reason or justification for introducing that formula. Each premise of the argument, that is, an assumption introduced as an hypothesis of the argument, is listed at the beginning of the sequence and is marked as a "premise" in lieu of other justification. The conclusion is listed on the last line. A proof is complete if every line follows from the previous ones by the correct application of a transformation rule. (For a contrasting approach, see proof-trees
).
Interpret
as "Assuming 
, infer 
". Read 
as "Assuming nothing, infer that 
implies 
", or "It is a tautology that 
implies 
", or "It is always true that 
implies 
".
and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows.
We define a truth assignment as a function
that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs
(or possible world
) where certain statements are true and others are not. The semantics of formulae can then be formalized by defining for which "state of affairs" they are considered to be true, which is what is done by the following definition.
We define when such a truth assignment
satisfies a certain wff
with the following rules:
With this definition we can now formalize what it means for a formula
to be implied by a certain set 
of formulae. Informally this is true if in all worlds that are possible given the set of formulae 
the formula 
also holds. This leads to the following formal definition: We say that a set 
of wffs semantically entails (or implies) a certain wff 
if all truth assignments that satisfy all the formulae in 
also satisfy 
Finally we define syntactical entailment such that
is syntactically entailed by 
if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:
Soundness : If the set of wffs
syntactically entails wff 
then 
semantically entails 
Completeness : If the set of wffs
semantically entails wff 
then 
syntactically entails 
For the above set of rules this is indeed the case.
Notational conventions: Let
be a variable ranging over sets of sentences. Let 
, 
, and 
range over sentences. For "
syntactically entails 
" we write "
proves 
". For "
semantically entails 
" we write "
implies 
".
We want to show: (
)(
)(if 
proves 
, then 
implies 
).
We note that "
proves 
" has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If 
proves 
, then ...". So our proof proceeds by induction.
Notice that Basis Step II can be omitted for natural deduction
systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth
.
The Basis step(s) demonstrate(s) that the simplest provable sentences from
are also implied by 
, for any 
. (The is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable—by considering each case where we might reach a logical conclusion using an inference rule—and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from "
" we can derive "
or 
". In III.a We assume that if 
is provable it is implied. We also know that if 
is provable then "
or 
" is provable. We have to show that then "
or 
" too is implied. We do so by appeal to the semantic definition and the assumption we just made. 
is provable from 
, we assume. So it is also implied by 
. So any semantic valuation making all of 
true makes 
true. But any valuation making 
true makes "
or 
" true, by the defined semantics for "or". So any valuation which makes all of 
true makes "
or 
" true. So "
or 
" is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case analysis of all the rules of inference, showing that each "preserves" semantic implication.
By the definition of provability, there are no sentences provable other than by being a member of
, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.
We adopt the same notational conventions as above.
We want to show: If
implies 
, then 
proves 
. We proceed by contraposition
: We show instead that if
does not prove 
then 
does not imply 
.
QED
, then there is a truth table
for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulae, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using "(P is true implies S) implies ((P is false implies S) implies S)". Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.
is an assignment to each propositional symbol
of
of one or the other (but not both) of the truth values truth
(T) and falsity (F), and an assignment to the connective symbols
of
of their usual truth-functional meanings. An interpretation of a truth-functional propositional calculus may also be expressed in terms of truth tables.
For
distinct propositional symbols there are 
distinct possible interpretations. For any particular symbol 
, for example, there are 
possible interpretations:
For the pair
, 
there are 
possible interpretations:
Since
has 
, that is, denumerably many propositional symbols, there are 
, and therefore uncountably many
distinct possible interpretations of
.
and 
are formulas of 
and 
is an interpretation of 
then:
Some consequences of these definitions:
, 
and 
stand for well-formed formulæ. (The wffs themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:
:
.
and the conclusion to the right of the turnstile. Then the deduction theorem
can be stated as follows:
This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.
On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof
inference rule which is part of the first version of propositional calculus introduced in this article.
The converse of DT is also valid:
in fact, the validity of the converse of DT is almost trivial compared to that of DT:
The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, the axiom AND-1,
can be transformed by means of the converse of the deduction theorem into the inference rule
which is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.
Prove:
(Reflexivity of implication).
Proof:
. In the case of propositional systems the axioms are terms built with logical connectives and the only inference rule is modus ponens. Equational logic as standardly used informally in high school algebra is a different kind of calculus from Hilbert systems. Its theorems are equations and its inference rules express the properties of equality, namely that it is a congruence on terms that admits substitution.
Classical propositional calculus as described above is equivalent to Boolean algebra, while intuitionistic propositional calculus
is equivalent to Heyting algebra
. The equivalence is shown by translation in each direction of the theorems of the respective systems. Theorems
of classical or intuitionistic propositional calculus are translated as equations 
of Boolean or Heyting algebra respectively. Conversely theorems 
of Boolean or Heyting algebra are translated as theorems 
of classical or propositional calculus respectively, for which 
is a standard abbreviation. In the case of Boolean algebra 
can also be translated as 
, but this translation is incorrect intuitionistically.
In both Boolean and Heyting algebra, inequality
can be used in place of equality. The equality 
is expressible as a pair of inequalities 
and 
. Conversely the inequality 
is expressible as the equality 
, or as 
. The significance of inequality for Hilbert-style systems is that it corresponds to the latter's deduction or entailment
symbol
. An entailment
is translated in the inequality version of the algebraic framework as
Conversely the algebraic inequality
is translated as the entailment
The difference between implication
and inequality or entailment
or 
is that the former is internal to the logic while the latter is external. Internal implication between two terms is another term of the same kind. Entailment as external implication between two terms expresses a metatruth outside the language of the logic, and is considered part of the metalanguage
. Even when the logic under study is intuitionistic, entailment is ordinarily understood classically as two-valued: either the left side entails, or is less-or-equal to, the right side, or it is not.
Similar but more complex translations to and from algebraic logics are possible for natural deduction systems as described above and for the sequent calculus
. The entailments of the latter can be interpreted as two-valued, but a more insightful interpretation is as a set, the elements of which can be understood as abstract proofs organized as the morphisms of a category
. In this interpretation the cut rule of the sequent calculus corresponds to composition in the category. Boolean and Heyting algebras enter this picture as special categories having at most one morphism per homset, i.e., one proof per entailment, corresponding to the idea that existence of proofs is all that matters: any proof will do and there is no point in distinguishing them.
For example, there are many families of graphs
that are close enough analogues of formal languages that the concept of a calculus is quite easily and naturally extended to them. Indeed, many species of graphs arise as parse graphs in the syntactic analysis of the corresponding families of text structures. The exigencies of practical computation on formal languages frequently demand that text strings be converted into pointer structure renditions of parse graphs, simply as a matter of checking whether strings are wffs or not. Once this is done, there are many advantages to be gained from developing the graphical analogue of the calculus on strings. The mapping from strings to parse graphs is called parsing
and the inverse mapping from parse graphs to strings is achieved by an operation that is called traversing
the graph.
, which is largely supplanted in modern logic, is in some ways simpler — but in other ways more complex — than propositional calculus.) The most immediate way to develop a more complex logical calculus is to introduce rules that are sensitive to more fine-grained details of the sentences being used.
First-order logic
(aka first-order predicate logic) results when the "atomic sentences" of propositional logic are broken up into terms
, variable
s, predicates, and quantifiers, all keeping the rules of propositional logic with some new ones introduced. (For example, from "All dogs are mammals" we may infer "If Rover is a dog then Rover is a mammal".) With the tools of first-order logic it is possible to formulate a number of theories, either with explicit axioms or by rules of inference, that can themselves be treated as logical calculi. Arithmetic
is the best known of these; others include set theory
and mereology
. Second-order logic
and other higher-order logic
s are formal extensions of first-order logic. Thus, it makes sense to refer to propositional logic as "zeroth-order logic", when comparing it with these logics.
Modal logic
also offers a variety of inferences that cannot be captured in propositional calculus. For example, from "Necessarily
" we may infer that 
. From 
we may infer "It is possible that 
". The translation between modal logics and algebraic logics is as for classical and intuitionistic logics but with the introduction of a unary operator on Boolean or Heyting algebras, different from the Boolean operations, interpreting the possibility modality, and in the case of Heyting algebra a second operator interpreting necessity (for Boolean algebra this is redundant since necessity is the De Morgan dual of possibility). The first operator preserves 0 and disjunction while the second preserves 1 and conjunction.
Many-valued logics are those allowing sentences to have values other than true and false. (For example, neither and both are standard "extra values"; "continuum logic" allows each sentence to have any of an infinite number of "degrees of truth" between true and false.) These logics often require calculational devices quite distinct from propositional calculus. When the values form a Boolean algebra (which may have more than two or even infinitely many values), many-valued logic reduces to classical logic; many-valued logics are therefore only of independent interest when the values form an algebra that is not Boolean.
problem. However, practical methods exist (e.g., DPLL algorithm
, 1962; Chaff algorithm
, 2001) that are very fast for many useful cases. Recent work has extended the SAT solver algorithms to work with propositions containing arithmetic expressions; these are the SMT solvers.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a propositional calculus or logic (also called sentential calculus or sentential logic) is a formal system
Formal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
in which formulas
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
of a formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
may be interpreted
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
as representing propositions. A system
Deductive system
A deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
of inference rules
Rule of inference
In logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
and axiom
Axiom
In traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s allows certain formulas to be derived, called theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s; which may be interpreted as true propositions. The series of formulas which is constructed within such a system is called a derivation
Formal proof
A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
and the last formula of the series is a theorem, whose derivation may be interpreted as a proof of the truth of the proposition represented by the theorem.
Truth-functional propositional logic is a propositional logic whose interpretation limits the truth values of its propositions to two, usually true and false. Truth-functional propositional logic and systems isomorphic to it are considered to be zeroth-order logic
Zeroth-order logic
Zeroth-order logic is first-order logic without quantifiers. A finitely axiomatizable zeroth-order logic is isomorphic to a propositional logic. Zeroth-order logic with axiom schema is a more expressive system than propositional logic...
.
Terminology
In general terms, a calculus is a formal systemFormal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
that consists of a set of syntactic expressions (well-formed formulæ
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
or wffs), a distinguished subset of these expressions (axioms), plus a set of formal rules that define a specific binary relation
Binary relation
In mathematics, a binary relation on a set A is a collection of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2 = . More generally, a binary relation between two sets A and B is a subset of...
, intended to be interpreted as logical equivalence
Logical equivalence
In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...
, on the space of expressions.
When the formal system is intended to be a logical system, the expressions are meant to be interpreted as statements, and the rules, known as inference rules, are typically intended to be truth-preserving. In this setting, the rules (which may include axioms) can then be used to derive ("infer") formulæ representing true statements from given formulæ representing true statements.
The set of axioms may be empty, a nonempty finite set, a countably infinite set, or be given by axiom schema
Axiom schema
In mathematical logic, an axiom schema generalizes the notion of axiom.An axiom schema is a formula in the language of an axiomatic system, in which one or more schematic variables appear. These variables, which are metalinguistic constructs, stand for any term or subformula of the system, which...
ta. A formal grammar
Formal grammar
A formal grammar is a set of formation rules for strings in a formal language. The rules describe how to form strings from the language's alphabet that are valid according to the language's syntax...
recursively defines the expressions and well-formed formulæ (wffs) of the language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
. In addition a semantics
Semantics
Semantics is the study of meaning. It focuses on the relation between signifiers, such as words, phrases, signs and symbols, and what they stand for, their denotata....
may be given which defines truth and valuation
Valuation (logic)
In logic and model theory, a valuation can be:*In propositional logic, an assignment of truth values to propositional variables, with a corresponding assignment of truth values to all propositional formulas with those variables....
s (or interpretations
Interpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
).
The language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
of a propositional calculus consists of
- a set of primitive symbols, variously referred to as atomic formulaAtomic formulaIn mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
e, placeholders, proposition letters, or variables, and - a set of operator symbols, variously interpreted as logical operators or logical connectives.
A well-formed formula
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
(wff) is any atomic formula, or any formula that can be built up from atomic formulæ by means of operator symbols according to the rules of the grammar.
Mathematicians sometimes distinguish between propositional constants, propositional variables, and schemata. Propositional constants represent some particular proposition, while propositional variables range over the set of all atomic propositions. Schemata, however, range over all propositions. It is common to represent propositional constants by
, , and , propositional variables by , , and , and schematic letters are often Greek letters, most often , , and .Basic concepts
The following outlines a standard propositional calculus. Many different formulations exist which are all more or less equivalent but differ in the details of- their language, that is, the particular collection of primitive symbols and operator symbols,
- the set of axioms, or distinguished formulæ, and
- the set of inference rules.
We may represent any given proposition with a letter which we call a propositional constant, analogous to representing a number by a letter in mathematics, for instance,
. We require that all propositions have exactly one of two truth-values: true or false. To take an example, let be the proposition that it is raining outside. This will be true if it is raining outside and false otherwise.- We then define truth-functional operators, beginning with negation. We write
to represent the negation of 
, which can be thought of as the denial of 
. In the example above, 
expresses that it is not raining outside, or by a more standard reading: "It is not the case that it is raining outside." When 
is true, 
is false; and when 
is false, 
is true. 
always has the same truth-value as 
. - Conjunction is a truth-functional connective which forms a proposition out of two simpler propositions, for example,
and 
. The conjunction of 
and 
is written 
, and expresses that each are true. We read 
as "
and 
". For any two propositions, there are four possible assignments of truth values:
-
is true and 
is true -
is true and 
is false -
is false and 
is true -
is false and 
is false
-
- The conjunction of
and 
is true in case 1 and is false otherwise. Where 
is the proposition that it is raining outside and 
is the proposition that a cold-front is over Kansas, 
is true when it is raining outside and there is a cold-front over Kansas. If it is not raining outside, then 
is false; and if there is no cold-front over Kansas, then 
is false.
- Disjunction resembles conjunction in that it forms a proposition out of two simpler propositions. We write it
, and it is read "
or 
". It expresses that either 
or 
is true. Thus, in the cases listed above, the disjunction of 
and 
is true in all cases except 4. Using the example above, the disjunction expresses that it is either raining outside or there is a cold front over Kansas. (Note, this use of disjunction is supposed to resemble the use of the English word "or". However, it is most like the English inclusive "or", which can be used to express the truth of at least one of two propositions. It is not like the English exclusiveExclusive disjunctionThe logical operation exclusive disjunction, also called exclusive or , is a type of logical disjunction on two operands that results in a value of true if exactly one of the operands has a value of true...
"or", which expresses the truth of exactly one of two propositions. That is to say, the exclusive "or" is false when both
and 
are true (case 1). An example of the exclusive or is: You may have a bagel or a pastry, but not both. Sometimes, given the appropriate context, the addendum "but not both" is omitted but implied.) - Material conditional also joins two simpler propositions, and we write
, which is read "if 
then 
". The proposition to the left of the arrow is called the antecedent and the proposition to the right is called the consequent. (There is no such designation for conjunction or disjunction, since they are commutative operations.) It expresses that 
is true whenever 
is true. Thus it is true in every case above except case 2, because this is the only case when 
is true but 
is not. Using the example, if 
then 
expresses that if it is raining outside then there is a cold-front over Kansas. The material conditional is often confused with physical causation. The material conditional, however, only relates two propositions by their truth-values—which is not the relation of cause and effect. It is contentious in the literature whether the material implication represents logical causation. - Biconditional joins two simpler propositions, and we write
, which is read "
if and only if 
". It expresses that 
and 
have the same truth-value, thus 
if and only if 
is true in cases 1 and 4, and false otherwise.
- Disjunction resembles conjunction in that it forms a proposition out of two simpler propositions. We write it
It is extremely helpful to look at the truth table
Truth table
A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—to compute the functional values of logical expressions on each of their functional arguments, that is, on each combination of values taken by their...
s for these different operators, as well as the method of analytic tableaux
Method of analytic tableaux
In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure...
.
Closure under operations
Propositional logic is closed under truth-functional connectives. That is to say, for any proposition, is also a proposition. Likewise, for any propositions and , is a proposition, and similarly for disjunction, conditional, and biconditional. This implies that, for instance, is a proposition, and so it can be conjoined with another proposition. In order to represent this, we need to use parentheses to indicate which proposition is conjoined with which. For instance, is not a well-formed formula, because we do not know if we are conjoining with or if we are conjoining with . Thus we must write either to represent the former, or to represent the latter. By evaluating the truth conditions, we see that both expressions have the same truth conditions (will be true in the same cases), and moreover that any proposition formed by arbitrary conjunctions will have the same truth conditions, regardless of the location of the parentheses. This means that conjunction is associative, however, one should not assume that parentheses never serve a purpose. For instance, the sentence does not have the same truth conditions as , so they are different sentences distinguished only by the parentheses. One can verify this by the truth-table method referenced above.Note: For any arbitrary number of propositional constants, we can form a finite number of cases which list their possible truth-values. A simple way to generate this is by truth-tables, in which one writes
, , …, for any list of propositional constants—that is to say, any list of propositional constants with entries. Below this list, one writes rows, and below one fills in the first half of the rows with true (or T) and the second half with false (or F). Below one fills in one-quarter of the rows with T, then one-quarter with F, then one-quarter with T and the last quarter with F. The next column alternates between true and false for each eighth of the rows, then sixteenths, and so on, until the last propositional constant varies between T and F for each row. This will give a complete listing of cases or truth-value assignments possible for those propositional constants.Argument
The propositional calculus then defines an argumentArgument
In philosophy and logic, an argument is an attempt to persuade someone of something, or give evidence or reasons for accepting a particular conclusion.Argument may also refer to:-Mathematics and computer science:...
as a set of propositions. A valid argument is a set of propositions, the last of which follows from—or is implied by—the rest. All other arguments are invalid. The simplest valid argument is modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
, one instance of which is the following set of propositions:
This is a set of three propositions, each line is a proposition, and the last follows from the rest. The first two lines are called premises, and the last line the conclusion. We say that any proposition
follows from any set of propositions , if must be true whenever every member of the set is true. In the argument above, for any and , whenever and are true, necessarily is true. Notice that, when is true, we cannot consider cases 3 and 4 (from the truth table). When is true, we cannot consider case 2. This leaves only case 1, in which Q is also true. Thus Q is implied by the premises.This generalizes schematically. Thus, where
and may be any propositions at all,Other argument forms are convenient, but not necessary. Given a complete set of axioms (see below for one such set), modus ponens is sufficient to prove all other argument forms in propositional logic, and so we may think of them as derivative. Note, this is not true of the extension of propositional logic to other logics like first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
. First-order logic requires at least one additional rule of inference in order to obtain completeness
Completeness
In general, an object is complete if nothing needs to be added to it. This notion is made more specific in various fields.-Logical completeness:In logic, semantic completeness is the converse of soundness for formal systems...
.
The significance of argument in formal logic is that one may obtain new truths from established truths. In the first example above, given the two premises, the truth of
is not yet known or stated. After the argument is made, is deduced. In this way, we define a deduction system as a set of all propositions that may be deduced from another set of propositions. For instance, given the set of propositions , we can define a deduction system, , which is the set of all propositions which follow from . Reiteration is always assumed, so . Also, from the first element of , last element, as well as modus ponens, is a consequence, and so . Because we have not included sufficiently complete axioms, though, nothing else may be deduced. Thus, even though most deduction systems studied in propositional logic are able to deduce , this one is too weak to prove such a proposition.Generic description of a propositional calculus
A propositional calculus is a formal systemFormal system
In formal logic, a formal system consists of a formal language and a set of inference rules, used to derive an expression from one or more other premises that are antecedently supposed or derived . The axioms and rules may be called a deductive apparatus...
, where:- The alpha set
is a finite set of elements called proposition symbols or propositional variablePropositional variableIn mathematical logic, a propositional variable is a variable which can either be true or false...
s. Syntactically speaking, these are the most basic elements of the formal language
, otherwise referred to as atomic formulæAtomic formulaIn mathematical logic, an atomic formula is a formula with no deeper propositional structure, that is, a formula that contains no logical connectives or equivalently a formula that has no strict subformulas. Atoms are thus the simplest well-formed formulas of the logic...
or terminal elements. In the examples to follow, the elements of
are typically the letters 
, 
, 
, and so on.
- The omega set
is a finite set of elements called operator symbolsOperation (mathematics)The general operation as explained on this page should not be confused with the more specific operators on vector spaces. For a notion in elementary mathematics, see arithmetic operation....
or logical connectiveLogical connectiveIn logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s. The set
is partitionedPartition of a setIn mathematics, a partition of a set X is a division of X into non-overlapping and non-empty "parts" or "blocks" or "cells" that cover all of X...
into disjoint subsets as follows:
- In this partition,
is the set of operator symbols of arityArityIn logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the dimension of the domain in the corresponding Cartesian product...
.
- In the more familiar propositional calculi,
is typically partitioned as follows:
- A frequently adopted convention treats the constant logical valueLogical valueIn logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth.In classical logic, with its intended semantics, the truth values are true and false; that is, classical logic is a two-valued logic...
s as operators of arity zero, thus:
- Some writers use the tildeTildeThe tilde is a grapheme with several uses. The name of the character comes from Portuguese and Spanish, from the Latin titulus meaning "title" or "superscription", though the term "tilde" has evolved and now has a different meaning in linguistics....
(~), or N, instead of
; and some use the ampersandAmpersandAn ampersand is a logogram representing the conjunction word "and". The symbol is a ligature of the letters in et, Latin for "and".-Etymology:...
(&), the prefixed K, or
instead of 
. Notation varies even more for the set of logical values, with symbols like {false, true}, {F, T}, or 
all being seen in various contexts instead of {0, 1}.
- The zeta set
is a finite set of transformation rules that are called inference rules when they acquire logical applications.
- The iota set
is a finite set of initial points that are called axiomAxiomIn traditional logic, an axiom or postulate is a proposition that is not proven or demonstrated but considered either to be self-evident or to define and delimit the realm of analysis. In other words, an axiom is a logical statement that is assumed to be true...
s when they receive logical interpretations.
The language of
, also known as its set of formulæ, well-formed formulaWell-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
s or wffs, is inductively defined by the following rules:
- Base: Any element of the alpha set
is a formula of 
. - If
are formulæ and 
is in 
, then 
is a formula. - Closed: Nothing else is a formula of
.
Repeated applications of these rules permits the construction of complex formulæ. For example:
- By rule 1,
is a formula. - By rule 2,
is a formula. - By rule 1,
is a formula. - By rule 2,
is a formula.
Example 1. Simple axiom system
Let, where , , , are defined as follows:- The alpha set
, is a finite set of symbols that is large enough to supply the needs of a given discussion, for example:
- Of the three connectives for conjunction, disjunction, and implication (
, 
, and 
), one can be taken as primitive and the other two can be defined in terms of it and negation (
). Indeed, all of the logical connectives can be defined in terms of a sole sufficient operator. The biconditional (
) can of course be defined in terms of conjunction and implication, with 
defined as 
.
/>Adopting negation and implication as the two primitive operations of a propositional calculus is tantamount to having the omega set
partition as follows:
- An axiom system discovered by Jan Łukasiewicz formulates a propositional calculus in this language as follows. The axioms are all substitution instances of:
- The rule of inference is modus ponensModus ponensIn classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
(i.e., from
and 
, infer 
). Then 
is defined as 
, and 
is defined as 
.
Example 2. Natural deduction system
Let, where , , , are defined as follows:- The alpha set
, is a finite set of symbols that is large enough to supply the needs of a given discussion, for example:
-
- The omega set
partitions as follows:
-
In the following example of a propositional calculus, the transformation rules are intended to be interpreted as the inference rules of a so-called natural deduction system. The particular system presented here has no initial points, which means that its interpretation for logical applications derives its theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s from an empty axiom set.
- The set of initial points is empty, that is,
. - The set of transformation rules,
, is described as follows:
Our propositional calculus has ten inference rules. These rules allow us to derive other true formulae given a set of formulae that are assumed to be true. The first nine simply state that we can infer certain wffs from other wffs. The last rule however uses hypothetical reasoning in the sense that in the premise of the rule we temporarily assume an (unproven) hypothesis to be part of the set of inferred formulae to see if we can infer a certain other formula. Since the first nine rules don't do this they are usually described as non-hypothetical rules, and the last one as a hypothetical rule.
Reductio ad absurdum
Reductio ad absurdum
In logic, proof by contradiction is a form of proof that establishes the truth or validity of a proposition by showing that the proposition's being false would imply a contradiction...
(negation introduction) : From
and [accepting leads to a proof that ], infer .Double negative elimination
Double negative elimination
In propositional logic, the inference rules double negative elimination allow deriving the double negative equivalent by adding or removing a pair of negation signs...
: From
, infer .Conjunction introduction
Conjunction introduction
Conjunction introduction is the inference that, if p is true, and q is true, then the conjunction p and q is true.For example, if it's true that it's raining, and it's true that I'm inside, then it's true that "it's raining and I'm inside"....
: From
and , infer .Conjunction elimination: From
, infer .
- From
, infer 
.
Disjunction introduction
Disjunction introduction
Disjunction introduction or Addition is a valid, simple argument form in logic:or in logical operator notation: A \vdash A \or B The argument form has one premise, A, and an unrelated proposition, B...
: From
, infer .
- From
, infer 
.
Disjunction elimination
Disjunction elimination
In propositional logic disjunction elimination, or proof by cases, is the inference that, if "A or B" is true, and A entails C, and B entails C, then we may justifiably infer C...
: From
and and , infer .Biconditional introduction
Biconditional introduction
In mathematical logic, biconditional introduction is the rule of inference that, if B follows from A, and A follows from B, then A if and only if B....
: From
and , infer .Biconditional elimination
Biconditional elimination
Biconditional elimination allows one to infer a conditional from a biconditional: if is true, then one may infer either direction of the biconditional, and ....
: From
, infer .
- From
, infer 
.
Modus ponens
Modus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
(conditional elimination) : From
and , infer .Conditional proof
Conditional proof
A conditional proof is a proof that takes the form of asserting a conditional, and proving that the antecedent of the conditional necessarily leads to the consequent....
(conditional introduction) : From [accepting
allows a proof of ], infer .Basic and derived argument forms
| Basic and Derived Argument Forms | ||
|---|---|---|
| Name | Sequent | Description |
| Modus Ponens |  |
If  then  ;  ; therefore  |
| Modus Tollens |  |
If  then  ; not  ; therefore not  |
| Hypothetical Syllogism |  |
If  then  ; if  then  ; therefore, if  then  |
| Disjunctive Syllogism |  |
Either  or  , or both; not  ; therefore,  |
| Constructive Dilemma |  |
If  then  ; and if  then  ; but  or  ; therefore  or  |
| Destructive Dilemma |  |
If  then  ; and if  then  ; but not  or not  ; therefore not  or not  |
| Bidirectional Dilemma |  |
If  then  ; and if  then  ; but  or not  ; therefore  or not  |
| Simplification |  |
 and  are true; therefore  is true |
| Conjunction |  |
 and  are true separately; therefore they are true conjointly |
| Addition |  |
 is true; therefore the disjunction ( or  ) is true |
| Composition |  |
If  then  ; and if  then  ; therefore if  is true then  and  are true |
| De Morgan's Theorem (1) |  |
The negation of ( and  ) is equiv. to (not  or not  ) |
| De Morgan's Theorem (2) |  |
The negation of ( or  ) is equiv. to (not  and not  ) |
| Commutation (1) |  |
( or  ) is equiv. to ( or  ) |
| Commutation (2) |  |
( and  ) is equiv. to ( and  ) |
| Commutation (3) |  |
( is equiv. to  ) is equiv. to ( is equiv. to  ) |
| Association (1) |  |
 or ( or  ) is equiv. to ( or  ) or  |
| Association (2) |  |
 and ( and  ) is equiv. to ( and  ) and  |
| Distribution (1) |  |
 and ( or  ) is equiv. to ( and  ) or ( and  ) |
| Distribution (2) |  |
 or ( and  ) is equiv. to ( or  ) and ( or  ) |
| Double Negation |  |
 is equivalent to the negation of not  |
| Transposition |  |
If  then  is equiv. to if not  then not  |
| Material Implication |  |
If  then  is equiv. to not  or  |
| Material Equivalence (1) |  |
( is equiv. to  ) means (if  is true then  is true) and (if  is true then  is true) |
| Material Equivalence (2) |  |
( is equiv. to  ) means either ( and  are true) or (both  and  are false) |
| Material Equivalence (3) |  |
( is equiv. to  ) means, both ( or not  is true) and (not  or  is true) |
| Exportation |  |
from (if  and  are true then  is true) we can prove (if  is true then  is true, if  is true) |
| Importation |  |
If  then (if  then  ) is equivalent to if  and  then  |
| Tautology (1) |  |
 is true is equiv. to  is true or  is true |
| Tautology (2) |  |
 is true is equiv. to  is true and  is true |
| Tertium non datur (Law of Excluded Middle) |  |
 or not  is true |
| Law of Non-Contradiction |  |
 and not  is false, is a true statement |
Proofs in propositional calculus
One of the main uses of a propositional calculus, when interpreted for logical applications, is to determine relations of logical equivalence between propositional formulæ. These relationships are determined by means of the available transformation rules, sequences of which are called derivations or proofs.In the discussion to follow, a proof is presented as a sequence of numbered lines, with each line consisting of a single formula followed by a reason or justification for introducing that formula. Each premise of the argument, that is, an assumption introduced as an hypothesis of the argument, is listed at the beginning of the sequence and is marked as a "premise" in lieu of other justification. The conclusion is listed on the last line. A proof is complete if every line follows from the previous ones by the correct application of a transformation rule. (For a contrasting approach, see proof-trees
Method of analytic tableaux
In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first-order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure...
).
Example of a proof
- To be shown that
.
- One possible proof of this (which, though valid, happens to contain more steps than are necessary) may be arranged as follows:
| Example of a Proof | ||
|---|---|---|
| Number | Formula | Reason |
| 1 |  |
premise |
| 2 |  |
From (1) by disjunction introduction |
| 3 |  |
From (1) and (2) by conjunction introduction |
| 4 |  |
From (3) by conjunction elimination |
| 5 |  |
Summary of (1) through (4) |
| 6 |  |
From (5) by conditional proof |
Interpret
as "Assuming , infer ". Read as "Assuming nothing, infer that implies ", or "It is a tautology that implies ", or "It is always true that implies ".Soundness and completeness of the rules
The crucial properties of this set of rules are that they are soundSoundness
In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the property of preserving truth, but this is not the case in general. The word...
and complete. Informally this means that the rules are correct and that no other rules are required. These claims can be made more formal as follows.
We define a truth assignment as a function
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
that maps propositional variables to true or false. Informally such a truth assignment can be understood as the description of a possible state of affairs
State of affairs
The state of affairs is that combination of circumstances applying within a society or group at a particular time. The current state of affairs may be considered acceptable by many observers, but not necessarily by all. The state of affairs may present a challenge, or be complicated, or contain a...
(or possible world
Possible world
In philosophy and logic, the concept of a possible world is used to express modal claims. The concept of possible worlds is common in contemporary philosophical discourse and has also been disputed.- Possibility, necessity, and contingency :...
) where certain statements are true and others are not. The semantics of formulae can then be formalized by defining for which "state of affairs" they are considered to be true, which is what is done by the following definition.
We define when such a truth assignment
satisfies a certain wffWell-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
with the following rules:
-
satisfies the propositional variable 
if and only ifIf and only ifIn logic and related fields such as mathematics and philosophy, if and only if is a biconditional logical connective between statements....
-
satisfies 
if and only if 
does not satisfy 
-
satisfies 
if and only if 
satisfies both 
and 
-
satisfies 
if and only if 
satisfies at least one of either 
or 
-
satisfies 
if and only if it is not the case that 
satisfies 
but not 
-
satisfies 
if and only if 
satisfies both 
and 
or satisfies neither one of them
With this definition we can now formalize what it means for a formula
to be implied by a certain set of formulae. Informally this is true if in all worlds that are possible given the set of formulae the formula also holds. This leads to the following formal definition: We say that a set of wffs semantically entails (or implies) a certain wff if all truth assignments that satisfy all the formulae in also satisfy Finally we define syntactical entailment such that
is syntactically entailed by if and only if we can derive it with the inference rules that were presented above in a finite number of steps. This allows us to formulate exactly what it means for the set of inference rules to be sound and complete:Soundness : If the set of wffs
syntactically entails wff then semantically entails Completeness : If the set of wffs
semantically entails wff then syntactically entails For the above set of rules this is indeed the case.
Sketch of a soundness proof
(For most logical systems, this is the comparatively "simple" direction of proof)Notational conventions: Let
be a variable ranging over sets of sentences. Let , , and range over sentences. For " syntactically entails " we write " proves ". For " semantically entails " we write " implies ".We want to show: (
)()(if proves , then implies ).We note that "
proves " has an inductive definition, and that gives us the immediate resources for demonstrating claims of the form "If proves , then ...". So our proof proceeds by induction.- Basis. Show: If
is a member of 
, then 
implies 
. - Basis. Show: If
is an axiom, then 
implies 
. - Inductive step (induction on
, the length of the proof):
- Assume for arbitrary
and 
that if 
proves 
in 
or fewer steps, then 
implies 
. - For each possible application of a rule of inference at step
, leading to a new theorem 
, show that 
implies 
.
- Assume for arbitrary
Notice that Basis Step II can be omitted for natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
systems because they have no axioms. When used, Step II involves showing that each of the axioms is a (semantic) logical truth
Logical truth
Logical truth is one of the most fundamental concepts in logic, and there are different theories on its nature. A logical truth is a statement which is true and remains true under all reinterpretations of its components other than its logical constants. It is a type of analytic statement.Logical...
.
The Basis step(s) demonstrate(s) that the simplest provable sentences from
are also implied by , for any . (The is simple, since the semantic fact that a set implies any of its members, is also trivial.) The Inductive step will systematically cover all the further sentences that might be provable—by considering each case where we might reach a logical conclusion using an inference rule—and shows that if a new sentence is provable, it is also logically implied. (For example, we might have a rule telling us that from "" we can derive " or ". In III.a We assume that if is provable it is implied. We also know that if is provable then " or " is provable. We have to show that then " or " too is implied. We do so by appeal to the semantic definition and the assumption we just made. is provable from , we assume. So it is also implied by . So any semantic valuation making all of true makes true. But any valuation making true makes " or " true, by the defined semantics for "or". So any valuation which makes all of true makes " or " true. So " or " is implied.) Generally, the Inductive step will consist of a lengthy but simple case-by-case analysis of all the rules of inference, showing that each "preserves" semantic implication.By the definition of provability, there are no sentences provable other than by being a member of
, an axiom, or following by a rule; so if all of those are semantically implied, the deduction calculus is sound.Sketch of completeness proof
(This is usually the much harder direction of proof.)We adopt the same notational conventions as above.
We want to show: If
implies , then proves . We proceed by contrapositionContraposition
In traditional logic, contraposition is a form of immediate inference in which from a given proposition another is inferred having for its subject the contradictory of the original predicate, and in some cases involving a change of quality . For its symbolic expression in modern logic see the rule...
: We show instead that if
does not prove then does not imply .-
does not prove 
. (Assumption) - If
does not prove 
, then we can construct an (infinite) "Maximal Set", 
, which is a superset of 
and which also does not prove 
.
- Place an "ordering" on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them
, 
, … - Define a series
of sets (
, 
, …) inductively:
-
- If
proves 
, then 
- If
does not prove 
, then 
-
- Define
as the union of all the 
. (That is, 
is the set of all the sentences that are in any 
.) - It can be easily shown that
-
contains (is a superset of) 
(by (b.i)); -
does not prove 
(because if it proves 
then some sentence was added to some 
which caused it to prove '
; but this was ruled out by definition); and -
is a "Maximal Set" (with respect to 
): If any more sentences whatever were added to 
, it would prove 
. (Because if it were possible to add any more sentences, they should have been added when they were encountered during the construction of the 
, again by definition)
-
- Place an "ordering" on all the sentences in the language (e.g., shortest first, and equally long ones in extended alphabetical ordering), and number them
- If
is a Maximal Set (wrt 
), then it is "truth-like". This means that it contains the sentence "
" only if it does not contain the sentence not-
; If it contains "
" and contains "If 
then 
" then it also contains "
"; and so forth. - If
is truth-like there is a "
-Canonical" valuation of the language: one that makes every sentence in 
true and everything outside 
false while still obeying the laws of semantic composition in the language. - A
-canonical valuation will make our original set 
all true, and make 
false. - If there is a valuation on which
are true and 
is false, then 
does not (semantically) imply 
.
QED
Q.E.D.
Q.E.D. is an initialism of the Latin phrase , which translates as "which was to be demonstrated". The phrase is traditionally placed in its abbreviated form at the end of a mathematical proof or philosophical argument when what was specified in the enunciation — and in the setting-out —...
Another outline for a completeness proof
If a formula is a tautologyTautology (logic)
In logic, a tautology is a formula which is true in every possible interpretation. Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921; it had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternate sense...
, then there is a truth table
Truth table
A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—to compute the functional values of logical expressions on each of their functional arguments, that is, on each combination of values taken by their...
for it which shows that each valuation yields the value true for the formula. Consider such a valuation. By mathematical induction on the length of the subformulae, show that the truth or falsity of the subformula follows from the truth or falsity (as appropriate for the valuation) of each propositional variable in the subformula. Then combine the lines of the truth table together two at a time by using "(P is true implies S) implies ((P is false implies S) implies S)". Keep repeating this until all dependencies on propositional variables have been eliminated. The result is that we have proved the given tautology. Since every tautology is provable, the logic is complete.
Interpretation of a truth-functional propositional calculus
An interpretation of a truth-functional propositional calculus is an assignment to each propositional symbolPropositional variable
In mathematical logic, a propositional variable is a variable which can either be true or false...
of
of one or the other (but not both) of the truth values truthTruth
Truth has a variety of meanings, such as the state of being in accord with fact or reality. It can also mean having fidelity to an original or to a standard or ideal. In a common usage, it also means constancy or sincerity in action or character...
(T) and falsity (F), and an assignment to the connective symbols
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
of
of their usual truth-functional meanings. An interpretation of a truth-functional propositional calculus may also be expressed in terms of truth tables.For
distinct propositional symbols there are distinct possible interpretations. For any particular symbol , for example, there are possible interpretations:
-
is assigned T, or -
is assigned F.
For the pair
, there are possible interpretations:
- both are assigned T,
- both are assigned F,
-
is assigned T and 
is assigned F, or -
is assigned F and 
is assigned T.
Since
has , that is, denumerably many propositional symbols, there are , and therefore uncountably manyCardinality of the continuum
In set theory, the cardinality of the continuum is the cardinality or “size” of the set of real numbers \mathbb R, sometimes called the continuum. It is an infinite cardinal number and is denoted by |\mathbb R| or \mathfrak c ....
distinct possible interpretations of
.Interpretation of a sentence of truth-functional propositional logic
If and are formulas of and is an interpretation of then:- A sentence of propositional logic is true under an interpretation
iff 
assigns the truth value T to that sentence. If a sentence is trueTrueTrue may refer to:* Truth, the state of being in accord with fact or reality-Music:* True , 1996* True , 2002* True , 1983** "True"...
under an interpretation, then that interpretation is called a model of that sentence. -
is false under an interpretation 
iff 
is not true under 
. - A sentence of propositional logic is logically valid iff it is true under every interpretation
means that 
is logically valid - A sentence
of propositional logic is a semantic consequence of a sentence 
iff there is no interpretation under which 
is true and 
is false. - A sentence of propositional logic is consistentConsistencyConsistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
iff it is true under at least one interpretation. It is inconsistent if it is not consistent.
Some consequences of these definitions:
- For any given interpretation a given formula is either true or false.
- No formula is both true and false under the same interpretation.
is false for a given interpretation iff 
is true for that interpretation; and 
is true under an interpretation iff 
is false under that interpretation.- If
and 
are both true under a given interpretation, then 
is true under that interpretation. - If
and 
, then 
. 
is true under 
iff 
is not true under 
.
is true under 
iff either 
is not true under 
or 
is true under 
.- A sentence
of propositional logic is a semantic consequence of a sentence 
iff 
is logically valid, that is, 
iff 
.
Alternative calculus
It is possible to define another version of propositional calculus, which defines most of the syntax of the logical operators by means of axioms, and which uses only one inference rule.Axioms
Let, and stand for well-formed formulæ. (The wffs themselves would not contain any Greek letters, but only capital Roman letters, connective operators, and parentheses.) Then the axioms are as follows:| Axioms | ||
|---|---|---|
| Name | Axiom Schema | Description |
| THEN-1 |  |
Add hypothesis  , implication introduction |
| THEN-2 |  |
Distribute hypothesis  over implication |
| AND-1 |  |
Eliminate conjunction |
| AND-2 |  |
|
| AND-3 |  |
Introduce conjunction |
| OR-1 |  |
Introduce disjunction |
| OR-2 |  |
|
| OR-3 |  |
Eliminate disjunction |
| NOT-1 |  |
Introduce negation |
| NOT-2 |  |
Eliminate negation |
| NOT-3 |  |
Excluded middle, classical logic |
| IFF-1 |  |
Eliminate equivalence |
| IFF-2 |  |
|
| IFF-3 |  |
Introduce equivalence |
- Axiom THEN-2 may be considered to be a "distributive property of implication with respect to implication."
- Axioms AND-1 and AND-2 correspond to "conjunction elimination". The relation between AND-1 and AND-2 reflects the commutativity of the conjunction operator.
- Axiom AND-3 corresponds to "conjunction introduction."
- Axioms OR-1 and OR-2 correspond to "disjunction introduction." The relation between OR-1 and OR-2 reflects the commutativity of the disjunction operator.
- Axiom NOT-1 corresponds to "reductio ad absurdum."
- Axiom NOT-2 says that "anything can be deduced from a contradiction."
- Axiom NOT-3 is called "tertium non daturLaw of excluded middleIn logic, the law of excluded middle is the third of the so-called three classic laws of thought. It states that for any proposition, either that proposition is true, or its negation is....
" (LatinLatinLatin is an Italic language originally spoken in Latium and Ancient Rome. It, along with most European languages, is a descendant of the ancient Proto-Indo-European language. Although it is considered a dead language, a number of scholars and members of the Christian clergy speak it fluently, and...
: "a third is not given") and reflects the semantic valuation of propositional formulae: a formula can have a truth-value of either true or false. There is no third truth-value, at least not in classical logic. Intuitionistic logicIntuitionistic logicIntuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
ians do not accept the axiom NOT-3.
Inference rule
The inference rule is modus ponensModus ponens
In classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
:
.Meta-inference rule
Let a demonstration be represented by a sequence, with hypotheses to the left of the turnstileTurnstile (symbol)
In mathematical logic and computer science the symbol \vdash has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails"...
and the conclusion to the right of the turnstile. Then the deduction theorem
Deduction theorem
In mathematical logic, the deduction theorem is a metatheorem of first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then proving B from this assumption. The deduction theorem explains why proofs of conditional...
can be stated as follows:
- If the sequence
- has been demonstrated, then it is also possible to demonstrate the sequence
.
This deduction theorem (DT) is not itself formulated with propositional calculus: it is not a theorem of propositional calculus, but a theorem about propositional calculus. In this sense, it is a meta-theorem, comparable to theorems about the soundness or completeness of propositional calculus.
On the other hand, DT is so useful for simplifying the syntactical proof process that it can be considered and used as another inference rule, accompanying modus ponens. In this sense, DT corresponds to the natural conditional proof
Conditional proof
A conditional proof is a proof that takes the form of asserting a conditional, and proving that the antecedent of the conditional necessarily leads to the consequent....
inference rule which is part of the first version of propositional calculus introduced in this article.
The converse of DT is also valid:
- If the sequence
- has been demonstrated, then it is also possible to demonstrate the sequence
in fact, the validity of the converse of DT is almost trivial compared to that of DT:
- If
-
- then
- 1:
- 2:
- 1:
- and from (1) and (2) can be deduced
- 3:
- 3:
- by means of modus ponens, Q.E.D.
The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, the axiom AND-1,
can be transformed by means of the converse of the deduction theorem into the inference rule
which is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.
Example of a proof
The following is an example of a (syntactical) demonstration, involving only axioms THEN-1 and THEN-2:Prove:
(Reflexivity of implication).Proof:
-
- Axiom THEN-2 with
, 
, 
- Axiom THEN-2 with
-
- Axiom THEN-1 with
, 
- Axiom THEN-1 with
-
- From (1) and (2) by modus ponens.
-
- Axiom THEN-1 with
, 
- Axiom THEN-1 with
-
- From (3) and (4) by modus ponens.
Equivalence to equational logics
The preceding alternative calculus is an example of a Hilbert-style deduction systemHilbert-style deduction system
In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert...
. In the case of propositional systems the axioms are terms built with logical connectives and the only inference rule is modus ponens. Equational logic as standardly used informally in high school algebra is a different kind of calculus from Hilbert systems. Its theorems are equations and its inference rules express the properties of equality, namely that it is a congruence on terms that admits substitution.
Classical propositional calculus as described above is equivalent to Boolean algebra, while intuitionistic propositional calculus
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
is equivalent to Heyting algebra
Heyting algebra
In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
. The equivalence is shown by translation in each direction of the theorems of the respective systems. Theorems
of classical or intuitionistic propositional calculus are translated as equations of Boolean or Heyting algebra respectively. Conversely theorems of Boolean or Heyting algebra are translated as theorems of classical or propositional calculus respectively, for which is a standard abbreviation. In the case of Boolean algebra can also be translated as , but this translation is incorrect intuitionistically.In both Boolean and Heyting algebra, inequality
can be used in place of equality. The equality is expressible as a pair of inequalities and . Conversely the inequality is expressible as the equality , or as . The significance of inequality for Hilbert-style systems is that it corresponds to the latter's deduction or entailmentEntailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
symbol
. An entailment
is translated in the inequality version of the algebraic framework as
Conversely the algebraic inequality
is translated as the entailment
-
.
The difference between implication
and inequality or entailmentEntailment
In logic, entailment is a relation between a set of sentences and a sentence. Let Γ be a set of one or more sentences; let S1 be the conjunction of the elements of Γ, and let S2 be a sentence: then, Γ entails S2 if and only if S1 and not-S2 are logically inconsistent...
or is that the former is internal to the logic while the latter is external. Internal implication between two terms is another term of the same kind. Entailment as external implication between two terms expresses a metatruth outside the language of the logic, and is considered part of the metalanguageMetalanguage
Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...
. Even when the logic under study is intuitionistic, entailment is ordinarily understood classically as two-valued: either the left side entails, or is less-or-equal to, the right side, or it is not.
Similar but more complex translations to and from algebraic logics are possible for natural deduction systems as described above and for the sequent calculus
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
. The entailments of the latter can be interpreted as two-valued, but a more insightful interpretation is as a set, the elements of which can be understood as abstract proofs organized as the morphisms of a category
Category (mathematics)
In mathematics, a category is an algebraic structure that comprises "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose...
. In this interpretation the cut rule of the sequent calculus corresponds to composition in the category. Boolean and Heyting algebras enter this picture as special categories having at most one morphism per homset, i.e., one proof per entailment, corresponding to the idea that existence of proofs is all that matters: any proof will do and there is no point in distinguishing them.
Graphical calculi
It is possible to generalize the definition of a formal language from a set of finite sequences over a finite basis to include many other sets of mathematical structures, so long as they are built up by finitary means from finite materials. What's more, many of these families of formal structures are especially well-suited for use in logic.For example, there are many families of graphs
Graph (mathematics)
In mathematics, a graph is an abstract representation of a set of objects where some pairs of the objects are connected by links. The interconnected objects are represented by mathematical abstractions called vertices, and the links that connect some pairs of vertices are called edges...
that are close enough analogues of formal languages that the concept of a calculus is quite easily and naturally extended to them. Indeed, many species of graphs arise as parse graphs in the syntactic analysis of the corresponding families of text structures. The exigencies of practical computation on formal languages frequently demand that text strings be converted into pointer structure renditions of parse graphs, simply as a matter of checking whether strings are wffs or not. Once this is done, there are many advantages to be gained from developing the graphical analogue of the calculus on strings. The mapping from strings to parse graphs is called parsing
Parsing
In computer science and linguistics, parsing, or, more formally, syntactic analysis, is the process of analyzing a text, made of a sequence of tokens , to determine its grammatical structure with respect to a given formal grammar...
and the inverse mapping from parse graphs to strings is achieved by an operation that is called traversing
Graph traversal
Graph traversal refers to the problem of visiting all the nodes in a graph in a particular manner. Tree traversal is a special case of graph traversal...
the graph.
Other logical calculi
Propositional calculus is about the simplest kind of logical calculus in current use. It can be extended in several ways. (Aristotelian "syllogistic" calculusTerm logic
In philosophy, term logic, also known as traditional logic or aristotelian logic, is a loose name for the way of doing logic that began with Aristotle and that was dominant until the advent of modern predicate logic in the late nineteenth century...
, which is largely supplanted in modern logic, is in some ways simpler — but in other ways more complex — than propositional calculus.) The most immediate way to develop a more complex logical calculus is to introduce rules that are sensitive to more fine-grained details of the sentences being used.
First-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
(aka first-order predicate logic) results when the "atomic sentences" of propositional logic are broken up into terms
Singular term
There is no really adequate definition of singular term. Here are some definitions proposed by different writers:# A term that tells us which individual is being talked about....
, variable
Variable (mathematics)
In mathematics, a variable is a value that may change within the scope of a given problem or set of operations. In contrast, a constant is a value that remains unchanged, though often unknown or undetermined. The concepts of constants and variables are fundamental to many areas of mathematics and...
s, predicates, and quantifiers, all keeping the rules of propositional logic with some new ones introduced. (For example, from "All dogs are mammals" we may infer "If Rover is a dog then Rover is a mammal".) With the tools of first-order logic it is possible to formulate a number of theories, either with explicit axioms or by rules of inference, that can themselves be treated as logical calculi. Arithmetic
Arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
is the best known of these; others include set theory
Set theory
Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
and mereology
Mereology
In philosophy and mathematical logic, mereology treats parts and the wholes they form...
. Second-order logic
Second-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
and other higher-order logic
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
s are formal extensions of first-order logic. Thus, it makes sense to refer to propositional logic as "zeroth-order logic", when comparing it with these logics.
Modal logic
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
also offers a variety of inferences that cannot be captured in propositional calculus. For example, from "Necessarily
" we may infer that . From we may infer "It is possible that ". The translation between modal logics and algebraic logics is as for classical and intuitionistic logics but with the introduction of a unary operator on Boolean or Heyting algebras, different from the Boolean operations, interpreting the possibility modality, and in the case of Heyting algebra a second operator interpreting necessity (for Boolean algebra this is redundant since necessity is the De Morgan dual of possibility). The first operator preserves 0 and disjunction while the second preserves 1 and conjunction.Many-valued logics are those allowing sentences to have values other than true and false. (For example, neither and both are standard "extra values"; "continuum logic" allows each sentence to have any of an infinite number of "degrees of truth" between true and false.) These logics often require calculational devices quite distinct from propositional calculus. When the values form a Boolean algebra (which may have more than two or even infinitely many values), many-valued logic reduces to classical logic; many-valued logics are therefore only of independent interest when the values form an algebra that is not Boolean.
Solvers
Finding solutions to propositional logic formulas is an NP-completeNP-complete
In computational complexity theory, the complexity class NP-complete is a class of decision problems. A decision problem L is NP-complete if it is in the set of NP problems so that any given solution to the decision problem can be verified in polynomial time, and also in the set of NP-hard...
problem. However, practical methods exist (e.g., DPLL algorithm
DPLL algorithm
The Davis–Putnam–Logemann–Loveland algorithm is a complete, backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem....
, 1962; Chaff algorithm
Chaff algorithm
Chaff is an algorithm for solving instances of the Boolean satisfiability problem in programming. It was designed by researchers at Princeton University, USA...
, 2001) that are very fast for many useful cases. Recent work has extended the SAT solver algorithms to work with propositions containing arithmetic expressions; these are the SMT solvers.
Higher logical levels
- First-order logicFirst-order logicFirst-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
- Second-order propositional logicSecond-order propositional logicA second-order propositional logic is a propositional logic extended with quantification over propositions. A special case are the logics that allow second-order Boolean propositions, where quantifiers may range either just over the Boolean truth values, or over the Boolean-valued truth...
- Second-order logicSecond-order logicIn logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
- Higher-order logicHigher-order logicIn mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
Related topics
- Ampheck
- Boolean algebra (logic)
- Boolean algebra (structure)
- Boolean algebra topics
- Boolean domainBoolean domainIn mathematics and abstract algebra, a Boolean domain is a set consisting of exactly two elements whose interpretations include false and true...
- Boolean function
- Boolean-valued functionBoolean-valued functionA boolean-valued function, in some usages is a predicate or a proposition, is a function of the type f : X → B, where X is an arbitrary set and where B is a boolean domain....
- Categorical logicCategorical logicCategorical logic is a branch of category theory within mathematics, adjacent to mathematical logic but more notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a category, and an interpretation by a functor...
- Combinational logicCombinational logicIn digital circuit theory, combinational logic is a type of digital logic which is implemented by boolean circuits, where the output is a pure function of the present input only. This is in contrast to sequential logic, in which the output depends not only on the present input but also on the...
- Combinatory logicCombinatory logicCombinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
- Conceptual graphConceptual graphConceptual graphs are a formalism for knowledge representation. In the first published paper on CGs, John F. Sowa used them to represent the conceptual schemas used in database systems...
- Disjunctive syllogismDisjunctive syllogismA disjunctive syllogism, also known as disjunction-elimination and or-elimination , and historically known as modus tollendo ponens,, is a classically valid, simple argument form:where \vdash represents the logical assertion....
- Entitative graphEntitative graphAn entitative graph is an element of the diagrammatic syntax for logic that Charles Sanders Peirce developed under the name of qualitative logic beginning in the 1880's, taking the coverage of the formalism only as far as the propositional or sentential aspects of logic are concerned...
- Existential graphExistential graphAn existential graph is a type of diagrammatic or visual notation for logical expressions, proposed by Charles Sanders Peirce, who wrote on graphical logic as early as 1882, and continued to develop the method until his death in 1914.-The graphs:...
- Frege's propositional calculusFrege's propositional calculusIn mathematical logic Frege's propositional calculus was the first axiomatization of propositional calculus. It was invented by Gottlob Frege, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus .It...
- Implicational propositional calculusImplicational propositional calculusIn mathematical logic, the implicational propositional calculus is a version of classical propositional calculus which uses only one connective, called implication or conditional...
- Intuitionistic propositional calculus
- Laws of FormLaws of FormLaws of Form is a book by G. Spencer-Brown, published in 1969, that straddles the boundary between mathematics and philosophy...
- Logical graphLogical graphA logical graph is a special type of diagramatic structure in any one of several systems of graphical syntax that Charles Sanders Peirce developed for logic....
- Logical valueLogical valueIn logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth.In classical logic, with its intended semantics, the truth values are true and false; that is, classical logic is a two-valued logic...
- Minimal negation operator
- Multigrade operatorMultigrade operatorIn logic and mathematics, a multigrade operator \Omega is a parametric operator with parameter k in the set N of non-negative integers....
- OperationOperation (mathematics)The general operation as explained on this page should not be confused with the more specific operators on vector spaces. For a notion in elementary mathematics, see arithmetic operation....
- Parametric operator
- Peirce's lawPeirce's lawIn logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that involves only one sort of connective, namely...
- Propositional formulaPropositional formulaIn propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
- Symmetric differenceSymmetric differenceIn mathematics, the symmetric difference of two sets is the set of elements which are in either of the sets and not in their intersection. The symmetric difference of the sets A and B is commonly denoted by A\,\Delta\,B\,orA \ominus B....
- Truth tableTruth tableA truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—to compute the functional values of logical expressions on each of their functional arguments, that is, on each combination of values taken by their...
Further reading
- 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.Chen Chung ChangChen Chung Chang is a mathematician who works in model theory. He obtained his PhD from Berkeley in 1955 on "Cardinal and Ordinal Factorization of Relation Types" under Alfred Tarski. He wrote the standard text on model theory. Chang's conjecture is named after him...
and Keisler, H.J.Howard Jerome KeislerH. Jerome Keisler is an American mathematician, currently professor emeritus at University of Wisconsin–Madison. His research has included model theory and non-standard analysis.His Ph.D...
(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.Robert R. KorfhageRobert Roy Korfhage was an American computer scientist, famous for his contributions to information retrieval and several textbooks....
(1974), Discrete Computational Structures, Academic Press, New York, NY. - Lambek, J.Joachim LambekJoachim Lambek is Peter Redpath Emeritus Professor of Pure Mathematics at McGill University, where he earned his Ph.D. degree in 1950 with Hans Julius Zassenhaus as advisor. He is called Jim by his friends.- Scholarly work :...
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.
External links
- Klement, Kevin C. (2006), "Propositional Logic", in James Fieser and Bradley Dowden (eds.), Internet Encyclopedia of PhilosophyInternet Encyclopedia of PhilosophyThe Internet Encyclopedia of Philosophy is a free online encyclopedia on philosophical topics and philosophers founded by James Fieser in 1995. The current general editors are James Fieser and Bradley Dowden...
, Eprint. - Introduction to Mathematical Logic
- Formal Predicate Calculus, contains a systematic formal development along the lines of Alternative calculus
- Elements of Propositional Calculus
- forall x: an introduction to formal logic, by P.D. Magnus, covers formal semantics and proof theoryProof theoryProof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
for sentential logic. - Propositional Logic (GFDLed)