Same orchard arithmetic, but loaded entirely through .pltg files with an empty initial environment. Proves the loader bootstraps Peano notation, axioms, imports, and derives from scratch — no Python-side setup needed.
"""
Demo: Apple Arithmetic (.pltg)
Scenario: Same orchard arithmetic, but loaded entirely through .pltg
files with an empty initial environment. Proves the loader bootstraps
Peano notation, axioms, imports, and derives from scratch — no
Python-side setup needed.
"""
import json
import logging
import os
import sys
from parseltongue import load_main
def provenance(system, name):
print(json.dumps(system.provenance(str(name)), indent=2))
return True
def consistency(system):
report = system.consistency()
print(f" {report}")
return report.consistent
def verify(system, name):
system.verify_manual(str(name))
return True
def dump_env(system):
env = system.engine.env
print(f" Environment has {len(env)} entries: {list(env.keys()) if env else '(empty)'}")
return True
def state(system):
print(f" {system}")
return True
def list_axioms(system):
for ax in system.list_axioms():
print(f" {ax}")
return True
def list_terms(system):
for t in system.list_terms():
print(f" {t}")
return True
def list_theorems(system):
for t in system.list_theorems():
print(f" {t}")
return True
def print_theorem(system, name):
name = str(name)
if name in system.theorems:
print(f" {system.theorems[name]}")
return True
def pltg_print(_system, *args):
print(*[str(a).replace("\\n", "\n") for a in args])
return True
if __name__ == "__main__":
plog = logging.getLogger("parseltongue")
plog.setLevel(logging.WARNING)
handler = logging.StreamHandler(sys.stdout)
handler.setFormatter(logging.Formatter(" [%(levelname)s] %(message)s"))
plog.addHandler(handler)
os.chdir(os.path.dirname(__file__))
load_main(
"demo.pltg",
{
"dump-env": dump_env,
"print": pltg_print,
"provenance": provenance,
"consistency": consistency,
"verify": verify,
"state": state,
"list-axioms": list_axioms,
"list-terms": list_terms,
"list-theorems": list_theorems,
"print-theorem": print_theorem,
},
initial_env={},
overridable=True,
)
; ==========================================================
; Parseltongue DSL — Counting Observations & Apple Arithmetic
; ==========================================================
(print "============================================================")
(print "Parseltongue DSL — Counting Observations & Apple Arithmetic")
(print "============================================================")
(print "\n--- Environment check ---")
(dump-env)
; --- Phase 0: Load source documents ---
(print "\n--- Phase 0: Load source documents ---")
(load-document "Counting Observations" "resources/counting_observations.txt")
(load-document "Eden Inventory" "resources/eden_inventory.txt")
; --- Phase 1: Introduce primitive symbols ---
(print "\n--- Phase 1: Introduce primitive symbols ---")
(print " Starting with:")
(state)
(import (quote src.primitives))
(defterm local-zero src.primitives.zero :origin "import")
(defterm local-succ src.primitives.succ :origin "import")
(print " Introduced: zero, succ, =, +, -, >, *")
(state)
; --- Phase 2: Axioms of Peano arithmetic ---
(print "\n--- Phase 2: Axioms of Peano arithmetic ---")
(import (quote src.axioms))
(print " Axioms:")
(list-axioms)
; --- Phase 3: Concrete theorems via :bind ---
(print "\n--- Phase 3: Concrete theorems via :bind ---")
(derive three-plus-zero src.axioms.add-identity
:bind ((?n (local-succ (local-succ (local-succ local-zero)))))
:using (src.axioms.add-identity local-succ local-zero))
(derive commute-3-2 src.axioms.add-commutative
:bind ((?a (local-succ (local-succ (local-succ local-zero))))
(?b (local-succ (local-succ local-zero))))
:using (src.axioms.add-commutative local-succ local-zero))
(derive add-step-3-1 src.axioms.add-succ
:bind ((?n (local-succ (local-succ (local-succ local-zero))))
(?m local-zero))
:using (src.axioms.add-succ local-zero local-succ))
(print " Concrete theorems:")
(print-theorem "three-plus-zero")
(print-theorem "commute-3-2")
(print-theorem "add-step-3-1")
; --- Phase 4: Orchard inventory — morning ---
(print "\n--- Phase 4: Orchard inventory — morning ---")
(import (quote src.morning))
(defterm morning-total (+ src.morning.eve-morning src.morning.adam-morning)
:evidence (evidence "Eden Inventory"
:quotes ("Combined morning harvest was 🍎🍎🍎🍎🍎🍎🍎🍎 apples")
:explanation "Sum of Eve and Adam's morning picks"))
(defterm adam-picked-more (> src.morning.adam-morning src.morning.eve-morning)
:evidence (evidence "Eden Inventory"
:quotes ("Adam picked more apples than Eve in the morning")
:explanation "Adam's count exceeds Eve's"))
(print " Terms:")
(list-terms)
; --- Phase 5: Morning commutativity ---
(print "\n--- Phase 5: Morning commutativity ---")
(derive morning-commutes src.axioms.add-commutative
:bind ((?a src.morning.eve-morning) (?b src.morning.adam-morning))
:using (src.axioms.add-commutative src.morning.eve-morning src.morning.adam-morning)
:evidence (evidence "Eden Inventory"
:quotes ("Combined morning harvest was 🍎🍎🍎🍎🍎🍎🍎🍎 apples")
:explanation "eve + adam = adam + eve"))
(print-theorem "morning-commutes")
; --- Phase 6: Afternoon harvest ---
(print "\n--- Phase 6: Afternoon harvest ---")
(import (quote src.afternoon))
(defterm afternoon-total (+ src.afternoon.serpent-afternoon src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Combined afternoon harvest was 🍎🍎🍎🍎🍎🍎 apples")
:explanation "Sum of Serpent and Eve's afternoon picks"))
(defterm eve-daily (+ src.morning.eve-morning src.afternoon.eve-afternoon)
:evidence (evidence "Eden Inventory"
:quotes ("Eve's daily total is 🍎🍎🍎🍎🍎 apples")
:explanation "Eve's combined morning + afternoon"))
(defterm daily-total (+ morning-total afternoon-total)
:evidence (evidence "Eden Inventory"
:quotes ("Total harvest for the day was 🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎 apples")
:explanation "Grand total = morning + afternoon"))
(defterm morning-advantage (- morning-total afternoon-total)
:evidence (evidence "Eden Inventory"
:quotes ("The morning shift outproduced the afternoon by 🍎🍎 apples")
:explanation "Difference between shift totals"))
; --- Phase 7: Diff — what if Eve tried the forbidden apple? ---
(print "\n--- Phase 7: Diff — what if Eve tried the forbidden apple? ---")
(defterm eve-morning-alt (succ (succ zero))
:origin "Hypothetical: Eve tried the forbidden apple — SS0 instead of SSS0")
(diff eve-check
:replace src.morning.eve-morning
:with eve-morning-alt)
; --- Phase 8: Provenance ---
(print "\n--- Phase 8: Provenance ---")
(print " Provenance of morning-commutes:")
(provenance "morning-commutes")
; --- Phase 9: Consistency report ---
(print "\n--- Phase 9: Consistency report ---")
(consistency)
(print "\n Resolving unverified items...")
(verify "eve-morning-alt")
(verify "src.axioms.eq-reflexive")
(verify "src.primitives.=")
(print "\n After verification:")
(consistency)
; --- Summary ---
(print "\n============================================================")
(state)
(print "\nAll axioms:")
(list-axioms)
(print "\nAll theorems:")
(list-theorems)
(print "\n============================================================")
(print "Peano arithmetic built from observational field notes.")
(print "Every symbol introduced as a term, every property stated")
(print "as a parameterized axiom, concrete theorems via :bind.")
(print "All in successor notation — no numeric primitives.")
(print "============================================================")
(print "\n--- Environment check ---")
(dump-env)Field Notes: Observations on Shuffling Apples
Researcher: E. Peano, Fruit Laboratory
Observation 1: Piling Up
When placing apples into a basket one by one, every pile is reached by
adding one more apple to the previous pile. We decided to mark an empty
basket as "zero".
Observation 2: Combining Collections
When we pour one basket into another, the resulting pile is the union of
both. Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples.
We repeated this trial many times with identical results.
Observation 3: Order Independence
The order of combining does not matter — pouring basket A into basket B gives
the same pile as pouring basket B into basket A. We confirmed this by
swapping the pour direction across all trials.
Observation 4: Adding Nothing
Adding nothing to a basket does not change the pile. A basket of apples
still has the same apples after we pretend to pour an empty basket into it.
Observation 5: Comparing Collections
The basket with more apples is always heavier. If basket A has 🍎🍎🍎🍎🍎 and
basket B has 🍎🍎🍎, then basket A has more. The difference is found by
removing apples from the larger pile until it matches the smaller.
Observation 6: Swap Invariance
Swapping all apples between two equal baskets does not change either pile.
If both baskets have 🍎🍎🍎🍎 apples, after swapping they still each have 🍎🍎🍎🍎.
Observation 7: Equal Groups
Having several baskets each holding the same pile of apples is the same as
adding that pile repeatedly. Multiplication is a shortcut for combining
equal groups.
Garden of Eden — Daily Harvest Log
Date: October 15
Morning Shift
Eve picked 🍎🍎🍎 apples from the east grove.
Adam picked 🍎🍎🍎🍎🍎 apples from the west grove.
Combined morning harvest was 🍎🍎🍎🍎🍎🍎🍎🍎 apples.
Adam picked more apples than Eve in the morning.
Afternoon Shift
Serpent picked 🍎🍎🍎🍎 apples from the south grove.
Eve picked 🍎🍎 more apples from the east grove.
Combined afternoon harvest was 🍎🍎🍎🍎🍎🍎 apples.
Daily Summary
Eve's daily total is 🍎🍎🍎🍎🍎 apples.
Total harvest for the day was 🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎 apples.
Adam had the highest individual count with 🍎🍎🍎🍎🍎 apples.
The morning shift outproduced the afternoon by 🍎🍎 apples.
; Phase 6: Afternoon harvest
; Note: succ/zero are used here without explicit imports. This works because
; they are forward-declared primitives — evaluation returns them as bare
; Symbols, producing formal expressions like (succ (succ zero)). If these
; were computed terms requiring real evaluation, imports would be needed.
(defterm serpent-afternoon (succ (succ (succ (succ zero))))
:evidence (evidence "Eden Inventory"
:quotes ("Serpent picked 🍎🍎🍎🍎 apples from the south grove")
:explanation "Serpent's afternoon count: SSSS0"))
(defterm eve-afternoon (succ (succ zero))
:evidence (evidence "Eden Inventory"
:quotes ("Eve picked 🍎🍎 more apples from the east grove")
:explanation "Eve's afternoon count: SS0"))
; Phase 2: Axioms of Peano arithmetic
(defterm zero src.primitives.zero :origin "import")
(defterm succ src.primitives.succ :origin "import")
(defterm = src.primitives.= :origin "import")
(defterm + src.primitives.+ :origin "import")
(defterm - src.primitives.- :origin "import")
(defterm > src.primitives.> :origin "import")
(defterm * src.primitives.* :origin "import")
(axiom eq-reflexive (= ?x ?x)
:evidence (evidence "Counting Observations"
:quotes ("If both baskets have 🍎🍎🍎🍎 apples, after swapping they still each have 🍎🍎🍎🍎")
:explanation "Equality is reflexive: any pile equals itself"))
(axiom add-identity (= (+ ?n zero) ?n)
:evidence (evidence "Counting Observations"
:quotes ("Adding nothing to a basket does not change the pile")
:explanation "Additive identity: n + 0 = n"))
(axiom add-succ (= (+ ?n (succ ?m)) (succ (+ ?n ?m)))
:evidence (evidence "Counting Observations"
:quotes ("every pile is reached by adding one more apple to the previous pile")
:explanation "Addition step: n + S(m) = S(n + m)"))
(axiom add-commutative (= (+ ?a ?b) (+ ?b ?a))
:evidence (evidence "Counting Observations"
:quotes ("The order of combining does not matter")
:explanation "Commutativity: a + b = b + a"))
(axiom mul-zero (= (* ?n zero) zero)
:evidence (evidence "Counting Observations"
:quotes ("We decided to mark an empty basket as \"zero\"")
:explanation "Multiplication by zero: n * 0 = 0"))
(axiom mul-succ (= (* ?n (succ ?m)) (+ (* ?n ?m) ?n))
:evidence (evidence "Counting Observations"
:quotes ("Multiplication is a shortcut for combining equal groups")
:explanation "Multiplication step: n * S(m) = n*m + n"))
; Phase 4: Morning harvest
(defterm eve-morning (succ (succ (succ zero)))
:evidence (evidence "Eden Inventory"
:quotes ("Eve picked 🍎🍎🍎 apples from the east grove")
:explanation "Eve's morning count: SSS0"))
(defterm adam-morning (succ (succ (succ (succ (succ zero)))))
:evidence (evidence "Eden Inventory"
:quotes ("Adam picked 🍎🍎🍎🍎🍎 apples from the west grove")
:explanation "Adam's morning count: SSSSS0"))
; Phase 1: Primitive symbols
(defterm zero
:evidence (evidence "Counting Observations"
:quotes ("We decided to mark an empty basket as \"zero\"")
:explanation "Zero: the label for an empty collection"))
(defterm succ
:evidence (evidence "Counting Observations"
:quotes ("every pile is reached by adding one more apple to the previous pile")
:explanation "Successor: produces the next pile"))
(defterm =
:evidence (evidence "Counting Observations"
:quotes ("If both baskets have 🍎🍎🍎🍎 apples, after swapping they still each have 🍎🍎🍎🍎")
:explanation "Equality: two piles that look the same"))
(defterm +
:evidence (evidence "Counting Observations"
:quotes ("Combining 🍎🍎🍎 apples with 🍎🍎 apples always gives 🍎🍎🍎🍎🍎 apples")
:explanation "Addition: combining two collections"))
(defterm -
:evidence (evidence "Counting Observations"
:quotes ("The difference is found by removing apples from the larger pile until it matches the smaller")
:explanation "Subtraction: finding the difference"))
(defterm >
:evidence (evidence "Counting Observations"
:quotes ("If basket A has 🍎🍎🍎🍎🍎 and basket B has 🍎🍎🍎, then basket A has more")
:explanation "Greater-than: heavier basket has more"))
(defterm *
:evidence (evidence "Counting Observations"
:quotes ("Multiplication is a shortcut for combining equal groups")
:explanation "Multiplication: repeated addition"))