In some comments on this forum I selected and shared excerpts of what I was reading, and I found this helpful in focusing on the content and its most relevant parts, so I want to continue doing so. This OP is nothing but excerpts from the “Propositional Logic (Stanford Encyclopedia of Philosophy)” article written by philosopher Curtis Franks. As I have expressed elsewhere, logic seems to me like the most conceptually fundamental topic, other than learning a language, because establishing any conclusions whatsoever requires rules, argumentation and inference. This article, however, is more of a reference work than an introduction, as an introduction is designed to teach you how to do proofs. If there is no objection to me dumping notes like this I may follow up with other articles like “Truth” and “Epistemology” and “Skepticism”.
“Propositional logic is the study of the meanings of, and the inferential relationships that hold among, sentences based on the role that … the propositional connectives have in determining those sentences’ truth or assertability conditions.”
"Propositional logic is the study of … a specification of a standard of logicality, wherein only the meanings of the propositional connectives are considered in evaluating things such as the cogency of a deduction or a sentence’s truth conditions.
A sentential connective is a linguistic particle that binds sentences to create a new compound sentence or that inflects a single sentence to create a new sentence. Among the sentential connectives, a propositional connective has the characteristic feature that when the original sentences it operates on are (or express) propositions, the new sentence that results from its application also is (or expresses) a proposition. There are … many competing theories about what a proposition is … For this reason, the precise demarcation of which linguistic particles qualify as propositional connectives is somewhat vague and even contentious."
“…the development of and plurality of systems of propositional logic can only be appreciated when no particular conception of proposition is in place. The only stipulations are that the connectives operate always on whole sentences and never on sub-sentential items … and that they create sentences in the same evaluation class as the ones they operate on, never higher-order expressions about the sentences in that class.”
1. Basic Framework
“The formal language of propositional logic consists of “atomic” propositional variables, p1, p2, p3, …, and propositional connectives, c1^1, c2^1, c3^1, …, c1^2, c2^2, c3^2, …, c1^3, … The expressions’ subscripts are used to distinguish them from one another… The propositional connectives’ superscripts indicate their “arity”, i.e., the number of propositions that they operate on in order to create a new proposition.”
“Every formula is built up stepwise from atoms through a finite application of propositional connectives.”
“It is customary to indicate the specific connectives one is studying with special characters, typically ∧, ∨, ⊃, ¬, [and] to use infix notation for binary connectives… [Wikipedia: “Infix notation is the notation commonly used in arithmetical … formulae and statements.”] It is also common to investigate properties of propositional formulas that do not depend on the occurrence of atoms fundamentally, in which case formula variables A, B, C, etc. appear in the expression.”
2. The Classical Interpretation
“…a natural first move is to try to specify formal rules of inference or precise assertability conditions that capture … the role that … natural language predicates serve in informal reasoning. Two of the earliest specifications were in terms of truth functions and in terms of axiomatic deduction systems.”
2.1 Truth-functionality
"The truth-functional analysis of propositional logic proceeds by associating … truth functions with … propositional connectives. The classical case … [is] where the truth value space is bivalent. …the natural language particles “not”, “or”, and “and” … associate … with the three connectives labeled earlier ¬, ∨, and ∧… Under this interpretation, one can define:
1. A is a classical propositional validity if it evaluates as T on every possible assignment of values to its atomic propositional variables;
2. A is classically satisfiable if it evaluates as T on at least one possible assignment of values to its atomic propositional variables (and is classically unsatisfiable otherwise);
3. A is a classical propositional consequence of B if on no assignment of values to the atoms that occur in A and B on which B evaluates as T, does A evaluate as F;
4. A is a classical propositional equivalent of B if A and B evaluate as T on precisely the same assignments of values to atoms."
"…the language of propositional logic restricted to the connectives ¬, ∨, and ∧ corresponds with the formulas of the familiar two element Boolean algebra [1 and 0]… The familiar Boolean laws of:
-interchange:
If A and B are equivalent, and A occurs as a subformula of C1, then the result of replacing an occurrence of A in C1 with B is a formula C2 that is equivalent to C1.
-substitution:
If A and B1 and C1 are any formulas whatsoever, then the result of replacing each occurrence of the propositional variable p in B1 and C1 with A are formulas B2 and C2 with the properties: B2 is valid if B1 is; B2 is unsatisfiable if B1 is; B2 is a consequence of C2 if B1 is a consequence of C1; B2 and C2 are equivalent if B1 and C1 are.
-complementation:
A ∨ ¬A is a classical validity (called the “law of excluded middle” (LEM) in propositional logic).
-double complementation:
¬¬A is equivalent to A.
-commutativity:
A ∧ B is equivalent to B ∧ A, and A ∨ B is equivalent to B ∨ A.
-associativity:
(A ∧ B) ∧ C is equivalent to A ∧ (B ∧ C), and (A ∨ B) ∨ C is equivalent to A ∨ (B ∨ C).
-distribution:
A ∨ (B1 ∧ B2 ∧ … ∧ Bn) is equivalent to (A ∨ B1) ∧ (A ∨ B2) ∧ … ∧ (A ∨ Bn) and A ∧ (B1 ∨ B2 ∨ … ∨ Bn) is equivalent to (A ∧ B1) ∨ (A ∧ B2) ∨ … ∨ (A ∧ Bn).
-De Morgan equivalence:
¬(B1 ∧ B2 ∧ … ∧ Bn) is equivalent to ¬B1 ∨ ¬B2 ∨ … ∨ ¬Bn and ¬(B1 ∨ B2 ∨ … ∨ Bn) is equivalent to ¬B1 ∧ ¬B2 ∧ … ∧ ¬Bn.
therefore apply to this language of “Boolean propositional formulas”."
2.1.1 Normal forms
"Consider any other propositional connective denoted *, of any arity, … and suppose that with it too is associated a … truth function."
"There is a simple algorithm for constructing a Boolean formula that is equivalent to *(A, B, C): For each row of the defining table for * in which the output value is T , construct a conjunction of each propositional variable that is assigned T and the negation of each propositional variable that is assigned F in that row’s input… Then disjoin these conjunctions."
"It is clear that this formula will evaluate as T on all the rows that *(A, B, C) did and as false on all the other rows… Thus we have verified the Disjunctive Normal Form (DNF) theorem:
Theorem 1. Any formula of propositional logic under the classical interpretation is equivalent to a disjunction of conjunctions of propositional variables and negated propositional variables.
Similar reasoning can be used to verify equivalence to a “conjunctive normal formula”, a conjunction of disjunctions of propositional variables and negated propositional variables."
2.1.2 Truth-functional completeness
“One corollary of the DNF theorem is that Boolean logic—the fragment of propositional logic with only the connectives ¬, ∧, and ∨—is in a sense just as expressive as full classical propositional logic with infinitely many connectives of infinitely many arities… [It] is “truth-functionally complete”.”
“A ∧ B is the classical equivalent of ¬(¬A ∨ ¬B)… So the pair {∨, ¬} is truth-functionally complete. Likewise, A ∨ B abbreviates ¬(¬A ∧ ¬B): {∧, ¬} is truth-functionally complete.”
2.1.4 The material conditional
“…the “material conditional” … is often denoted ⊃… A ⊃ B is equivalent to the Boolean expression ¬A ∨ B.”
“[Frege] wrote, “the causal connection implicit in the word ‘if’ …is not expressed by our symbols” (1972: 116).”
2.1.5 Decidability
“A logic is said to be decidable if there is a reliable method for determining whether a formula is satisfiable. Classical propositional logic is … decidable: Given an arbitrary formula, … enumerate in the tabular method … each of the possible sequences of truth values that can be input to its atomic propositional variables, and compute the composition of functions on each of these inputs. Because formulas are finite strings of symbols, each contains only a finite number, say n , of atoms, so that the truth-table will have exactly 2^n rows.”
2.2 Deduction
"The propositional axioms in Frege’s system are:
axiom 1: A ⊃ (B ⊃ A)
axiom 2: (C ⊃ (B ⊃ A)) ⊃ ((C ⊃ B) ⊃ (C ⊃ A))
axiom 3: (B ⊃ A) ⊃ (¬A ⊃ ¬B)
axiom 4: A ⊃ ¬¬A
axiom 5: ¬¬A ⊃ A
The inference rules of are:
-modus ponens: A ⊃ B, A, therefore B.
-substitution: If p is an atomic variable in B, and C is any formula whatsoever, then let B’ be the result of replacing every occurrence of p with C, and from B infer B’.
A proof is defined as a finite sequence of formulas, each one of which either is an axiom or follows from previous entries in the sequence by an application of an inference rule. A theorem is a formula which occurs as the final entry in a proof… CPC stands for “the classical propositional calculus”… Frege’s system is in two senses adequate for representing classical propositional logic: …the pair {¬, ⊃} is truth-functionally complete… Moreover, the system is complete in the sense that all and only the classical propositional tautologies are theorems."
“…one can also introduce the notion of deduction from hypotheses: If S is a set of formulas, then a sequence of formulas whose last entry is A and in which every entry either is an axiom, a member of S, or the result of an application of an inference rule from earlier entries is called a derivation of A from S… One does not want … every formula to be deducible from a propositional variable… In moving from pure axiomatic provability to the idea of deduction from arbitrary hypotheses, therefore, the substitution rule is restricted to be applicable only to axioms… With this restriction in place, we can denote the derivability of A from the set S by S ⊢ A.”
2.2.2.1 Consistency
“A formal deductive system S is consistent if for no formula A is ⊢ A and ⊢ ¬A. To prove consistency of CPC, Hilbert reasoned as follows: Let the sentence letters range over the numbers 1 and 0, interpret the disjunction symbol as multiplication and the negation symbol as the function 1 - x… Hilbert observed that the axioms are each interpreted as functions that return the value 0 on every input, and that the rules of inference each preserve this property. Furthermore, the negation of any theorem is constant 1 and therefore unprovable. Thus, no formula is provable if its negation also is.”
2.2.2.2 Maximality
"A formal deductive system is maximal if any proper extension of it is inconsistent. Hilbert used the same interpretation from his consistency argument to show:
Theorem 4. CPC is maximal."
2.2.2.3 Completeness
“The Completeness Theorem describes an exact correspondence between the truth-functional and deductive frameworks.”
2.2.2.4 Completeness as semi-decidability
“The set of theorems of a formal deductive system can be seen to be recursively enumerable.”
“Therefore, given a formula A, … If A is valid, then by completeness it is provable, and one will discover a proof of it after examining some finite number of strings. On the other hand, if A is not valid, the search will never halt.”
2.2.2.5 Independence
"…the classical interpretation of ¬ is the function that returns 1 on the input 0 and returns 0 on the input 1… If we modify the interpretation so that ¬ returns 1 on the input 1 and returns 0 on the input 0, then axioms 1, 2, 4, and 5 are still interpreted as constant 0 functions, whereas axiom 3 returns 1 on the input {0, 1}. The inference rules still preserve the property of being constant 0 on this modified interpretation, so we know that axiom 3 cannot be proved using only axioms 1, 2, 4, and 5 and that without axiom 3 Frege’s system would not be complete.
For a more interesting example, …
…one can verify that … axiom 5 is … independent of the first four axioms."
2.3 Gentzen’s calculi
2.3.1 Natural deduction
“Natural deduction is an early and emblematic achievement in “proof-theoretic semantics”: the tradition of specifying definitions in inferential, rather than denotational, terms.”
“[Gerhard] Gentzen wrote: “The introductions represent …the “definitions” of the symbols concerned.” (1934–35: §II 5.13)”
2.3.2 Sequent calculus
“Gentzen’s propositional sequent calculi … present logical inference in the form of sequents: expressions of the form “Γ → Δ” in which Greek letters stand for (possibly empty) finite sequences of formula.”
3. Non-Classical Interpretations
“Here we survey some of the most prevalent alternative systems of propositional logic.”
3.1 Multi-valued logics
“4-valued logics have been used to model computation on databases containing conflicting information—here the values correspond with the information states “true”, “false”, “both”, and “neither” (see Belnap 1977).”
“Another important class of multi-valued logics are the infinitely-valued “fuzzy logics”. These have been used in order to provide an analysis of propositions with vague terms, which can be thought of as admitting degrees of truth.”
3.2 Constructive logics
“…simply rejecting the LEM leads to a subtle deviation from the classical interpretation… The intuitionistic propositional calculus IPC has been studied in great depth.”
"In 1933b, Gödel provided … translation from IPC to the modal logic S4. S4 is CPC supplemented with a new primitive symbol □ so that, if A is a formula, then □A is a formula, a new rule of inference:
A, therefore □A
and three new axioms:
1. □A ⊃ A
2. □A (□(A B) □B)
3. □A □□A"
3.3 Relevance and connexive logics
“…some writers have proposed overcoming the apparent inadequacies of the material conditional… Relevance logicians suggest that many of the features exhibited by the material conditional … seem like departures from speakers’ intuitions.”
“Connexive logicians aim … to make good of the intuition that for a conditional statement to be true, the negation of its consequent should be incompatible with its antecedent… “Aristotle’s thesis” (Prior Analytics) can be formalized as ¬(¬A ⊃ A)… Sometimes instead the formula ¬(A ⊃ ¬A) is called Aristotle’s thesis. Systems of connexive logic accept both as axioms, as well as the principles (A ⊃ B) ⊃ ¬(A ⊃ ¬B) and (A ⊃ ¬B) ⊃ ¬(A ⊃ B)… (These latter two principles are interderivable, over the base theory IPC, with Aristotle’s theses).”
“Some … approaches are “paraconsistent”, i.e., they allow theorems A and ¬A but do not allow the derivation of arbitrary formulas from this contradiction. Paraconsistent approaches are often interpretable with the 4-valued truth-assignment mentioned above.”
3.4 Linear logic
“…linear logic (introduced in Girard 1987) can be thought of as an attempt to discover in the fine structure of formal logic those propositional connectives that play specific inference-tracking roles that ordinary expressions might be too crude to articulate.”
“…there are two versions of LEM.”
“Just as intuitionistic logic replaced the classical understanding of a conditional A ⊃ B “either A is false or B is true” with a procedural claim “Given A, I can produce B”, linear logic is able to distinguish claims “Given one copy of A, I can produce one copy of B” from “Given three copies of A, I can produce one copy of B”. This allows modeling of propositions about resource use in computation.”
"…the linear modalities are introduced. These are unary connectives… governed by the same left and right rules as the necessity and possibility operators of modal logic S4. This makes it unclear whether full linear logic LL with their inclusion qualifies as a propositional logic."
“As stressed in the introduction to this article, a helpful attitude for the development of propositional logic is to bracket questions about the nature of propositions.”