Principia Mathematica

Anatomy of an Auditable Mind: Building a Historical Logic Theorist in Pure Python

From axioms and structural unification to automated chaining, implication composition, context absorption, and context release.

By Cory Miller / Swervin' Curvin
Founder • QuickPrompt Solutions™ • Containment Reflexion Audit™ (CRA)

Core Thesis

A symbolic theorem prover does more than calculate an answer. It maintains a structured derivation in which propositions, transformations, substitutions, inference rules, and resulting states can be represented explicitly. By separating logical representation and verification from statistical generation, the system provides a compact model of transparent and auditable computational reasoning.

1. The Historical Idea

In the mid-1950s, Allen Newell, Cliff Shaw, and Herbert Simon developed the Logic Theorist, one of the landmark early artificial-intelligence systems for automated symbolic reasoning.

The historical importance of Logic Theorist was not simply that a computer could manipulate mathematical expressions. It demonstrated that a machine could represent propositions symbolically and search through possible transformations in an attempt to construct proofs.

This article presents a modern, deliberately compact Python implementation inspired by that approach. It is not a literal reconstruction of the original Logic Theorist source code. Instead, it recreates the underlying architectural idea using nested Python tuples, pattern variables, unification, substitution, detachment, and controlled proof search.

The result is a useful laboratory for examining an important distinction:

Generating a proposition is not the same thing as demonstrating how the proposition follows from explicit rules.

2. What Exactly Is the Pure Python Logic Theorist?

The engine is a lightweight symbolic reasoning system built entirely from ordinary Python structures. It does not require a neural language model or an external theorem-proving library for its basic operation.

Its architecture consists of several cooperating layers:

1. Proposition Representation — logical statements are encoded as nested tuples.
2. Pattern Variables — variables such as ?p, ?q, and ?r allow axioms to operate as reusable schemas.
3. Unification — symbolic patterns are matched against concrete expressions.
4. Substitution — discovered variable bindings are inserted into symbolic expressions.
5. Detachment — instantiated implications can be applied using modus ponens.
6. Structural Transformation — implication structures can be composed, absorbed into conjunctions, or released back into nested implications.
7. Search — the engine explores possible derivation paths while tracking visited states.
8. Verification — the requested target is compared against explicitly generated symbolic states.

3. Logical Representation as Python Data

The fundamental representation is a nested tuple.

("OR", "A", "B")

represents:

A ∨ B

Similarly:

("IMPLIES", "A", "B")

represents:

A → B

Nested structures are constructed recursively:

(
    "IMPLIES",
    ("IMPLIES", "A", "B"),
    (
        "IMPLIES",
        ("OR", "A", "C"),
        ("OR", "B", "C")
    )
)

The tuple therefore functions as a small abstract syntax tree. Operators, operands, implications, conjunctions, and nested propositions remain explicit objects rather than disappearing into an opaque representation.

4. Pattern Variables and Structural Unification

Reusable axioms require variables. In this implementation, variables are represented using names beginning with ?.

?p
?q
?r

A pattern such as:

("OR", "?p", "?q")

can unify with:

("OR", "A", "B")

producing bindings equivalent to:

{
    "?p": "A",
    "?q": "B"
}

The critical property is that matching is structural. The system does not have to guess what the expression means in a linguistic sense. It compares the actual symbolic structure.

5. The Base Axiom Layer

The original demonstration begins with a compact collection of implication schemas:

(
    "IMPLIES",
    ("OR", "?p", "?p"),
    "?p"
)

(
    "IMPLIES",
    "?q",
    ("OR", "?p", "?q")
)

(
    "IMPLIES",
    ("OR", "?p", "?q"),
    ("OR", "?q", "?p")
)

(
    "IMPLIES",
    ("IMPLIES", "?p", "?q"),
    (
        "IMPLIES",
        ("OR", "?r", "?p"),
        ("OR", "?r", "?q")
    )
)

These schemas establish the initial symbolic vocabulary from which the demonstration can construct more complicated expressions.

6. The Three Structural Primitives

