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)
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:
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:
- Proposition Representation — logical statements are encoded as nested tuples.
-
Pattern Variables —
variables such as
?p,?q, and?rallow axioms to operate as reusable schemas. - Unification — symbolic patterns are matched against concrete expressions.
- Substitution — discovered variable bindings are inserted into symbolic expressions.
- Detachment — instantiated implications can be applied using modus ponens.
- Structural Transformation — implication structures can be composed, absorbed into conjunctions, or released back into nested implications.
- Search — the engine explores possible derivation paths while tracking visited states.
- 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:
Similarly:
("IMPLIES", "A", "B")represents:
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
?rA 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
Hypothetical Syllogism allows two conditional relationships to be composed into a third conditional relationship.
Given:
q → r
the system can establish:
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
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
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
Exportation performs the inverse structural transformation. A conjunctive antecedent is expanded into nested conditional assumptions.
↓
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
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 None10. 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 StateEach transformation produces another symbolic state. The proof therefore becomes a sequence rather than an unexplained final answer.
S0 → S1 → S2 → S3 → ... → Sn11. 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.
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) → rExportation reverses that transformation:
(p ∧ q) → rbecomes:
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.
pqrp ∧ qq → rp → r(p ∧ q) → rp → (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:
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.xBecause 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
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 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.
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
