Propositional logic

Propositional logic is a type of classical logic that studies how to make and understand statements that can be either true or false. It is also known as statement logic, sentential calculus, or propositional calculus. This area of logic focuses on propositions—statements that can be true or false—and how they relate to each other.

In propositional logic, we connect simple statements using special symbols called logical connectives. These connectives include conjunction, which means "and"; disjunction, which means "or"; implication, which means "if...then"; biconditional, which means "if and only if"; and negation, which means "not." These tools help us build more complex statements from simpler ones.

Unlike first-order logic, propositional logic does not deal with objects, properties of objects, or quantities like "all" or "some." Instead, it forms the basic foundation that is used in more advanced types of logic. Propositional logic is often studied using a special language where statements are represented by letters, and connectives are shown with symbols. This makes it easier to analyze and understand logical relationships.

Notational variants of the connectives
Connective	Symbol
AND	A ∧ B {\displaystyle A\land B} , A ⋅ B {\displaystyle A\cdot B} , A B {\displaystyle AB} , A & B {\displaystyle A\&B} , A & & B {\displaystyle A\&\&B}
equivalent	A ≡ B {\displaystyle A\equiv B} , A ⇔ B {\displaystyle A\Leftrightarrow B} , A ⇋ B {\displaystyle A\leftrightharpoons B}
implies	A ⇒ B {\displaystyle A\Rightarrow B} , A ⊃ B {\displaystyle A\supset B} , A → B {\displaystyle A\rightarrow B}
NAND	A ∧ ¯ B {\displaystyle A{\overline {\land }}B} , A ∣ B {\displaystyle A\mid B} , A ⋅ B ¯ {\displaystyle {\overline {A\cdot B}}}
nonequivalent	A ≢ B {\displaystyle A\not \equiv B} , A ⇎ B {\displaystyle A\not \Leftrightarrow B} , A ↮ B {\displaystyle A\nleftrightarrow B}
NOR	A ∨ ¯ B {\displaystyle A{\overline {\lor }}B} , A ↓ B {\displaystyle A\downarrow B} , A + B ¯ {\displaystyle {\overline {A+B}}}
NOT	¬ A {\displaystyle \neg A} , − A {\displaystyle -A} , A ¯ {\displaystyle {\overline {A}}} , ∼ A {\displaystyle \sim A}
OR	A ∨ B {\displaystyle A\lor B} , A + B {\displaystyle A+B} , A ∣ B {\displaystyle A\mid B} , A ∥ B {\displaystyle A\parallel B}
XNOR	A ⊙ B {\displaystyle A\odot B}
XOR	A ∨ _ B {\displaystyle A{\underline {\lor }}B} , A ⊕ B {\displaystyle A\oplus B}

History

Main article: History of logic

Propositional logic was first developed by the ancient philosopher Chrysippus in the 3rd century BC. His work focused on statements, unlike older logic that focused on terms. Much of this early work was lost over time.

Later, important ideas about logic were developed by mathematicians like Gottfried Leibniz. In the 20th century, new ways to understand propositional logic were created, such as truth tables. These tools helped make logic clearer and easier to study.

Sentences

Main article: Proposition

Propositional logic is a way to study how we decide if a sentence is true based only on special words that connect ideas, like "and," "or," and "not." It looks at statements—simple sentences that can be true or false.

Propositional logic works with statements, which are sentences that tell us something and can be true or false. For example:

Wikipedia is a free online encyclopedia that anyone can edit.
London is the capital of England.
All Wikipedia editors speak at least three languages.

We can also make more complex sentences by connecting simpler ones using words like "and," "or," and "not." Here are some examples:

Wikipedia is a free online encyclopedia that anyone can edit, and millions already have. (using "and")
It is not true that all Wikipedia editors speak at least three languages. (using "not")
Either London is the capital of England, or London is the capital of the United Kingdom, or both. (using "or")

Arguments

Main article: Argument

An argument is a pair of things: a set of sentences called the premises, and a sentence called the conclusion. The conclusion is said to follow from the premises, and the premises are said to support the conclusion.

Example argument

Here’s an example of an argument in propositional logic:

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

The logical form of this argument is called modus ponens, which is a classically valid form. In classical logic, this argument is valid, meaning that if the premises are true, the conclusion must also be true. However, whether it is sound depends on real-world facts.