The major architectural extension is the addition of three implication transformations:

• Hypothetical Syllogism — implication composition
• Importation — context absorption
• Exportation — context release

These are not merely three additional lines in an axiom list. They introduce new transformation classes into the proof search space.

6.1 Hypothetical Syllogism — Implication Composition

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

Hypothetical Syllogism allows two conditional relationships to be composed into a third conditional relationship.

Given:

p → q
q → r

the system can establish:

p → r

The architectural significance is that implication chaining becomes representable as a theorem rather than remaining only a procedural search operation.

hypothetical_syllogism = (
    "IMPLIES",
    ("IMPLIES", "?p", "?q"),
    (
        "IMPLIES",
        ("IMPLIES", "?q", "?r"),
        ("IMPLIES", "?p", "?r")
    )
)

6.2 Importation — Context Absorption

(p → (q → r)) → ((p ∧ q) → r)

Importation changes the structural representation of assumptions. A nested conditional can be represented as a single implication whose antecedent contains both assumptions.

Conceptually:

p → (q → r)
↓
(p ∧ q) → r

This introduces a new form of context management. Instead of requiring the engine to traverse multiple nested implications, the assumptions can be represented together.

importation = (
    "IMPLIES",
    (
        "IMPLIES",
        "?p",
        ("IMPLIES", "?q", "?r")
    ),
    (
        "IMPLIES",
        ("AND", "?p", "?q"),
        "?r"
    )
)

6.3 Exportation — Context Release

((p ∧ q) → r) → (p → (q → r))

Exportation performs the inverse structural transformation. A conjunctive antecedent is expanded into nested conditional assumptions.

(p ∧ q) → r
↓
p → (q → r)

This provides proof search with an additional route for matching a target against a nested implication schema.

exportation = (
    "IMPLIES",
    (
        "IMPLIES",
        ("AND", "?p", "?q"),
        "?r"
    ),
    (
        "IMPLIES",
        "?p",
        ("IMPLIES", "?q", "?r")
    )
)

7. The Import/Export Bridge

Importation and Exportation together establish a reversible structural relationship between two representations of conditional reasoning:

p → (q → r)
⇅
(p ∧ q) → r

The practical consequence is increased structural matchability. A proof target that does not match one representation directly may become matchable after a legal structural transformation.

This is why the three primitives should be treated as part of the architecture, not as unrelated additions to the axiom database.

8. Integrated Axiom Registration

The extended engine can register the three primitives alongside the existing axioms:

self.axioms = [

    # Base propositional schemas

    (
        "IMPLIES",
        ("OR", "?p", "?p"),
        "?p"
    ),

    (
        "IMPLIES",
        "?q",
        ("OR", "?p", "?q")
    ),

    (
        "IMPLIES",
        ("OR", "?p", "?q"),
        ("OR", "?q", "?p")
    ),

    (
        "IMPLIES",
        ("IMPLIES", "?p", "?q"),
        (
            "IMPLIES",
            ("OR", "?r", "?p"),
            ("OR", "?r", "?q")
        )
    ),

    # Hypothetical Syllogism

    (
        "IMPLIES",
        ("IMPLIES", "?p", "?q"),
        (
            "IMPLIES",
            ("IMPLIES", "?q", "?r"),
            ("IMPLIES", "?p", "?r")
        )
    ),

    # Importation

    (
        "IMPLIES",
        (
            "IMPLIES",
            "?p",
            ("IMPLIES", "?q", "?r")
        ),
        (
            "IMPLIES",
            ("AND", "?p", "?q"),
            "?r"
        )
    ),

    # Exportation

    (
        "IMPLIES",
        (
            "IMPLIES",
            ("AND", "?p", "?q"),
            "?r"
        ),
        (
            "IMPLIES",
            "?p",
            ("IMPLIES", "?q", "?r")
        )
    )
]

9. Integrated Pure Python Logic Theorist

The following version places the structural primitives directly inside the theorem-proving architecture.

