10. MODAL LOGIC
Outline
James Fieser, UT Martin
updated 12/4/2025
A. MODAL PROPOSITIONS
The term “classical logic” refers to the system developed by Frege and Russell, which involves propositional and predicate calculus. Non-classical logics arise when philosophers or mathematicians notice problems in classical logic and then do one of two things: (1) extend classical logic with new operators, or (2) revise classical logic by rejecting one or more of its main principles. Modal logic does the first of these by introducing two new operators: “□” (box) and “◊” (diamond). At the close of this chapter we will briefly note other types of non-classical logics, but the focus here is on modal logic. Historically, modal logic began with Aristotle, who treated necessity and possibility within syllogistic reasoning. Modern modal logic came much later. In 1918 C.I. Lewis introduced “□” notation to represent logical necessity. In following decades, modal systems were developed applying □ and ◊ to new subject matters. Georg Henrik von Wright applied modality to ethics, Arthur Prior to time, and Jaakko Hintikka to knowledge and belief.
1. Definition of Modal Logic
• Modal logics (broad sense): logic of different aspects (or “modes”) of truth, which builds upon standard systems of propositional and predicate logic.
• Modal logic (narrow sense): propositional calculus plus modal operators □p (it is necessary that p) and ◊p (it is possible that p)
2. Types of Modal Logics (in the broad sense)
Modality Operator Expression
Alethic □ □p (it is necessary that p)
◊ ◊p (it is possible that p)
Deontic O Op (it is obligatory that p)
P Pp (it is permitted that p)
F Fp (it is forbidden that p)
Utility U Up (it is preferable that p)
Temporal G Gp (it will always be the case that p)
F Fp (it will be the case that p)
H Hp (it has always been the case that p)
P Pp (it was the case that p)
Epistemic K Kp (it is known that p)
Doxastic B Bp (it is believed that p)
Agency A Ap (the agent is able to bring it about that p)
Counterfactual □→ p □→ q (if p had obtained then q would have obtained)
3. Types of possibility: modal logic can use any of these
• Logical possibility: it is logically possible for a colored object to not be red, but impossible for a red object to not be colored
• Metaphysical possibility: it is metaphysically possible for a substance to be in the form of a sphere, but impossible for a substance to have no form whatsoever
• Physical (nomological) possibility: it is physically possible to change water into hydrogen and oxygen, but impossible to change water into gold
• Technological (practical) possibility: it is technologically possible to travel to Mars in one year, but impossible in one day
• Temporal (historical) possibility: it is temporally possible for war to break out tomorrow, but impossible for Abraham Lincoln to become president tomorrow (i.e., impossible for all worlds that share our history up to Lincoln’s death)
4. Examples of modal propositions
Simple modal propositions (p=Paul is an alien)
◊p (it is possible that Paul is an alien)
□p (it is necessary that Paul is an alien)
Logically equivalent modal propositions (can be substituted for each other)
~◊p same as □~p (it is impossible that Paul is an alien; or, it could not be true that Paul is an alien; or it p must be false that Paul is an alien)
~□p same as ◊~p (it is not necessary that Paul is an alien; or, it is possible that Paul is not an alien)
◊p same as ~□~p (it is possible that Paul is an alien; or it is not necessary that Paul is not an alien
□p same as ~◊~p (it is necessary that Paul is an alien; or it is impossible that Paul is not an alien)
Compound modal propositions
Where
p=Paul is an alien
q=Quincy is an alien hunter
◊p & ◊q (it is possible that Paul is an alien and it is possible that Quincy is an alien hunter)
p v ◊q (Paul is an alien or it is possible that Quincy is an alien hunter)
◊(p → q) (it is possible that if Paul is an alien then Quincy is an alien hunter)
Compound modal propositions of special interest
p & ◊~p (p obtains but it is possible that it might not have; i.e., p is a contingent truth)
e.g., my eyes are blue, but it's possible that they might not have been blue
◊(p & q) (it is possible that p and q are both true; i.e., p and q are compatible)
e.g.,: it is possible both that both Jill has U.S. citizenship and she has British citizenship
~◊(p & q) (it is impossible that P and Q are both true; i.e., P and Q are incompatible)
e.g., it is not possible that both this object is a cube and this object is a sphere
□(p → q) (it is necessary that if p then q; i.e., p necessarily entails q)
e.g., it is necessary that if Joe is a bachelor, then Joe is unmarried
Modal propositions with quantifiers of predicate logic
Ǝx(Fx & Gx) & ◊Cx (there exists some x such that x is F and x is G, and it is possible x is C)
e.g. this frog is green and it is possible that this frog croaks
∀x(Fx → Gx) & ◊Cx (for all x, if x is F then x is G, and it is possible that x is C)
e.g., all frogs are green, and it is possible that they croak
B. POSSIBLE WORLD SEMANTICS
Possible world semantics are rules for determining the truth values of propositions in various worlds. Recall in propositional logic the role that truth tables played in explaining the logical operators of conjunction (&), disjunction (v), negation (~), and conditional (→). The meaning of these operators was defined by the layout of T and F in their truth tables, and those assignments are the semantics of propositional connectives. In modal logic, the operators of necessity (□) and possibility (◊) require something more. Truth tables alone cannot define them, and so modal logic uses a different approach called possible world semantics, which evaluates truth relative to many worlds rather than just one. In this system, a proposition is not judged only in the actual world but across a range of possible worlds. A statement such as □p means that p is true in every world under consideration, while ◊p means that p is true in at least one world. In other words, necessity covers all worlds, and possibility requires only one. This approach was introduced by Saul Kripke, first in his paper “A Completeness Theorem in Modal Logic” (1959), and elaborated more fully in Semantical Considerations on Modal Logic (1963).
1. Four types of accessibility relations between possible worlds
Possible world semantics involves what are called "accessibility relations". As an analogy, think a science fiction of alternate universes. Let's call our actual universe w1 (world 1). Alternate universes would be w2, w3, w4, etc. Suppose that scientists built portals to some of these alternate worlds, such as a portal in w1 that would give us access to w2, where, for example, we could see what was going on there. Consider, next, four possible portal configurations for accessing possible worlds: (a) serial, (b) reflexive, (c) symmetrical, and (d) transitive. Below are the four basic accessibility relations, each considered in isolation of the others only.
a. Serial relation (alone): every world has access to at least one world
{w1}———→ {w2}
e.g., Think about different kinds of permissions we can set on our Facebook accounts for accessing people's photos. If I set up in Facebook only serial access, then, (a) I can access your photos, but (b) I cannot access my own photos, and (c) you cannot access my photos.
b. Reflexive relation (alone): every world can access itself
{w1}
↻
e.g., If I set up in Facebook only a reflexive access, then, (a) I can access my own photos, but (b) I cannot access your or anyone else's photos.
c. Symmetric relation (alone): for all worlds, w1, w2, if w1 has access to w2, then w2 has access to w1
{w1} ←———→ {w2}
e.g., If I set up in Facebook only a symmetrical access, then, (a) you and I can access each other's photos, but (a) I cannot access my own photos.
d. Transitive relation (alone): For all worlds, w1, w2, w3, if w1 has access to w2, and w2 has access to w3, then w1 has access to w3
{w1} ———→ {w2} ———→ {w3}
⤷————————————↗
e.g., If I set up in Facebook only a transitive access, then, (a) I can access your photos, and (b) I can access your friends' photos, but (c) none of you can access mine, and (d) I cannot access my own.
e. Serial, reflexive, symmetrical, and transitive relations combined: every world accesses every other world
e.g., If I set up in Facebook an access that exhibits all four of these, then, (a) I can access your photos, (b) I can access my own photos, (c) I can access your friends' photos, (d) you can access my photos, and (e) your friends can access my photos. In essence, everyone has access to everyone else's photos.
2. Determining the truth value of modal propositions like ◊p using possible world semantics
Informally, based on possible world semantics, ◊p is true in our world (w1) if and only if it is true in at least one world to which w1 has access (e.g., to w2, w3, w4, and maybe even w1 itself). By contrast, □p is true in our world (w1) if and only if it is true in every world to which w1 has access (e.g., to w2, w3, w4, and maybe even w1 itself).
a. Example (serial): consider the following serial relationship between three (and only three) possible worlds:
{w1} ———→ {w2 ~p}
———→ {w3 p}
In this setup, ◊p is true only in w1, □p is not true in any. For, w1 has access to both w2 and w3, but p obtains in only w3 and not in w2.
b. Example (reflexive): consider the following reflexive relationship between three (and only three) possible worlds, where each world can access only itself:
{w1 p} ↻
{w2 ~p} ↻
{w3 p} ↻
In this setup, ◊p is true in w1 and w3, and false in w2 (since each world only accesses itself, and p is true in w1 and w3 but not in w2). Similarly, □p is true in w1 and w3, and false in w2, for the same reason.
c. Example (symmetrical): consider the following symmetrical relationship between three (and only three) possible worlds:
{w1 p} ←→ {w2 ~p}
←→ {w3 p}
In this setup, ◊p is true in every world, since each has access to at least one world where p holds (w1 itself, w3 itself, and w2 can reach both). However, □p is true only in w3, since p is true in the only world that w3 has access to, which is not the case in w1 and w2.
d. Example (transitive): consider the following translative relationship between three (and only three) possible worlds:
{w1 p} ———→ {w2 ~p} ———→ {w3 p}
⤷————————————↗
In this setup, ◊p is true in w1 and w2 because p obtains in w3 which both w1 and w2 have access to. However, □p is true in no world.
b. Formal definitions of necessity and possibility using possible world semantics
1. Necessity: □p is true in world w1 if and only if p is true in every world accessible to w1
{w1 □p} iff ———→ {w2 p=true}
———→ {w3 p=true}
2. Possibility: ◊p is true in world w1 if and only if p is true in some world accessible to w1 (i.e., at least one must be true, others can be false but don't need to be)
{w1 ◊p} iff ———→ {w2 p=false}
———→ {w3 p=true}
C. NORMAL MODAL LOGIC SYSTEMS (K or stronger)
Axioms in modal logic attempt to express intuitive truths about necessity and possibility, such as □p → p (whatever is necessary is the case). Modal logicians have developed systems defined by different combinations of axioms, six of which are presented below. Philosophers generally use S4 or S5 for real-world reasoning, where S5 makes stronger assumptions than S4. The earlier systems (K, D, T, B) are comparatively minimal and do not fully capture our everyday understanding of necessity and possibility, although they matter as the building blocks of the more realistic systems. We begin with the simplest system, K, and add axioms step by step until we reach the two most commonly used systems, S4 and S5. A modal logic is considered “normal” if it includes Axiom K and the necessitation rule. The necessitation rule says that if a wff A is a theorem, then we may infer □A (discussed further below). Philosophers generally use S4 or S5 for philosophical applications, where S5 makes stronger assumptions than S4 about how worlds are related.
1. System K
Special Features
Axiom K: □(p → q) → (□p → □q) (distribution: the operator outside the parentheses can be distributed to both the antecedent and consequent inside the parentheses)
Relation: none
Total features
All Axioms: K
All relations: none
2. System D
Special Features
Axiom D: □p→◊p (whatever is necessary is possible, e.g., if it is necessary that 2+2=4, then it is possible that 2+2=4)
Relation: serial
Total features
All Axioms: K + D
All relations: serial
3. System T (or M)
Special Features
Axiom T: □p→p (whatever is necessary is the case; e.g., if it is necessary that 2+2=4, then 2+2=4)
Relation: reflexive
Total features
All Axioms: K + T
All relations: reflexive
Important corollary: p → ◊p (whatever is the case is possible; e.g., if 2+2=4, then it is possible that 2+2=4)
4. System B
Special Features
Axiom B: p→□◊p (whatever is the case, is necessarily possible; e.g., if 2+2=4, then, of necessity, it is possible that 2+2=4)
Relation: symmetric
Total features
All Axioms: K + T + B
All relations: reflexive and symmetric
Important Corollary: ◊□p→p (whatever is possibly necessary is the case; e.g., if it is possible that of necessary 2+2=4, then 2+2=4)
5. System S4
Special Features
Axiom 4: □p→□□p (whatever is necessary is necessarily necessary; e.g., if it is necessary that 2+2=4, then, of necessity, it is necessity that 2+2=4)
Relation: transitive
Total features
All Axioms: K + T + 4
All relations: reflexive and transitive
Important corollary: ◊◊p→◊p (reduces strings of similar operators; e.g., if it is possible that it is possible that 2+2=4, then it is possible that 2+2=4)
6. System S5
Special Features
Axiom 5: ◊p→□◊p (whatever is possible is necessarily possible; e.g., if it is possible that 2+2=4, then it is necessary that it is possible that 2+2=4)
Relation: Euclidian (alternatively, reflexive + symmetric + transitive, which is logically equivalent)
Total features
All Axioms: K + T + 5 (or K + B + 4)
All relations: reflexive, symmetric, and transitive, i.e., every world accesses every other world
Important Corollary: ◊□p→□p (whatever is possibly necessary is necessary; reduces strings of operators to the last one; e.g., if it is possible that it is necessary that 2+2=4, then it is necessary that 2+2=4)
D. MODAL ONTOLOGICAL ARGUMENT FOR GOD
The ontological argument for God's existence is a famous proof devised by medieval philosopher Anselm which attempts to demonstrate that the attribute of existence is built into the definition of God as "the greatest possible being" (or, in Anselm's words, God is "that than which nothing greater can be conceived”). Logicians have attempted to represent Anslem's argument in different ways. We will look at two here: a version based solely on the logical operators in propositional logic, and one based on the S5 system of modal logic.
1. Simple version in propositional logic
Intuition: the idea of God is that of a necessary being (the highest level of existence).
Abbreviations:
p=it is possible that a necessary being exists,
q=a necessary being exists
The argument
1. ~p v q
[either it is impossible that a necessary being exists, or a necessary being exists]
2. p
[it is possible that a necessary being exists; alternately ~~p it is not the case that it is impossible that a necessary being exists]
3. ˫ q
[a necessary being exists (1, 2 DS)]
2. Simple version in modal logic
Where p=God exists
1. ◊□p→□p
[if it is possible that God necessarily exists, then God necessarily exists (from corollary axiom in modal system S5)]
2. ◊□p
[it is possible that God necessarily exists (from intuition about possibility)]
3. □p
[God necessarily exists (1, 2 MP)]
4. □p → p
[if God necessarily exists then God exists (from system T axiom)]
5. ˫ p
[God exists (4, 3 MP)]
3. Possible world diagram of modal ontological argument, using S5 which has the three relations of being reflexive, symmetrical and transitive (i.e., every world is accessible to every other world)
Where w1 is the actual world, assume that ◊□p is true (i.e., it is possible that God necessarily exists, premise 2 above); thus, □p obtains in some world w2):
↷ ↷ ↷ ↷
{w1}←——→ {w2 □p} ←——→ {w3}←——→ {w4}
↖———————————↗
↖—————————————↗
↖———————————————————↗
Now, if □p obtains in w2, this means that p must also obtain in every world accessible to w2, including w1 and w3 (through symmetry), and w4 (through transitivity). Since w1 has access to every world that w2 has access to (and p obtains in all of these worlds) then □p also obtains in w1. Thus, if □p obtains in w1, then p also obtains in w1.
4. Controversy between whether S4 or S5 in the ontological argument
Should modal logic system S4 or S5 be the default system of modal logic that represents our normal intuitions about logical possibility? S5 has an axiom that establishes the symmetry relation, but S4 does not have that axiom and symmetry. The ontological argument works in S5 because of the symmetry axiom, but the argument does not work in S4 which lacks the symmetry axiom. The success of the S5 ontological argument comes down to whether the symmetry axiom should be part of our default modal logic system.
E. MODAL PROOFS WITH AXIOMS
Proofs in modal logic are superimposed on the rules of propositional and predicate calculus, but with their own unique modal rules and axioms.
1. Rules and Axioms
• Necessitation Rule (NEC): if wff A is a proved theorem (e.g., truth table tautology such as “p v ~p”), then we may infer □A
Explanation: recall the rule "theorem introduction" (TI) in propositional calculus, which allows introducing into a proof any tautology, such as "p v ~p”, and "~(p & ~p)". We may do that here too, but with the added feature of adding to these the necessity operator, such as "□(p v ~p)”, and "□[~(p & ~p)]". That is, if a proposition A is a tautology (i.e., it is true in every truth table scenario), then that proposition A is necessary (i.e., □A). In short, the necessitation rule allows creating out of thin air a modal proposition that may be inserted into a modal proof as needed.
• Change Modal Operator Rule (CMO)
◊p ↔ ~□~p
□p ↔ ~◊~p
~□p ↔ ◊~p
□~p ↔ ~◊p
• Major Axioms (for the S5 modal system)
A1: ◊p ↔ ~□~p [CMO]
A2: □(p →q) → (□p → □q) [Axiom K, distribution]
A3: □p → p [Axiom T]
A4: ◊p → □◊p [Axiom 5]
2. Example Proofs
The example proofs below contain no premises, only the conclusion is stipulated. The proof consists of creating premises by drawing on axioms, and using the rules of propositional calculus to draw inferences until the conclusion is reached.
(1) Prove the following proposition using modal rules and axioms: ˫ ~◊~B→ B
Answer (modal rules/axioms highlighted):
1. ˫ ~◊~B→ B
2. □B → B [A3]
3. ˫ ~◊~B→ B [2 CMO]
(2) Prove the following proposition using modal rules and axioms: ˫ ~□◊D → □~D
Answer:
1. ˫ ~□◊D → □~D
2. ◊D → □◊D [A4]
3. ~□◊D → ~◊D [2 TRANS]
4. ˫~□◊D → □~D [3 CMO]
(3) Prove the following proposition using modal rules and axioms: ˫ F → ◊F
Answer:
1. ˫ F → ◊F
2. □~F→ ~F [A3]
3. ~~F → ~□~F [2 TRANS]
4. F → ~□~F [3 DN]
5. ◊F ↔ ~□~F [A1]
6. ~□~F → ◊F [5 ↔E]
7. ˫ F → ◊F [4, 6 HS]
(4) Prove the following proposition using predicate calculus and modal rules: (∀x)□(P(x) → Q(x)) [5 ∀I]
Answer:
1. □(∀x)(P(x) → Q(x))
2. ˫ (∀x)□(P(x) → Q(x))
3. (∀x)(P(x) → Q(x)) [1 □E]
4. P(a) → Q(a) [3 ∀E]
5. □(P(a) → Q(a)) [4 □I]
6. (∀x)□(P(x) → Q(x)) [5 ∀I]
E. POSSIBLE-WORLD PROOF METHOD (Kripke-style tableaux)
In modal logic, one way to test whether a formula must be true is to try to build a counterexample world in which it fails. We may draw worlds as circles (alternatively as squares), show accessibility with arrows, and write statements inside those worlds to indicate what is true there. If we assume the formula is false and then try to construct a world where it fails, we may be forced to add more worlds and more statements. If this process leads to a contradiction in some world, then no counterexample is possible and the formula must hold. The method is visual and step-by-step, and often gives insight that symbolic proofs hide.
Goal: Show that □p → p is valid in system T (reflexive).
We attempt to refute it by assuming that ~(□p → p) is true in W1.
Start with world W1:
┌───────────┐
│ W1 │
│ ~(□p→p) │ (assumption for reductio)
└───────────┘
~(□p → p) becomes □p & ~p (negated conditional rule)
□p & ~p becomes separate wffs □p, ~p (simplification, &E)
┌───────────┐
│ W1 │
│ □p │
│ ~p │
└───────────┘
□p at W1 forces every world accessible from W1 to contain p.
System T is reflexive, which implies that W1 accesses itself, thus W1 contains p
┌───────────┐
│ W1 │
│ □p │
│ ~p │
│ p │
└───────────┘
Contradiction at W1: p and ~p
Assumption ~(□p → p) refuted, thus □p → p holds in system T
F. NON-CLASSICAL LOGIC
Classical logic assumes (1) every statement is either true or false, (2) contradictions make every statement provable (explosion), and (3) the material conditional correctly represents all “if-then” statements. These assumptions work well for ordinary deductive reasoning, but they face problems in areas such as counterfactuals, vagueness, future contingents, semantic paradoxes, and theories of mathematical proof. Non-classical logics modify one or more of these assumptions. The six areas below cover the most common alternatives.
1. Modal Logic
Basic Idea: Add operators for necessity and possibility (□p = p is necessary; ◇p = p is possible).
Motivation: Classical logic cannot express modal claims, such as what must be true or what might have been the case. Modal logic uses “possible worlds” semantics to evaluate these operators.
Core Principles:
□p → p
If □(p → q) and □p, then □q
Applications: Metaphysics (“necessary identity”), epistemology (knowledge and belief), philosophy of language (rigid designation), ethics (obligation), and computer science (program verification).
2. Intuitionist Logic
Basic Idea: Reject the law of excluded middle (p v ~p) unless one can actually prove p or ~p.
Motivation: Truth depends on construction. A statement is true only if there is a proof, not just because it cannot be false.
Consequences:
~~p → p is not valid.
Some classical derivations fail, especially indirect proofs.
Applications: Constructive mathematics, theories of computability, and the philosophy of mathematical practice.
3. Many-Valued Logic
Basic Idea: Allow more than two truth values. Common systems include three-valued logics with True, False, and Undefined (or Indeterminate).
Motivation: Some sentences do not seem strictly true or false. Examples include future contingent statements and vague predicates.
Two Strategies: (1) Truth gaps: some statements are neither true nor false. (2) Truth gluts: some statements are both true and false.
Typical Examples: “There will be a sea battle tomorrow.” “This sentence is false.”
Applications: Natural language semantics, logic of vagueness, database theory, handling undefined terms.
4. Paraconsistent Logic
Basic Idea: Allow certain contradictions without deriving every possible statement (avoid explosion).
Classical Problem: From a contradiction p & ~p, classical logic allows inference of any statement q. This trivializes the system.
Key Feature: Reject the rule that a single contradiction entitles one to infer everything.
Motivation: Real reasoning sometimes tolerates inconsistent data during inquiry. Scientific theories, legal codes, or large information systems may contain unresolved contradictions without disabling reasoning.
Applications: Metaphysics, semantics of paradox, AI reasoning with inconsistent knowledge bases.
5. Relevant Logic
Basic Idea: Require that premises share relevant content with conclusions in implications and entailments.
Classical Problem: The material conditional allows implications with no relation between antecedent and consequent, such as: “If the sky is green, then 2 + 2 = 4”
Motivating Principle: Valid inference should preserve information, not just truth value.
Formal Strategy: Modify implication rules so that p → q requires p to be relevant to q in some specified sense (semantic structure or proof-theoretic constraint).
Applications: Philosophy of logic, theories of implication, and reasoning systems that demand premise-conclusion relevance.
6. Fuzzy Logic
Basic Idea: Replace bivalence with a continuum of truth values between 0 and 1.
Motivation: Some predicates are inherently vague (“tall,” “bald,” “heap”). Assigning a degree of truth captures the idea of borderline cases.
Characteristic Feature: Truth becomes a matter of degree rather than a sharp divide.
Typical Case: A person of borderline height may have a truth value of .65 for “Tall,” not simply true or false.
Applications: Sorites paradoxes, linguistics, decision theory, engineering, and control systems (fuzzy controllers).
G. METALOGIC AND AXIOMATIC SYSTEMS
Metalogic is the study of logic itself. Instead of using logic to prove statements, metalogic asks questions about how logical systems work, how they’re built, and what makes them reliable. It treats logic like an object of investigation, much the way physics studies physical systems or linguistics studies language. In short, logic is about reasoning, and metalogic is about reasoning about reasoning.
1. Areas of metalogic
There are six main areas of inquiry in metalogic, each asking a big-picture question about how a logical system behaves.
(1) Reliability: Does the system ever lead us from true premises to a false conclusion?
Example: if a valid argument could prove something false from true assumptions, we wouldn’t trust the logic at all.
(2) Power: Can the system prove everything that is logically true within it?
Example: if the system knows that “if p then q” is always true but can’t prove it, then something is missing from its toolkit.
(3) Self-consistency: Does the system ever prove both a statement and its opposite?
Example: if a logic could prove p and also prove ~p, then every conclusion would become meaningless.
(4) Decidability: Is there a mechanical or step-by-step method that could answer every reasoning problem within the system?
Example: like a calculator can always decide whether two numbers add up to 10, is there a similar guaranteed method for logic problems?
(5) Compactness: If something can be proven using many premises, can it also be proven using only some of them?
(6) Completeness: Does the system prove all and only the statements that are logically valid (i.e., nothing true is unprovable, and nothing false is provable)?
Example: if a statement is true in every possible interpretation, completeness guarantees there is a proof of it somewhere in the system.
Example: Kripke proved soundness and completeness theorems showing that the axiomatic system K proves exactly those modal formulas that are valid under possible world semantics.
2. Axiomatic Systems vs. Rule-Based Systems
Most logic textbooks teach systems with several rules, such as modus ponens, modus tollens, and conditional proof. Students can apply these rules one at a time, which makes proofs feel natural and close to ordinary reasoning. In metalogic, the systems look different. They are axiom-based and rely almost entirely on one rule: modus ponens. This keeps the system small, which makes it easier to study how logic behaves without juggling many rules at once. These are often called “Hilbert-style” named after David Hilbert who introduced this style of system. The axioms selected come from the basic logical patterns that we commonly accept without proof. We choose them so that, when combined with Modus Ponens, they allow us to derive all other logical truths.
Example 1: prove p → p
Rule of inference:
(R1) Modus Ponens: from p and p → q infer q
Axiom schemas:
(A1) p → (q → p)
(A2) (p → (q → r)) → ((p → q) → (p → r))
Theorem to prove:
(Thm) p → p
Proof
1. p → (p → p)
[A1 (q=p)]
2. p → ((p → p) → p)
[A1 (q=(p → p))]
3. (p → ((p → p) → p)) → ((p → (p → p)) → (p → p))
[A2 (q=(p → p), r=p)]
4. (p → (p → p)) → (p → p)
[2, 3 MP]
5. Therefore, p → p
[1, 4 MP]