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:
-
Proposition Representation —
logical statements are encoded as nested tuples.
-
Pattern Variables —
variables such as
?p, ?q, and ?r
allow 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:
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.
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:
(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
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