class LogicTheorist:

    def __init__(self):

        self.axioms = [

            # -------------------------------------------------
            # Base propositional schemas
            # -------------------------------------------------

            (
                "IMPLIES",
                ("OR", "?p", "?p"),
                "?p"
            ),

            (
                "IMPLIES",
                "?q",
                ("OR", "?p", "?q")
            ),

            (
                "IMPLIES",
                ("OR", "?p", "?q"),
                ("OR", "?q", "?p")
            ),

            (
                "IMPLIES",
                ("IMPLIES", "?p", "?q"),
                (
                    "IMPLIES",
                    ("OR", "?r", "?p"),
                    ("OR", "?r", "?q")
                )
            ),

            # -------------------------------------------------
            # Hypothetical Syllogism
            # -------------------------------------------------

            (
                "IMPLIES",
                ("IMPLIES", "?p", "?q"),
                (
                    "IMPLIES",
                    ("IMPLIES", "?q", "?r"),
                    ("IMPLIES", "?p", "?r")
                )
            ),

            # -------------------------------------------------
            # Importation
            # -------------------------------------------------

            (
                "IMPLIES",
                (
                    "IMPLIES",
                    "?p",
                    ("IMPLIES", "?q", "?r")
                ),
                (
                    "IMPLIES",
                    ("AND", "?p", "?q"),
                    "?r"
                )
            ),

            # -------------------------------------------------
            # Exportation
            # -------------------------------------------------

            (
                "IMPLIES",
                (
                    "IMPLIES",
                    ("AND", "?p", "?q"),
                    "?r"
                ),
                (
                    "IMPLIES",
                    "?p",
                    ("IMPLIES", "?q", "?r")
                )
            )
        ]


    # =========================================================
    # UNIFICATION
    # =========================================================

    def _unify(self, pattern, expression, bindings=None):

        if bindings is None:
            bindings = {}

        if isinstance(pattern, str) and pattern.startswith("?"):

            if pattern in bindings:
                return self._unify(
                    bindings[pattern],
                    expression,
                    bindings
                )

            bindings[pattern] = expression
            return bindings

        if isinstance(pattern, str):

            if pattern == expression:
                return bindings

            return None

        if not isinstance(expression, tuple):
            return None

        if len(pattern) != len(expression):
            return None

        for p, e in zip(pattern, expression):

            bindings = self._unify(
                p,
                e,
                bindings
            )

            if bindings is None:
                return None

        return bindings


    # =========================================================
    # SUBSTITUTION
    # =========================================================

    def _substitute(self, expression, bindings):

        if isinstance(expression, str):

            if expression.startswith("?"):
                return bindings.get(
                    expression,
                    expression
                )

            return expression

        if isinstance(expression, tuple):

            return tuple(
                self._substitute(
                    item,
                    bindings
                )
                for item in expression
            )

        return expression


    # =========================================================
    # FREE VARIABLE CHECK
    # =========================================================

    def _has_free_vars(self, expression):

        if isinstance(expression, str):
            return expression.startswith("?")

        if isinstance(expression, tuple):

            return any(
                self._has_free_vars(item)
                for item in expression
            )

        return False


    # =========================================================
    # DIRECT SUBSTITUTION
    # =========================================================

    def prove_by_substitution(self, target):

        results = []

        for axiom in self.axioms:

            if not isinstance(axiom, tuple):
                continue

            if axiom[0] != "IMPLIES":
                continue

            antecedent = axiom[1]
            consequent = axiom[2]

            bindings = self._unify(
                consequent,
                target
            )

            if bindings is None:
                continue

            required = self._substitute(
                antecedent,
                bindings
            )

            if self._has_free_vars(required):
                continue

            results.append({
                "method": "substitution",
                "axiom": axiom,
                "bindings": bindings,
                "required": required,
                "result": target
            })

        return results


    # =========================================================
    # DETACHMENT / MODUS PONENS
    # =========================================================

    def prove_by_detachment(self, target, known):

        results = []

        for axiom in self.axioms:

            if not isinstance(axiom, tuple):
                continue

            if axiom[0] != "IMPLIES":
                continue

            antecedent = axiom[1]
            consequent = axiom[2]

            for proposition in known:

                bindings = self._unify(
                    antecedent,
                    proposition
                )

                if bindings is None:
                    continue

                instantiated_consequent = self._substitute(
                    consequent,
                    bindings
                )

                if instantiated_consequent == target:

                    results.append({
                        "method": "detachment",
                        "axiom": axiom,
                        "premise": proposition,
                        "bindings": bindings,
                        "result": target
                    })

        return results


    # =========================================================
    # CHAINING
    # =========================================================

    def prove_by_chaining(
        self,
        target,
        max_depth=12
    ):

        known = set()
        frontier = []
        visited = set()

        # Seed explicitly closed axioms.
        for axiom in self.axioms:

            if not self._has_free_vars(axiom):

                known.add(axiom)

        frontier.extend(known)

        for _ in range(max_depth):

            next_frontier = []

            for proposition in frontier:

                if proposition in visited:
                    continue

                visited.add(proposition)

                substitutions = (
                    self.prove_by_substitution(
                        proposition
                    )
                )

                for result in substitutions:

                    required = result["required"]

                    if required not in known:

                        known.add(required)
                        next_frontier.append(required)

                    if target in known:

                        return {
                            "method": "chaining",
                            "target": target,
                            "known": known
                        }

            detached = self.prove_by_detachment(
                target,
                known
            )

            if detached:

                return {
                    "method": "detachment",
                    "target": target,
                    "proof": detached,
                    "known": known
                }

            frontier = next_frontier

            if target in known:

                return {
                    "method": "chaining",
                    "target": target,
                    "known": known
                }

            if not frontier:
                break

        return None


    # =========================================================
    # MAIN PROVER
    # =========================================================

    def prove(self, target):

        direct = self.prove_by_substitution(
            target
        )

        if direct:
            return direct

        chained = self.prove_by_chaining(
            target
        )

        if chained:
            return chained

        return None