Validity and soundness

Main articles: Validity (logic) and Soundness

An argument is valid if it is necessary that, when all the premises are true, the conclusion is also true. In other words, it is impossible for all the premises to be true while the conclusion is false.

Validity is different from soundness. An argument is sound if it is valid and all its premises are true. If it is not both valid and true, then it is unsound.

Logic helps us identify valid arguments by showing that the conclusion is a logical consequence of the premises. This means there is no situation where the premises are true but the conclusion is not true.

Formalization

Propositional logic is studied using a special set of rules and symbols. These symbols, called formulas, help us understand how ideas connect to each other. This system lets us see if a conclusion makes sense based on the ideas we start with.

In propositional logic, we often use letters like P and Q to stand for whole statements. For example, P might mean "It's raining" and Q might mean "It's cloudy." This helps us focus on how the ideas fit together without getting lost in the details of the words.

There are different ways to show these connections, and one common way is called Gentzen notation. In this method, we write the starting ideas above a line and the conclusion we reach below the line. This shows how the conclusion follows from the starting ideas using special rules.

Language

The language of propositional logic has two main parts:

Atomic formulas: These are basic ideas or statements that can be either true or false. We call them things like "p", "q", or "r".
Connectives: These are symbols we use to combine atomic formulas into more complex statements. Examples include "and", "or", and "if...then".

A well-formed formula is any atomic formula or a combination of atomic formulas using connectives, following specific rules. This means we can build up more complicated statements from simple ones by using these connectives in the right way.

For example:

"p" is a well-formed formula.
If we have "p" and "q", we can write "p and q" as a well-formed formula.
We can also write things like "if p then q" or "p or q".

These rules help us know which combinations of symbols make sense in propositional logic.

Semantics

Propositional logic, also known as statement logic or sentential calculus, is a branch of classical logic. It helps us understand how statements can be true or false and how they connect to each other.

In this type of logic, every statement can only be one of two things: true or false. For example, the statement "Wikipedia is a free online encyclopedia that anyone can edit" is true, while "Wikipedia is a paper encyclopedia" is false.

This system works for any set of statements, assuming there are only two possible values — true or false — and each statement has one of these values. It also forms the basis for more complex logic systems that allow for more than two values.

p {\displaystyle p}	q {\displaystyle q}	p ∧ q {\displaystyle p\land q}	p ∨ q {\displaystyle p\lor q}	p → q {\displaystyle p\rightarrow q}	p ⇔ q {\displaystyle p\Leftrightarrow q}	¬ p {\displaystyle \neg p}	¬ q {\displaystyle \neg q}
T	T	T	T	T	T	F	F
T	F	F	T	F	F	F	T
F	T	F	T	T	F	T	F
F	F	F	F	T	T	T	T

Proof systems

See also: Proof theory and Proof calculus

Proof systems in propositional logic are ways to show if a statement is true or false. There are two main types: semantic proof systems and syntactic proof systems. Semantic proof systems look at whether a statement is true in every possible situation. Syntactic proof systems use rules to see if a statement can be made from other statements.

Semantic proof systems use truth tables to check all possible situations. Truth tables list all the ways a statement can be true or false. Another method is semantic tableaux, which uses a tree to explore different situations.

Syntactic proof systems use rules to change statements step by step. One way is using axioms, which are basic true statements. Another way is natural deduction, which uses simple rules to build up conclusions. There is also sequent calculus, which uses sequences of statements to show logical steps.

Semantic proof via truth tables

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

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

Semantic proof via tableaux

Main article: Method of analytic tableaux

Truth tables can become very long when there are many variables, so another way to check if statements are true or false is called analytic tableaux. This method works well because it only looks at the important cases where the facts are true or the result is false.

Analytic tableaux for propositional logic follow special rules. These rules help us understand if a statement is always true or if it can sometimes be false. When we apply these rules, we might find that a statement and its opposite are both true at the same time, which means there is a problem or contradiction. If all the paths we follow end in such problems, then the original statement cannot be true. This helps us prove if a statement is always true or if an argument makes sense.

List of classically valid argument forms

In propositional logic, some ways of putting ideas together always make sense, no matter what the ideas are. We can use special charts to check if these combinations are always true. These true combinations help us understand how ideas connect with each other.

Name	Sequent	Description
Modus Ponens	( ( p → q ) ∧ p ) ⊨ q {\displaystyle ((p\to q)\land p)\models q}	If p then q; p; therefore q
Modus Tollens	( ( p → q ) ∧ ¬ q ) ⊨ ¬ p {\displaystyle ((p\to q)\land \neg q)\models \neg p}	If p then q; not q; therefore not p
Hypothetical Syllogism	( ( p → q ) ∧ ( q → r ) ) ⊨ ( p → r ) {\displaystyle ((p\to q)\land (q\to r))\models (p\to r)}	If p then q; if q then r; therefore, if p then r
Disjunctive Syllogism	( ( p ∨ q ) ∧ ¬ p ) ⊨ q {\displaystyle ((p\lor q)\land \neg p)\models q}	Either p or q, or both; not p; therefore, q
Constructive Dilemma	( ( p → q ) ∧ ( r → s ) ∧ ( p ∨ r ) ) ⊨ ( q ∨ s ) {\displaystyle ((p\to q)\land (r\to s)\land (p\lor r))\models (q\lor s)}	If p then q; and if r then s; but p or r; therefore q or s
Destructive Dilemma	( ( p → q ) ∧ ( r → s ) ∧ ( ¬ q ∨ ¬ s ) ) ⊨ ( ¬ p ∨ ¬ r ) {\displaystyle ((p\to q)\land (r\to s)\land (\neg q\lor \neg s))\models (\neg p\lor \neg r)}	If p then q; and if r then s; but not q or not s; therefore not p or not r
Bidirectional Dilemma	( ( p → q ) ∧ ( r → s ) ∧ ( p ∨ ¬ s ) ) ⊨ ( q ∨ ¬ r ) {\displaystyle ((p\to q)\land (r\to s)\land (p\lor \neg s))\models (q\lor \neg r)}	If p then q; and if r then s; but p or not s; therefore q or not r
Simplification	( p ∧ q ) ⊨ p {\displaystyle (p\land q)\models p}	p and q are true; therefore p is true
Conjunction	p , q ⊨ ( p ∧ q ) {\displaystyle p,q\models (p\land q)}	p and q are true separately; therefore they are true conjointly
Addition	p ⊨ ( p ∨ q ) {\displaystyle p\models (p\lor q)}	p is true; therefore the disjunction (p or q) is true
Composition of conjunction	( ( p → q ) ∧ ( p → r ) ) {\displaystyle ((p\to q)\land (p\to r))} ⟚ ( p → ( q ∧ r ) ) {\displaystyle (p\to (q\land r))}	If p then q; and if p then r; therefore if p is true then q and r are true
Composition of disjunction	( ( p → q ) ∨ ( p → r ) ) {\displaystyle ((p\to q)\lor (p\to r))} ⟚ ( p → ( q ∨ r ) ) {\displaystyle (p\to (q\lor r))}	If p then q; or if p then r; therefore if p is true then q or r is true
De Morgan's Theorem (1)	¬ ( p ∧ q ) {\displaystyle \neg (p\land q)} ⟚ ( ¬ p ∨ ¬ q ) {\displaystyle (\neg p\lor \neg q)}	The negation of (p and q) is equiv. to (not p or not q)
De Morgan's Theorem (2)	¬ ( p ∨ q ) {\displaystyle \neg (p\lor q)} ⟚ ( ¬ p ∧ ¬ q ) {\displaystyle (\neg p\land \neg q)}	The negation of (p or q) is equiv. to (not p and not q)
Commutation (1)	( p ∨ q ) {\displaystyle (p\lor q)} ⟚ ( q ∨ p ) {\displaystyle (q\lor p)}	(p or q) is equiv. to (q or p)
Commutation (2)	( p ∧ q ) {\displaystyle (p\land q)} ⟚ ( q ∧ p ) {\displaystyle (q\land p)}	(p and q) is equiv. to (q and p)
Commutation (3)	( p ↔ q ) {\displaystyle (p\leftrightarrow q)} ⟚ ( q ↔ p ) {\displaystyle (q\leftrightarrow p)}	(p iff q) is equiv. to (q iff p)
Association (1)	( p ∨ ( q ∨ r ) ) {\displaystyle (p\lor (q\lor r))} ⟚ ( ( p ∨ q ) ∨ r ) {\displaystyle ((p\lor q)\lor r)}	p or (q or r) is equiv. to (p or q) or r
Association (2)	( p ∧ ( q ∧ r ) ) {\displaystyle (p\land (q\land r))} ⟚ ( ( p ∧ q ) ∧ r ) {\displaystyle ((p\land q)\land r)}	p and (q and r) is equiv. to (p and q) and r
Distribution (1)	( p ∧ ( q ∨ r ) ) {\displaystyle (p\land (q\lor r))} ⟚ ( ( p ∧ q ) ∨ ( p ∧ r ) ) {\displaystyle ((p\land q)\lor (p\land r))}	p and (q or r) is equiv. to (p and q) or (p and r)
Distribution (2)	( p ∨ ( q ∧ r ) ) {\displaystyle (p\lor (q\land r))} ⟚ ( ( p ∨ q ) ∧ ( p ∨ r ) ) {\displaystyle ((p\lor q)\land (p\lor r))}	p or (q and r) is equiv. to (p or q) and (p or r)
Double Negation	p {\displaystyle p} ⟚ ¬ ¬ p {\displaystyle \neg \neg p}	p is equivalent to the negation of not p
Transposition	( p → q ) {\displaystyle (p\to q)} ⟚ ( ¬ q → ¬ p ) {\displaystyle (\neg q\to \neg p)}	If p then q is equiv. to if not q then not p
Material Implication	( p → q ) {\displaystyle (p\to q)} ⟚ ( ¬ p ∨ q ) {\displaystyle (\neg p\lor q)}	If p then q is equiv. to not p or q
Material Equivalence (1)	( p ↔ q ) {\displaystyle (p\leftrightarrow q)} ⟚ ( ( p → q ) ∧ ( q → p ) ) {\displaystyle ((p\to q)\land (q\to p))}	(p iff q) is equiv. to (if p is true then q is true) and (if q is true then p is true)
Material Equivalence (2)	( p ↔ q ) {\displaystyle (p\leftrightarrow q)} ⟚ ( ( p ∧ q ) ∨ ( ¬ p ∧ ¬ q ) ) {\displaystyle ((p\land q)\lor (\neg p\land \neg q))}	(p iff q) is equiv. to either (p and q are true) or (both p and q are false)
Material Equivalence (3)	( p ↔ q ) {\displaystyle (p\leftrightarrow q)} ⟚ ( ( p ∨ ¬ q ) ∧ ( ¬ p ∨ q ) ) {\displaystyle ((p\lor \neg q)\land (\neg p\lor q))}	(p iff q) is equiv to., both (p or not q is true) and (not p or q is true)
Exportation	( ( p ∧ q ) → r ) ⊨ ( p → ( q → r ) ) {\displaystyle ((p\land q)\to r)\models (p\to (q\to r))}	from (if p and q are true then r is true) we can prove (if q is true then r is true, if p is true)
Importation	( p → ( q → r ) ) ⊨ ( ( p ∧ q ) → r ) {\displaystyle (p\to (q\to r))\models ((p\land q)\to r)}	If p then (if q then r) is equivalent to if p and q then r
Idempotence of disjunction	p {\displaystyle p} ⟚ ( p ∨ p ) {\displaystyle (p\lor p)}	p is true is equiv. to p is true or p is true
Idempotence of conjunction	p {\displaystyle p} ⟚ ( p ∧ p ) {\displaystyle (p\land p)}	p is true is equiv. to p is true and p is true
Tertium non datur (Law of Excluded Middle)	⊨ ( p ∨ ¬ p ) {\displaystyle \models (p\lor \neg p)}	p or not p is true
Law of Non-Contradiction	⊨ ¬ ( p ∧ ¬ p ) {\displaystyle \models \neg (p\land \neg p)}	p and not p is false, is a true statement
Explosion	( p ∧ ¬ p ) ⊨ q {\displaystyle (p\land \neg p)\models q}	p and not p; therefore q