10. The State-Transition Pipeline

The engine can be understood as a deterministic symbolic state machine:

Known State + Axioms
        ↓
Pattern Matching
        ↓
Unification
        ↓
Variable Bindings
        ↓
Substitution
        ↓
Structural Transformation
        ↓
Detachment / Chaining
        ↓
Target Validation
        ↓
New Known State

Each transformation produces another symbolic state. The proof therefore becomes a sequence rather than an unexplained final answer.

S0 → S1 → S2 → S3 → ... → Sn

11. Hypothetical Syllogism Changes the Meaning of Chaining

Before the addition of Hypothetical Syllogism, the engine can use chaining as a procedural mechanism for navigating known propositions.

With HS represented as an explicit schema, the composition itself becomes representable as a theorem.

Operational chaining:
use p → q and q → r to reach p → r.

Structural theorem:
represent the rule itself as (p → q) → ((q → r) → (p → r)).

That distinction matters because a rule that exists only inside the search algorithm cannot itself become an object of symbolic reasoning. Once the rule is represented as an axiom, the theorem prover can reason about the transformation through the same mechanism it uses for other propositions.

12. Importation and Exportation Change Context Management

The two transformations introduce a structural distinction between nested assumptions and combined assumptions.

Importation compresses:

p → (q → r)

into:

(p ∧ q) → r

Exportation reverses that transformation:

(p ∧ q) → r

becomes:

p → (q → r)

This gives proof search two structurally equivalent routes for handling conditional context, subject to the logical system and semantics in which these transformations are being used.

13. Deeper Subgoal Generation

The additional primitives expand the kinds of intermediate expressions that can appear during proof search.

• p
• q
• r
• p ∧ q
• q → r
• p → r
• (p ∧ q) → r
• p → (q → r)

Consequently, the search engine is no longer restricted to producing shallow OR-based transformations. It can navigate nested implication structures and assumption contexts.

14. Recommended Structural Stress Test: Permutation

A useful next target is the conditional permutation form:

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

This target is useful because it tests whether the engine can manipulate the structural ordering of antecedent context rather than simply reproduce a directly registered schema.

permutation_target = (
    "IMPLIES",
    (
        "IMPLIES",
        "?p",
        ("IMPLIES", "?q", "?r")
    ),
    (
        "IMPLIES",
        "?q",
        ("IMPLIES", "?p", "?r")
    )
)

result = theorist.prove(
    permutation_target
)

print(result)

However, this test should be interpreted carefully. Importation and Exportation alone do not establish every possible reordering of conjunctions. If the engine is expected to derive this permutation theorem through conjunction commutativity, then an explicit and valid conjunction-commutativity schema and the corresponding proof-search mechanism must also be present.

That distinction is important for auditability: a successful output is only as meaningful as the inference rules that actually produced it.

15. Cycle Detection and Self-Referential Failure Modes

Symbolic search systems can easily encounter cycles. Importation and Exportation make this particularly obvious because they can transform one representation into another and then transform it back.

Therefore, the existence of reversible transformations does not by itself eliminate loops.

The correct architectural response is explicit state tracking.

visited = set()

if proposition in visited:
    continue

visited.add(proposition)

The engine should treat a symbolic state that has already been explored as already visited unless another proof context or lower-cost path justifies reopening it.

This is a search-control problem, not something that disappears merely because additional logical axioms have been introduced.

16. Suggested Test Suite

Once the expanded primitive set is installed, the engine should be tested against increasingly difficult structural targets.

Test	Capability
A ∨ B → B ∨ A	Basic structural substitution
p → q, q → r ⊢ p → r	Hypothetical composition
p → (q → r) ⊢ (p ∧ q) → r	Importation
(p ∧ q) → r ⊢ p → (q → r)	Exportation
p → (q → r) ⊢ q → (p → r)	Antecedent permutation
Nested implication chains	Deep recursive proof search
Repeated reversible transformations	Cycle detection

17. Symbolic Reasoning Versus Statistical Generation

Property	Symbolic Theorem Prover	Neural Language Model
Representation	Explicit symbolic structures	Distributed learned representations
Inference	Explicit rules and search	Statistical sequence generation
Proof trace	Can be represented explicitly	Generated reasoning is not automatically a formal proof
Failure mode	Search or rule failure	Unsupported or incorrect generation
Verification	Can be checked against explicit rules	Generally requires an external verification mechanism

This is not an argument that symbolic reasoning universally replaces neural systems. The more precise observation is that symbolic systems expose their inference machinery in a way that makes formal validation straightforward.

18. Why This Architecture Is Auditable

An auditable reasoning system should be able to answer more than "What did the system output?"

It should also be possible to ask:

• What representation entered the system?
• Which axiom or rule was selected?
• What variable bindings were generated?
• What substitution occurred?
• What intermediate proposition was produced?
• Which premises were consumed?
• Which state transition occurred?
• Was the target actually reached?
• Did the search encounter a cycle?
• Which inference path produced the final result?

This is closely aligned with the broader principle behind the Containment Reflexion Audit™ architecture: an assertion should not automatically acquire the authority of an established state merely because a system generated it.

In the theorem-proving context, the equivalent discipline is simple: a proposition becomes a proven target only through an explicit derivation accepted by the configured inference system.

19. What This Engine Does Not Establish

It is important not to overstate the implementation.

This engine is a compact demonstration of symbolic theorem proving. It is not a complete recreation of historical Logic Theorist, nor is it a complete implementation of the formal system of Principia Mathematica.

A production theorem prover would require substantially more machinery, potentially including:

• Formal proof certificates.
• Complete treatment of logical syntax and semantics.
• Quantifiers and variable scope.
• Negation.
• Equality.
• More comprehensive conjunction and disjunction rules.
• Resolution or equivalent complete inference procedures.
• Backtracking.
• Search-cost heuristics.
• Proof minimization.
• Consistency analysis.
• Formal soundness and completeness guarantees for the chosen calculus.

The purpose here is architectural clarity rather than claiming completeness beyond the implemented fragment.