Syntactic proof via natural deduction

Main article: Natural deduction

Natural deduction is a way to show that something is true by using special rules. These rules help us connect different ideas and statements. There are no starting truths other than these rules, and they guide us in building proofs step by step.

There are different ways people write these proofs, using various symbols and formats. Some look like trees, others like boxes, and some use simple lines. This article uses a style made popular by E.J. Lemmon and Benson Mates, which is easy to follow and display.

A proof is a list of statements, where each statement is either something we assume to be true or something we figure out using the rules from earlier steps. Each step shows what we assumed, which rule we used, and which earlier steps helped us get to this one.

There are special rules that help us work with certain connections between ideas. These rules include ways to start with an assumption and ways to finish a proof, even when things seem impossible. Some easier rules can be used instead of the more complex ones.

List of Inference Rules
Rule Name	Alternative names	Annotation	Assumption set	Statement
Rule of Assumptions	Assumption	A	The current line number.	At any stage of the argument, introduce a proposition as an assumption of the argument.
Conjunction introduction	Ampersand introduction, conjunction (CONJ)	m, n &I	The union of the assumption sets at lines m and n.	From φ {\displaystyle \varphi } and ψ {\displaystyle \psi } at lines m and n, infer φ & ψ {\displaystyle \varphi ~\&~\psi } .
Conjunction elimination	Simplification (S), ampersand elimination	m &E	The same as at line m.	From φ & ψ {\displaystyle \varphi ~\&~\psi } at line m, infer φ {\displaystyle \varphi } and ψ {\displaystyle \psi } .
Disjunction introduction	Addition (ADD)	m ∨I	The same as at line m.	From φ {\displaystyle \varphi } at line m, infer φ ∨ ψ {\displaystyle \varphi \lor \psi } , whatever ψ {\displaystyle \psi } may be.
Disjunction elimination	Wedge elimination, dilemma (DL)	j,k,l,m,n ∨E	The lines j,k,l,m,n.	From φ ∨ ψ {\displaystyle \varphi \lor \psi } at line j, and an assumption of φ {\displaystyle \varphi } at line k, and a derivation of χ {\displaystyle \chi } from φ {\displaystyle \varphi } at line l, and an assumption of ψ {\displaystyle \psi } at line m, and a derivation of χ {\displaystyle \chi } from ψ {\displaystyle \psi } at line n, infer χ {\displaystyle \chi } .
Disjunctive Syllogism	Wedge elimination (∨E), modus tollendo ponens (MTP)	m,n DS	The union of the assumption sets at lines m and n.	From φ ∨ ψ {\displaystyle \varphi \lor \psi } at line m and − φ {\displaystyle -\varphi } at line n, infer ψ {\displaystyle \psi } ; from φ ∨ ψ {\displaystyle \varphi \lor \psi } at line m and − ψ {\displaystyle -\psi } at line n, infer φ {\displaystyle \varphi } .
Arrow elimination	Modus ponendo ponens (MPP), modus ponens (MP), conditional elimination	m, n →E	The union of the assumption sets at lines m and n.	From φ → ψ {\displaystyle \varphi \to \psi } at line m, and φ {\displaystyle \varphi } at line n, infer ψ {\displaystyle \psi } .
Arrow introduction	Conditional proof (CP), conditional introduction	n, →I (m)	Everything in the assumption set at line n, excepting m, the line where the antecedent was assumed.	From ψ {\displaystyle \psi } at line n, following from the assumption of φ {\displaystyle \varphi } at line m, infer φ → ψ {\displaystyle \varphi \to \psi } .
Reductio ad absurdum	Indirect Proof (IP), negation introduction (−I), negation elimination (−E)	m, n RAA (k)	The union of the assumption sets at lines m and n, excluding k (the denied assumption).	From a sentence and its denial at lines m and n, infer the denial of any assumption appearing in the proof (at line k).
Double arrow introduction	Biconditional definition (Df ↔), biconditional introduction	m, n ↔ I	The union of the assumption sets at lines m and n.	From φ → ψ {\displaystyle \varphi \to \psi } and ψ → φ {\displaystyle \psi \to \varphi } at lines m and n, infer φ ↔ ψ {\displaystyle \varphi \leftrightarrow \psi } .
Double arrow elimination	Biconditional definition (Df ↔), biconditional elimination	m ↔ E	The same as at line m.	From φ ↔ ψ {\displaystyle \varphi \leftrightarrow \psi } at line m, infer either φ → ψ {\displaystyle \varphi \to \psi } or ψ → φ {\displaystyle \psi \to \varphi } .
Double negation	Double negation elimination	m DN	The same as at line m.	From − − φ {\displaystyle --\varphi } at line m, infer φ {\displaystyle \varphi } .
Modus tollendo tollens	Modus tollens (MT)	m, n MTT	The union of the assumption sets at lines m and n.	From φ → ψ {\displaystyle \varphi \to \psi } at line m, and − ψ {\displaystyle -\psi } at line n, infer − φ {\displaystyle -\varphi } .