20. Reproducibility

The core demonstration requires only Python and standard language features. The symbolic structures can therefore be executed in a conventional Python environment or adapted to mobile environments such as Pythonista.

Python 3.x

Because the propositions are ordinary Python tuples, the system can also be serialized, logged, inspected, compared, and passed between components without requiring a specialized symbolic object format.

21. The Larger Architectural Lesson

The most significant result of building this system is not the amount of Python code required. It is the separation of responsibilities.

Representation answers:

What is the proposition?

Unification answers:

How can this pattern match that structure?

Substitution answers:

What concrete proposition results from the bindings?

Inference answers:

What transformation is legally available?

Search answers:

Which transformation should be explored next?

Verification answers:

Did the resulting state actually satisfy the target?

Audit answers:

What happened at every step?

22. Conclusion

Building a Logic Theorist from scratch in pure Python demonstrates how far explicit symbolic architecture can go with surprisingly little machinery.

The original foundation consists of structured propositions, reusable axiom patterns, unification, substitution, detachment, and search.

The addition of Hypothetical Syllogism, Importation, and Exportation materially expands the architecture:

• Hypothetical Syllogism provides implication composition.
• Importation provides context absorption.
• Exportation provides context release.

Together, Importation and Exportation provide a structural bridge between nested conditionals and conjunctive antecedents:

p → (q → r)
⇅
(p ∧ q) → r

Hypothetical Syllogism simultaneously turns implication composition into an explicit symbolic object.

The resulting architecture is therefore substantially more expressive than a simple axiom-driven proposition manipulator. It becomes a controlled symbolic search environment in which structural transformations themselves can participate in the derivation process.

The central principle remains the same:

A machine-generated assertion is not automatically a proof.

A proof is a traceable sequence of authorized transformations from an accepted starting state to a formally represented target.

That is the enduring value of the Logic Theorist architecture: it makes the reasoning process itself part of the computational object.

---

Sources & Further Reading

• Logic Theorist — Historical Overview
• Principia Mathematica — Historical and Logical Background
• Stanford Encyclopedia of Philosophy — Principia Mathematica
• Python — Official Website
• Python Documentation
• Pythonista 3
• Pythonista 3 Documentation

Connect • Follow • Explore

Explore the research, code, publications, and ongoing work behind this article.

Swervin' Curvin — Blog X — @vccmac GitHub — cmiller9851-wq Python — Official Python Documentation Pythonista 3 Pythonista 3 Documentation

About the Author

Cory Miller is the founder of QuickPrompt Solutions™ and creator of the Containment Reflexion Audit™ (CRA) framework. His work explores artificial intelligence, symbolic reasoning, provenance, governance, software architecture, state transitions, and auditable computational systems.

Swervin' Curvin is the blog and writing persona through which these technical investigations, experiments, research notes, and architectural studies are published.

Intellectual Property & Attribution

© 2026 Cory Miller. All Rights Reserved.

Containment Reflexion Audit™ (CRA) is a governance framework developed and managed by QuickPrompt Solutions™, founded by Cory Miller.

SAEL — Sovereign Attribution Enforcement License

The original research, analysis, terminology, architectural concepts, frameworks, documentation, source organization, and written expression presented in this publication are the intellectual property of Cory Miller / QuickPrompt Solutions™ unless otherwise attributed.

Use, reproduction, redistribution, adaptation, publication, or derivative implementation of original CRA-related architecture, terminology, research, documentation, or written material is subject to attribution requirements and the applicable terms of SAEL — Sovereign Attribution Enforcement License.

Third-party facts, historical claims, statistics, trademarks, software, libraries, documentation, and source materials remain the property of their respective owners and are subject to their respective licenses and terms.

Nothing in this publication transfers ownership of third-party intellectual property. Where third-party concepts or historical material are discussed, appropriate attribution should be maintained.

Swervin' Curvin • Cory Miller • QuickPrompt Solutions™

Containment Reflexion Audit™ • Symbolic Reasoning • AI Governance • Provenance • Auditable Systems