Derivation of MTT from MPP and RAA
Assumption set	Line number	Sentence of proof	Annotation
1	1	P → Q {\displaystyle P\to Q}	A
2	2	− Q {\displaystyle -Q}	A
3	3	P {\displaystyle P}	A
1, 3	4	Q {\displaystyle Q}	1, 3 →E
1, 2	5	− P {\displaystyle -P}	2, 4 RAA

Syntactic proof via axioms

Main article: Hilbert system

It is possible to prove things in a special way by using basic rules that are always true. These rules are called axioms. We can start with a few simple ideas and build more complex ideas from them using a rule called modus ponens. Another way is to use axiom schemas, which are like templates for many different rules.

This section talks about some important sets of rules for propositional logic. For more examples and ideas about these rule sets, see the article Axiomatic system (logic).

Frege's Begriffsschrift

Axiomatic proof has been used since ancient times, like in Euclid's book *Elements of Geometry. But in propositional logic, it started with Gottlob Frege's Begriffsschrift. Frege used only two basic ideas: implication and negation. He had six key rules:

Proposition 1: a → ( b → a )
Proposition 2: ( c → ( b → a ) ) → ( ( c → b ) → ( c → a ) )
Proposition 8: ( d → ( b → a ) ) → ( b → ( d → a ) )
Proposition 28: ( b → a ) → ( ¬ a → ¬ b )
Proposition 31: ¬ ¬ a → a
Proposition 41: a → ¬ ¬ a

Frege used these rules with modus ponens and a rule for swapping parts of sentences to create a full and correct system for propositional logic.

Łukasiewicz's P₂

Jan Łukasiewicz showed that one of Frege's rules was not needed. He also showed that three other rules could be replaced with just one rule: ( ¬ p → ¬ q ) → ( q → p ). So, Łukasiewicz created a system with three rules:

p → ( q → p )
( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) )
( ¬ p → ¬ q ) → ( q → p )

Like Frege's system, this one also uses a rule for swapping parts and modus ponens.

Schematic form of P₂

Instead of swapping parts, we can use the rules in a general way. We use letters that can stand for any sentence. The three rules become:

φ → ( ψ → φ )
( φ → ( ψ → χ ) ) → ( ( φ → ψ ) → ( φ → χ ) )
( ¬ φ → ¬ ψ ) → ( ψ → φ )

This way of showing the rules is named after John von Neumann and is used in the Metamath "set.mm" database.

Proof example in P₂

Here is an example of proving A → A using P₂:

A → ( ( B → A ) → A ) (from rule A1)
( A → ( ( B → A ) → A ) ) → ( ( A → ( B → A ) ) → ( A → A ) ) (from rule A2)
( A → ( B → A ) ) → ( A → A ) (from steps 1 and 2 using modus ponens)
A → ( B → A ) (from rule A1)
A → A (from steps 4 and 3 using modus ponens)

Metalogic

Classical propositional logic has some special properties that make it easy to study. It is sound, meaning that if a statement can be proven true, then it is actually true. It is also complete, which means that if a statement is true, then it can be proven true using the rules of logic.

Another important property is compactness. This means that a group of statements can all be true at the same time if and only if every small group of them can also be true together. Finally, classical propositional logic is decidable. This means we can always figure out whether a statement is true, false, or always true by checking its meaning step by step.

Solvers

One big difference between propositional calculus and predicate calculus is that we can always figure out if a statement in propositional calculus can be true. This is called solving for "satisfiability." It can be hard to solve, but there are smart ways to do it quickly for many useful cases. There are special tools called SAT solvers that help with this, and some of these tools can even handle math problems mixed into the statements.

History

Sentences