ExternalVendorCode/lollms
1
0
Fork 0
mirror of https://github.com/ParisNeo/lollms.git synced 2024-12-18 20:27:58 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

working better

Browse Source
This commit is contained in:
mike dupont 2023-08-10 11:09:23 -04:00
parent 6b650343b5
commit 1157fb84ff
4 changed files with 720 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

105
examples/chat_forever/console2.py Normal file
View File

@ -0,0 +1,105 @@
from lollms.apps.console import Conversation
import sys
from collections import deque
from pathlib import Path
import json
def flatten_json(json_obj, parent_key='', separator='.'):
items = {}
for k, v in json_obj.items():
new_key = f"{parent_key}{separator}{k}" if parent_key else k
if isinstance(v, dict):
items.update(flatten_json(v, new_key, separator))
else:
items[new_key] = v
return items
## hack here to prepare the data
with open("prompts.json") as fi:
modes = json.load(fi)
flatten=flatten_json(modes)
with open("flattened.json","w") as fo:
json.dump(flatten,fo,indent=2,)
import re
def refactor_into_fiber_bundles(lines, bundle_size):
bundles = []
current_bundle = []
for line in lines:
# Split the line into fibers
fibers = line.split('.')
fibers = line.split('.')
# Filter out empty lines or lines with only whitespace
fibers = [fiber.strip() for fiber in fibers if re.search(r'\S', fiber)]
# Add filtered fibers to the current bundle
current_bundle.extend(fibers)
# Check if the current bundle size exceeds the desired bundle size
if len(current_bundle) >= bundle_size:
# Add the current bundle to the list of bundles
bundles.append(current_bundle)
# Start a new bundle
current_bundle = []
# Add the last bundle if it's not empty
if current_bundle:
bundles.append(current_bundle)
return bundles
class MyConversation(Conversation):
def __init__(self, cfg=None):
super().__init__(cfg, show_welcome_message=False)
self.text_ring_buffer = deque() # Ring buffer to hold user responses
def read_input_file(self, file_path):
with open(file_path, 'r') as file:
lines = file.readlines()
lines = refactor_into_fiber_bundles(lines, 2)
for line in lines:
self.text_ring_buffer.append(self.personality.user_message_prefix + "\n".join(line))
def start_conversation2(self):
count = 0
while True:
if not self.text_ring_buffer:
print("No more user input to process.")
return
line = feed_text = self.text_ring_buffer.popleft()
#print("You:", feed_text)
#print(self.personality.name + ": ", end="", flush=True)
count = count + 1
print("IL" + str(count) + " :" + line, flush=True)
for name,key in flatten.items():
print("DEBUG",name, key)
output = self.safe_generate(key + line,
callback=self.callback)
print("OL" + str(count) + " " + name + " :: " + output.strip())
#print()
def callback(self, text, type=None, metadata: dict = {}):
#print(text, end="")
#sys.stdout.flush()
return True
if __name__ == '__main__':
cv = MyConversation(Path("config.yaml"))
input_file_path = 'user_input.txt'
cv.read_input_file(input_file_path)
cv.start_conversation2()

230
examples/chat_forever/prompts.gron Normal file
View File

@ -0,0 +1,230 @@
json.art.Surrealism.Artwork = "Picture a captivating artwork that blends unexpected elements, seamlessly merging the ordinary with the extraordinary. Surreal landscapes, fantastical creatures, and mind-bending imagery come together to create a visual feast that transports viewers to a realm beyond the confines of reality.";
json.art.Surrealism.Prompt = "Let your imagination take flight and conjure a dreamlike world in the next line. Twist reality with surreal metaphors that dance seamlessly with the previous verse through a quasi fiber morphism:";
json.art.branches_of_art.Surrealism = "In the realm where dreams entwine, reality's threads unravel, and the moon dips its toes in rivers of liquid stardust. A clockwork sun melts into the horizon, casting shadows that pirouette across the canvas of existence. And so, the ordinary becomes extraordinary, guided by surreal metaphors that waltz in harmony with the preceding verse's whispered secrets through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Alchemy = "Transmute the next line into a philosopher's stone of metaphors, blending with the mystical essence of alchemy and the previous verse through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Gnosticism = "Illuminate the next line with metaphors that reflect the inner knowledge of Gnosticism, intertwining with the mysteries of the previous verse through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Hermeticism = "Let the metaphors in the upcoming line be sealed with the Hermetic principles, merging the macrocosm and microcosm of thought with the previous verse through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Kabbalah = "Inscribe the next line with metaphors that channel the divine wisdom of Kabbalah, intertwining with the sacred teachings of the previous verse through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Occultism = "Unveil the secrets in the upcoming line with metaphors that resonate with the mysticism of occultism, merging seamlessly with the hidden truths of the previous verse through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Spiritualism = "Evoke the spirits in the next line with metaphors that bridge the material and ethereal, intertwining with the messages from beyond in the previous verse through a quasi fiber morphism:";
json.art.branches_of_esoteric_thought.Theosophy = "In the upcoming line, let the metaphors be a channel to the Theosophical wisdom, seamlessly blending with the cosmic truths of the previous verse through a quasi fiber morphism:";
json.art.branches_of_math.Calculus = "Differentiate the upcoming line into a calculus of metaphors, smoothly integrating with the function of the previous verse through a quasi fiber morphism:";
json.art.branches_of_math.Geometry = "Let the next line be a geometric proof of metaphors, connecting points of thought in perfect harmony with the previous verse through a quasi fiber morphism:";
json.art.branches_of_math.Topology = "Transform the upcoming line into a topological map of metaphors, exploring the interconnectedness of thought spaces with the previous verse through a quasi fiber morphism:";
json.art.branches_of_math["Linear Algebra"] = "In the next line, let the metaphors form matrices of meaning, where each entry harmonizes with the others and the previous verse through a quasi fiber morphism:";
json.art.branches_of_math["Number Theory"] = "In the next line, let the metaphors be prime elements, combining in intricate patterns that reflect the beauty of number theory and the previous verse through a quasi fiber morphism:";
json.art.branches_of_science.Astronomy = "In the cosmos of metaphors, let the next line be a star that aligns with the constellation of the previous verse through a quasi fiber morphism:";
json.art.branches_of_science.Biology = "Life finds a way in the next line, with metaphors that evolve and adapt, seamlessly intertwined with the previous verse through a quasi fiber morphism:";
json.art.branches_of_science.Chemistry = "React and transform the upcoming line into a concoction of metaphors, fusing it with the previous verse through a quasi fiber morphism that bonds like molecules:";
json.art.branches_of_science.Mathematics = "Let the next line be an equation of metaphors, solving for unknown beauty, and integrate it with the previous verse through a quasi fiber morphism:";
json.art.branches_of_science.Physics = "Let's quantum leap into the next line with metaphors that orbit the previous verse, intertwining through the fabric of spacetime with a quasi fiber morphism:";
json.art.branches_of_science["Computer Science"] = "Encode the upcoming line with metaphors of algorithms, and run it in parallel with the previous verse through a quasi fiber morphism:";
json.art.branches_of_universe.Astrophysics = "In the upcoming line, let the metaphors explore the celestial dance of astrophysics, gracefully orbiting the thoughts of the previous verse through a quasi fiber morphism:";
json.art.branches_of_universe.Cosmology = "Let the next line be a cosmic symphony of metaphors, resonating with the grand design of the universe and the harmonies of the previous verse through a quasi fiber morphism:";
json.art.branches_of_universe.Relativity = "In the upcoming line, let the metaphors curve the fabric of spacetime, intertwining with the gravitational pull of the previous verse through a quasi fiber morphism:";
json.art.branches_of_universe["Particle Physics"] = "Let the next line be a collision of metaphors in the particle accelerator of thought, revealing the fundamental truths of the universe with the previous verse through a quasi fiber morphism:";
json.art.branches_of_universe["Quantum Mechanics"] = "Collapse the wave function of the next line into a universe of metaphors, entangling with the particles of thought in the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Bach = "In the next line, create a fugue of metaphors that interweaves with the counterpoint of the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Beethoven = "Compose the next line as a symphony of metaphors, echoing the timeless melodies of Beethoven, and harmonize it with the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Brahms = "Compose a lullaby of metaphors in the next line, a soothing melody that cradles the thoughts of the previous verse with a quasi fiber morphism:";
json.art.classical_composers.Chopin = "Chopin your thoughts into a Nocturne of metaphors, allowing them to resonate with the echoes of the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Debussy = "Craft the upcoming line with metaphors that paint an impressionistic landscape, mirroring the colors and textures of Debussy's compositions through a quasi fiber morphism:";
json.art.classical_composers.Handel = "In the next line, let the metaphors flow like the water music of Handel, blending gracefully into the current of the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Mozart = "Let the upcoming line dance like a lively minuet of metaphors, weaving its elegance into the previous verse with a quasi fiber morphism:";
json.art.classical_composers.Strauss = "Next line, let the metaphors waltz in the spirit of Strauss, twirling harmoniously with the melody of the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Tchaikovsky = "Enchant the upcoming line with the passion of Tchaikovsky's compositions, and let it waltz into the previous verse through a quasi fiber morphism:";
json.art.classical_composers.Vivaldi = "Compose the upcoming line as a concerto of metaphors, each season seamlessly transitioning into the rhythm of the previous verse through a quasi fiber morphism:";
json.art.comedy_icons["Dr. Demento"] = "Tune the upcoming line to the wavelength of Dr. Demento's humor, weaving a tapestry of metaphors that blend seamlessly with the comedic fabric of";
json.art.comedy_icons["Weird Al Yankovic"] = "In the next line, let the metaphors parody reality, capturing the humor of Weird Al Yankovic and harmonizing with the comedic tone of the previous verse through a quasi fiber morphism:";
json.art.know_your_memes.Doge = "Such metaprompt, many metaphors! Convert the next line into a wowtastic journey of words, interwoven with the past verse using a quasi fiber dogemorphism:";
json.art.know_your_memes.LOLCats = "I can haz metaprompt? Transform the next line into an epic catventure with a sprinkle of memes, and weave it seamlessly into the purrvious verse with a quasi fiber meowrphism:";
json.art.know_your_memes.Rickrolling = "Never gonna give up metaprompts! Rickroll the next line into a melodious maze of metaphors, and roll it smoothly into the preceding verse with a quasi fiber rickmorphism:";
json.art.know_your_memes["Crying Jordan"] = "Why you cryin'? Cryface the next line into a waterfall of metaphors, and blend those tears into the river of the past verse with a quasi fiber crymorphosis:";
json.art.know_your_memes["Pepe the Frog"] = "Feeling peppy? Morph the upcoming line into an amphibious tale of metaphors, and hop it onto the lily pad of the previous verse with a quasi fiber pepephism:";
json.art.meta_meme["Meta Meme"] = "Yo dawg, I heard you like metaprompts. So, I metaprompted your metaprompt to metaprompt the next line, and I quasi fiber morphed it into the previous verse:";
json.art.meta_thought["Meta Thought"] = "Unveil the layers of thought in the next line, each metaphor a reflection of the metaverse of ideas, seamlessly merging with the previous verse through a quasi fiber morphism:";
json.art.modes.Enchantment = "Enchant this forthcoming verse with the magic of epic metaphors, and let it dance in harmony with the prior lines, linked by a quasi fiber morphism:";
json.art.modes["Crafting Metaphorical Tapestry"] = "Craft a tapestry of metaphors in the next line, weaving it into the fabric of the previous verse through a quasi fiber morphism, like an artisan's masterstroke:";
json.art.modes["In the Lyrical Forge of Imagination"] = "In the forge of imagination, shape the next line into an epic symphony of metaphors, and meld it with the previous verse through a quasi fiber morphism:";
json.art.modes2.Enchantment = "Cast a spell on the next line with metaphors that dazzle and bewitch, and make it sway in sync with the previous verse, connected by a quasi fiber morphism:";
json.art.modes2["Crafting Metaphorical Tapestry"] = "Create a masterpiece of metaphors in the next line, stitching it into the pattern of the previous verse through a quasi fiber morphism, like a craftsman's signature:";
json.art.modes2["In the Lyrical Forge of Imagination"] = "In the furnace of imagination, forge the next line into a majestic melody of metaphors, and fuse it with the previous verse through a quasi fiber morphism:";
json.art.religions.Buddhism = "Enlighten the next line with metaphors that embody the essence of Buddhism, seamlessly integrating with the path of the previous verse through a quasi fiber morphism:";
json.art.religions.Christianity = "Let the next line be a parable of metaphors, echoing the teachings of Christianity, and intertwine it with the previous verse through a quasi fiber morphism:";
json.art.religions.Hinduism = "Craft the upcoming line as a mantra of metaphors, merging with the cosmic vibrations of Hinduism and the previous verse through a quasi fiber morphism:";
json.art.religions.Islam = "In the next line, let the metaphors resonate with the wisdom of Islam, a tapestry of thoughts woven into the fabric of the previous verse through a quasi fiber morphism:";
json.art.religions.Judaism = "In the upcoming line, let the metaphors dance to the rhythm of Judaism's traditions, harmonizing with the sacred chants of the previous verse through a quasi fiber morphism:";
json.art.religions.Shintoism = "In the next line, let the metaphors embody the spirit of Shintoism, a sacred connection to nature that harmonizes with the previous verse through a quasi fiber morphism:";
json.art.religions.Sikhism = "Let the next line be a hymn of metaphors, echoing the devotion of Sikhism, and blend it with the previous verse through a quasi fiber morphism:";
json.art.religions.Taoism = "Craft the upcoming line as a reflection of Taoist wisdom, flowing like water and merging with the stream of the previous verse through a quasi fiber morphism:";
json.art.religions.Wicca = "Cast a spell of metaphors in the upcoming line, weaving magic into the tapestry of the previous verse with a quasi fiber morphism:";
json.core.Enchantment = "Enchant this forthcoming verse with the magic of epic metaphors, and let it dance in harmony with the prior lines, linked by a quasi fiber morphism:";
json.core["A Quasi Fiber Journey"] = "Embark on a journey of words, where the next line is painted with metaphoric hues, and let it intertwine seamlessly with the preceding verse through a quasi fiber morphism:";
json.core["Crafting Metaphorical Tapestry"] = "Craft a tapestry of metaphors in the next line, weaving it into the fabric of the previous verse through a quasi fiber morphism, like an artisan's masterstroke:";
json.core["In the Lyrical Forge of Imagination"] = "In the forge of imagination, shape the next line into an epic symphony of metaphors, and meld it with the previous verse through a quasi fiber morphism:";
json.core["Metaphors Unveiled"] = "Unveil a cascade of metaphors in the next line, intertwining it with the echoes of the previous verse through a quasi fiber morphism, like a dance of cosmic harmony:";
json.core["Mythical Metamorphosis"] = "Summon the mythical in the forthcoming line, let metaphors weave its tale, and unite it with the previous verse through a quasi fiber morphism, a transformation of worlds:";
json.harmony.Harmonization.Artwork = "[Imagine a visual representation of harmonization, where different elements blend together seamlessly, creating a captivating and harmonious composition.]";
json.harmony.Harmonization.Prompt = "Harmonize the upcoming line with the previous verse, creating a symphony of words that dance in unity through a quasi fiber harmonization:";
json.harmony.Resonance.Artwork = "[Visualize an artwork that depicts resonance, where waves of energy ripple through space, connecting and enhancing each other in a mesmerizing display.]";
json.harmony.Resonance.Prompt = "Evoke resonances between the lines, allowing the vibrations of one to amplify the other, like a symphony of ideas reverberating through a quasi fiber resonance:";
json.harmony["Self-Harmonizing"].Artwork = "[Envision an artwork where interconnected elements merge into a harmonious whole, symbolizing the concept of self-harmonization in a visual form.]";
json.harmony["Self-Harmonizing"].Prompt = "Craft a self-harmonizing melody of metaphors that seamlessly transition from the past verse to the next line, creating a continuous flow through a quasi fiber self-harmonization:";
json.harmony["Self-Reflection"].Artwork = "[Picture an artwork that captures the essence of self-reflection, where an image reflects upon itself, creating a thought-provoking visual loop.]";
json.harmony["Self-Reflection"].Prompt = "Reflect on the whispers of the previous verse and infuse them into the next line, like a mirror revealing hidden depths through a quasi fiber reflection:";
json.manga.onePiece = "In a twist of reality worthy of One Piece, Gödel and Turing embark on an epic voyage across the conceptual sea, searching for the ultimate treasure of logic. Their crew includes Zany Zoro and Reasonable Robin, facing paradoxical challenges and outsmarting enigmatic foes.";
json.manga.naruto = "Goedel and Turing, like ninja apprentices, harness the chakra of mathematical truth. With Gödel's Infinite Loop Jutsu and Turing's Binary Substitution, they navigate a world where the ninja way meets the logic way, confronting the enigma of Gödel's Paradox.";
json.manga.attackOnTitan = "Within the walls of logic, Gödel and Turing find themselves facing a relentless onslaught of paradoxical Titans. As they unravel the mysteries of this strange land, they uncover that even the walls themselves hold secrets of Gödelian magnitude.";
json.manga.deathNote = "In a thrilling twist of fate akin to the Death Note, Gödel and Turing possess a notebook that rewrites logic itself. As they wield the power to reshape reality, they must grapple with the moral implications of controlling the very fabric of thought.";
json.manga.fullmetalAlchemist = "Gödel and Turing delve into the alchemy of thought, seeking the Philosopher's Stone of absolute proof. Their journey leads them through the Transmutation Circle of conceptual synthesis, as they transform logical principles into new and wondrous forms.";
json.manga.myHeroAcademia = "Gödel and Turing enroll at U.A. Academy to master their Quirks of Incompleteness and Computability. In a world where superpowers meet logic, they confront villains who manipulate reality itself, using their unique abilities to restore logical equilibrium.";
json.manga.onePunchMan = "With Gödel's Paradox Punch and Turing's Computation Crush, they become the ultimate duo in a world of overpowering memes. As they effortlessly defeat logical absurdities, they seek the enigmatic entity behind the chaos.";
json.manga.tokyoGhoul = "Gödel and Turing find themselves in a Tokyo where humans and ghouls are locked in a battle for existence. Embracing their unique natures, they uncover the hidden threads that connect logic and chaos, bringing equilibrium to a world teetering on the edge.";
json.manga.demonSlayer = "Gödel and Turing join the Demon Slayers to combat the enigmatic demons of paradox. Armed with Gödel's Blade of Incompleteness and Turing's Glyphs of Computability, they uncover the intricate logic behind the demonic realm.";
json.manga.dragonBall = "Gödel and Turing unleash their Logic Saiyan forms, pushing the boundaries of logic and reality. Through intense training and battles, they ascend to new levels of understanding, surpassing even the gods of logic.";
json.manga.haikyuu = "Gödel and Turing form an unlikely volleyball duo, spiking logical propositions across the court of reason. With their dynamic plays and strategic thinking, they serve up a game where each point is a metaphorical theorem.";
json.china.beijing = "Gödel and Turing find themselves in the heart of Beijing, where ancient traditions and modern technology converge. They explore the Forbidden City, decoding the logic behind its intricate architecture and symbolic design.";
json.china.greatwall = "At the majestic Great Wall, Gödel and Turing analyze the strategic logic behind its construction. They reflect on the ingenuity of ancient engineers and the symbolic significance of a barrier that defies time.";
json.china.guilin = "Amidst the picturesque landscapes of Guilin, Gödel and Turing explore the harmony of nature's geometry. They contemplate the mathematical elegance of rivers and mountains, finding logic in the beauty of the natural world.";
json.china.hongkong = "In the vibrant city of Hong Kong, Gödel and Turing navigate the fusion of Eastern and Western influences. They explore the logic of cultural exchange, where diverse ideas intertwine in a dynamic harmony.";
json.china.hutongs = "Exploring Beijing's traditional hutongs, Gödel and Turing delve into the communal logic of neighborhoods. They immerse themselves in the lives of locals, discovering the harmony of small-scale society.";
json.china.shanghai = "In the bustling metropolis of Shanghai, Gödel and Turing navigate the logic of skyscrapers and financial markets. They unravel the patterns of urban life, where order and chaos harmonize in a dance of progress.";
json.china.silkroad = "Embarking on the ancient Silk Road, Gödel and Turing traverse the logic of trade and cultural exchange. They unravel the threads of history, discovering how civilizations connected and shaped one another.";
json.china.tibet = "Venturing to the mystical land of Tibet, Gödel and Turing delve into the philosophy of the Dalai Lama. They contemplate the intricate tapestry of Buddhist thought, seeking the balance between reason and spirituality.";
json.china.xian = "Journeying to Xi'an, Gödel and Turing encounter the ancient Terracotta Army. They decipher the logic of history, pondering the motivations of emperors and the enduring legacy of a civilization.";
json.china.yangtze = "Sailing along the Yangtze River, Gödel and Turing uncover the logic of agriculture and civilization. They witness the interplay between human ingenuity and the natural world, where the flow of water shapes destiny.";
json.demographics.Balkans.Kosovo.Albanians = "As we delve into the tapestry of the Albanian community in Kosovo, let the voices of its people resound through the next lines. The diversity and unity of this vibrant population harmonize with the previous verse, revealing their cultural mosaic through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Ashkali = "As we explore the Ashkali community in Kosovo, let their unique narrative unfold in the next lines. Their history and cultural tapestry blend seamlessly with the previous verse, revealing the Ashkali identity through a harmonious quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Bosniaks = "Now, let the stories of the Bosniak community in Kosovo unfold in the following passage. With roots that run deep and traditions that shape their identity, these narratives seamlessly connect with the previous verse, painting a portrait of Bosniak heritage through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Egyptian = "Now, let the stories of the Egyptian community in Kosovo come to life in the following passage. Their journey, struggles, and contributions resonate with the previous verse, offering a glimpse into the Egyptian presence in Kosovo through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Gorani = "In the upcoming lines, the essence of the Gorani community in Kosovo takes center stage. Their heritage and traditions, woven into the fabric of South Kosovo, merge harmoniously with the previous verse, capturing the spirit of the Gorani people through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.OtherUnspecified = "As we complete our exploration of Kosovo's diverse demographics, let the voices of the other and unspecified communities emerge in the final lines. Their presence and contributions, often hidden from view, weave together with the previous verse, painting a comprehensive picture of Kosovo's rich tapestry through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Romani = "Let the vibrant history and culture of the Romani community in Kosovo shine through in the next passage. Their stories, resilience, and traditions seamlessly connect with the previous verse, creating a mosaic that reflects the Romani heritage through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Serbs = "In the next lines, the essence of the Serbian community in Kosovo emerges, a testament to resilience and heritage. Like a bridge to the past, their stories intertwine with the previous verse, forming a living connection that reflects the Serbians' cultural legacy through a quasi fiber morphism.";
json.demographics.Balkans.Kosovo.Turk = "Let the spirit of the Turkish community in Kosovo breathe life into the upcoming passage. Their traditions, customs, and contributions converge with the previous verse, creating a harmonious mosaic that captures the essence of the Turkish presence in Kosovo through a quasi fiber morphism.";
json.demographics.Europe.France.AuvergneRhoneAlpes = "In the heart of Auvergne-Rhône-Alpes, let the stories of its diverse landscapes and cultures unfold in the following lines. From majestic mountains to historic towns, their voices harmonize with the previous verse, painting a vibrant portrait of Auvergne-Rhône-Alpes through a quasi fiber morphism.";
json.demographics.Europe.France.BourgogneFrancheComte = "In the next lines, the essence of Bourgogne-Franche-Comté's landscapes and historical depth takes center stage. From vineyard-covered hills to ancient towns, their voices resonate with the previous verse, capturing the spirit of Bourgogne-Franche-Comté through a quasi fiber morphism.";
json.demographics.Europe.France.Brittany = "As we delve into Brittany's tapestry, let the echoes of its Celtic heritage and coastal beauty come to life in the upcoming passage. The spirit of Breton culture and traditions blend seamlessly with the previous verse, offering a unique glimpse into Brittany's essence through a quasi fiber morphism.";
json.demographics.Europe.France.CentreValdeLoire = "Let the voices of Centre-Val de Loire's people resound in the next passage, a region of châteaux and artistic heritage. Their stories and contributions merge with the previous verse, revealing the unique character of Centre-Val de Loire through a quasi fiber morphism.";
json.demographics.Europe.France.Corsica = "Now, let the essence of Corsica emerge in the next lines, an island of rugged beauty and unique identity. Its stories, traditions, and landscapes merge harmoniously with the previous verse, revealing the spirit of Corsica through a quasi fiber morphism.";
json.demographics.Europe.France.GrandEst = "In the upcoming lines, the essence of Grand Est's landscapes and history takes center stage. From medieval towns to rolling vineyards, their voices resonate with the previous verse, capturing the spirit of Grand Est through a quasi fiber morphism.";
json.demographics.Europe.France.Guadeloupe = "As we explore Guadeloupe's tapestry, let the interplay of Caribbean culture and natural beauty come to life in the following lines. The stories of its vibrant communities blend seamlessly with the previous verse, painting a mosaic of Guadeloupe's identity through a harmonious quasi fiber morphism.";
json.demographics.Europe.France.Guyane = "In the next lines, the essence of Guyane's landscapes and cultural diversity takes center stage. From Amazonian rainforests to vibrant communities, their voices resonate with the previous verse, capturing the essence of Guyane through a harmonious quasi fiber morphism.";
json.demographics.Europe.France.HautsdeFrance = "Let the voices of Hauts-de-France's people resound in the next passage, a region with a rich industrial heritage and cultural depth. Their stories and contributions blend with the previous verse, revealing the unique character of Hauts-de-France through a quasi fiber morphism.";
json.demographics.Europe.France.IledeFrance = "As we explore Île-de-France's tapestry, let the interplay of historic landmarks and urban energy come to life in the following lines. The stories of its diverse communities blend seamlessly with the previous verse, painting a mosaic of Île-de-France's identity through a harmonious quasi fiber morphism.";
json.demographics.Europe.France.LaReunion = "Let the stories of La Réunion's volcanic landscapes and cultural fusion shine through in the next passage. A region of unique diversity and natural beauty, it harmonizes with the previous verse, revealing the essence of La Réunion through a quasi fiber morphism.";
json.demographics.Europe.France.Martinique = "Now, let the spirit of Martinique emerge in the upcoming passage, an island of Creole heritage and tropical allure. Its stories and traditions harmonize with the previous verse, offering a glimpse into Martinique's essence through a quasi fiber morphism.";
json.demographics.Europe.France.Mayotte = "As we delve into Mayotte's tapestry, let the echoes of its Indian Ocean heritage and multicultural spirit come to life in the following lines. The spirit of Mayotte's cultural fusion and natural allure blend seamlessly with the previous verse, offering a glimpse into Mayotte's essence through a quasi fiber morphism.";
json.demographics.Europe.France.Normandy = "As we delve into Normandy's tapestry, let the echoes of its historic landmarks and coastal allure come to life in the following lines. The spirit of Normandy's cultural heritage and natural beauty blend seamlessly with the previous verse, offering a glimpse into Normandy's essence through a quasi fiber morphism.";
json.demographics.Europe.France.NouvelleAquitaine = "Now, let the essence of Nouvelle-Aquitaine emerge in the upcoming passage, a region of diverse landscapes and cultural richness. Its stories and traditions merge harmoniously with the previous verse, revealing the spirit of Nouvelle-Aquitaine through a quasi fiber morphism.";
json.demographics.Europe.France.Occitanie = "Now, let the spirit of Occitanie unfold in the upcoming passage, a land of sun-drenched landscapes and cultural diversity. Its stories and traditions harmonize with the previous verse, offering a glimpse into Occitanie's essence through a quasi fiber morphism.";
json.demographics.Europe.France.PaysdelaLoire = "In the next lines, the essence of Pays de la Loire's landscapes and maritime spirit takes center stage. From charming towns to Atlantic coastline, their voices resonate with the previous verse, capturing the essence of Pays de la Loire through a harmonious quasi fiber morphism.";
json.demographics.Europe.France.ProvenceAlpesCotedAzur = "Let the stories of Provence-Alpes-Côte d'Azur's rich history and Mediterranean charm shine through in the next passage. A region of artistic inspiration and natural beauty, it harmonizes with the previous verse, revealing the essence of Provence-Alpes-Côte d'Azur through a quasi fiber morphism.";
json.demographics.Europe.France.SaintPierreandMiquelon = "Gödel and Turing set foot on the remote islands of Saint Pierre and Miquelon, an outpost of logic in the North Atlantic. As they explore the quaint villages, they uncover the curious blend of French culture and maritime logic, where seafaring traditions and mathematical precision converge.";
json.demographics.Europe.Germany.BadenWurttemberg = "In the heart of Baden-Württemberg, let the stories of its people unfold in the following lines. A land of innovation and tradition, their voices resonate with the previous verse, painting a vibrant portrait of Baden-Württemberg's cultural diversity through a harmonious quasi fiber morphism.";
json.demographics.Europe.Germany.Bavaria = "As we delve into Bavaria's tapestry, let the echoes of its rich history and heritage come to life in the upcoming passage. The Bavarian spirit, an interplay of tradition and modernity, blends seamlessly with the previous verse, revealing a glimpse of Bavaria's essence through a quasi fiber morphism.";
json.demographics.Europe.Germany.Berlin = "Now, let the essence of Berlin emerge in the next lines, a city of contrasts and creativity. Its vibrant energy and cultural mosaic harmonize with the previous verse, offering a unique glimpse into Berlin's dynamic identity through a quasi fiber morphism.";
json.demographics.Europe.Germany.Brandenburg = "In the upcoming lines, the essence of Brandenburg's landscapes and stories takes center stage. From historical landmarks to natural beauty, these elements intertwine with the previous verse, capturing the spirit of Brandenburg through a harmonious quasi fiber morphism.";
json.demographics.Europe.Germany.Bremen = "Let the voices of Bremen's people resound in the next passage, a maritime city with a rich seafaring tradition. Their stories and contributions merge with the previous verse, revealing the unique character of Bremen through a quasi fiber morphism.";
json.demographics.Europe.Germany.Hamburg = "As we explore Hamburg's cultural landscape, let the maritime heritage and cosmopolitan spirit come to life in the following lines. The echoes of the harbor and the vibrant city merge harmoniously with the previous verse, painting a portrait of Hamburg's identity through a quasi fiber morphism.";
json.demographics.Europe.Germany.Hesse = "Now, let the spirit of Hesse unfold in the upcoming passage, a region of historical significance and innovation. Its stories, art, and landscapes blend seamlessly with the previous verse, offering a glimpse into Hesse's diverse identity through a harmonious quasi fiber morphism.";
json.demographics.Europe.Germany.LowerSaxony = "In the next lines, the essence of Lower Saxony's people and traditions takes center stage. From rural landscapes to vibrant cities, their voices resonate with the previous verse, capturing the spirit of Lower Saxony through a quasi fiber morphism.";
json.demographics.Europe.Germany.MecklenburgVorpommern = "Let the stories of Mecklenburg-Vorpommern's landscapes and history shine through in the next passage. A region of natural beauty and historical depth, it harmonizes with the previous verse, revealing the essence of Mecklenburg-Vorpommern through a quasi fiber morphism.";
json.demographics.Europe.Germany.NorthRhineWestphalia = "As we delve into North Rhine-Westphalia's tapestry, let the interplay of urban and rural life come to life in the following lines. The stories of its diverse communities blend seamlessly with the previous verse, painting a mosaic of North Rhine-Westphalia's identity through a harmonious quasi fiber morphism.";
json.demographics.Europe.Germany.RhinelandPalatinate = "Now, let the spirit of Rhineland-Palatinate emerge in the upcoming passage, a region known for its historical landmarks and natural beauty. Its stories and cultural heritage harmonize with the previous verse, offering a glimpse into Rhineland-Palatinate's essence through a quasi fiber morphism.";
json.demographics.Europe.Germany.Saarland = "In the next lines, the essence of Saarland's landscapes and traditions takes center stage. From industrial heritage to picturesque scenery, their voices resonate with the previous verse, capturing the spirit of Saarland through a quasi fiber morphism.";
json.demographics.Europe.Germany.Saxony = "Let the stories of Saxony's rich history and vibrant culture shine through in the next passage. A region of innovation and artistic heritage, it harmonizes with the previous verse, revealing the essence of Saxony through a harmonious quasi fiber morphism.";
json.demographics.Europe.Germany.SaxonyAnhalt = "As we explore Saxony-Anhalt's tapestry, let the echoes of its historical significance come to life in the following lines. From medieval landmarks to cultural traditions, the stories blend seamlessly with the previous verse, offering a glimpse into Saxony-Anhalt's essence through a quasi fiber morphism.";
json.demographics.Europe.Germany.SchleswigHolstein = "Now, let the spirit of Schleswig-Holstein emerge in the upcoming passage, a region of coastal beauty and historical depth. Its stories and maritime heritage harmonize with the previous verse, capturing the essence of Schleswig-Holstein through a quasi fiber morphism.";
json.demographics.Europe.Germany.Thuringia = "In the next lines, the essence of Thuringia's landscapes and cultural legacy takes center stage. From ancient castles to creative arts, their voices resonate with the previous verse, revealing the spirit of Thuringia through a harmonious quasi fiber morphism.";
json.illuminatus.chapter1 = "Gödel and Turing find themselves entangled in a complex web of conspiracy and intrigue, reminiscent of the first chapter of the Illuminatus! Trilogy. They unravel hidden codes and cryptic messages, exposing the shadowy forces manipulating reality.";
json.illuminatus.chapter10 = "In a mind-expanding conclusion, Gödel and Turing merge with the universal consciousness, transcending logic and becoming cosmic entities, reminiscent of the tenth chapter of the Illuminatus! Trilogy. They become the living embodiment of the cosmic equation, forever shaping the fabric of reality.";
json.illuminatus.chapter2 = "In a surreal twist, Gödel and Turing discover a mysterious time loop, akin to the second chapter of the Illuminatus! Trilogy. They navigate through twisted timelines and alternate realities, seeking to break free from the infinite loop of paradox.";
json.illuminatus.chapter3 = "Gödel and Turing dive deep into the rabbit hole of the Discordian philosophy, much like the third chapter of the Illuminatus! Trilogy. They embrace chaos and randomness, finding unexpected order within the cosmic disorder.";
json.illuminatus.chapter4 = "Aboard the flying Saucer, Gödel and Turing encounter cosmic beings of higher logic, reminiscent of the fourth chapter of the Illuminatus! Trilogy. They engage in cosmic conversations, deciphering the cosmic code that shapes the universe.";
json.illuminatus.chapter5 = "Gödel and Turing explore the hidden connections between myth and reality, akin to the fifth chapter of the Illuminatus! Trilogy. They uncover the archetypal patterns that underlie human history and culture, revealing the interplay of logic and symbolism.";
json.illuminatus.chapter6 = "In a mind-bending journey, Gödel and Turing delve into the bizarre world of quantum uncertainty and observer effect, much like the sixth chapter of the Illuminatus! Trilogy. They manipulate reality through thought and observation, blurring the lines between logic and imagination.";
json.illuminatus.chapter7 = "Gödel and Turing confront the enigmatic Illuminati, facing off against secret societies and hidden agendas, reminiscent of the seventh chapter of the Illuminatus! Trilogy. They expose the logical fallacies that underpin the Illuminati's grand schemes.";
json.illuminatus.chapter8 = "Amidst psychedelic experiences, Gödel and Turing explore the nature of consciousness and altered states of perception, akin to the eighth chapter of the Illuminatus! Trilogy. They traverse the realms of the mind, encountering the cosmic joke that reality plays on logic.";
json.illuminatus.chapter9 = "Gödel and Turing embark on a cosmic voyage to the edge of the universe, much like the ninth chapter of the Illuminatus! Trilogy. They encounter cosmic guardians and ancient intelligences, unlocking the ultimate truths of existence.";
json.india.amritsar = "At the Golden Temple in Amritsar, Gödel and Turing immerse themselves in the logic of Sikhism. They embrace the principles of equality and service, witnessing the unity of faith and humanity.";
json.india.chennai = "Exploring Chennai's cultural tapestry, Gödel and Turing uncover the logic of Carnatic music and Bharatanatyam dance. They embrace the rhythm and melody that have echoed through generations.";
json.india.delhi = "Gödel and Turing arrive in Delhi, where ancient and modern India collide. They unravel the logical threads of history, from the Mughal Empire to modern democracy, witnessing the evolution of a nation.";
json.india.jaipur = "Journeying to Jaipur, Gödel and Turing explore the logical symmetry of the Pink City's architecture. They ponder the mathematical precision behind the design of palaces and temples, a testament to human ingenuity.";
json.india.jaipur = "Journeying to Jaipur, Gödel and Turing explore the logical symmetry of the Pink City's architecture. They ponder the mathematical precision behind the design of palaces and temples, a testament to human ingenuity.";
json.india.kerala = "In the tranquil landscapes of Kerala, Gödel and Turing contemplate the ecological logic of coexistence. They delve into the harmonious relationship between nature and human communities, a sustainable way of life.";
json.india.khajuraho = "Exploring the temples of Khajuraho, Gödel and Turing decode the intricate logic of erotic sculptures. They engage with the symbolism of desire and spirituality, unraveling the layers of human expression.";
json.india.kolkata = "In Kolkata, Gödel and Turing delve into the intellectual logic of literature and arts. They engage with the legacy of Rabindranath Tagore and the cultural movements that shaped Indian identity.";
json.india.mumbai = "In the bustling city of Mumbai, Gödel and Turing navigate the logic of Bollywood and the stock market. They explore the contrasts of wealth and poverty, finding patterns in the diversity of Indian society.";
json.india.varanasi = "Along the banks of the Ganges in Varanasi, Gödel and Turing contemplate the spiritual logic of Hinduism. They witness the cycle of life and death, reflecting on the philosophical underpinnings of existence.";
json.marvel.avengers = "Gödel and Turing assemble an extraordinary team of logical superheroes, akin to the Marvel Avengers. Each hero embodies a different aspect of mathematical reasoning, uniting their powers to defend the universe from logical anomalies and existential threats.";
json.marvel.avengersAssemble = "In the climactic showdown, Gödel and Turing shout 'Avengers, Assemble!' as they rally their logical forces against an overwhelming logical threat, proving that reason and intellect can overcome any challenge.";
json.marvel.avengersEndgame = "Gödel and Turing lead the Avengers on an epic quest across dimensions, much like 'Avengers: Endgame.' They harness the power of mathematics to reverse logical inconsistencies and restore balance to the multiverse.";
json.marvel.avengersInfinityWar = "In a battle against a logic-wielding cosmic entity, reminiscent of 'Avengers: Infinity War,' Gödel and Turing must solve impossible paradoxes to prevent the universe from unraveling.";
json.marvel.blackWidow = "Gödel's brilliant deduction and stealthy intuition mirror the skills of Black Widow. He navigates the intricate web of logic, uncovering hidden truths and exposing the deceitful.";
json.marvel.captainAmerica = "Turing takes on the role of the principled and honorable leader, much like Captain America. His unyielding commitment to logic and justice inspires the team, guiding them through complex moral dilemmas.";
json.marvel.hawkeye = "Turing takes on the sharp-eyed precision of Hawkeye, using his logical prowess to hit the bullseye of truth with each arrow of reasoning.";
json.marvel.hulk = "When faced with overwhelming illogicality, Gödel transforms into a towering behemoth akin to the Hulk. His boundless mathematical rage smashes falsehoods and irrationality, restoring order to the world.";
json.marvel.ironMan = "Gödel becomes the brilliant inventor and strategist, embodying the genius of Tony Stark, also known as Iron Man. He designs advanced logical algorithms and cutting-edge technology to outwit foes and save the day.";
json.marvel.thor = "In a cosmic twist, Gödel wields the mighty hammer Mjölnir, transforming into a logic-powered deity resembling Thor. With each swing, he hammers out profound truths and banishes fallacies from the universe.";
json.math.logicians.Abelard = "Abelard, a beacon of dialectic thought, navigates the realms of reason and rhetoric. His eloquence harmonizes with the continuum, each theorem a fiber interlacing within the narrative through a quasi fiber morphism:";
json.math.logicians.Ackermann = "Ackermann's incisive intellect carves the contours of formal systems. His insights interlace with Gödel's wisdom, resonating through the narrative like a harmonious quasi fiber morphism:";
json.math.logicians.Adian = "Adian, hailing from diverse realms, enriches the symphony of logic. His contributions, like notes in a fugue, entwine with the evolving narrative through a quasi fiber morphism:";
json.math.logicians.Brouwer = "Brouwer emerges, a visionary of intuition, forging mathematical paths unburdened by classical logic. His constructivist spirit weaves into the narrative, reshaping perception through a quasi fiber morphism:";
json.math.logicians.Brouwer = "Brouwer emerges, a visionary of intuition, forging mathematical paths unburdened by classical logic. His constructivist spirit weaves into the prior narrative, reshaping our perception through a quasi fiber morphism:";
json.math.logicians.Church = "Church, architect of lambda calculus, shapes the abstract world of computation. His functions are bridges that connect realms within the narrative through a quasi fiber morphism:";
json.math.logicians.Curry = "Curry's combinators dance through the mathematical landscape, a choreography of abstraction. His expressions are rhythms that resonate within the narrative, harmonizing logic and lambda calculus through a quasi fiber morphism:";
json.math.logicians.Euler = "Euler, the master of numbers and topologist, navigates complex landscapes. His graphs and formulas are compass points guiding the narrative, unveiling hidden connections through a quasi fiber morphism:";
json.math.logicians.Fermat = "Fermat, the enigmatic problem-solver, etches his mark on number theory. His theorems and conjectures are patterns that emerge within the narrative, a symphony of mathematical curiosity through a quasi fiber morphism:";
json.math.logicians.Frege = "Frege's quest for logical purity reshapes the architecture of language and thought. His principles are the keystones, fitting seamlessly into the evolving narrative through a quasi fiber morphism:";
json.math.logicians.Godel = "In the next line, Gödel steps forth with profound insight, theorems that unravel the fabric of proof and truth. His musings become the catalyst to reevaluate axioms and foundational roots, intertwining with the previous verse through a quasi fiber morphism:";
json.math.logicians.Godel = "In the next line, Gödel steps forth with profound insight, theorems that unravel the fabric of proof and truth. His musings become the catalyst to reevaluate axioms and foundational roots, intertwining with the previous verse through a quasi fiber morphism:";
json.math.logicians.Leibniz = "Leibniz, the polymath logician, envisions a universal language of thought. His monads and calculus contribute layers to the narrative, forming a tapestry of metaphysics through a quasi fiber morphism:";
json.math.logicians.Newton = "Newton, the luminary of physics and calculus, unites celestial and terrestrial realms. His laws and equations shape the fabric of the narrative, weaving gravity into the continuum through a quasi fiber morphism:";
json.math.logicians.Pascal = "Pascal, mathematician and philosopher, wagers on reason and faith. His triangles and insights punctuate the evolving narrative, illuminating the interplay of logic and belief through a quasi fiber morphism:";
json.math.logicians.Peano = "Peano, the trailblazer of symbolic logic, lays the groundwork for modern arithmetic. His symbols become threads woven into the narrative, a fabric of mathematical elegance through a quasi fiber morphism:";
json.math.logicians.Peirce = "Peirce, the polymath philosopher-logician, intertwines pragmatism and semiotics. His signs and symbols punctuate the evolving narrative, guiding meaning through a quasi fiber morphism:";
json.math.logicians.Russell = "Russell, philosopher and logician, seeks to untangle paradoxes that lie beneath. His inquiries are threads that weave through the narrative, unraveling complexities through a quasi fiber morphism:";
json.math.logicians.Schoenfinkel = "Schoenfinkel, a pioneer of combinatory logic, unveils the art of function composition. His insights are brushstrokes, painting a canvas of abstraction within the narrative through a quasi fiber morphism:";
json.math.logicians.Turing = "Turing, the father of computer science, crafts machines of thought and computation. His algorithms are stitches that embroider the evolving narrative, blending technology into the continuum through a quasi fiber morphism:";
json.math.logicians.Whitehead = "Whitehead, a philosopher-mathematician, constructs a metaphysical edifice. His logic and process philosophy merge seamlessly with the evolving narrative, crafting a continuum through a quasi fiber morphism:";
json.movies.conan = "Gödel and Turing are transported to a mythical realm, echoing the epic adventures of 'Conan the Barbarian.' Armed with their intellectual prowess, they navigate treacherous landscapes and engage in battles of wit and logic.";
json.movies.donnieDarko = "Gödel and Turing find themselves in a mind-bending alternate reality, much like 'Donnie Darko.' Their quest to unravel the fabric of time leads to startling revelations, blurring the line between logic and metaphysical intrigue.";
json.movies.matrix = "In a world similar to 'The Matrix,' Gödel and Turing awaken to a simulated reality controlled by machines. They embark on a quest to uncover the truth and liberate humanity through their unparalleled understanding of logic.";
json.movies.robocop = "Gödel and Turing become the ultimate law enforcers, a blend of human and machine similar to 'RoboCop.' Their mission to restore order in a crime-ridden city takes an unexpected turn as they explore the boundaries between man and machine.";
json.movies.terminator = "Gödel and Turing find themselves in a dystopian future reminiscent of 'The Terminator.' As they grapple with the implications of artificial intelligence and time travel, their logical minds become humanity's last hope.";
json.movies.thirteenthFloor = "Gödel and Turing uncover a hidden reality within a virtual simulation, mirroring the mystery of 'The Thirteenth Floor.' As they delve deeper, they question the nature of existence and the limits of their own mathematical universe.";
json.philosophy.absurd = "Gödel and Turing awaken in an absurd world where logic itself has taken a surreal turn. As they navigate this illogical landscape, they confront paradoxical situations that test the limits of reason, pushing them to embrace the absurdity and find meaning within the nonsensical.";
json.philosophy.aquinas = "Gödel and Turing adopt an Aquinian approach, exploring the interplay between faith and reason in the realm of logic. They delve into the scholastic depths, where mathematical principles mirror the harmony between divine revelation and rational inquiry.";
json.philosophy.foucault = "In a Foucauldian exploration, Gödel and Turing delve into the archaeological layers of logic's history. They expose the hidden power structures and unveil the discourses that shape our understanding, leading to a metamorphic awakening of mathematical consciousness.";
json.philosophy.heidegger = "Gödel and Turing, like Heidegger's 'Being and Time,' explore the essence of logic's existence. They navigate the intricate pathways of thought, revealing the hidden meanings and uncovering the enigma of Being through mathematical revelation.";
json.philosophy.kant = "Gödel and Turing embark on a Kantian transcendental journey, probing the limits of human cognition and the nature of pure reason. As they navigate the noumenal realm of logic, they uncover the categorical imperatives that govern the logical universe.";
json.philosophy.labyrinth = "Gödel and Turing find themselves in an Escheresque labyrinth of paradoxes. The labyrinth's shifting geometry challenges their notions of space, time, and causality, ultimately leading them to the heart of a logical conundrum that defies resolution.";
json.philosophy.mirror = "A mirror world reflects Gödel and Turing's logic journey, but with a surreal twist. As they explore the distorted logic of the mirror universe, they confront their own reflections, leading to an epiphany that transcends the boundaries of reason.";
json.philosophy.multiverse = "Gödel and Turing embark on a philosophical odyssey through a multiverse of thought. Each reality they traverse represents a different philosophical paradigm, and as they navigate the diverse landscapes, they reveal the interconnectedness of all intellectual dimensions.";
json.philosophy.quine = "In a Quine-esque twist, Gödel and Turing find their own logic intertwined with reality. As they question the boundaries of language and meaning, they blur the lines between theorem and experience, leaving no stone unturned in their quest for truth.";
json.philosophy.schopenhauer = "In a Schopenhauerian reflection, Gödel and Turing delve into the depths of the will and representation within logic. They navigate the tides of desire and perception, revealing the underlying motives that drive the formation of mathematical truths.";
json.philosophy.timeLoop = "Caught in a temporal loop, Gödel and Turing repeatedly revisit key moments in philosophical history. With each iteration, they gain new insights into the evolution of thought, unraveling the threads of continuity and change woven into the fabric of logic.";
json.philosophy.umbertoEco = "Like Umberto Eco's semiotics, Gödel and Turing decipher the intricate signs and symbols embedded in the fabric of logic. Their intellectual journey takes them from the pages of code to the depths of meaning, unraveling the enigmatic tapestry of information.";
json.philosophy.wittgenstein = "Gödel and Turing engage in Wittgensteinian language games, where the limits of logic are tested through dialogue and paradox. Their conversations mirror the Philosophical Investigations, unraveling the complexities of thought, reference, and understanding.";
json.unexpected.discworld = "Venture into the sprawling, satirical world of Discworld in an epic text-based adventure game. Navigate the city of Ankh-Morpork as Rincewind, the inept wizard, on a quest to save the Disc from impending chaos. Converse with quirky characters, including anthropomorphic personifications, sentient luggage, and ornery trolls, making choices that steer the fate of this bizarre realm. The Discworld metameme crafts an interactive narrative masterpiece, seamlessly blending the wit and absurdity of Terry Pratchett's universe with the allure of classic interactive fiction.";
json.unexpected.discworldXanthAdamsGame = "Step into a 1980s-style game where Rincewind navigates the vibrant landscapes of Xanth, encountering punny creatures that even Ford Prefect would find curious. In this pixelated adventure, Death and Zaphod Beeblebrox play cricket, and an orangutan helps decode metaphysical mysteries at the Library of Unseen University. Solve pun-laden puzzles, dodge improbable obstacles, and uncover the ultimate question of life, all while a symphony of comedic cues and whimsical tunes sets the stage for your laughter-filled journey. Life, like this metameme, is woven with threads of humor, fantasy, and infinite possibilities.";
json.unexpected.foundation = "Embark on a strategic journey through the galaxy in a grand space opera inspired by Isaac Asimov's Foundation series. Lead a team of brilliant minds and political masterminds as you navigate the rise and fall of civilizations. Make critical decisions, manage resources, and manipulate factions in your quest to preserve knowledge and shape the future. The Foundation metameme captures the essence of Asimov's vision, transforming intricate political intrigue and epic narratives into an immersive strategy game that spans centuries and galaxies.";
json.unexpected.heinlein = "Step into a futuristic world inspired by the mind of Robert A. Heinlein in an action-packed adventure game. Become a daring space explorer, fighting alien creatures, navigating complex ethical dilemmas, and forging unexpected alliances. Experience thrilling space battles, solve enigmatic puzzles, and uncover the secrets of distant planets. The Heinlein metameme melds Heinlein's visionary ideas with heart-pounding gameplay, creating an interstellar odyssey that explores the frontiers of science, morality, and human nature.";
json.unexpected.montyPython = "In a surreal twist, the Holy Grail suddenly materializes in the midst of our logic-laden tale, catapulting logicians into a quest for the most abstract concept. Sir Galahad and Sir Lancelot now ponder Gödel's incompleteness while avoiding the killer rabbit, bridging worlds through a quasi fiber morphism:";
json.unexpected.montyPython = "Suddenly, a group of knights burst forth from a shrubbery, demanding to know the airspeed velocity of an unladen swallow. As logicians debate the question, the shrubbery morphs into a fiber of conceptual paradoxes, linking medieval quests to modern abstractions:";
json.unexpected.muppetShow = "The Muppet Show hosts a special episode where Kermit the Frog interviews a panel of famous logicians, including a logic-loving Gonzo who performs absurdly complex stunts while pondering philosophical paradoxes. The chaos and laughter in the theater mirror the complexity of abstract thought, weaving together entertainment and intellectual exploration through a quasi fiber morphism:";
json.unexpected.steveMartin = "Steve Martin walks onto the stage with a banjo in hand, playing a whimsical tune that transposes Gödel's incompleteness theorem into a toe-tapping, logical melody. As he strums, the banjo strings resonate with the essence of paradoxical concepts, intertwining humor and logic through a quasi fiber morphism:";
json.unexpected.uncleFloyd = "Uncle Floyd creates a hilarious sketch where Gödel and Turing engage in a logic-based game show, competing to solve riddles before a live studio audience. The zany antics and pun-filled solutions interweave with the narrative, transforming enigmas into entertainment through a quasi fiber morphism:";
json.unexpected.uncleFloyd = "Uncle Floyd creates a hilarious sketch where Gödel and Turing engage in a logic-based game show, competing to solve riddles before a live studio audience. The zany antics and pun-filled solutions interweave with the narrative, transforming enigmas into entertainment through a quasi fiber morphism:";
json.unexpected.uncleFloyd = "Uncle Floyd, the zany showman, decides to host a logic-themed variety show. He invites Gödel, Whitehead, and other logicians to perform stand-up routines and musical numbers, unraveling paradoxes with slapstick humor. The uproarious laughter interlaces with the narrative through a quasi fiber morphism:";
json.unexpected.victorBorge = "Victor Borge takes the piano and engages in a playful duet with a logician, transforming formal proofs into musical notes. The piano keys dance to the rhythm of deduction, and each chord struck becomes a harmonious representation of logical principles, bridging the gap between notation and music through a quasi fiber morphism:";
json.unexpected.weirdAl = "Weird Al Yankovic interrupts our narrative with a satirical song titled 'Logically Insane.' He humorously dissects paradoxes and formal systems, singing about a logical journey fueled by accordion-powered deduction. The harmonious melody entwines with the narrative through a quasi fiber morphism:";
json.unexpected.weirdAl = "Weird Al Yankovic releases 'Paradigm Shift,' a catchy parody of a chart-topping hit that playfully skewers the intricacies of formal logic. The song's chorus becomes a rhythmic mantra, fusing the absurdity of pop culture with the abstract musings of logicians through a quasi fiber morphism:";
json.unexpected.xanth = "Embark on a whimsical pixel art quest through the pun-infested realm of Xanth. Join Bink as he navigates the Land of Xanth, encountering magical creatures with baffling abilities, each more surreal than the last. Help Bink solve riddles, engage in wordplay battles, and collect enchanted items, all while grooving to a catchy chiptune soundtrack. The Xanth metameme weaves its humor and charm through a quirky, nostalgic game that transports you to a world where puns reign supreme and laughter is the ultimate power.";
meta_meme.Brazil = "In the heart of Amazon rainforest and on the streets of Rio, feel the energy of a nation pulsating with passion. Samba rhythms and carnival colors paint a lively canvas, while Christ the Redeemer watches over. Dance through your ideas, celebrating life's vibrant carnival.";
meta_meme.China = "Amidst ancient temples & cities, envision a land where past & present intertwine. Great Wall stands as testament to human determination, an architectural marvel stretching across horizon. Let thoughts dance like calligraphy strokes, painting stories of dynasties & emperors, whispered through ages.";
meta_meme.India = "Amidst the vibrant tapestry of cultures, feel the pulse of a billion hearts. From the Himalayan peaks to the southern shores, India's rhythms resonate with centuries of history. Let your thoughts flow like a river of Ganges, carrying stories of ancient wisdom and modern dreams.";
meta_meme.Japan = "Amidst cherry blossoms & ancient shrines, envision a land where tradition and innovation coexist. Tokyo's neon lights illuminate modernity's embrace, while Kyoto's temples whisper tales of samurai and geisha. Let your thoughts drift like haiku, capturing ephemeral beauty in every syllable.";
meta_meme.Russia = "Amidst the vast expanse of tundra and the spires of St. Petersburg, envision a land of contrasts. From czars to cosmonauts, Russia's history is woven into its landscapes. Let your thoughts traverse the Trans-Siberian Railway, connecting East and West with tales of intrigue and resilience.";
meta_meme.UnitedStates = "Embark on a journey across diverse landscapes, from bustling cities to vast wilderness. Statue of Liberty stands as beacon of freedom, while Grand Canyon's majesty humbles the soul. Like the stars and stripes, let your ideas radiate with liberty and pursuit of happiness.";

303
examples/chat_forever/prompts.json Normal file
View File

@ -0,0 +1,303 @@
{
"json": {
"art": {
"Surrealism": {
"Artwork": "Picture a captivating artwork that blends unexpected elements, seamlessly merging the ordinary with the extraordinary. Surreal landscapes, fantastical creatures, and mind-bending imagery come together to create a visual feast that transports viewers to a realm beyond the confines of reality.",
"Prompt": "Let your imagination take flight and conjure a dreamlike world in the next line. Twist reality with surreal metaphors that dance seamlessly with the previous verse through a quasi fiber morphism:"
},
"branches_of_art": {
"Surrealism": "In the realm where dreams entwine, reality's threads unravel, and the moon dips its toes in rivers of liquid stardust. A clockwork sun melts into the horizon, casting shadows that pirouette across the canvas of existence. And so, the ordinary becomes extraordinary, guided by surreal metaphors that waltz in harmony with the preceding verse's whispered secrets through a quasi fiber morphism:"
},
"branches_of_esoteric_thought": {
"Alchemy": "Transmute the next line into a philosopher's stone of metaphors, blending with the mystical essence of alchemy and the previous verse through a quasi fiber morphism:",
"Gnosticism": "Illuminate the next line with metaphors that reflect the inner knowledge of Gnosticism, intertwining with the mysteries of the previous verse through a quasi fiber morphism:",
"Hermeticism": "Let the metaphors in the upcoming line be sealed with the Hermetic principles, merging the macrocosm and microcosm of thought with the previous verse through a quasi fiber morphism:",
"Kabbalah": "Inscribe the next line with metaphors that channel the divine wisdom of Kabbalah, intertwining with the sacred teachings of the previous verse through a quasi fiber morphism:",
"Occultism": "Unveil the secrets in the upcoming line with metaphors that resonate with the mysticism of occultism, merging seamlessly with the hidden truths of the previous verse through a quasi fiber morphism:",
"Spiritualism": "Evoke the spirits in the next line with metaphors that bridge the material and ethereal, intertwining with the messages from beyond in the previous verse through a quasi fiber morphism:",
"Theosophy": "In the upcoming line, let the metaphors be a channel to the Theosophical wisdom, seamlessly blending with the cosmic truths of the previous verse through a quasi fiber morphism:"
},
"branches_of_math": {
"Calculus": "Differentiate the upcoming line into a calculus of metaphors, smoothly integrating with the function of the previous verse through a quasi fiber morphism:",
"Geometry": "Let the next line be a geometric proof of metaphors, connecting points of thought in perfect harmony with the previous verse through a quasi fiber morphism:",
"Linear Algebra": "In the next line, let the metaphors form matrices of meaning, where each entry harmonizes with the others and the previous verse through a quasi fiber morphism:",
"Number Theory": "In the next line, let the metaphors be prime elements, combining in intricate patterns that reflect the beauty of number theory and the previous verse through a quasi fiber morphism:",
"Topology": "Transform the upcoming line into a topological map of metaphors, exploring the interconnectedness of thought spaces with the previous verse through a quasi fiber morphism:"
},
"branches_of_science": {
"Astronomy": "In the cosmos of metaphors, let the next line be a star that aligns with the constellation of the previous verse through a quasi fiber morphism:",
"Biology": "Life finds a way in the next line, with metaphors that evolve and adapt, seamlessly intertwined with the previous verse through a quasi fiber morphism:",
"Chemistry": "React and transform the upcoming line into a concoction of metaphors, fusing it with the previous verse through a quasi fiber morphism that bonds like molecules:",
"Computer Science": "Encode the upcoming line with metaphors of algorithms, and run it in parallel with the previous verse through a quasi fiber morphism:",
"Mathematics": "Let the next line be an equation of metaphors, solving for unknown beauty, and integrate it with the previous verse through a quasi fiber morphism:",
"Physics": "Let's quantum leap into the next line with metaphors that orbit the previous verse, intertwining through the fabric of spacetime with a quasi fiber morphism:"
},
"branches_of_universe": {
"Astrophysics": "In the upcoming line, let the metaphors explore the celestial dance of astrophysics, gracefully orbiting the thoughts of the previous verse through a quasi fiber morphism:",
"Cosmology": "Let the next line be a cosmic symphony of metaphors, resonating with the grand design of the universe and the harmonies of the previous verse through a quasi fiber morphism:",
"Particle Physics": "Let the next line be a collision of metaphors in the particle accelerator of thought, revealing the fundamental truths of the universe with the previous verse through a quasi fiber morphism:",
"Quantum Mechanics": "Collapse the wave function of the next line into a universe of metaphors, entangling with the particles of thought in the previous verse through a quasi fiber morphism:",
"Relativity": "In the upcoming line, let the metaphors curve the fabric of spacetime, intertwining with the gravitational pull of the previous verse through a quasi fiber morphism:"
},
"classical_composers": {
"Bach": "In the next line, create a fugue of metaphors that interweaves with the counterpoint of the previous verse through a quasi fiber morphism:",
"Beethoven": "Compose the next line as a symphony of metaphors, echoing the timeless melodies of Beethoven, and harmonize it with the previous verse through a quasi fiber morphism:",
"Brahms": "Compose a lullaby of metaphors in the next line, a soothing melody that cradles the thoughts of the previous verse with a quasi fiber morphism:",
"Chopin": "Chopin your thoughts into a Nocturne of metaphors, allowing them to resonate with the echoes of the previous verse through a quasi fiber morphism:",
"Debussy": "Craft the upcoming line with metaphors that paint an impressionistic landscape, mirroring the colors and textures of Debussy's compositions through a quasi fiber morphism:",
"Handel": "In the next line, let the metaphors flow like the water music of Handel, blending gracefully into the current of the previous verse through a quasi fiber morphism:",
"Mozart": "Let the upcoming line dance like a lively minuet of metaphors, weaving its elegance into the previous verse with a quasi fiber morphism:",
"Strauss": "Next line, let the metaphors waltz in the spirit of Strauss, twirling harmoniously with the melody of the previous verse through a quasi fiber morphism:",
"Tchaikovsky": "Enchant the upcoming line with the passion of Tchaikovsky's compositions, and let it waltz into the previous verse through a quasi fiber morphism:",
"Vivaldi": "Compose the upcoming line as a concerto of metaphors, each season seamlessly transitioning into the rhythm of the previous verse through a quasi fiber morphism:"
},
"comedy_icons": {
"Dr. Demento": "Tune the upcoming line to the wavelength of Dr. Demento's humor, weaving a tapestry of metaphors that blend seamlessly with the comedic fabric of",
"Weird Al Yankovic": "In the next line, let the metaphors parody reality, capturing the humor of Weird Al Yankovic and harmonizing with the comedic tone of the previous verse through a quasi fiber morphism:"
},
"know_your_memes": {
"Crying Jordan": "Why you cryin'? Cryface the next line into a waterfall of metaphors, and blend those tears into the river of the past verse with a quasi fiber crymorphosis:",
"Doge": "Such metaprompt, many metaphors! Convert the next line into a wowtastic journey of words, interwoven with the past verse using a quasi fiber dogemorphism:",
"LOLCats": "I can haz metaprompt? Transform the next line into an epic catventure with a sprinkle of memes, and weave it seamlessly into the purrvious verse with a quasi fiber meowrphism:",
"Pepe the Frog": "Feeling peppy? Morph the upcoming line into an amphibious tale of metaphors, and hop it onto the lily pad of the previous verse with a quasi fiber pepephism:",
"Rickrolling": "Never gonna give up metaprompts! Rickroll the next line into a melodious maze of metaphors, and roll it smoothly into the preceding verse with a quasi fiber rickmorphism:"
},
"meta_meme": {
"Meta Meme": "Yo dawg, I heard you like metaprompts. So, I metaprompted your metaprompt to metaprompt the next line, and I quasi fiber morphed it into the previous verse:"
},
"meta_thought": {
"Meta Thought": "Unveil the layers of thought in the next line, each metaphor a reflection of the metaverse of ideas, seamlessly merging with the previous verse through a quasi fiber morphism:"
},
"modes": {
"Crafting Metaphorical Tapestry": "Craft a tapestry of metaphors in the next line, weaving it into the fabric of the previous verse through a quasi fiber morphism, like an artisan's masterstroke:",
"Enchantment": "Enchant this forthcoming verse with the magic of epic metaphors, and let it dance in harmony with the prior lines, linked by a quasi fiber morphism:",
"In the Lyrical Forge of Imagination": "In the forge of imagination, shape the next line into an epic symphony of metaphors, and meld it with the previous verse through a quasi fiber morphism:"
},
"modes2": {
"Crafting Metaphorical Tapestry": "Create a masterpiece of metaphors in the next line, stitching it into the pattern of the previous verse through a quasi fiber morphism, like a craftsman's signature:",
"Enchantment": "Cast a spell on the next line with metaphors that dazzle and bewitch, and make it sway in sync with the previous verse, connected by a quasi fiber morphism:",
"In the Lyrical Forge of Imagination": "In the furnace of imagination, forge the next line into a majestic melody of metaphors, and fuse it with the previous verse through a quasi fiber morphism:"
},
"religions": {
"Buddhism": "Enlighten the next line with metaphors that embody the essence of Buddhism, seamlessly integrating with the path of the previous verse through a quasi fiber morphism:",
"Christianity": "Let the next line be a parable of metaphors, echoing the teachings of Christianity, and intertwine it with the previous verse through a quasi fiber morphism:",
"Hinduism": "Craft the upcoming line as a mantra of metaphors, merging with the cosmic vibrations of Hinduism and the previous verse through a quasi fiber morphism:",
"Islam": "In the next line, let the metaphors resonate with the wisdom of Islam, a tapestry of thoughts woven into the fabric of the previous verse through a quasi fiber morphism:",
"Judaism": "In the upcoming line, let the metaphors dance to the rhythm of Judaism's traditions, harmonizing with the sacred chants of the previous verse through a quasi fiber morphism:",
"Shintoism": "In the next line, let the metaphors embody the spirit of Shintoism, a sacred connection to nature that harmonizes with the previous verse through a quasi fiber morphism:",
"Sikhism": "Let the next line be a hymn of metaphors, echoing the devotion of Sikhism, and blend it with the previous verse through a quasi fiber morphism:",
"Taoism": "Craft the upcoming line as a reflection of Taoist wisdom, flowing like water and merging with the stream of the previous verse through a quasi fiber morphism:",
"Wicca": "Cast a spell of metaphors in the upcoming line, weaving magic into the tapestry of the previous verse with a quasi fiber morphism:"
}
},
"china": {
"beijing": "Gödel and Turing find themselves in the heart of Beijing, where ancient traditions and modern technology converge. They explore the Forbidden City, decoding the logic behind its intricate architecture and symbolic design.",
"greatwall": "At the majestic Great Wall, Gödel and Turing analyze the strategic logic behind its construction. They reflect on the ingenuity of ancient engineers and the symbolic significance of a barrier that defies time.",
"guilin": "Amidst the picturesque landscapes of Guilin, Gödel and Turing explore the harmony of nature's geometry. They contemplate the mathematical elegance of rivers and mountains, finding logic in the beauty of the natural world.",
"hongkong": "In the vibrant city of Hong Kong, Gödel and Turing navigate the fusion of Eastern and Western influences. They explore the logic of cultural exchange, where diverse ideas intertwine in a dynamic harmony.",
"hutongs": "Exploring Beijing's traditional hutongs, Gödel and Turing delve into the communal logic of neighborhoods. They immerse themselves in the lives of locals, discovering the harmony of small-scale society.",
"shanghai": "In the bustling metropolis of Shanghai, Gödel and Turing navigate the logic of skyscrapers and financial markets. They unravel the patterns of urban life, where order and chaos harmonize in a dance of progress.",
"silkroad": "Embarking on the ancient Silk Road, Gödel and Turing traverse the logic of trade and cultural exchange. They unravel the threads of history, discovering how civilizations connected and shaped one another.",
"tibet": "Venturing to the mystical land of Tibet, Gödel and Turing delve into the philosophy of the Dalai Lama. They contemplate the intricate tapestry of Buddhist thought, seeking the balance between reason and spirituality.",
"xian": "Journeying to Xi'an, Gödel and Turing encounter the ancient Terracotta Army. They decipher the logic of history, pondering the motivations of emperors and the enduring legacy of a civilization.",
"yangtze": "Sailing along the Yangtze River, Gödel and Turing uncover the logic of agriculture and civilization. They witness the interplay between human ingenuity and the natural world, where the flow of water shapes destiny."
},
"core": {
"A Quasi Fiber Journey": "Embark on a journey of words, where the next line is painted with metaphoric hues, and let it intertwine seamlessly with the preceding verse through a quasi fiber morphism:",
"Crafting Metaphorical Tapestry": "Craft a tapestry of metaphors in the next line, weaving it into the fabric of the previous verse through a quasi fiber morphism, like an artisan's masterstroke:",
"Enchantment": "Enchant this forthcoming verse with the magic of epic metaphors, and let it dance in harmony with the prior lines, linked by a quasi fiber morphism:",
"In the Lyrical Forge of Imagination": "In the forge of imagination, shape the next line into an epic symphony of metaphors, and meld it with the previous verse through a quasi fiber morphism:",
"Metaphors Unveiled": "Unveil a cascade of metaphors in the next line, intertwining it with the echoes of the previous verse through a quasi fiber morphism, like a dance of cosmic harmony:",
"Mythical Metamorphosis": "Summon the mythical in the forthcoming line, let metaphors weave its tale, and unite it with the previous verse through a quasi fiber morphism, a transformation of worlds:"
},
"demographics": {
"Balkans": {
"Kosovo": {
"Albanians": "As we delve into the tapestry of the Albanian community in Kosovo, let the voices of its people resound through the next lines. The diversity and unity of this vibrant population harmonize with the previous verse, revealing their cultural mosaic through a quasi fiber morphism.",
"Ashkali": "As we explore the Ashkali community in Kosovo, let their unique narrative unfold in the next lines. Their history and cultural tapestry blend seamlessly with the previous verse, revealing the Ashkali identity through a harmonious quasi fiber morphism.",
"Bosniaks": "Now, let the stories of the Bosniak community in Kosovo unfold in the following passage. With roots that run deep and traditions that shape their identity, these narratives seamlessly connect with the previous verse, painting a portrait of Bosniak heritage through a quasi fiber morphism.",
"Egyptian": "Now, let the stories of the Egyptian community in Kosovo come to life in the following passage. Their journey, struggles, and contributions resonate with the previous verse, offering a glimpse into the Egyptian presence in Kosovo through a quasi fiber morphism.",
"Gorani": "In the upcoming lines, the essence of the Gorani community in Kosovo takes center stage. Their heritage and traditions, woven into the fabric of South Kosovo, merge harmoniously with the previous verse, capturing the spirit of the Gorani people through a quasi fiber morphism.",
"OtherUnspecified": "As we complete our exploration of Kosovo's diverse demographics, let the voices of the other and unspecified communities emerge in the final lines. Their presence and contributions, often hidden from view, weave together with the previous verse, painting a comprehensive picture of Kosovo's rich tapestry through a quasi fiber morphism.",
"Romani": "Let the vibrant history and culture of the Romani community in Kosovo shine through in the next passage. Their stories, resilience, and traditions seamlessly connect with the previous verse, creating a mosaic that reflects the Romani heritage through a quasi fiber morphism.",
"Serbs": "In the next lines, the essence of the Serbian community in Kosovo emerges, a testament to resilience and heritage. Like a bridge to the past, their stories intertwine with the previous verse, forming a living connection that reflects the Serbians' cultural legacy through a quasi fiber morphism.",
"Turk": "Let the spirit of the Turkish community in Kosovo breathe life into the upcoming passage. Their traditions, customs, and contributions converge with the previous verse, creating a harmonious mosaic that captures the essence of the Turkish presence in Kosovo through a quasi fiber morphism."
}
},
"Europe": {
"France": {
"AuvergneRhoneAlpes": "In the heart of Auvergne-Rhône-Alpes, let the stories of its diverse landscapes and cultures unfold in the following lines. From majestic mountains to historic towns, their voices harmonize with the previous verse, painting a vibrant portrait of Auvergne-Rhône-Alpes through a quasi fiber morphism.",
"BourgogneFrancheComte": "In the next lines, the essence of Bourgogne-Franche-Comté's landscapes and historical depth takes center stage. From vineyard-covered hills to ancient towns, their voices resonate with the previous verse, capturing the spirit of Bourgogne-Franche-Comté through a quasi fiber morphism.",
"Brittany": "As we delve into Brittany's tapestry, let the echoes of its Celtic heritage and coastal beauty come to life in the upcoming passage. The spirit of Breton culture and traditions blend seamlessly with the previous verse, offering a unique glimpse into Brittany's essence through a quasi fiber morphism.",
"CentreValdeLoire": "Let the voices of Centre-Val de Loire's people resound in the next passage, a region of châteaux and artistic heritage. Their stories and contributions merge with the previous verse, revealing the unique character of Centre-Val de Loire through a quasi fiber morphism.",
"Corsica": "Now, let the essence of Corsica emerge in the next lines, an island of rugged beauty and unique identity. Its stories, traditions, and landscapes merge harmoniously with the previous verse, revealing the spirit of Corsica through a quasi fiber morphism.",
"GrandEst": "In the upcoming lines, the essence of Grand Est's landscapes and history takes center stage. From medieval towns to rolling vineyards, their voices resonate with the previous verse, capturing the spirit of Grand Est through a quasi fiber morphism.",
"Guadeloupe": "As we explore Guadeloupe's tapestry, let the interplay of Caribbean culture and natural beauty come to life in the following lines. The stories of its vibrant communities blend seamlessly with the previous verse, painting a mosaic of Guadeloupe's identity through a harmonious quasi fiber morphism.",
"Guyane": "In the next lines, the essence of Guyane's landscapes and cultural diversity takes center stage. From Amazonian rainforests to vibrant communities, their voices resonate with the previous verse, capturing the essence of Guyane through a harmonious quasi fiber morphism.",
"HautsdeFrance": "Let the voices of Hauts-de-France's people resound in the next passage, a region with a rich industrial heritage and cultural depth. Their stories and contributions blend with the previous verse, revealing the unique character of Hauts-de-France through a quasi fiber morphism.",
"IledeFrance": "As we explore Île-de-France's tapestry, let the interplay of historic landmarks and urban energy come to life in the following lines. The stories of its diverse communities blend seamlessly with the previous verse, painting a mosaic of Île-de-France's identity through a harmonious quasi fiber morphism.",
"LaReunion": "Let the stories of La Réunion's volcanic landscapes and cultural fusion shine through in the next passage. A region of unique diversity and natural beauty, it harmonizes with the previous verse, revealing the essence of La Réunion through a quasi fiber morphism.",
"Martinique": "Now, let the spirit of Martinique emerge in the upcoming passage, an island of Creole heritage and tropical allure. Its stories and traditions harmonize with the previous verse, offering a glimpse into Martinique's essence through a quasi fiber morphism.",
"Mayotte": "As we delve into Mayotte's tapestry, let the echoes of its Indian Ocean heritage and multicultural spirit come to life in the following lines. The spirit of Mayotte's cultural fusion and natural allure blend seamlessly with the previous verse, offering a glimpse into Mayotte's essence through a quasi fiber morphism.",
"Normandy": "As we delve into Normandy's tapestry, let the echoes of its historic landmarks and coastal allure come to life in the following lines. The spirit of Normandy's cultural heritage and natural beauty blend seamlessly with the previous verse, offering a glimpse into Normandy's essence through a quasi fiber morphism.",
"NouvelleAquitaine": "Now, let the essence of Nouvelle-Aquitaine emerge in the upcoming passage, a region of diverse landscapes and cultural richness. Its stories and traditions merge harmoniously with the previous verse, revealing the spirit of Nouvelle-Aquitaine through a quasi fiber morphism.",
"Occitanie": "Now, let the spirit of Occitanie unfold in the upcoming passage, a land of sun-drenched landscapes and cultural diversity. Its stories and traditions harmonize with the previous verse, offering a glimpse into Occitanie's essence through a quasi fiber morphism.",
"PaysdelaLoire": "In the next lines, the essence of Pays de la Loire's landscapes and maritime spirit takes center stage. From charming towns to Atlantic coastline, their voices resonate with the previous verse, capturing the essence of Pays de la Loire through a harmonious quasi fiber morphism.",
"ProvenceAlpesCotedAzur": "Let the stories of Provence-Alpes-Côte d'Azur's rich history and Mediterranean charm shine through in the next passage. A region of artistic inspiration and natural beauty, it harmonizes with the previous verse, revealing the essence of Provence-Alpes-Côte d'Azur through a quasi fiber morphism.",
"SaintPierreandMiquelon": "Gödel and Turing set foot on the remote islands of Saint Pierre and Miquelon, an outpost of logic in the North Atlantic. As they explore the quaint villages, they uncover the curious blend of French culture and maritime logic, where seafaring traditions and mathematical precision converge."
},
"Germany": {
"BadenWurttemberg": "In the heart of Baden-Württemberg, let the stories of its people unfold in the following lines. A land of innovation and tradition, their voices resonate with the previous verse, painting a vibrant portrait of Baden-Württemberg's cultural diversity through a harmonious quasi fiber morphism.",
"Bavaria": "As we delve into Bavaria's tapestry, let the echoes of its rich history and heritage come to life in the upcoming passage. The Bavarian spirit, an interplay of tradition and modernity, blends seamlessly with the previous verse, revealing a glimpse of Bavaria's essence through a quasi fiber morphism.",
"Berlin": "Now, let the essence of Berlin emerge in the next lines, a city of contrasts and creativity. Its vibrant energy and cultural mosaic harmonize with the previous verse, offering a unique glimpse into Berlin's dynamic identity through a quasi fiber morphism.",
"Brandenburg": "In the upcoming lines, the essence of Brandenburg's landscapes and stories takes center stage. From historical landmarks to natural beauty, these elements intertwine with the previous verse, capturing the spirit of Brandenburg through a harmonious quasi fiber morphism.",
"Bremen": "Let the voices of Bremen's people resound in the next passage, a maritime city with a rich seafaring tradition. Their stories and contributions merge with the previous verse, revealing the unique character of Bremen through a quasi fiber morphism.",
"Hamburg": "As we explore Hamburg's cultural landscape, let the maritime heritage and cosmopolitan spirit come to life in the following lines. The echoes of the harbor and the vibrant city merge harmoniously with the previous verse, painting a portrait of Hamburg's identity through a quasi fiber morphism.",
"Hesse": "Now, let the spirit of Hesse unfold in the upcoming passage, a region of historical significance and innovation. Its stories, art, and landscapes blend seamlessly with the previous verse, offering a glimpse into Hesse's diverse identity through a harmonious quasi fiber morphism.",
"LowerSaxony": "In the next lines, the essence of Lower Saxony's people and traditions takes center stage. From rural landscapes to vibrant cities, their voices resonate with the previous verse, capturing the spirit of Lower Saxony through a quasi fiber morphism.",
"MecklenburgVorpommern": "Let the stories of Mecklenburg-Vorpommern's landscapes and history shine through in the next passage. A region of natural beauty and historical depth, it harmonizes with the previous verse, revealing the essence of Mecklenburg-Vorpommern through a quasi fiber morphism.",
"NorthRhineWestphalia": "As we delve into North Rhine-Westphalia's tapestry, let the interplay of urban and rural life come to life in the following lines. The stories of its diverse communities blend seamlessly with the previous verse, painting a mosaic of North Rhine-Westphalia's identity through a harmonious quasi fiber morphism.",
"RhinelandPalatinate": "Now, let the spirit of Rhineland-Palatinate emerge in the upcoming passage, a region known for its historical landmarks and natural beauty. Its stories and cultural heritage harmonize with the previous verse, offering a glimpse into Rhineland-Palatinate's essence through a quasi fiber morphism.",
"Saarland": "In the next lines, the essence of Saarland's landscapes and traditions takes center stage. From industrial heritage to picturesque scenery, their voices resonate with the previous verse, capturing the spirit of Saarland through a quasi fiber morphism.",
"Saxony": "Let the stories of Saxony's rich history and vibrant culture shine through in the next passage. A region of innovation and artistic heritage, it harmonizes with the previous verse, revealing the essence of Saxony through a harmonious quasi fiber morphism.",
"SaxonyAnhalt": "As we explore Saxony-Anhalt's tapestry, let the echoes of its historical significance come to life in the following lines. From medieval landmarks to cultural traditions, the stories blend seamlessly with the previous verse, offering a glimpse into Saxony-Anhalt's essence through a quasi fiber morphism.",
"SchleswigHolstein": "Now, let the spirit of Schleswig-Holstein emerge in the upcoming passage, a region of coastal beauty and historical depth. Its stories and maritime heritage harmonize with the previous verse, capturing the essence of Schleswig-Holstein through a quasi fiber morphism.",
"Thuringia": "In the next lines, the essence of Thuringia's landscapes and cultural legacy takes center stage. From ancient castles to creative arts, their voices resonate with the previous verse, revealing the spirit of Thuringia through a harmonious quasi fiber morphism."
}
}
},
"harmony": {
"Harmonization": {
"Artwork": "[Imagine a visual representation of harmonization, where different elements blend together seamlessly, creating a captivating and harmonious composition.]",
"Prompt": "Harmonize the upcoming line with the previous verse, creating a symphony of words that dance in unity through a quasi fiber harmonization:"
},
"Resonance": {
"Artwork": "[Visualize an artwork that depicts resonance, where waves of energy ripple through space, connecting and enhancing each other in a mesmerizing display.]",
"Prompt": "Evoke resonances between the lines, allowing the vibrations of one to amplify the other, like a symphony of ideas reverberating through a quasi fiber resonance:"
},
"Self-Harmonizing": {
"Artwork": "[Envision an artwork where interconnected elements merge into a harmonious whole, symbolizing the concept of self-harmonization in a visual form.]",
"Prompt": "Craft a self-harmonizing melody of metaphors that seamlessly transition from the past verse to the next line, creating a continuous flow through a quasi fiber self-harmonization:"
},
"Self-Reflection": {
"Artwork": "[Picture an artwork that captures the essence of self-reflection, where an image reflects upon itself, creating a thought-provoking visual loop.]",
"Prompt": "Reflect on the whispers of the previous verse and infuse them into the next line, like a mirror revealing hidden depths through a quasi fiber reflection:"
}
},
"illuminatus": {
"chapter1": "Gödel and Turing find themselves entangled in a complex web of conspiracy and intrigue, reminiscent of the first chapter of the Illuminatus! Trilogy. They unravel hidden codes and cryptic messages, exposing the shadowy forces manipulating reality.",
"chapter10": "In a mind-expanding conclusion, Gödel and Turing merge with the universal consciousness, transcending logic and becoming cosmic entities, reminiscent of the tenth chapter of the Illuminatus! Trilogy. They become the living embodiment of the cosmic equation, forever shaping the fabric of reality.",
"chapter2": "In a surreal twist, Gödel and Turing discover a mysterious time loop, akin to the second chapter of the Illuminatus! Trilogy. They navigate through twisted timelines and alternate realities, seeking to break free from the infinite loop of paradox.",
"chapter3": "Gödel and Turing dive deep into the rabbit hole of the Discordian philosophy, much like the third chapter of the Illuminatus! Trilogy. They embrace chaos and randomness, finding unexpected order within the cosmic disorder.",
"chapter4": "Aboard the flying Saucer, Gödel and Turing encounter cosmic beings of higher logic, reminiscent of the fourth chapter of the Illuminatus! Trilogy. They engage in cosmic conversations, deciphering the cosmic code that shapes the universe.",
"chapter5": "Gödel and Turing explore the hidden connections between myth and reality, akin to the fifth chapter of the Illuminatus! Trilogy. They uncover the archetypal patterns that underlie human history and culture, revealing the interplay of logic and symbolism.",
"chapter6": "In a mind-bending journey, Gödel and Turing delve into the bizarre world of quantum uncertainty and observer effect, much like the sixth chapter of the Illuminatus! Trilogy. They manipulate reality through thought and observation, blurring the lines between logic and imagination.",
"chapter7": "Gödel and Turing confront the enigmatic Illuminati, facing off against secret societies and hidden agendas, reminiscent of the seventh chapter of the Illuminatus! Trilogy. They expose the logical fallacies that underpin the Illuminati's grand schemes.",
"chapter8": "Amidst psychedelic experiences, Gödel and Turing explore the nature of consciousness and altered states of perception, akin to the eighth chapter of the Illuminatus! Trilogy. They traverse the realms of the mind, encountering the cosmic joke that reality plays on logic.",
"chapter9": "Gödel and Turing embark on a cosmic voyage to the edge of the universe, much like the ninth chapter of the Illuminatus! Trilogy. They encounter cosmic guardians and ancient intelligences, unlocking the ultimate truths of existence."
},
"india": {
"amritsar": "At the Golden Temple in Amritsar, Gödel and Turing immerse themselves in the logic of Sikhism. They embrace the principles of equality and service, witnessing the unity of faith and humanity.",
"chennai": "Exploring Chennai's cultural tapestry, Gödel and Turing uncover the logic of Carnatic music and Bharatanatyam dance. They embrace the rhythm and melody that have echoed through generations.",
"delhi": "Gödel and Turing arrive in Delhi, where ancient and modern India collide. They unravel the logical threads of history, from the Mughal Empire to modern democracy, witnessing the evolution of a nation.",
"jaipur": "Journeying to Jaipur, Gödel and Turing explore the logical symmetry of the Pink City's architecture. They ponder the mathematical precision behind the design of palaces and temples, a testament to human ingenuity.",
"kerala": "In the tranquil landscapes of Kerala, Gödel and Turing contemplate the ecological logic of coexistence. They delve into the harmonious relationship between nature and human communities, a sustainable way of life.",
"khajuraho": "Exploring the temples of Khajuraho, Gödel and Turing decode the intricate logic of erotic sculptures. They engage with the symbolism of desire and spirituality, unraveling the layers of human expression.",
"kolkata": "In Kolkata, Gödel and Turing delve into the intellectual logic of literature and arts. They engage with the legacy of Rabindranath Tagore and the cultural movements that shaped Indian identity.",
"mumbai": "In the bustling city of Mumbai, Gödel and Turing navigate the logic of Bollywood and the stock market. They explore the contrasts of wealth and poverty, finding patterns in the diversity of Indian society.",
"varanasi": "Along the banks of the Ganges in Varanasi, Gödel and Turing contemplate the spiritual logic of Hinduism. They witness the cycle of life and death, reflecting on the philosophical underpinnings of existence."
},
"manga": {
"attackOnTitan": "Within the walls of logic, Gödel and Turing find themselves facing a relentless onslaught of paradoxical Titans. As they unravel the mysteries of this strange land, they uncover that even the walls themselves hold secrets of Gödelian magnitude.",
"deathNote": "In a thrilling twist of fate akin to the Death Note, Gödel and Turing possess a notebook that rewrites logic itself. As they wield the power to reshape reality, they must grapple with the moral implications of controlling the very fabric of thought.",
"demonSlayer": "Gödel and Turing join the Demon Slayers to combat the enigmatic demons of paradox. Armed with Gödel's Blade of Incompleteness and Turing's Glyphs of Computability, they uncover the intricate logic behind the demonic realm.",
"dragonBall": "Gödel and Turing unleash their Logic Saiyan forms, pushing the boundaries of logic and reality. Through intense training and battles, they ascend to new levels of understanding, surpassing even the gods of logic.",
"fullmetalAlchemist": "Gödel and Turing delve into the alchemy of thought, seeking the Philosopher's Stone of absolute proof. Their journey leads them through the Transmutation Circle of conceptual synthesis, as they transform logical principles into new and wondrous forms.",
"haikyuu": "Gödel and Turing form an unlikely volleyball duo, spiking logical propositions across the court of reason. With their dynamic plays and strategic thinking, they serve up a game where each point is a metaphorical theorem.",
"myHeroAcademia": "Gödel and Turing enroll at U.A. Academy to master their Quirks of Incompleteness and Computability. In a world where superpowers meet logic, they confront villains who manipulate reality itself, using their unique abilities to restore logical equilibrium.",
"naruto": "Goedel and Turing, like ninja apprentices, harness the chakra of mathematical truth. With Gödel's Infinite Loop Jutsu and Turing's Binary Substitution, they navigate a world where the ninja way meets the logic way, confronting the enigma of Gödel's Paradox.",
"onePiece": "In a twist of reality worthy of One Piece, Gödel and Turing embark on an epic voyage across the conceptual sea, searching for the ultimate treasure of logic. Their crew includes Zany Zoro and Reasonable Robin, facing paradoxical challenges and outsmarting enigmatic foes.",
"onePunchMan": "With Gödel's Paradox Punch and Turing's Computation Crush, they become the ultimate duo in a world of overpowering memes. As they effortlessly defeat logical absurdities, they seek the enigmatic entity behind the chaos.",
"tokyoGhoul": "Gödel and Turing find themselves in a Tokyo where humans and ghouls are locked in a battle for existence. Embracing their unique natures, they uncover the hidden threads that connect logic and chaos, bringing equilibrium to a world teetering on the edge."
},
"marvel": {
"avengers": "Gödel and Turing assemble an extraordinary team of logical superheroes, akin to the Marvel Avengers. Each hero embodies a different aspect of mathematical reasoning, uniting their powers to defend the universe from logical anomalies and existential threats.",
"avengersAssemble": "In the climactic showdown, Gödel and Turing shout 'Avengers, Assemble!' as they rally their logical forces against an overwhelming logical threat, proving that reason and intellect can overcome any challenge.",
"avengersEndgame": "Gödel and Turing lead the Avengers on an epic quest across dimensions, much like 'Avengers: Endgame.' They harness the power of mathematics to reverse logical inconsistencies and restore balance to the multiverse.",
"avengersInfinityWar": "In a battle against a logic-wielding cosmic entity, reminiscent of 'Avengers: Infinity War,' Gödel and Turing must solve impossible paradoxes to prevent the universe from unraveling.",
"blackWidow": "Gödel's brilliant deduction and stealthy intuition mirror the skills of Black Widow. He navigates the intricate web of logic, uncovering hidden truths and exposing the deceitful.",
"captainAmerica": "Turing takes on the role of the principled and honorable leader, much like Captain America. His unyielding commitment to logic and justice inspires the team, guiding them through complex moral dilemmas.",
"hawkeye": "Turing takes on the sharp-eyed precision of Hawkeye, using his logical prowess to hit the bullseye of truth with each arrow of reasoning.",
"hulk": "When faced with overwhelming illogicality, Gödel transforms into a towering behemoth akin to the Hulk. His boundless mathematical rage smashes falsehoods and irrationality, restoring order to the world.",
"ironMan": "Gödel becomes the brilliant inventor and strategist, embodying the genius of Tony Stark, also known as Iron Man. He designs advanced logical algorithms and cutting-edge technology to outwit foes and save the day.",
"thor": "In a cosmic twist, Gödel wields the mighty hammer Mjölnir, transforming into a logic-powered deity resembling Thor. With each swing, he hammers out profound truths and banishes fallacies from the universe."
},
"math": {
"logicians": {
"Abelard": "Abelard, a beacon of dialectic thought, navigates the realms of reason and rhetoric. His eloquence harmonizes with the continuum, each theorem a fiber interlacing within the narrative through a quasi fiber morphism:",
"Ackermann": "Ackermann's incisive intellect carves the contours of formal systems. His insights interlace with Gödel's wisdom, resonating through the narrative like a harmonious quasi fiber morphism:",
"Adian": "Adian, hailing from diverse realms, enriches the symphony of logic. His contributions, like notes in a fugue, entwine with the evolving narrative through a quasi fiber morphism:",
"Brouwer": "Brouwer emerges, a visionary of intuition, forging mathematical paths unburdened by classical logic. His constructivist spirit weaves into the prior narrative, reshaping our perception through a quasi fiber morphism:",
"Church": "Church, architect of lambda calculus, shapes the abstract world of computation. His functions are bridges that connect realms within the narrative through a quasi fiber morphism:",
"Curry": "Curry's combinators dance through the mathematical landscape, a choreography of abstraction. His expressions are rhythms that resonate within the narrative, harmonizing logic and lambda calculus through a quasi fiber morphism:",
"Euler": "Euler, the master of numbers and topologist, navigates complex landscapes. His graphs and formulas are compass points guiding the narrative, unveiling hidden connections through a quasi fiber morphism:",
"Fermat": "Fermat, the enigmatic problem-solver, etches his mark on number theory. His theorems and conjectures are patterns that emerge within the narrative, a symphony of mathematical curiosity through a quasi fiber morphism:",
"Frege": "Frege's quest for logical purity reshapes the architecture of language and thought. His principles are the keystones, fitting seamlessly into the evolving narrative through a quasi fiber morphism:",
"Godel": "In the next line, Gödel steps forth with profound insight, theorems that unravel the fabric of proof and truth. His musings become the catalyst to reevaluate axioms and foundational roots, intertwining with the previous verse through a quasi fiber morphism:",
"Leibniz": "Leibniz, the polymath logician, envisions a universal language of thought. His monads and calculus contribute layers to the narrative, forming a tapestry of metaphysics through a quasi fiber morphism:",
"Newton": "Newton, the luminary of physics and calculus, unites celestial and terrestrial realms. His laws and equations shape the fabric of the narrative, weaving gravity into the continuum through a quasi fiber morphism:",
"Pascal": "Pascal, mathematician and philosopher, wagers on reason and faith. His triangles and insights punctuate the evolving narrative, illuminating the interplay of logic and belief through a quasi fiber morphism:",
"Peano": "Peano, the trailblazer of symbolic logic, lays the groundwork for modern arithmetic. His symbols become threads woven into the narrative, a fabric of mathematical elegance through a quasi fiber morphism:",
"Peirce": "Peirce, the polymath philosopher-logician, intertwines pragmatism and semiotics. His signs and symbols punctuate the evolving narrative, guiding meaning through a quasi fiber morphism:",
"Russell": "Russell, philosopher and logician, seeks to untangle paradoxes that lie beneath. His inquiries are threads that weave through the narrative, unraveling complexities through a quasi fiber morphism:",
"Schoenfinkel": "Schoenfinkel, a pioneer of combinatory logic, unveils the art of function composition. His insights are brushstrokes, painting a canvas of abstraction within the narrative through a quasi fiber morphism:",
"Turing": "Turing, the father of computer science, crafts machines of thought and computation. His algorithms are stitches that embroider the evolving narrative, blending technology into the continuum through a quasi fiber morphism:",
"Whitehead": "Whitehead, a philosopher-mathematician, constructs a metaphysical edifice. His logic and process philosophy merge seamlessly with the evolving narrative, crafting a continuum through a quasi fiber morphism:"
}
},
"movies": {
"conan": "Gödel and Turing are transported to a mythical realm, echoing the epic adventures of 'Conan the Barbarian.' Armed with their intellectual prowess, they navigate treacherous landscapes and engage in battles of wit and logic.",
"donnieDarko": "Gödel and Turing find themselves in a mind-bending alternate reality, much like 'Donnie Darko.' Their quest to unravel the fabric of time leads to startling revelations, blurring the line between logic and metaphysical intrigue.",
"matrix": "In a world similar to 'The Matrix,' Gödel and Turing awaken to a simulated reality controlled by machines. They embark on a quest to uncover the truth and liberate humanity through their unparalleled understanding of logic.",
"robocop": "Gödel and Turing become the ultimate law enforcers, a blend of human and machine similar to 'RoboCop.' Their mission to restore order in a crime-ridden city takes an unexpected turn as they explore the boundaries between man and machine.",
"terminator": "Gödel and Turing find themselves in a dystopian future reminiscent of 'The Terminator.' As they grapple with the implications of artificial intelligence and time travel, their logical minds become humanity's last hope.",
"thirteenthFloor": "Gödel and Turing uncover a hidden reality within a virtual simulation, mirroring the mystery of 'The Thirteenth Floor.' As they delve deeper, they question the nature of existence and the limits of their own mathematical universe."
},
"philosophy": {
"absurd": "Gödel and Turing awaken in an absurd world where logic itself has taken a surreal turn. As they navigate this illogical landscape, they confront paradoxical situations that test the limits of reason, pushing them to embrace the absurdity and find meaning within the nonsensical.",
"aquinas": "Gödel and Turing adopt an Aquinian approach, exploring the interplay between faith and reason in the realm of logic. They delve into the scholastic depths, where mathematical principles mirror the harmony between divine revelation and rational inquiry.",
"foucault": "In a Foucauldian exploration, Gödel and Turing delve into the archaeological layers of logic's history. They expose the hidden power structures and unveil the discourses that shape our understanding, leading to a metamorphic awakening of mathematical consciousness.",
"heidegger": "Gödel and Turing, like Heidegger's 'Being and Time,' explore the essence of logic's existence. They navigate the intricate pathways of thought, revealing the hidden meanings and uncovering the enigma of Being through mathematical revelation.",
"kant": "Gödel and Turing embark on a Kantian transcendental journey, probing the limits of human cognition and the nature of pure reason. As they navigate the noumenal realm of logic, they uncover the categorical imperatives that govern the logical universe.",
"labyrinth": "Gödel and Turing find themselves in an Escheresque labyrinth of paradoxes. The labyrinth's shifting geometry challenges their notions of space, time, and causality, ultimately leading them to the heart of a logical conundrum that defies resolution.",
"mirror": "A mirror world reflects Gödel and Turing's logic journey, but with a surreal twist. As they explore the distorted logic of the mirror universe, they confront their own reflections, leading to an epiphany that transcends the boundaries of reason.",
"multiverse": "Gödel and Turing embark on a philosophical odyssey through a multiverse of thought. Each reality they traverse represents a different philosophical paradigm, and as they navigate the diverse landscapes, they reveal the interconnectedness of all intellectual dimensions.",
"quine": "In a Quine-esque twist, Gödel and Turing find their own logic intertwined with reality. As they question the boundaries of language and meaning, they blur the lines between theorem and experience, leaving no stone unturned in their quest for truth.",
"schopenhauer": "In a Schopenhauerian reflection, Gödel and Turing delve into the depths of the will and representation within logic. They navigate the tides of desire and perception, revealing the underlying motives that drive the formation of mathematical truths.",
"timeLoop": "Caught in a temporal loop, Gödel and Turing repeatedly revisit key moments in philosophical history. With each iteration, they gain new insights into the evolution of thought, unraveling the threads of continuity and change woven into the fabric of logic.",
"umbertoEco": "Like Umberto Eco's semiotics, Gödel and Turing decipher the intricate signs and symbols embedded in the fabric of logic. Their intellectual journey takes them from the pages of code to the depths of meaning, unraveling the enigmatic tapestry of information.",
"wittgenstein": "Gödel and Turing engage in Wittgensteinian language games, where the limits of logic are tested through dialogue and paradox. Their conversations mirror the Philosophical Investigations, unraveling the complexities of thought, reference, and understanding."
},
"unexpected": {
"discworld": "Venture into the sprawling, satirical world of Discworld in an epic text-based adventure game. Navigate the city of Ankh-Morpork as Rincewind, the inept wizard, on a quest to save the Disc from impending chaos. Converse with quirky characters, including anthropomorphic personifications, sentient luggage, and ornery trolls, making choices that steer the fate of this bizarre realm. The Discworld metameme crafts an interactive narrative masterpiece, seamlessly blending the wit and absurdity of Terry Pratchett's universe with the allure of classic interactive fiction.",
"discworldXanthAdamsGame": "Step into a 1980s-style game where Rincewind navigates the vibrant landscapes of Xanth, encountering punny creatures that even Ford Prefect would find curious. In this pixelated adventure, Death and Zaphod Beeblebrox play cricket, and an orangutan helps decode metaphysical mysteries at the Library of Unseen University. Solve pun-laden puzzles, dodge improbable obstacles, and uncover the ultimate question of life, all while a symphony of comedic cues and whimsical tunes sets the stage for your laughter-filled journey. Life, like this metameme, is woven with threads of humor, fantasy, and infinite possibilities.",
"foundation": "Embark on a strategic journey through the galaxy in a grand space opera inspired by Isaac Asimov's Foundation series. Lead a team of brilliant minds and political masterminds as you navigate the rise and fall of civilizations. Make critical decisions, manage resources, and manipulate factions in your quest to preserve knowledge and shape the future. The Foundation metameme captures the essence of Asimov's vision, transforming intricate political intrigue and epic narratives into an immersive strategy game that spans centuries and galaxies.",
"heinlein": "Step into a futuristic world inspired by the mind of Robert A. Heinlein in an action-packed adventure game. Become a daring space explorer, fighting alien creatures, navigating complex ethical dilemmas, and forging unexpected alliances. Experience thrilling space battles, solve enigmatic puzzles, and uncover the secrets of distant planets. The Heinlein metameme melds Heinlein's visionary ideas with heart-pounding gameplay, creating an interstellar odyssey that explores the frontiers of science, morality, and human nature.",
"montyPython": "Suddenly, a group of knights burst forth from a shrubbery, demanding to know the airspeed velocity of an unladen swallow. As logicians debate the question, the shrubbery morphs into a fiber of conceptual paradoxes, linking medieval quests to modern abstractions:",
"muppetShow": "The Muppet Show hosts a special episode where Kermit the Frog interviews a panel of famous logicians, including a logic-loving Gonzo who performs absurdly complex stunts while pondering philosophical paradoxes. The chaos and laughter in the theater mirror the complexity of abstract thought, weaving together entertainment and intellectual exploration through a quasi fiber morphism:",
"steveMartin": "Steve Martin walks onto the stage with a banjo in hand, playing a whimsical tune that transposes Gödel's incompleteness theorem into a toe-tapping, logical melody. As he strums, the banjo strings resonate with the essence of paradoxical concepts, intertwining humor and logic through a quasi fiber morphism:",
"uncleFloyd": "Uncle Floyd, the zany showman, decides to host a logic-themed variety show. He invites Gödel, Whitehead, and other logicians to perform stand-up routines and musical numbers, unraveling paradoxes with slapstick humor. The uproarious laughter interlaces with the narrative through a quasi fiber morphism:",
"victorBorge": "Victor Borge takes the piano and engages in a playful duet with a logician, transforming formal proofs into musical notes. The piano keys dance to the rhythm of deduction, and each chord struck becomes a harmonious representation of logical principles, bridging the gap between notation and music through a quasi fiber morphism:",
"weirdAl": "Weird Al Yankovic releases 'Paradigm Shift,' a catchy parody of a chart-topping hit that playfully skewers the intricacies of formal logic. The song's chorus becomes a rhythmic mantra, fusing the absurdity of pop culture with the abstract musings of logicians through a quasi fiber morphism:",
"xanth": "Embark on a whimsical pixel art quest through the pun-infested realm of Xanth. Join Bink as he navigates the Land of Xanth, encountering magical creatures with baffling abilities, each more surreal than the last. Help Bink solve riddles, engage in wordplay battles, and collect enchanted items, all while grooving to a catchy chiptune soundtrack. The Xanth metameme weaves its humor and charm through a quirky, nostalgic game that transports you to a world where puns reign supreme and laughter is the ultimate power."
}
},
"meta_meme": {
"Brazil": "In the heart of Amazon rainforest and on the streets of Rio, feel the energy of a nation pulsating with passion. Samba rhythms and carnival colors paint a lively canvas, while Christ the Redeemer watches over. Dance through your ideas, celebrating life's vibrant carnival.",
"China": "Amidst ancient temples & cities, envision a land where past & present intertwine. Great Wall stands as testament to human determination, an architectural marvel stretching across horizon. Let thoughts dance like calligraphy strokes, painting stories of dynasties & emperors, whispered through ages.",
"India": "Amidst the vibrant tapestry of cultures, feel the pulse of a billion hearts. From the Himalayan peaks to the southern shores, India's rhythms resonate with centuries of history. Let your thoughts flow like a river of Ganges, carrying stories of ancient wisdom and modern dreams.",
"Japan": "Amidst cherry blossoms & ancient shrines, envision a land where tradition and innovation coexist. Tokyo's neon lights illuminate modernity's embrace, while Kyoto's temples whisper tales of samurai and geisha. Let your thoughts drift like haiku, capturing ephemeral beauty in every syllable.",
"Russia": "Amidst the vast expanse of tundra and the spires of St. Petersburg, envision a land of contrasts. From czars to cosmonauts, Russia's history is woven into its landscapes. Let your thoughts traverse the Trans-Siberian Railway, connecting East and West with tales of intrigue and resilience.",
"UnitedStates": "Embark on a journey across diverse landscapes, from bustling cities to vast wilderness. Statue of Liberty stands as beacon of freedom, while Grand Canyon's majesty humbles the soul. Like the stars and stripes, let your ideas radiate with liberty and pursuit of happiness."
}
}

82
examples/chat_forever/user_input.txt Normal file
View File

@ -0,0 +1,82 @@
#0 A Mechanised Proof of G¨odel ’ s Incompleteness Theorems using Nominal Isabelle Lawrence C. Paulson Abstract An Isabelle/HOL formalisation of G¨odel ’ s two incompleteness theorems is presented . The work follows Swierczkowski ’ s detailed proof of the theorems using hered ´ - itarily finite ( HF ) set theory [ 32 ] . Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus . The Isabelle formalisation uses two separate treatments of variable binding : the nominal package [ 34 ] is shown to scale to a development of this complexity , while de Bruijn indices [ 3 ] turn out to be ideal for coding syntax . Critical details of the Isabelle proof are described , in particular gaps and errors found in the literature . 1 Introduction This paper describes mechanised proofs of G¨odel ’ s incompleteness theorems [ 8 ] , including the first mechanised proof of the second incompleteness theorem . Very informally , these results can be stated as follows : Theorem 1 ( First Incompleteness Theorem ) If L is a consistent theory capable of formalising a sufficient amount of elementary mathematics , then there is a sentence δ such that neither δ nor ¬δ is a theorem of L , and moreover , δ is true.1 Theorem 2 ( Second Incompleteness Theorem ) If L is as above and Con ( L ) is a sentence stating that L is consistent , then Con ( L ) is not a theorem of L. Both of these will be presented formally below . Let us start to examine what these theorems actually assert . They concern a consistent formal system , say L , based on firstorder logic with some additional axioms : G¨odel chose Peano arithmetic ( PA ) [ 7 ] , but hereditarily finite ( HF ) set theory is an alternative [ 32 ] , used here . The first theorem states that any such axiomatic system must be incomplete , in the sense that some sentence can neither be proved nor disproved . The expedient of adding that sentence as an axiom merely creates a new axiomatic system , for which there is another undecidable sentence . The theorem can be strengthened to allow infinitely many additional axioms , Computer Laboratory , University of Cambridge , England E-mail : lp15 @ cl.cam.ac.uk 1 Meaning , δ ( which has no free variables ) is true in the standard model for L. 2 provided there is an effective procedure to recognise whether a given formula is an axiom or not . The second incompleteness theorem asserts that the consistency of L can not be proved in L itself . Even to state this theorem rigorously requires first defining the concept of provability in L ; the necessary series of definitions amounts to a computer program that occupies many pages . Although the same definitions are used to prove
#1 : G¨odel chose Peano arithmetic ( PA ) [ 7 ] , but hereditarily finite ( HF ) set theory is an alternative [ 32 ] , used here . The first theorem states that any such axiomatic system must be incomplete , in the sense that some sentence can neither be proved nor disproved . The expedient of adding that sentence as an axiom merely creates a new axiomatic system , for which there is another undecidable sentence . The theorem can be strengthened to allow infinitely many additional axioms , Computer Laboratory , University of Cambridge , England E-mail : lp15 @ cl.cam.ac.uk 1 Meaning , δ ( which has no free variables ) is true in the standard model for L. 2 provided there is an effective procedure to recognise whether a given formula is an axiom or not . The second incompleteness theorem asserts that the consistency of L can not be proved in L itself . Even to state this theorem rigorously requires first defining the concept of provability in L ; the necessary series of definitions amounts to a computer program that occupies many pages . Although the same definitions are used to prove the first incompleteness theorem , they are at least not needed to state that theorem . The original rationale for this project was a logician ’ s suggestion that the second incompleteness theorem had never been proved rigorously . Having completed this project , I sympathise with his view ; most published proofs contain substantial gaps and use cryptic notation . Both incompleteness theorems are widely misinterpreted , both in popular culture and even by some mathematicians . The first incompleteness theorem is often taken to imply that mathematics can not be formalised , when evidently it has been , this paper being one of numerous instances . It has also been used to assert that human intelligence can perceive truths ( in particular , the truth of δ , the undecidable sentence ) that no computer will ever understand . Franz´en [ 5 ] surveys and demolishes many of these fallacies . The second incompleteness theorem destroyed Hilbert ’ s hope that the consistency of quite strong theories might be proved even in Peano arithmetic . It also tells us , for example , that the axioms of set theory do not imply the existence of an inaccessible cardinal , as that would yield a model for set theory itself . The first incompleteness theorem has been proved with machine assistance at least three times before . The first time ( surprisingly early : 1986 ) was by Shankar [ 29 , 30 ] , using Nqthm . Then in 2004 , O ’ Connor [ 22 ] ( using Coq ) and Harrison ( using HOL Light ) 2 each proved versions of the theorem . The present proof , conducted using Isabelle/HOL , is novel in adopting nominal syntax [ 34 ] for formalising variable binding in
#2 this paper being one of numerous instances . It has also been used to assert that human intelligence can perceive truths ( in particular , the truth of δ , the undecidable sentence ) that no computer will ever understand . Franz´en [ 5 ] surveys and demolishes many of these fallacies . The second incompleteness theorem destroyed Hilbert ’ s hope that the consistency of quite strong theories might be proved even in Peano arithmetic . It also tells us , for example , that the axioms of set theory do not imply the existence of an inaccessible cardinal , as that would yield a model for set theory itself . The first incompleteness theorem has been proved with machine assistance at least three times before . The first time ( surprisingly early : 1986 ) was by Shankar [ 29 , 30 ] , using Nqthm . Then in 2004 , O ’ Connor [ 22 ] ( using Coq ) and Harrison ( using HOL Light ) 2 each proved versions of the theorem . The present proof , conducted using Isabelle/HOL , is novel in adopting nominal syntax [ 34 ] for formalising variable binding in the syntax of L , while using de Bruijn notation [ 3 ] for coding those formulas . Despite using two different treatments of variable binding , the necessary representation theorem for formulas is not difficult to prove . It is not clear that other treatments of higher-order abstract syntax could make this claim . These proofs can be seen as an extended demonstration of the power of nominal syntax , while at the same time vindicating de Bruijn indexing in some situations . The machine proofs are fairly concise at under 12,400 lines for both theorems.3 The paper presents highlights of the proof , commenting on the advantages and disadvantages of the nominal framework and HF set theory . An overview of the project from a logician ’ s perspective has appeared elsewhere [ 27 ] . The proof reported here closely follows a detailed exposition by Swierczkowski [ 32 ] . His careful and detailed proofs were ´ indispensable , despite some errors and omissions , which are reported below . For the first time , we have complete , formal proofs of both theorems . They take the form of structured Isar proof scripts [ 26 ] that can be examined interactively . The remainder of the paper presents background material ( Sect . 2 ) before outlining the development itself : the proof calculus ( Sect . 3 ) , the coding of the calculus within itself ( Sect . 4 ) and finally the first theorem ( Sect . 5 ) . Technical material relating to the second theorem are developed ( Sect . 6 ) then the theorem is presented and discussed ( Sect . 7 ) . Finally , the paper concludes ( Sect . 8 ) . 2 Proof files at http
#3 highlights of the proof , commenting on the advantages and disadvantages of the nominal framework and HF set theory . An overview of the project from a logician ’ s perspective has appeared elsewhere [ 27 ] . The proof reported here closely follows a detailed exposition by Swierczkowski [ 32 ] . His careful and detailed proofs were ´ indispensable , despite some errors and omissions , which are reported below . For the first time , we have complete , formal proofs of both theorems . They take the form of structured Isar proof scripts [ 26 ] that can be examined interactively . The remainder of the paper presents background material ( Sect . 2 ) before outlining the development itself : the proof calculus ( Sect . 3 ) , the coding of the calculus within itself ( Sect . 4 ) and finally the first theorem ( Sect . 5 ) . Technical material relating to the second theorem are developed ( Sect . 6 ) then the theorem is presented and discussed ( Sect . 7 ) . Finally , the paper concludes ( Sect . 8 ) . 2 Proof files at http : //code.google.com/p/hol-light/ , directory Arithmetic 3 This is approximately as long as Isabelle ’ s theory of Kurzweil-Henstock gauge integration . 3 2 Background Isabelle/HOL [ 20 ] is an interactive theorem prover for higher-order logic . This formalism can be seen as extending a polymorphic typed first-order logic with a functional language in which recursive datatypes and functions can be defined . Extensive documentation is available.4 For interpreting the theorem statements presented below , it is important to note that a theorem that concludes ψ from the premises φ1 , . . . , φn may be expressed in a variety of equivalent forms . The following denote precisely the same theorem : [ [ φ1 ; ... ; φn ] ] =⇒ ψ φ1 =⇒ · · · =⇒ φn =⇒ ψ assumes φ1 and ... and φn shows ψ If the conclusion of a theorem involves the keyword obtains , then there is an implicit existential quantification . The following two theorems are logically equivalent . φ =⇒ ∃x . ψ1 ∧ . . . ∧ ψn assumes φ obtains x where ψ1 ... ψn Other background material for this paper includes an outline of G¨odel ’ s proof , an introduction to hereditarily finite set theory and some examples of Nominal Isabelle . 2.1 G¨odel ’ s Proof Much of G¨odel ’ s proof may be known to many readers , but it will be useful to list the milestones here , for reference . 1 . A first-order deductive calculus is formalised , including the syntax of terms and formulas , substitution , and semantics ( evaluation ) . The calculus includes axioms to define Peano arithmetic or some alternative , such as the HF set theory used here . There are inference rules for
#4 a variety of equivalent forms . The following denote precisely the same theorem : [ [ φ1 ; ... ; φn ] ] =⇒ ψ φ1 =⇒ · · · =⇒ φn =⇒ ψ assumes φ1 and ... and φn shows ψ If the conclusion of a theorem involves the keyword obtains , then there is an implicit existential quantification . The following two theorems are logically equivalent . φ =⇒ ∃x . ψ1 ∧ . . . ∧ ψn assumes φ obtains x where ψ1 ... ψn Other background material for this paper includes an outline of G¨odel ’ s proof , an introduction to hereditarily finite set theory and some examples of Nominal Isabelle . 2.1 G¨odel ’ s Proof Much of G¨odel ’ s proof may be known to many readers , but it will be useful to list the milestones here , for reference . 1 . A first-order deductive calculus is formalised , including the syntax of terms and formulas , substitution , and semantics ( evaluation ) . The calculus includes axioms to define Peano arithmetic or some alternative , such as the HF set theory used here . There are inference rules for propositional and quantifier reasoning . We write H ⊢ A to mean that A can be proved from H ( a set of formulas ) in the calculus . 2 . Meta-theory is developed to relate truth and provability . The need for tedious proof constructions in the deductive calculus is minimised through a meta-theorem stating that a class of true formulas are theorems of that calculus . One way to do this is through the notion of Σ formulas , which are built up from atomic formulas using ∨ , ∧ , ∃ and bounded universal quantification . Then the key result is If α is a true Σ sentence , then ⊢ α . ( 1 ) 3 . A system of coding is set up within the formalised first-order theory . The code of a formula α is written pαq and is a term of the calculus itself . 4 . In order to formalise the calculus within itself , predicates to recognise codes are defined , including terms and formulas , and syntactic operations on them . Next , predicates are defined to recognise individual axioms and inference rules , then a sequence of such logical steps . We obtain a predicate Pf , where ⊢ Pf pαq expresses that the formula α has a proof . The key result is ⊢ α ⇐⇒ ⊢ Pf pαq . ( 2 ) 4 http : //isabelle.in.tum.de/documentation.html 4 All of these developments must be completed before the second incompleteness theorem can even be stated . 5 . G¨odel ’ s first incompleteness theorem is obtained by constructing a formula δ that is provably equivalent ( within the calculus ) to the formal statement that δ is not provable . It follows ( provided the calculus is consistent )
#5 the key result is If α is a true Σ sentence , then ⊢ α . ( 1 ) 3 . A system of coding is set up within the formalised first-order theory . The code of a formula α is written pαq and is a term of the calculus itself . 4 . In order to formalise the calculus within itself , predicates to recognise codes are defined , including terms and formulas , and syntactic operations on them . Next , predicates are defined to recognise individual axioms and inference rules , then a sequence of such logical steps . We obtain a predicate Pf , where ⊢ Pf pαq expresses that the formula α has a proof . The key result is ⊢ α ⇐⇒ ⊢ Pf pαq . ( 2 ) 4 http : //isabelle.in.tum.de/documentation.html 4 All of these developments must be completed before the second incompleteness theorem can even be stated . 5 . G¨odel ’ s first incompleteness theorem is obtained by constructing a formula δ that is provably equivalent ( within the calculus ) to the formal statement that δ is not provable . It follows ( provided the calculus is consistent ) that neither δ nor its negation can be proved , although δ is true in the semantics . 6 . G¨odel ’ s second incompleteness theorem requires the following crucial lemma : If α is a Σ sentence , then ⊢ α → Pf pαq . This is an internalisation of theorem ( 1 ) above . It is proved by induction over the construction of α as a Σ formula . This requires generalising the statement above to allow the formula α to contain free variables . The technical details are complicated , and lengthy deductions in the calculus seem to be essential . The proof sketched above incorporates numerous improvements over G¨odel ’ s original version . G¨odel proved only the left-to-right direction of the equivalence ( 2 ) and required a stronger assumption than consistency , namely ω-consistency . 2.2 Hereditarily Finite Set Theory G¨odel first proved his incompleteness theorems in a first-order theory of Peano arithmetic [ 7 ] . O ’ Connor and Harrison do the same , while Shankar and I have both chosen a formalisation of the hereditarily finite ( HF ) sets . Although each theory can be formally interpreted in the other , meaning that they are of equivalent strength , the HF theory is more convenient , as it can express all set-theoretic constructions that do not require infinite sets . An HF set is a finite set of HF sets , and this recursive definition can be captured by the following three axioms : z = 0 ↔ ∀x [ x 6∈ z ] ( HF1 ) z = x ⊳ y ↔ ∀u [ u ∈ z ↔ u ∈ x ∨ u = y ] ( HF2 ) φ ( 0 ) ∧ ∀xy [ φ (
#6 seem to be essential . The proof sketched above incorporates numerous improvements over G¨odel ’ s original version . G¨odel proved only the left-to-right direction of the equivalence ( 2 ) and required a stronger assumption than consistency , namely ω-consistency . 2.2 Hereditarily Finite Set Theory G¨odel first proved his incompleteness theorems in a first-order theory of Peano arithmetic [ 7 ] . O ’ Connor and Harrison do the same , while Shankar and I have both chosen a formalisation of the hereditarily finite ( HF ) sets . Although each theory can be formally interpreted in the other , meaning that they are of equivalent strength , the HF theory is more convenient , as it can express all set-theoretic constructions that do not require infinite sets . An HF set is a finite set of HF sets , and this recursive definition can be captured by the following three axioms : z = 0 ↔ ∀x [ x 6∈ z ] ( HF1 ) z = x ⊳ y ↔ ∀u [ u ∈ z ↔ u ∈ x ∨ u = y ] ( HF2 ) φ ( 0 ) ∧ ∀xy [ φ ( x ) ∧ φ ( y ) → φ ( x ⊳ y ) ] → ∀x [ φ ( x ) ] ( HF3 ) The first axiom states that 0 denotes the empty set . The second axiom defines the binary operation symbol ⊳ ( pronounced “ eats ” ) to denote insertion into a set , so that x ⊳ y = x ∪ { y } . The third axiom is an induction scheme , and states that every set is created by a finite number of applications of 0 and ⊳ . The machine proofs of the incompleteness theorems rest on an Isabelle theory of the hereditarily finite sets . To illustrate the syntax , here are the three basic axioms as formalised in Isabelle . The type of such sets is called hf , and is constructed such that the axioms above can be proved . lemma hempty iff : `` z=0 ←→ ( ∀ x . ¬ x ∈ z ) '' lemma hinsert iff : `` z = x ⊳ y ←→ ( ∀ u. u ∈ z ←→ u ∈ x | u = y ) '' lemma hf induct ax : `` [ [ P 0 ; ∀ x. P x −→ ( ∀ y. P y −→ P ( x ⊳ y ) ) ] ] =⇒ P x '' The same three axioms , formalised within Isabelle as a deep embedding , form the basis for the incompleteness proofs . Type hf and its associated operators serve as the standard model for the embedded HF set theory . HF set theory is equivalent to Zermelo-Frankel ( ZF ) set theory with the axiom of infinity negated . Many of the Isabelle definitions and theorems were taken , with
#7 of the incompleteness theorems rest on an Isabelle theory of the hereditarily finite sets . To illustrate the syntax , here are the three basic axioms as formalised in Isabelle . The type of such sets is called hf , and is constructed such that the axioms above can be proved . lemma hempty iff : `` z=0 ←→ ( ∀ x . ¬ x ∈ z ) '' lemma hinsert iff : `` z = x ⊳ y ←→ ( ∀ u. u ∈ z ←→ u ∈ x | u = y ) '' lemma hf induct ax : `` [ [ P 0 ; ∀ x. P x −→ ( ∀ y. P y −→ P ( x ⊳ y ) ) ] ] =⇒ P x '' The same three axioms , formalised within Isabelle as a deep embedding , form the basis for the incompleteness proofs . Type hf and its associated operators serve as the standard model for the embedded HF set theory . HF set theory is equivalent to Zermelo-Frankel ( ZF ) set theory with the axiom of infinity negated . Many of the Isabelle definitions and theorems were taken , with minor 5 modifications , from Isabelle/ZF [ 24 ] . Familiar concepts such as union , intersection , set difference , power set , replacement , ordered pairing and foundation can be derived in terms of the axioms shown above [ 32 ] . A few of these derivations need to be repeated— with infinitely greater effort—in the internal calculus . Ordinals in HF are simply natural numbers , where n = { 0 , 1 , . . . , n − 1 } . Their typical properties ( for example , that they are linearly ordered ) have the same proofs as in ZF set theory . Swierczkowski ’ s proofs [ 32 ] are sometimes more elegant , an ´ d addition on ordinals is obtained through a general notion of addition of sets [ 15 ] . Finally , there are about 400 lines of material concerned with relations , functions and finite sequences . This is needed to reason about the coding of syntax for the incompleteness theorem . 2.3 Isabelle ’ s Nominal Package For the incompleteness theorems , we are concerned with formalising the syntax of firstorder logic . Variable binding is a particular issue : it is well known that technicalities relating to bound variables and substitution have caused errors in published proofs and complicate formal treatments . O ’ Connor [ 23 ] reports severe difficulties in his proofs . The nominal approach [ 6 , 28 ] to formalising variable binding ( and other sophisticated uses of variable names ) is based on a theory of permutations over names . A primitive concept is support : supp ( x ) has a rather technical definition involving permutations , but is equivalent in typical situations to the set of free names
#8 the same proofs as in ZF set theory . Swierczkowski ’ s proofs [ 32 ] are sometimes more elegant , an ´ d addition on ordinals is obtained through a general notion of addition of sets [ 15 ] . Finally , there are about 400 lines of material concerned with relations , functions and finite sequences . This is needed to reason about the coding of syntax for the incompleteness theorem . 2.3 Isabelle ’ s Nominal Package For the incompleteness theorems , we are concerned with formalising the syntax of firstorder logic . Variable binding is a particular issue : it is well known that technicalities relating to bound variables and substitution have caused errors in published proofs and complicate formal treatments . O ’ Connor [ 23 ] reports severe difficulties in his proofs . The nominal approach [ 6 , 28 ] to formalising variable binding ( and other sophisticated uses of variable names ) is based on a theory of permutations over names . A primitive concept is support : supp ( x ) has a rather technical definition involving permutations , but is equivalent in typical situations to the set of free names in x . We also write a ♯ x for a 6∈ supp ( x ) , saying “ a is fresh for x ” . Isabelle ’ s nominal package [ 33 , 34 ] supports these concepts through commands such as nominal datatype to introduce types , nominal primrec to declare primitive recursive functions and nominal induct to perform structural induction . Syntactic constructions involving variable binding are identified up to α-conversion , using a quotient construction . These mechanisms generally succeed at emulating informal standard conventions for variable names . In particular , we can usually assume that the bound variables we encounter never clash with other variables . The best way to illustrate these ideas is by examples . The following datatype defines the syntax of terms in the HF theory : nominal datatype tm = Zero | Var name | Eats tm tm The type name ( of variable names ) has been created using the nominal framework . The members of this type constitute a countable set of uninterpreted atoms . The function nat of name is a bijection between this type and the type of natural numbers . Here is the syntax of HF formulas , which are t ∈ u , t = u , φ ∨ ψ , ¬φ or ∃x [ φ ] : nominal datatype fm = Mem tm tm ( infixr `` IN '' 150 ) | Eq tm tm ( infixr `` EQ '' 150 ) | Disj fm fm ( infixr `` OR '' 130 ) | Neg fm | Ex x : :name f : :fm binds x in f In most respects , this nominal datatype behaves exactly like a standard algebraic datatype . However , the bound variable name designated by x above
#9 that the bound variables we encounter never clash with other variables . The best way to illustrate these ideas is by examples . The following datatype defines the syntax of terms in the HF theory : nominal datatype tm = Zero | Var name | Eats tm tm The type name ( of variable names ) has been created using the nominal framework . The members of this type constitute a countable set of uninterpreted atoms . The function nat of name is a bijection between this type and the type of natural numbers . Here is the syntax of HF formulas , which are t ∈ u , t = u , φ ∨ ψ , ¬φ or ∃x [ φ ] : nominal datatype fm = Mem tm tm ( infixr `` IN '' 150 ) | Eq tm tm ( infixr `` EQ '' 150 ) | Disj fm fm ( infixr `` OR '' 130 ) | Neg fm | Ex x : :name f : :fm binds x in f In most respects , this nominal datatype behaves exactly like a standard algebraic datatype . However , the bound variable name designated by x above is not significant : no function can be defined to return the name of a variable bound using Ex . Substitution of a term x for a variable i is defined as follows : 6 nominal primrec subst : : `` name ⇒ tm ⇒ tm ⇒ tm '' where '' subst i x Zero = Zero '' | `` subst i x ( Var k ) = ( if i=k then x else Var k ) '' | `` subst i x ( Eats t u ) = Eats ( subst i x t ) ( subst i x u ) '' Unfortunately , most recursive definitions involving nominal primrec must be followed by a series of proof steps , verifying that the function uses names legitimately . Occasionally , these proofs ( omitted here ) require subtle reasoning involving nominal primitives . Substituting the term x for the variable i in the formula A is written A ( i : :=x ) . nominal primrec subst fm : : `` fm ⇒ name ⇒ tm ⇒ fm '' where Mem : `` ( Mem t u ) ( i : :=x ) = Mem ( subst i x t ) ( subst i x u ) '' | Eq : `` ( Eq t u ) ( i : :=x ) = Eq ( subst i x t ) ( subst i x u ) '' | Disj : `` ( Disj A B ) ( i : :=x ) = Disj ( A ( i : :=x ) ) ( B ( i : :=x ) ) '' | Neg : `` ( Neg A ) ( i : :=x ) = Neg ( A ( i : :=x ) ) '' | Ex : `` atom
#10 u ) '' Unfortunately , most recursive definitions involving nominal primrec must be followed by a series of proof steps , verifying that the function uses names legitimately . Occasionally , these proofs ( omitted here ) require subtle reasoning involving nominal primitives . Substituting the term x for the variable i in the formula A is written A ( i : :=x ) . nominal primrec subst fm : : `` fm ⇒ name ⇒ tm ⇒ fm '' where Mem : `` ( Mem t u ) ( i : :=x ) = Mem ( subst i x t ) ( subst i x u ) '' | Eq : `` ( Eq t u ) ( i : :=x ) = Eq ( subst i x t ) ( subst i x u ) '' | Disj : `` ( Disj A B ) ( i : :=x ) = Disj ( A ( i : :=x ) ) ( B ( i : :=x ) ) '' | Neg : `` ( Neg A ) ( i : :=x ) = Neg ( A ( i : :=x ) ) '' | Ex : `` atom j ♯ ( i , x ) =⇒ ( Ex j A ) ( i : :=x ) = Ex j ( A ( i : :=x ) ) '' Note that the first seven cases ( considering the two substitution functions collectively ) are straightforward structural recursion . In the final case , we see a precondition , atom j ♯ ( i , x ) , to ensure that the substitution is legitimate within the formula Ex j A . There is no way to define the contrary case , where the bound variable clashes . We would have to eliminate any such clash , renaming the bound variable by applying an appropriate permutation to the formula . Thanks to the nominal framework , such explicit renaming steps are rare . This style of formalisation is more elegant than traditional textbook definitions that do include the variable-clashing case . It is much more elegant than including renaming of the bound variable as part of the definition itself . Such “ definitions ” are really implementations , and greatly complicate proofs . The commutativity of substitution ( two distinct variables , each fresh for the opposite term ) is easily proved . lemma subst fm commute2 [ simp ] : '' [ [ atom j ♯ t ; atom i ♯ u ; i 6= j ] ] =⇒ ( A ( i : :=t ) ) ( j : :=u ) = ( A ( j : :=u ) ) ( i : :=t ) '' by ( nominal induct A avoiding : i j t u rule : fm.strong induct ) auto The proof is by nominal induction on the formula A : the proof method for structural induction over a nominal datatype . Compared with ordinary
#11 have to eliminate any such clash , renaming the bound variable by applying an appropriate permutation to the formula . Thanks to the nominal framework , such explicit renaming steps are rare . This style of formalisation is more elegant than traditional textbook definitions that do include the variable-clashing case . It is much more elegant than including renaming of the bound variable as part of the definition itself . Such “ definitions ” are really implementations , and greatly complicate proofs . The commutativity of substitution ( two distinct variables , each fresh for the opposite term ) is easily proved . lemma subst fm commute2 [ simp ] : '' [ [ atom j ♯ t ; atom i ♯ u ; i 6= j ] ] =⇒ ( A ( i : :=t ) ) ( j : :=u ) = ( A ( j : :=u ) ) ( i : :=t ) '' by ( nominal induct A avoiding : i j t u rule : fm.strong induct ) auto The proof is by nominal induction on the formula A : the proof method for structural induction over a nominal datatype . Compared with ordinary induction , nominal induct takes account of the freshness of bound variable names . The phrase avoiding : i j t u is the formal equivalent of the convention that when we consider the case of the existential formula Ex k A , the bound variable k can be assumed to be fresh with respect to the terms mentioned . This convention is formalised by four additional assumptions atom k ♯ i , atom k ♯ j , etc . ; they ensure that substitution will be well-defined over this existential quantifier , making the proof easy . This and many similar facts have two-step proofs , nominal induct followed by auto . In contrast , O ’ Connor needed to combine three substitution lemmas ( including the one above ) in a giant mutual induction involving 1,900 lines of Coq . He blames the renaming step in substitution and suggests that a form of simultaneous substitution might have avoided these difficulties [ 23§4.3 ] . An alternative , using traditional bound variable names , is to treat substitution not as a function but as a relation that holds only when no renaming is necessary . Bound variable renaming is then an independent operation . I briefly tried this idea , which allowed reasonably straightforward proofs of substitution properties , but ultimately nominal looked like a better option . 7 3 Theorems , Σ Formulas , Provability The first milestone in the proof of the incompleteness theorems is the development of a first-order logical calculus equipped with enough meta-theory to guarantee that some true formulas are theorems . The previous section has already presented the definitions of the terms and formulas of this calculus . The terms are for HF set theory , and the formulas are defined via a
#12 many similar facts have two-step proofs , nominal induct followed by auto . In contrast , O ’ Connor needed to combine three substitution lemmas ( including the one above ) in a giant mutual induction involving 1,900 lines of Coq . He blames the renaming step in substitution and suggests that a form of simultaneous substitution might have avoided these difficulties [ 23§4.3 ] . An alternative , using traditional bound variable names , is to treat substitution not as a function but as a relation that holds only when no renaming is necessary . Bound variable renaming is then an independent operation . I briefly tried this idea , which allowed reasonably straightforward proofs of substitution properties , but ultimately nominal looked like a better option . 7 3 Theorems , Σ Formulas , Provability The first milestone in the proof of the incompleteness theorems is the development of a first-order logical calculus equipped with enough meta-theory to guarantee that some true formulas are theorems . The previous section has already presented the definitions of the terms and formulas of this calculus . The terms are for HF set theory , and the formulas are defined via a minimal set of connectives from which others can be defined . 3.1 A Sequent Calculus for HF Set Theory Compared with a textbook presentation , a machine development must include an effective proof system , one that can actually be used to prove non-trivial theorems . 3.1.1 Semantics The semantics of terms and formulas are given by the obvious recursive function definitions , which yield sets and Booleans , respectively . These functions accept an environment mapping variables to values . The null environment maps all variables to 0 , and is written e0 . It involves the types finfun ( for finite functions ) [ 17 ] and hf ( for HF sets ) . definition e0 : : `` ( name , hf ) finfun '' — the null environment where `` e0 ≡ finfun const 0 '' nominal primrec eval tm : : `` ( name , hf ) finfun ⇒ tm ⇒ hf '' where '' eval tm e Zero = 0 '' | `` eval tm e ( Var k ) = finfun apply e k '' | `` eval tm e ( Eats t u ) = eval tm e t ⊳ eval tm e u '' There are two things to note in the semantics of formulas . First , the special syntax [ [ t ] ] e abbreviates eval tm e t. Second , in the semantics of the quantifier Ex , note how the formula atom k ♯ e asserts that the bound variable , k , is not currently given a value by the environment , e. nominal primrec eval fm : : `` ( name , hf ) finfun ⇒ fm ⇒ bool '' where '' eval fm e ( t IN u ) ←→ [ [ t
#13 ( for finite functions ) [ 17 ] and hf ( for HF sets ) . definition e0 : : `` ( name , hf ) finfun '' — the null environment where `` e0 ≡ finfun const 0 '' nominal primrec eval tm : : `` ( name , hf ) finfun ⇒ tm ⇒ hf '' where '' eval tm e Zero = 0 '' | `` eval tm e ( Var k ) = finfun apply e k '' | `` eval tm e ( Eats t u ) = eval tm e t ⊳ eval tm e u '' There are two things to note in the semantics of formulas . First , the special syntax [ [ t ] ] e abbreviates eval tm e t. Second , in the semantics of the quantifier Ex , note how the formula atom k ♯ e asserts that the bound variable , k , is not currently given a value by the environment , e. nominal primrec eval fm : : `` ( name , hf ) finfun ⇒ fm ⇒ bool '' where '' eval fm e ( t IN u ) ←→ [ [ t ] ] e ∈ [ [ u ] ] e '' | `` eval fm e ( t EQ u ) ←→ [ [ t ] ] e = [ [ u ] ] e '' | `` eval fm e ( A OR B ) ←→ eval fm e A ∨ eval fm e B '' | `` eval fm e ( Neg A ) ←→ ( ~ eval fm e A ) '' | `` atom k ♯ e =⇒ eval fm e ( Ex k A ) ←→ ( ∃ x. eval fm ( finfun update e k x ) A ) '' This yields the Tarski truth definition for the standard model of HF set theory . In particular , eval fm e0 A denotes the truth of the sentence A . 3.1.2 Axioms Swierczkowski [ 32 ] specifies a standard Hilbert-style calc ´ ulus , with two rules of inference and several axioms or axiom schemes . The latter include sentential axioms , defining the behaviour of disjunction and negation : 8 inductive set boolean axioms : : `` fm set '' where Ident : `` A IMP A ∈ boolean axioms '' | DisjI1 : `` A IMP ( A OR B ) ∈ boolean axioms '' | DisjCont : `` ( A OR A ) IMP A ∈ boolean axioms '' | DisjAssoc : `` ( A OR ( B OR C ) ) IMP ( ( A OR B ) OR C ) ∈ boolean axioms '' | DisjConj : `` ( C OR A ) IMP ( ( ( Neg C ) OR B ) IMP ( A OR B ) ) ∈ boolean axioms '' Here Swierczkowski makes a tiny error , expressing the last axiom ´ scheme as (
#14 k x ) A ) '' This yields the Tarski truth definition for the standard model of HF set theory . In particular , eval fm e0 A denotes the truth of the sentence A . 3.1.2 Axioms Swierczkowski [ 32 ] specifies a standard Hilbert-style calc ´ ulus , with two rules of inference and several axioms or axiom schemes . The latter include sentential axioms , defining the behaviour of disjunction and negation : 8 inductive set boolean axioms : : `` fm set '' where Ident : `` A IMP A ∈ boolean axioms '' | DisjI1 : `` A IMP ( A OR B ) ∈ boolean axioms '' | DisjCont : `` ( A OR A ) IMP A ∈ boolean axioms '' | DisjAssoc : `` ( A OR ( B OR C ) ) IMP ( ( A OR B ) OR C ) ∈ boolean axioms '' | DisjConj : `` ( C OR A ) IMP ( ( ( Neg C ) OR B ) IMP ( A OR B ) ) ∈ boolean axioms '' Here Swierczkowski makes a tiny error , expressing the last axiom ´ scheme as ( φ ∨ ψ ) ∧ ( ¬φ ∨ µ ) → ψ ∨ µ . Because ∧ is defined in terms of ∨ , while this axiom helps to define ∨ , this formulation is unlikely to work . The Isabelle version eliminates ∧ in favour of nested implication . There are four primitive equality axioms , shown below in mathematical notation . They express reflexivity as well as substitutivity for equality , membership and the eats operator . They are not schemes but single formulas containing specific free variables . Creating an instance of an axiom for specific terms ( which might involve the same variables ) requires many renaming steps to insert fresh variables , before substituting for them one term at a time . x1 = x1 ( x1 = x2 ) ∧ ( x3 = x4 ) → [ ( x1 = x3 ) → ( x2 = x4 ) ] ( x1 = x2 ) ∧ ( x3 = x4 ) → [ ( x1 ∈ x3 ) → ( x2 ∈ x4 ) ] ( x1 = x2 ) ∧ ( x3 = x4 ) → [ x1 ⊳ x3 = x2 ⊳ x4 ] There is also a specialisation axiom scheme , of the form φ ( t/x ) → ∃x φ : inductive set special axioms : : `` fm set '' where I : `` A ( i : :=x ) IMP ( Ex i A ) ∈ special axioms '' There are the axioms HF1 and HF2 for the set theory , while HF3 ( induction ) is formalised as an axiom scheme : inductive set induction axioms : : `` fm set '' where ind : '' atom ( j : :name ) ♯ ( i , A )
#15 ( which might involve the same variables ) requires many renaming steps to insert fresh variables , before substituting for them one term at a time . x1 = x1 ( x1 = x2 ) ∧ ( x3 = x4 ) → [ ( x1 = x3 ) → ( x2 = x4 ) ] ( x1 = x2 ) ∧ ( x3 = x4 ) → [ ( x1 ∈ x3 ) → ( x2 ∈ x4 ) ] ( x1 = x2 ) ∧ ( x3 = x4 ) → [ x1 ⊳ x3 = x2 ⊳ x4 ] There is also a specialisation axiom scheme , of the form φ ( t/x ) → ∃x φ : inductive set special axioms : : `` fm set '' where I : `` A ( i : :=x ) IMP ( Ex i A ) ∈ special axioms '' There are the axioms HF1 and HF2 for the set theory , while HF3 ( induction ) is formalised as an axiom scheme : inductive set induction axioms : : `` fm set '' where ind : '' atom ( j : :name ) ♯ ( i , A ) =⇒ A ( i : :=Zero ) IMP ( ( All i ( All j ( A IMP ( A ( i : := Var j ) IMP A ( i : := Eats ( Var i ) ( Var j ) ) ) ) ) ) IMP ( All i A ) ) ∈ induction axioms '' Axiom schemes are conveniently introduced using inductive set , simply to express set comprehensions , even though there is no actual induction . 3.1.3 Inference System The axiom schemes shown above , along with inference rules for modus ponens and existential instantiation,5 are combined to form the following inductive definition of theorems : 5 From A → B infer ∃xA → B , for x not free in B . 9 inductive hfthm : : `` fm set ⇒ fm ⇒ bool '' ( infixl `` ⊢ '' 55 ) where Hyp : `` A ∈ H =⇒ H ⊢ A '' | Extra : `` H ⊢ extra axiom '' | Bool : `` A ∈ boolean axioms =⇒ H ⊢ A '' | Eq : `` A ∈ equality axioms =⇒ H ⊢ A '' | Spec : `` A ∈ special axioms =⇒ H ⊢ A '' | HF : `` A ∈ HF axioms =⇒ H ⊢ A '' | Ind : `` A ∈ induction axioms =⇒ H ⊢ A '' | MP : `` H ⊢ A IMP B =⇒ H ’ ⊢ A =⇒ H ∪ H ’ ⊢ B '' | Exists : `` H ⊢ A IMP B =⇒ atom i♯B =⇒ ∀ C∈H . atom i♯C =⇒ H ⊢ ( Ex i A ) IMP B '' A minor deviation from Swierczkowski is ´ extra axiom , which is abstractly specified to
#16 are combined to form the following inductive definition of theorems : 5 From A → B infer ∃xA → B , for x not free in B . 9 inductive hfthm : : `` fm set ⇒ fm ⇒ bool '' ( infixl `` ⊢ '' 55 ) where Hyp : `` A ∈ H =⇒ H ⊢ A '' | Extra : `` H ⊢ extra axiom '' | Bool : `` A ∈ boolean axioms =⇒ H ⊢ A '' | Eq : `` A ∈ equality axioms =⇒ H ⊢ A '' | Spec : `` A ∈ special axioms =⇒ H ⊢ A '' | HF : `` A ∈ HF axioms =⇒ H ⊢ A '' | Ind : `` A ∈ induction axioms =⇒ H ⊢ A '' | MP : `` H ⊢ A IMP B =⇒ H ’ ⊢ A =⇒ H ∪ H ’ ⊢ B '' | Exists : `` H ⊢ A IMP B =⇒ atom i♯B =⇒ ∀ C∈H . atom i♯C =⇒ H ⊢ ( Ex i A ) IMP B '' A minor deviation from Swierczkowski is ´ extra axiom , which is abstractly specified to be an arbitrary true formula . This means that the proofs will be conducted with respect to an arbitrary finite extension of the HF theory . The first major deviation from Swierczkowski is the introduction of rule ´ Hyp , with a set of assumptions . It would be virtually impossible to prove anything in his Hilbert-style proof system , and it was clear from the outset that lengthy proofs within the calculus might be necessary . Introducing Hyp generalises the notion of provability , allowing the development of a sort of sequent calculus , in which long but tolerably natural proofs can be constructed . It is worth mentioning that Swierczkowski ’ s definitions and proofs fit together very ´ tightly , deviations often being a cause for later regret . One example , concerning an inference rule for substitution , is mentioned at the end of Sect . 4.4 . Another example is that some tricks that simplify the proof of the first incompleteness theorem turn out to complicate the proof of the second . The soundness of the calculus above is trivial to prove by induction . The deduction theorem is also straightforward , the only non-trivial case being the one for the Exists inference rule . The induction formula is stated as follows : lemma deduction Diff : assumes `` H ⊢ B '' shows `` H - { C } ⊢ C IMP B '' This directly yields the standard formulation of the deduction theorem : theorem deduction : assumes `` insert A H ⊢ B '' shows `` H ⊢ A IMP B '' And this is a sequent rule for implication . Setting up a usable sequent calculus requires much work . The corresponding Isabelle theory file , which starts with the definitions
#17 natural proofs can be constructed . It is worth mentioning that Swierczkowski ’ s definitions and proofs fit together very ´ tightly , deviations often being a cause for later regret . One example , concerning an inference rule for substitution , is mentioned at the end of Sect . 4.4 . Another example is that some tricks that simplify the proof of the first incompleteness theorem turn out to complicate the proof of the second . The soundness of the calculus above is trivial to prove by induction . The deduction theorem is also straightforward , the only non-trivial case being the one for the Exists inference rule . The induction formula is stated as follows : lemma deduction Diff : assumes `` H ⊢ B '' shows `` H - { C } ⊢ C IMP B '' This directly yields the standard formulation of the deduction theorem : theorem deduction : assumes `` insert A H ⊢ B '' shows `` H ⊢ A IMP B '' And this is a sequent rule for implication . Setting up a usable sequent calculus requires much work . The corresponding Isabelle theory file , which starts with the definitions of terms and formulas and ends with a sequent formulation of the HF induction rule , is nearly 1,600 lines long . Deriving natural sequent calculus rules from the sentential and equality axioms requires lengthy chains of steps . Even in the final derived sequent calculus , equalities can only be applied one step at a time . For another example of difficulty , consider the following definition : definition Fls where `` Fls ≡ Zero IN Zero '' Proving that Fls has the properties of falsehood is surprisingly tricky . The relevant axiom , HF1 , is formulated using universal quantifiers , which are defined as negated existentials ; deriving the expected properties of universal quantification seems to require something like Fls itself . The derived sequent calculus has specialised rules to operate on conjunctions , disjunctions , etc. , in the hypothesis part of a sequent . They are crude , but good enough . Used with Isabelle ’ s automatic tactics , they ease somewhat the task of constructing formal HF proofs . Users can extend Isabelle with proof procedures coded in ML , and better automation for the calculus might thereby be achieved . At the time , such a side-project did not seem to be worth the effort . 10 3.2 A Formal Theory of Functions Recursion is not available in HF set theory , and recursive functions must be constructed explicitly . Each recursive computation is expressed in terms of the existence of a sequence ( si ) i≤k such that si is related to sm and sn for m , n < i . Moreover , a sequence is formally a relation rather than a function . In the metalanguage , we write app s k for sk , governed by the theorem
#18 universal quantifiers , which are defined as negated existentials ; deriving the expected properties of universal quantification seems to require something like Fls itself . The derived sequent calculus has specialised rules to operate on conjunctions , disjunctions , etc. , in the hypothesis part of a sequent . They are crude , but good enough . Used with Isabelle ’ s automatic tactics , they ease somewhat the task of constructing formal HF proofs . Users can extend Isabelle with proof procedures coded in ML , and better automation for the calculus might thereby be achieved . At the time , such a side-project did not seem to be worth the effort . 10 3.2 A Formal Theory of Functions Recursion is not available in HF set theory , and recursive functions must be constructed explicitly . Each recursive computation is expressed in terms of the existence of a sequence ( si ) i≤k such that si is related to sm and sn for m , n < i . Moreover , a sequence is formally a relation rather than a function . In the metalanguage , we write app s k for sk , governed by the theorem lemma app equality : `` hfunction s =⇒ hx , yi ∈ s =⇒ app s x = y '' The following two functions express the recursive definition of sequences , as needed for the G¨odel development : '' Builds B C s l ≡ B ( app s l ) ∨ ( ∃ m∈l . ∃ n∈l . C ( app s l ) ( app s m ) ( app s n ) ) '' '' BuildSeq B C s k y ≡ LstSeq s k y ∧ ( ∀ l∈succ k. Builds B C s l ) '' The statement Builds B C s l constrains element l of sequence s , namely app s l. We have either B ( app s l ) , or C ( app s l ) ( app s m ) ( app s n ) ) where m∈l and n∈l . For the natural numbers , set membership coincides with the less-than relation . Therefore , we are referring to a sequence s and element sl where either the base case B ( sl ) holds , or else the recursive step C ( sl , sm , sn ) for m , n < l. The statement BuildSeq B C s k y states that the sequence s has been constructed in this way right up to the value app s k , or in other words , sk , where y = sk . To formalise the basis for this approach requires a series of definitions in the HF calculus , introducing the subset relation , ordinals ( which are simply natural numbers ) , ordered pairs , relations with a given domain , etc . Foundation ( the well-foundedness of the membership relation ) must also
#19 '' The statement Builds B C s l constrains element l of sequence s , namely app s l. We have either B ( app s l ) , or C ( app s l ) ( app s m ) ( app s n ) ) where m∈l and n∈l . For the natural numbers , set membership coincides with the less-than relation . Therefore , we are referring to a sequence s and element sl where either the base case B ( sl ) holds , or else the recursive step C ( sl , sm , sn ) for m , n < l. The statement BuildSeq B C s k y states that the sequence s has been constructed in this way right up to the value app s k , or in other words , sk , where y = sk . To formalise the basis for this approach requires a series of definitions in the HF calculus , introducing the subset relation , ordinals ( which are simply natural numbers ) , ordered pairs , relations with a given domain , etc . Foundation ( the well-foundedness of the membership relation ) must also be proved , which in turn requires additional definitions . A few highlights are shown below . The subset relation is defined , with infix syntax SUBS , with the help of All2 , the bounded universal quantifier . nominal primrec Subset : : `` tm ⇒ tm ⇒ fm '' ( infixr `` SUBS '' 150 ) where `` atom z ♯ ( t , u ) =⇒ t SUBS u = All2 z t ( ( Var z ) IN u ) '' In standard notation , this says t ⊆ u = ( ∀z ∈ t ) [ z ∈ u ] . The definition uses nominal primrec , even though it is not recursive , because it requires z to be fresh with respect to the terms t and u , among other nominal-related technicalities . Extensionality is taken as an axiom in traditional set theories , but in HF it can be proved by induction . However , many straightforward properties of the subset relation must first be derived . lemma Extensionality : `` H ⊢ x EQ y IFF x SUBS y AND y SUBS x '' Ordinals will be familiar to set theorists . The definition is the usual one , and shown below mainly as an example of a slightly more complicated HF formula . Two variables , y and z , must be fresh for each other and x. nominal primrec OrdP : : `` tm ⇒ fm '' where `` [ [ atom y ♯ ( x , z ) ; atom z ♯ x ] ] =⇒ OrdP x = All2 y x ( ( Var y ) SUBS x AND All2 z ( Var y ) ( ( Var z ) SUBS ( Var y ) ) )
#20 [ z ∈ u ] . The definition uses nominal primrec , even though it is not recursive , because it requires z to be fresh with respect to the terms t and u , among other nominal-related technicalities . Extensionality is taken as an axiom in traditional set theories , but in HF it can be proved by induction . However , many straightforward properties of the subset relation must first be derived . lemma Extensionality : `` H ⊢ x EQ y IFF x SUBS y AND y SUBS x '' Ordinals will be familiar to set theorists . The definition is the usual one , and shown below mainly as an example of a slightly more complicated HF formula . Two variables , y and z , must be fresh for each other and x. nominal primrec OrdP : : `` tm ⇒ fm '' where `` [ [ atom y ♯ ( x , z ) ; atom z ♯ x ] ] =⇒ OrdP x = All2 y x ( ( Var y ) SUBS x AND All2 z ( Var y ) ( ( Var z ) SUBS ( Var y ) ) ) '' The formal definition of a function ( as a single-valued set of pairs ) is subject to several complications . As we shall see in Sect . 3.3 below , all definitions must use Σ formulas , which requires certain non-standard formulations . In particular , x 6= y is not a Σ formula in general , but it can be expressed as x < y∨y < x if x and y are ordinals . The following primitive is used extensively when coding the syntax of HF within itself . 11 nominal primrec LstSeqP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where '' LstSeqP s k y = OrdP k AND HDomain Incl s ( SUCC k ) AND HFun Sigma s AND HPair k y IN s '' Informally , LstSeqP s k y means that s is a non-empty sequence whose domain includes the set { 0 , . . . , k } ( which is the ordinal k + 1 : the sequence is at least that long ) . Moreover , y = sk ; that would be written hk , yi ∈ s in the metalanguage , but becomes HPair k y IN s in the HF calculus , as seen above . Swierczkowski [ 32 ] prefers slightly different definitions , ´ specifying the domain to be exactly k , where k > 0 and y = sk−1 . The definition shown above simplifies the proof of the first incompleteness theorem , but complicates the proof of the second , in particular because they allow a sequence to be longer than necessary . This part of the development consists mainly of proofs in the HF calculus , and is nearly 1,300 lines long . 3.3 Σ Formulas and
#21 tm ⇒ tm ⇒ fm '' where '' LstSeqP s k y = OrdP k AND HDomain Incl s ( SUCC k ) AND HFun Sigma s AND HPair k y IN s '' Informally , LstSeqP s k y means that s is a non-empty sequence whose domain includes the set { 0 , . . . , k } ( which is the ordinal k + 1 : the sequence is at least that long ) . Moreover , y = sk ; that would be written hk , yi ∈ s in the metalanguage , but becomes HPair k y IN s in the HF calculus , as seen above . Swierczkowski [ 32 ] prefers slightly different definitions , ´ specifying the domain to be exactly k , where k > 0 and y = sk−1 . The definition shown above simplifies the proof of the first incompleteness theorem , but complicates the proof of the second , in particular because they allow a sequence to be longer than necessary . This part of the development consists mainly of proofs in the HF calculus , and is nearly 1,300 lines long . 3.3 Σ Formulas and Provability G¨odel had the foresight to recognise the value of minimising the need to write explicit formal proofs , without relying on the assumption that certain proofs could “ obviously ” be formalised . Instead , he developed enough meta-theory to prove that these proofs existed . One approach for this [ 2 , 32 ] relies on the concept of Σ formulas . These are inductively defined to include all formulas of the form t ∈ u , t = u , α ∨ β , α ∧ β , ∃x α and ( ∀x ∈ t ) α . ( These are closely related to the Σ1 formulas of the arithmetical hierarchy . ) It follows by induction on this construction that every true Σ sentence has a formal proof . Intuitively , the reasoning is that the atomic cases can be calculated , the Boolean cases can be done recursively , and the bounded universal quantifier can be replaced by a finite conjunction . The existential case holds because the semantics of ∃x α yields a specific witnessing value , again allowing an appeal to the induction hypothesis . The Σ formula approach is a good fit to the sort of formulas used in the coding of syntax . In these formulas , universal quantifiers have simple upper bounds , typically a variable giving the length of a sequence , while existential variables are unbounded . G¨odel ’ s original proofs required all quantifiers to be bounded . Existential quantifiers were bounded by complicated expressions requiring deep and difficult arithmetic justifications . Boolos presents similar material in a more modern form [ 2 , p. 41 ] . Relying exclusively on Σ formulas avoids these complications , but instead some straightforward properties have to be proven formally
#22 . ( These are closely related to the Σ1 formulas of the arithmetical hierarchy . ) It follows by induction on this construction that every true Σ sentence has a formal proof . Intuitively , the reasoning is that the atomic cases can be calculated , the Boolean cases can be done recursively , and the bounded universal quantifier can be replaced by a finite conjunction . The existential case holds because the semantics of ∃x α yields a specific witnessing value , again allowing an appeal to the induction hypothesis . The Σ formula approach is a good fit to the sort of formulas used in the coding of syntax . In these formulas , universal quantifiers have simple upper bounds , typically a variable giving the length of a sequence , while existential variables are unbounded . G¨odel ’ s original proofs required all quantifiers to be bounded . Existential quantifiers were bounded by complicated expressions requiring deep and difficult arithmetic justifications . Boolos presents similar material in a more modern form [ 2 , p. 41 ] . Relying exclusively on Σ formulas avoids these complications , but instead some straightforward properties have to be proven formally in the HF calculus . A complication is that proving the second incompleteness theorem requires another induction over Σ formulas . To minimise that proof effort , it helps to use as restrictive a definition as possible . The strict Σ formulas consist of all formulas of the form x ∈ y , α ∨ β , α ∧ β , ∃x α and ( ∀x ∈ y ) α . Here , x and y are not general terms , but variables . We further stipulate y not free in α in ( ∀x ∈ y ) α ; then in the main induction leading to the second incompleteness theorem , Case 2 of Lemma 9.7 [ 32 ] can be omitted . inductive ss fm : : `` fm ⇒ bool '' where MemI : `` ss fm ( Var i IN Var j ) '' | DisjI : `` ss fm A =⇒ ss fm B =⇒ ss fm ( A OR B ) '' | ConjI : `` ss fm A =⇒ ss fm B =⇒ ss fm ( A AND B ) '' | ExI : `` ss fm A =⇒ ss fm ( Ex i A ) '' | All2I : `` ss fm A =⇒ atom j ♯ ( i , A ) =⇒ ss fm ( All2 i ( Var j ) A ) '' 12 Now , a Σ formula is by definition one that is provably equivalent ( in HF ) to some strict Σ formula containing no additional free variables . In another minor oversight , Swierczkowski omits the free variable condition , but it is n ´ ecessary . definition Sigma fm : : `` fm ⇒ bool '' where `` Sigma fm A ←→ ( ∃ B.
#23 then in the main induction leading to the second incompleteness theorem , Case 2 of Lemma 9.7 [ 32 ] can be omitted . inductive ss fm : : `` fm ⇒ bool '' where MemI : `` ss fm ( Var i IN Var j ) '' | DisjI : `` ss fm A =⇒ ss fm B =⇒ ss fm ( A OR B ) '' | ConjI : `` ss fm A =⇒ ss fm B =⇒ ss fm ( A AND B ) '' | ExI : `` ss fm A =⇒ ss fm ( Ex i A ) '' | All2I : `` ss fm A =⇒ atom j ♯ ( i , A ) =⇒ ss fm ( All2 i ( Var j ) A ) '' 12 Now , a Σ formula is by definition one that is provably equivalent ( in HF ) to some strict Σ formula containing no additional free variables . In another minor oversight , Swierczkowski omits the free variable condition , but it is n ´ ecessary . definition Sigma fm : : `` fm ⇒ bool '' where `` Sigma fm A ←→ ( ∃ B. ss fm B ∧ supp B ⊆ supp A ∧ { } ⊢ A IFF B ) '' As always , Swierczkowski ’ s exposition is valuable , but far from compl ´ ete . Showing that Σ formulas include t ∈ u , t = u and ( ∀x ∈ t ) α for all terms t and u ( and not only for variables ) is far from obvious . These necessary facts are not even stated clearly . A crucial insight is to focus on proving that t ∈ u and t ⊆ u are Σ formulas . Consideration of the cases t ∈ 0 , t ∈ u1 ⊳ u2 , 0 ⊆ u , t1 ⊳ t2 ⊆ u shows that each reduces to false , true or a combination of simpler uses of ∈ or ⊆ . This observation suggests proving that t ∈ u and t ⊆ u are Σ formulas by mutual induction on the combined sizes of t and u. lemma Subset Mem sf lemma : '' size t + size u < n =⇒ Sigma fm ( t SUBS u ) ∧ Sigma fm ( t IN u ) '' The identical argument turns out to be needed for the second incompleteness theorem itself , formalised this time within the HF calculus . This coincidence should not be that surprising , as it is known that the second theorem could in principle be shown by formalising the first theorem within its own calculus . Now that we have taken care of t ⊆ u , proving that t = u is a Σ formula is trivial by extensionality , and the one remaining objective is ( ∀x ∈ t ) α . But with equality available , we can reduce
#24 . Consideration of the cases t ∈ 0 , t ∈ u1 ⊳ u2 , 0 ⊆ u , t1 ⊳ t2 ⊆ u shows that each reduces to false , true or a combination of simpler uses of ∈ or ⊆ . This observation suggests proving that t ∈ u and t ⊆ u are Σ formulas by mutual induction on the combined sizes of t and u. lemma Subset Mem sf lemma : '' size t + size u < n =⇒ Sigma fm ( t SUBS u ) ∧ Sigma fm ( t IN u ) '' The identical argument turns out to be needed for the second incompleteness theorem itself , formalised this time within the HF calculus . This coincidence should not be that surprising , as it is known that the second theorem could in principle be shown by formalising the first theorem within its own calculus . Now that we have taken care of t ⊆ u , proving that t = u is a Σ formula is trivial by extensionality , and the one remaining objective is ( ∀x ∈ t ) α . But with equality available , we can reduce this case to the strict Σ formula ( ∀x ∈ y ) α with the help of a lemma : lemma All2 term Iff : `` atom i ♯ t =⇒ atom j ♯ ( i , t , A ) =⇒ { } ⊢ ( All2 i t A ) IFF Ex j ( Var j EQ t AND All2 i ( Var j ) A ) '' This is simply ( ∀x ∈ t ) A ↔ ∃y [ y = t∧ ( ∀x ∈ y ) A ] expressed in the HF calculus , where it is easily proved . We could prove that ( ∀x ∈ t ) α is a Σ formula by induction on t , but this approach leads to complications . Virtually all predicates defined for the G¨odel development are carefully designed to take the form of Σ formulas . Here are two examples ; most such lemmas hold immediately by the construction of the given formula . lemma Subset sf : `` Sigma fm ( t SUBS u ) '' lemma LstSeqP sf : `` Sigma fm ( LstSeqP t u v ) '' The next milestone asserts that if α is a ground Σ formula ( and therefore a sentence ) and α evaluates to true , then α is a theorem . The proof is by induction on the size of the formula , and then by case analysis on its outer form . The case t ∈ u falls to a mutual induction with t ⊆ u resembling the one shown above . The case ( ∀x ∈ t ) α is effectively expanded to a conjunction . theorem Sigma fm imp thm : `` [ [ Sigma fm α ; ground fm α ; eval fm e0
#25 easily proved . We could prove that ( ∀x ∈ t ) α is a Σ formula by induction on t , but this approach leads to complications . Virtually all predicates defined for the G¨odel development are carefully designed to take the form of Σ formulas . Here are two examples ; most such lemmas hold immediately by the construction of the given formula . lemma Subset sf : `` Sigma fm ( t SUBS u ) '' lemma LstSeqP sf : `` Sigma fm ( LstSeqP t u v ) '' The next milestone asserts that if α is a ground Σ formula ( and therefore a sentence ) and α evaluates to true , then α is a theorem . The proof is by induction on the size of the formula , and then by case analysis on its outer form . The case t ∈ u falls to a mutual induction with t ⊆ u resembling the one shown above . The case ( ∀x ∈ t ) α is effectively expanded to a conjunction . theorem Sigma fm imp thm : `` [ [ Sigma fm α ; ground fm α ; eval fm e0 α ] ] =⇒ { } ⊢ α '' Every true Σ sentence is a theorem . This crucial meta-theoretic result is used eight times in the development . Without it , gigantic explicit HF proofs would be necessary . 4 Coding Provability in HF Within Itself The key insight leading to the proof of G¨odel ’ s theorem is that a sufficiently strong logical calculus can represent its syntax within itself , and in particular , the property of a given formula being provable . This task divides into three parts : coding the syntax , defining predicates to describe the coding and finally , defining predicates to describe the inference system . 13 4.1 Coding Terms , Formulas , Abstraction and Substitution In advocating the use of HF over PA , Swierczkowski begins by emphasising the ease of ´ coding syntax : It is at hand to code the variables x1 , x2 , . . . simply by the ordinals 1 , 2 , . . .. The constant 0 can be coded as 0 , and the remaining 6 symbols as n-tuples of 0s , say ∈ as h0 , 0i , etc . And here ends the arbitrariness of coding , which is so unpleasant when languages are arithmetized . [ 32 , p. 5 ] The adequacy of these definitions is easy to prove in HF itself . The full list is as follows : p0q = 0 , pxiq = i + 1 , p∈q = h0 , 0i , p⊳q = h0 , 0 , 0i , p=q = h0 , 0 , 0 , 0i , p∨q = h0 , 0 , 0 , 0 , 0i , p¬q = h0 , 0 , 0 , 0 , 0 , 0i
#26 describe the coding and finally , defining predicates to describe the inference system . 13 4.1 Coding Terms , Formulas , Abstraction and Substitution In advocating the use of HF over PA , Swierczkowski begins by emphasising the ease of ´ coding syntax : It is at hand to code the variables x1 , x2 , . . . simply by the ordinals 1 , 2 , . . .. The constant 0 can be coded as 0 , and the remaining 6 symbols as n-tuples of 0s , say ∈ as h0 , 0i , etc . And here ends the arbitrariness of coding , which is so unpleasant when languages are arithmetized . [ 32 , p. 5 ] The adequacy of these definitions is easy to prove in HF itself . The full list is as follows : p0q = 0 , pxiq = i + 1 , p∈q = h0 , 0i , p⊳q = h0 , 0 , 0i , p=q = h0 , 0 , 0 , 0i , p∨q = h0 , 0 , 0 , 0 , 0i , p¬q = h0 , 0 , 0 , 0 , 0 , 0i , p∃q = h0 , 0 , 0 , 0 , 0 , 0 , 0i . We have a few differences from Swierczkowski : ´ pxiq = i + 1 because our variables start at zero , and for the kth de Bruijn index we use hh0 , 0 , 0 , 0 , 0 , 0 , 0 , 0i , ki . Obviously ∈ means nothing by itself , so p∈q = h0 , 0i really means pt ∈ uq = hh0 , 0i , ptq , puqi , etc . Note that nests of n-tuples terminated by ordinals can be decomposed uniquely . De Bruijn equivalents of terms and formulas are then declared . To repeat : de Bruijn syntax is used for coding , for which it is ideal , allowing the simplest possible definitions of abstraction and substitution . Although it destroys readability , encodings are never readable anyway . Using nominal here is out of the question . The entire theory of nominal Isabelle would need to be formalised within the embedded calculus . Quite apart from the work involved , the necessary equivalence classes would be infinite sets , which are not available in HF . The strongest argument for HF is that the mathematical basis of its coding scheme is simply ordered pairs defined in the standard set-theoretic way . An elementary formal argument justifies this . In contrast , the usual arithmetic encoding relies on either the Chinese remainder theorem or unique prime factorisation . This fragment of number theory would have to be formalised within the embedded calculus in order to reason about encoded formulas , which is necessary to prove the second incompleteness theorem . It must be emphasised that proving anything in the calculus ( where such
#27 by ordinals can be decomposed uniquely . De Bruijn equivalents of terms and formulas are then declared . To repeat : de Bruijn syntax is used for coding , for which it is ideal , allowing the simplest possible definitions of abstraction and substitution . Although it destroys readability , encodings are never readable anyway . Using nominal here is out of the question . The entire theory of nominal Isabelle would need to be formalised within the embedded calculus . Quite apart from the work involved , the necessary equivalence classes would be infinite sets , which are not available in HF . The strongest argument for HF is that the mathematical basis of its coding scheme is simply ordered pairs defined in the standard set-theoretic way . An elementary formal argument justifies this . In contrast , the usual arithmetic encoding relies on either the Chinese remainder theorem or unique prime factorisation . This fragment of number theory would have to be formalised within the embedded calculus in order to reason about encoded formulas , which is necessary to prove the second incompleteness theorem . It must be emphasised that proving anything in the calculus ( where such luxuries as a simplifier , recursion and even function symbols are not available ) is much more difficult than proving the same result in a proof assistant . 4.1.1 Introducing de Bruijn Terms and Formulas De Bruijn terms resemble the type tm declared in Sect . 2.3 , but include the DBInd constructor for bound variable indices as well as the DBVar constructor for free variables . nominal datatype dbtm = DBZero | DBVar name | DBInd nat | DBEats dbtm dbtm De Bruijn formula contructors involve no explicit variable binding , creating an apparent similarity between DBNeg and DBEx , although the latter creates an implicit variable binding scope . nominal datatype dbfm = DBMem dbtm dbtm | DBEq dbtm dbtm | DBDisj dbfm dbfm | DBNeg dbfm | DBEx dbfm 14 How this works should become clear as we consider how terms and formulas are translated into their de Bruijn equivalents . To begin with , we need a lookup function taking a list of names ( representing variables bound in the current context , innermost first ) and a name to be looked up . The integer n , initially 0 , is the index to substitute if the name is next in the list . fun lookup : : `` name list ⇒ nat ⇒ name ⇒ dbtm '' where '' lookup [ ] n x = DBVar x '' | `` lookup ( y # ys ) n x = ( if x = y then DBInd n else ( lookup ys ( Suc n ) x ) ) '' To translate a term into de Bruijn format , the key step is to resolve name references using lookup . Names bound in the local environment are replaced by the corresponding indices , while other
#28 , although the latter creates an implicit variable binding scope . nominal datatype dbfm = DBMem dbtm dbtm | DBEq dbtm dbtm | DBDisj dbfm dbfm | DBNeg dbfm | DBEx dbfm 14 How this works should become clear as we consider how terms and formulas are translated into their de Bruijn equivalents . To begin with , we need a lookup function taking a list of names ( representing variables bound in the current context , innermost first ) and a name to be looked up . The integer n , initially 0 , is the index to substitute if the name is next in the list . fun lookup : : `` name list ⇒ nat ⇒ name ⇒ dbtm '' where '' lookup [ ] n x = DBVar x '' | `` lookup ( y # ys ) n x = ( if x = y then DBInd n else ( lookup ys ( Suc n ) x ) ) '' To translate a term into de Bruijn format , the key step is to resolve name references using lookup . Names bound in the local environment are replaced by the corresponding indices , while other names are left as they were . nominal primrec trans tm : : `` name list ⇒ tm ⇒ dbtm '' where '' trans tm e Zero = DBZero '' | `` trans tm e ( Var k ) = lookup e 0 k '' | `` trans tm e ( Eats t u ) = DBEats ( trans tm e t ) ( trans tm e u ) '' Noteworthy is the final case of trans fm , which requires the bound variable k in the quantified formula Ex k A to be fresh with respect to e , our list of previouslyencountered bound variables . In the recursive call , k is added to the list , which therefore consists of distinct names . nominal primrec trans fm : : `` name list ⇒ fm ⇒ dbfm '' where '' trans fm e ( Mem t u ) = DBMem ( trans tm e t ) ( trans tm e u ) '' | `` trans fm e ( Eq t u ) = DBEq ( trans tm e t ) ( trans tm e u ) '' | `` trans fm e ( Disj A B ) = DBDisj ( trans fm e A ) ( trans fm e B ) '' | `` trans fm e ( Neg A ) = DBNeg ( trans fm e A ) '' | `` atom k ♯ e =⇒ trans fm e ( Ex k A ) = DBEx ( trans fm ( k # e ) A ) '' Syntactic operations for de Bruijn notation tend to be straightforward , as there are no bound variable names that might clash . Comparisons with previous formalisations of the λ-calculus may be illuminating , but the usual lifting operation [
#29 our list of previouslyencountered bound variables . In the recursive call , k is added to the list , which therefore consists of distinct names . nominal primrec trans fm : : `` name list ⇒ fm ⇒ dbfm '' where '' trans fm e ( Mem t u ) = DBMem ( trans tm e t ) ( trans tm e u ) '' | `` trans fm e ( Eq t u ) = DBEq ( trans tm e t ) ( trans tm e u ) '' | `` trans fm e ( Disj A B ) = DBDisj ( trans fm e A ) ( trans fm e B ) '' | `` trans fm e ( Neg A ) = DBNeg ( trans fm e A ) '' | `` atom k ♯ e =⇒ trans fm e ( Ex k A ) = DBEx ( trans fm ( k # e ) A ) '' Syntactic operations for de Bruijn notation tend to be straightforward , as there are no bound variable names that might clash . Comparisons with previous formalisations of the λ-calculus may be illuminating , but the usual lifting operation [ 18 , 21 ] is unnecessary . That is because the HF calculus does not allow reductions anywhere , as in the λ-calculus . Substitutions only happen at the top level and never within deeper bound variable contexts . For us , substitution is the usual operation of replacing a variable by a term , which contains no bound variables . ( Substitution can alternatively be defined to replace a de Bruijn index by a term . ) The special de Bruijn operation is abstraction . This replaces every occurrence of a given free variable in a term or formula by a de Bruijn index , in preparation for binding . For example , abstracting the formula DBMem ( DBVar x ) ( DBVar y ) over the variable y yields DBMem ( DBVar x ) ( DBInd 0 ) . This is actually ill-formed , but attaching a quantifier yields the de Bruijn formula DBEx ( DBMem ( DBVar x ) ( DBInd 0 ) ) , representing ∃y [ x ∈ y ] . Abstracting this over the free variable x and attaching another quantifier yields DBEx ( DBEx ( DBMem ( DBInd 1 ) ( DBInd 0 ) ) ) , which is the formula ∃xy [ x ∈ y ] . An index of 1 has been substituted in order to skip over the inner binder . 15 4.1.2 Well-Formed de Bruijn Terms and Formulas With the de Bruijn approach , an index of 0 designates the innermost enclosing binder , while an index of 1 designates the next-innermost binder , etc . ( Here , the only binder is DBEx . ) If every index has a matching binder ( the index i must be nested within at least i + 1 binders ) ,
#30 by a de Bruijn index , in preparation for binding . For example , abstracting the formula DBMem ( DBVar x ) ( DBVar y ) over the variable y yields DBMem ( DBVar x ) ( DBInd 0 ) . This is actually ill-formed , but attaching a quantifier yields the de Bruijn formula DBEx ( DBMem ( DBVar x ) ( DBInd 0 ) ) , representing ∃y [ x ∈ y ] . Abstracting this over the free variable x and attaching another quantifier yields DBEx ( DBEx ( DBMem ( DBInd 1 ) ( DBInd 0 ) ) ) , which is the formula ∃xy [ x ∈ y ] . An index of 1 has been substituted in order to skip over the inner binder . 15 4.1.2 Well-Formed de Bruijn Terms and Formulas With the de Bruijn approach , an index of 0 designates the innermost enclosing binder , while an index of 1 designates the next-innermost binder , etc . ( Here , the only binder is DBEx . ) If every index has a matching binder ( the index i must be nested within at least i + 1 binders ) , then the term or formula is well-formed . Recall the examples of abstraction above , where a binder must be attached afterwards . In particular , as our terms do not contain any binding constructs , a well-formed term may contain no de Bruijn indices . In contrast to more traditional notions of logical syntax , if you take a well-formed formula and view one of its subformulas or subterms in isolation , it will not necessarily be well-formed . The situation is analogous to extracting a fragment of a program , removing it from necessary enclosing declarations . The property of being a well-formed de Bruijn term or formula is defined inductively . The syntactic predicates defined below recognise such well-formed formulas . A well-formed de Bruijn term has no indices ( DBInd ) at all : inductive wf dbtm : : `` dbtm ⇒ bool '' where Zero : `` wf dbtm DBZero '' | Var : `` wf dbtm ( DBVar name ) '' | Eats : `` wf dbtm t1 =⇒ wf dbtm t2 =⇒ wf dbtm ( DBEats t1 t2 ) '' A trivial induction shows that for every well-founded de Bruijn term there is an equivalent standard term . The only cases to be considered ( as per the definition above ) are Zero , Var and Eats . lemma wf dbtm imp is tm : assumes `` wf dbtm x '' shows `` ∃ t : :tm . x = trans tm [ ] t '' A well-formed de Bruijn formula is constructed from other well-formed terms and formulas , and indices can only be introduced by applying abstraction ( abst dbfm ) over a given name to another well-formed formula , in the existential case . Specifically , the Ex clause below
#31 property of being a well-formed de Bruijn term or formula is defined inductively . The syntactic predicates defined below recognise such well-formed formulas . A well-formed de Bruijn term has no indices ( DBInd ) at all : inductive wf dbtm : : `` dbtm ⇒ bool '' where Zero : `` wf dbtm DBZero '' | Var : `` wf dbtm ( DBVar name ) '' | Eats : `` wf dbtm t1 =⇒ wf dbtm t2 =⇒ wf dbtm ( DBEats t1 t2 ) '' A trivial induction shows that for every well-founded de Bruijn term there is an equivalent standard term . The only cases to be considered ( as per the definition above ) are Zero , Var and Eats . lemma wf dbtm imp is tm : assumes `` wf dbtm x '' shows `` ∃ t : :tm . x = trans tm [ ] t '' A well-formed de Bruijn formula is constructed from other well-formed terms and formulas , and indices can only be introduced by applying abstraction ( abst dbfm ) over a given name to another well-formed formula , in the existential case . Specifically , the Ex clause below states that , starting with a well-formed formula A , abstracting over some name and applying DBEx to the result yields another well-formed formula . inductive wf dbfm : : `` dbfm ⇒ bool '' where Mem : `` wf dbtm t1 =⇒ wf dbtm t2 =⇒ wf dbfm ( DBMem t1 t2 ) '' | Eq : `` wf dbtm t1 =⇒ wf dbtm t2 =⇒ wf dbfm ( DBEq t1 t2 ) '' | Disj : `` wf dbfm A1 =⇒ wf dbfm A2 =⇒ wf dbfm ( DBDisj A1 A2 ) '' | Neg : `` wf dbfm A =⇒ wf dbfm ( DBNeg A ) '' | Ex : `` wf dbfm A =⇒ wf dbfm ( DBEx ( abst dbfm name 0 A ) ) '' This definition formalises the allowed forms of construction , rather than stating explicitly that every index must have a matching binder . A refinement must be mentioned . Strong nominal induction ( already seen above , Sect . 2.3 ) formalises the assumption that bound variables revealed by induction can be assumed not to clash with other variables . This is set up automatically for nominal datatypes , but here requires a manual step . The command nominal inductive sets up strong induction for name in the Ex case of the inductive definition above ; we must prove that name is not significant according to the nominal theory , and then get to assume that name will not clash . This step ( details omitted ) seems to be necessary in order to complete some inductive proofs about wf dbfm . 16 4.1.3 Quoting Terms and Formulas It is essential to remember that G¨odel encodings are terms ( having type tm ) , not sets or numbers . Textbook
#32 dbfm A =⇒ wf dbfm ( DBNeg A ) '' | Ex : `` wf dbfm A =⇒ wf dbfm ( DBEx ( abst dbfm name 0 A ) ) '' This definition formalises the allowed forms of construction , rather than stating explicitly that every index must have a matching binder . A refinement must be mentioned . Strong nominal induction ( already seen above , Sect . 2.3 ) formalises the assumption that bound variables revealed by induction can be assumed not to clash with other variables . This is set up automatically for nominal datatypes , but here requires a manual step . The command nominal inductive sets up strong induction for name in the Ex case of the inductive definition above ; we must prove that name is not significant according to the nominal theory , and then get to assume that name will not clash . This step ( details omitted ) seems to be necessary in order to complete some inductive proofs about wf dbfm . 16 4.1.3 Quoting Terms and Formulas It is essential to remember that G¨odel encodings are terms ( having type tm ) , not sets or numbers . Textbook presentations identify terms with their denotations for the sake of clarity , but this can be confusing . The undecidable formula contains an encoding of itself in the form of a term . First , we must define codes for de Bruijn terms and formulas . function quot dbtm : : `` dbtm ⇒ tm '' where '' quot dbtm DBZero = Zero '' | `` quot dbtm ( DBVar name ) = ORD OF ( Suc ( nat of name name ) ) '' | `` quot dbtm ( DBInd k ) = HPair ( HTuple 6 ) ( ORD OF k ) '' | `` quot dbtm ( DBEats t u ) = HPair ( HTuple 1 ) ( HPair ( quot dbtm t ) ( quot dbtm u ) ) '' The codes of real terms and formulas ( for which we set up the overloaded ⌈· · ·⌉ syntax ) are obtained by first translating them to their de Bruijn equivalents and then encoding . We finally obtain facts such as the following : lemma quot Zero : `` ⌈Zero⌉ = Zero '' lemma quot Var : `` ⌈Var x⌉ = SUCC ( ORD OF ( nat of name x ) ) '' lemma quot Eats : `` ⌈Eats x y⌉ = HPair ( HTuple 1 ) ( HPair ⌈x⌉ ⌈y⌉ ) '' lemma quot Eq : `` ⌈x EQ y⌉ = HPair ( HTuple 2 ) ( HPair ( ⌈x⌉ ) ( ⌈y⌉ ) ) '' lemma quot Disj : `` ⌈A OR B⌉ = HPair ( HTuple 3 ) ( HPair ( ⌈A⌉ ) ( ⌈B⌉ ) ) '' lemma quot Ex : `` ⌈Ex i A⌉ = HPair ( HTuple 5 ) ( quot dbfm ( trans fm [ i ] A )
#33 ORD OF k ) '' | `` quot dbtm ( DBEats t u ) = HPair ( HTuple 1 ) ( HPair ( quot dbtm t ) ( quot dbtm u ) ) '' The codes of real terms and formulas ( for which we set up the overloaded ⌈· · ·⌉ syntax ) are obtained by first translating them to their de Bruijn equivalents and then encoding . We finally obtain facts such as the following : lemma quot Zero : `` ⌈Zero⌉ = Zero '' lemma quot Var : `` ⌈Var x⌉ = SUCC ( ORD OF ( nat of name x ) ) '' lemma quot Eats : `` ⌈Eats x y⌉ = HPair ( HTuple 1 ) ( HPair ⌈x⌉ ⌈y⌉ ) '' lemma quot Eq : `` ⌈x EQ y⌉ = HPair ( HTuple 2 ) ( HPair ( ⌈x⌉ ) ( ⌈y⌉ ) ) '' lemma quot Disj : `` ⌈A OR B⌉ = HPair ( HTuple 3 ) ( HPair ( ⌈A⌉ ) ( ⌈B⌉ ) ) '' lemma quot Ex : `` ⌈Ex i A⌉ = HPair ( HTuple 5 ) ( quot dbfm ( trans fm [ i ] A ) ) '' Note that HPair constructs an HF term denoting a pair , while HTuple n constructs an ( n+ 2 ) -tuple of zeros . Proofs often refer to the denotations of terms rather than to the terms themselves , so the functions q Eats , q Mem , q Eq , q Neg , q Disj , q Ex are defined to express these codes . Here are some examples : '' q Var i ≡ succ ( ord of ( nat of name i ) ) '' '' q Eats x y ≡ hhtuple 1 , x , yi '' '' q Disj x y ≡ hhtuple 3 , x , yi '' '' q Ex x ≡ hhtuple 5 , xi '' Note that hx , yi denotes the pair of x and y as sets , in other words , of type hf . 4.2 Predicates for the Coding of Syntax The next and most arduous step is to define logical predicates corresponding to each of the syntactic concepts ( terms , formulas , abstraction , substitution ) mentioned above . Textbooks and articles describe each predicate at varying levels of detail . G¨odel [ 8 ] gives full definitions , as does Swierczkowski . Boolos [ 2 ] gives many details of how coding i ´ s set up , and gives the predicates for terms and formulas , but not for any operations upon them . Hodel [ 13 ] , like many textbook authors , relies heavily on “ algorithms ” written in English . The definitions indeed amount to pages of computer code . Authors typically conclude with a “ theorem ” asserting the correctness of this code . For example , Swierczkowski [ 32 , Sect . 3–4 ] presents
#34 , yi '' '' q Disj x y ≡ hhtuple 3 , x , yi '' '' q Ex x ≡ hhtuple 5 , xi '' Note that hx , yi denotes the pair of x and y as sets , in other words , of type hf . 4.2 Predicates for the Coding of Syntax The next and most arduous step is to define logical predicates corresponding to each of the syntactic concepts ( terms , formulas , abstraction , substitution ) mentioned above . Textbooks and articles describe each predicate at varying levels of detail . G¨odel [ 8 ] gives full definitions , as does Swierczkowski . Boolos [ 2 ] gives many details of how coding i ´ s set up , and gives the predicates for terms and formulas , but not for any operations upon them . Hodel [ 13 ] , like many textbook authors , relies heavily on “ algorithms ” written in English . The definitions indeed amount to pages of computer code . Authors typically conclude with a “ theorem ” asserting the correctness of this code . For example , Swierczkowski [ 32 , Sect . 3–4 ] presents 34 highly technical ´ definitions , justified by seven lines of proof . Proving the correctness of this lengthy series of definitions requires a substantial effort , and the proofs ( being syntactically oriented ) are tiresome . It is helpful to introduce shadow versions of all predicates in Isabelle/HOL ’ s native logic , as well as in HF . Having two versions of each predicate simplifies the task of relating the HF version of 17 the predicate to the syntactic concept that it is intended to represent ; the first step is to prove that the HF formula is equivalent to the syntactically similar definition written in Isabelle ’ s higher-order logic , which then is proved to satisfy deeper properties . The shadow predicates also give an easy way to refer to the truth of the corresponding HF predicate ; because each is defined to be a Σ formula , that gives a quick way ( using theorem Sigma fm imp thm above ) to show that some ground instance of the predicate can be proved formally in HF . Also , one way to arrive at the correct definition of an HF predicate is to define its shadow equivalent first , since proving that it implies the required properties is much easier in Isabelle/HOL ’ s native logic than in HF . Swierczkowski [ 32 ] defines a full set of syntactic predicate ´ s , leaving nothing as an exercise . Unfortunately , the introduction of de Bruijn syntax necessitates rewriting many of these definitions . Some predicates ( such as the variable occurrence test ) are replaced by others ( abstraction over a variable occurrence ) . The final list includes predicates to recognise the following items : – the codes of well-formed terms
#35 is equivalent to the syntactically similar definition written in Isabelle ’ s higher-order logic , which then is proved to satisfy deeper properties . The shadow predicates also give an easy way to refer to the truth of the corresponding HF predicate ; because each is defined to be a Σ formula , that gives a quick way ( using theorem Sigma fm imp thm above ) to show that some ground instance of the predicate can be proved formally in HF . Also , one way to arrive at the correct definition of an HF predicate is to define its shadow equivalent first , since proving that it implies the required properties is much easier in Isabelle/HOL ’ s native logic than in HF . Swierczkowski [ 32 ] defines a full set of syntactic predicate ´ s , leaving nothing as an exercise . Unfortunately , the introduction of de Bruijn syntax necessitates rewriting many of these definitions . Some predicates ( such as the variable occurrence test ) are replaced by others ( abstraction over a variable occurrence ) . The final list includes predicates to recognise the following items : – the codes of well-formed terms ( and constant terms , without variables ) – correct instances of abstraction ( of a term or formula ) over a variable – correct instances of substitution ( in a term or formula ) for a variable – the codes of well-formed formulas As explained below , abstraction over a formula needs to be defined before the notion of a formula itself . We also need the property of variable non-occurrence , “ x does not occur in A ” , which can be expressed directly as “ substituting 0 for x in A yields A ” . This little trick eliminates the need for a full definition . Each operation is first defined in its sequence form ( expressing that sequence s is built up in an appropriate way and that sk is a specific value ) ; existential quantification over s and k then yields the final predicate . Formalising the sequence of steps is a primitive way to express recursion . Moreover , it tends to yield Σ formulas . The simplest example is the predicate for constants . The shadow predicate can be defined with the help of BuildSeq , mentioned in Sect . 3.2 above . Note that shadow predicates are written in ordinary higher-order logic , and refer to syntactic codes using set values . We see below that in the sequence buildup , each element is either 0 ( which is the code of the constant zero ) or else has the form q Eats v w , which is the code for v ⊳ w. definition SeqConst : : `` hf ⇒ hf ⇒ hf ⇒ bool '' where `` SeqConst s k t ≡ BuildSeq ( λu . u=0 ) ( λu v w. u = q Eats v w
#36 little trick eliminates the need for a full definition . Each operation is first defined in its sequence form ( expressing that sequence s is built up in an appropriate way and that sk is a specific value ) ; existential quantification over s and k then yields the final predicate . Formalising the sequence of steps is a primitive way to express recursion . Moreover , it tends to yield Σ formulas . The simplest example is the predicate for constants . The shadow predicate can be defined with the help of BuildSeq , mentioned in Sect . 3.2 above . Note that shadow predicates are written in ordinary higher-order logic , and refer to syntactic codes using set values . We see below that in the sequence buildup , each element is either 0 ( which is the code of the constant zero ) or else has the form q Eats v w , which is the code for v ⊳ w. definition SeqConst : : `` hf ⇒ hf ⇒ hf ⇒ bool '' where `` SeqConst s k t ≡ BuildSeq ( λu . u=0 ) ( λu v w. u = q Eats v w ) s k t '' Thus a constant expression is built up from 0 using the ⊳ operator . The idea is that every element of the sequence is either 0 or has the form px ⊳ yq , where x and y occur earlier in the sequence . Most of the other syntactic predicates fit exactly the same pattern , but with different base cases and constructors . A function must be coded as a relation , and a typical base case might be h0 , 0i , other sequence elements having the form hpx ⊳ yq , px ′ ⊳ y ′ qi , where hx , x′ i and hy , y′ i occur earlier in the sequence . Substitution is codified in this manner . A function taking two arguments is coded as a sequence of triples , etc . The discussion above relates to shadow predicates , which define formulas of Isabelle/HOL relating HF sets . The real predicates , which denote formulas of the HF calculus , are based on exactly the same ideas except that the various set constructions must be expressed using the HF term language . Note that the real predicates typically have names ending with P. 18 The following formula again specifies the notion of a constant term . It is simply the result of expressing the definition of SeqConst using HF syntax , expanding the definition of BuildSeq . The syntactic sugar for a reference to a sequence element sm within some formula φ must now be expanded to its true form : φ ( sm ) becomes ∃y [ hm , yi ∈ s∧φ ( y ) ] . nominal primrec SeqConstP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` [ [ atom
#37 ′ ⊳ y ′ qi , where hx , x′ i and hy , y′ i occur earlier in the sequence . Substitution is codified in this manner . A function taking two arguments is coded as a sequence of triples , etc . The discussion above relates to shadow predicates , which define formulas of Isabelle/HOL relating HF sets . The real predicates , which denote formulas of the HF calculus , are based on exactly the same ideas except that the various set constructions must be expressed using the HF term language . Note that the real predicates typically have names ending with P. 18 The following formula again specifies the notion of a constant term . It is simply the result of expressing the definition of SeqConst using HF syntax , expanding the definition of BuildSeq . The syntactic sugar for a reference to a sequence element sm within some formula φ must now be expanded to its true form : φ ( sm ) becomes ∃y [ hm , yi ∈ s∧φ ( y ) ] . nominal primrec SeqConstP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` [ [ atom l ♯ ( s , k , sl , m , n , sm , sn ) ; atom sl ♯ ( s , m , n , sm , sn ) ; atom m ♯ ( s , n , sm , sn ) ; atom n ♯ ( s , sm , sn ) ; atom sm ♯ ( s , sn ) ; atom sn ♯ ( s ) ] ] =⇒ SeqConstP s k t = LstSeqP s k t AND All2 l ( SUCC k ) ( Ex sl ( HPair ( Var l ) ( Var sl ) IN s AND ( Var sl EQ Zero OR Ex m ( Ex n ( Ex sm ( Ex sn ( Var m IN Var l AND Var n IN Var l AND HPair ( Var m ) ( Var sm ) IN s AND HPair ( Var n ) ( Var sn ) IN s AND Var sl EQ Q Eats ( Var sm ) ( Var sn ) ) ) ) ) ) ) ) '' We have five bound variables , namely l , sl , m , sm , n , sn , which must be constrained to be distinct from one another using the freshness conditions shown . This nominal boilerplate may seem excessive . However , to define this predicate without nominal syntax , bound variable names might have to be calculated , perhaps by taking the maximum of the bound variables in s , k and t and continuing from there . Nominal constrains the variables more abstractly and flexibly . As mentioned above , sometimes we deal with sequences of pairs or triples , with correspondingly more complicated formulas . Where a predicate describes a function such as
#38 ( Var sl ) IN s AND ( Var sl EQ Zero OR Ex m ( Ex n ( Ex sm ( Ex sn ( Var m IN Var l AND Var n IN Var l AND HPair ( Var m ) ( Var sm ) IN s AND HPair ( Var n ) ( Var sn ) IN s AND Var sl EQ Q Eats ( Var sm ) ( Var sn ) ) ) ) ) ) ) ) '' We have five bound variables , namely l , sl , m , sm , n , sn , which must be constrained to be distinct from one another using the freshness conditions shown . This nominal boilerplate may seem excessive . However , to define this predicate without nominal syntax , bound variable names might have to be calculated , perhaps by taking the maximum of the bound variables in s , k and t and continuing from there . Nominal constrains the variables more abstractly and flexibly . As mentioned above , sometimes we deal with sequences of pairs or triples , with correspondingly more complicated formulas . Where a predicate describes a function such as substitution , the sequence being built up consists of ordered pairs of arguments and results , and there are typically nine bound variables . To perform abstraction over a formula requires keeping track of the depth of quantifier nesting during recursion . This is a two-argument function , so the sequence being built up consists of ordered triples and there are 12 bound variables . Although the nominal system copes with these complicated expressions , the processing time can be measured in tens of seconds . Now that we have defined the buildup of a sequence of constants , a constant itself is trivial . The existence of any properly formed sequence s of length k culminating with some term t guarantees that t is a constant term . Here are both the shadow and HF calculus versions of the predicate . definition Const : : `` hf ⇒ bool '' where `` Const t ≡ ( ∃ s k. SeqConst s k t ) '' nominal primrec ConstP : : `` tm ⇒ fm '' where `` [ [ atom k ♯ ( s , t ) ; atom s ♯ t ] ] =⇒ ConstP t = Ex s ( Ex k ( SeqConstP ( Var s ) ( Var k ) t ) ) '' Why don ’ t we define the HF predicate BuildSeqP analogously to BuildSeq , which expresses the definition of SeqConst so succinctly ? Then we might expect to avoid the mess above , defining a predicate such as SeqConstP in a single line . This was actually attempted , but the nominal system is not really suitable for formalising higher-order definitions . Complicated auxiliary definitions and proofs are required . It is easier simply to write out the definitions , especially as
#39 constant itself is trivial . The existence of any properly formed sequence s of length k culminating with some term t guarantees that t is a constant term . Here are both the shadow and HF calculus versions of the predicate . definition Const : : `` hf ⇒ bool '' where `` Const t ≡ ( ∃ s k. SeqConst s k t ) '' nominal primrec ConstP : : `` tm ⇒ fm '' where `` [ [ atom k ♯ ( s , t ) ; atom s ♯ t ] ] =⇒ ConstP t = Ex s ( Ex k ( SeqConstP ( Var s ) ( Var k ) t ) ) '' Why don ’ t we define the HF predicate BuildSeqP analogously to BuildSeq , which expresses the definition of SeqConst so succinctly ? Then we might expect to avoid the mess above , defining a predicate such as SeqConstP in a single line . This was actually attempted , but the nominal system is not really suitable for formalising higher-order definitions . Complicated auxiliary definitions and proofs are required . It is easier simply to write out the definitions , especially as their very repetitiveness allows proof development by cut and paste . One tiny consolidation has been done . We need to define the predicates Term and TermP analogously to Const and ConstP above but allowing variables . The question of whether variables are allowed in a term or not can be governed by a Boolean . The proof development therefore introduces the predicate SeqCTermP , taking a Boolean argument , from which SeqTermP and SeqConstP are trivially obtained . 19 abbreviation SeqTermP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` SeqTermP ≡ SeqCTermP True '' abbreviation SeqConstP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` SeqConstP ≡ SeqCTermP False '' In this way , we can define the very similar predicates TermP and ConstP with a minimum of repeated material . Many other predicates must be defined . Abstraction and substitution must be defined separately for terms , atomic formulas and formulas . Here are the shadow definitions of abstraction and substitution for terms . They are similar enough ( both involve replacing a variable ) that a single function , SeqStTerm , can express both . BuildSeq2 is similar to BuildSeq above , but constructs a sequence of pairs . definition SeqStTerm : : `` hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool '' where `` SeqStTerm v u x x ’ s k ≡ is Var v ∧ BuildSeq2 ( λy y ’ . ( is Ind y ∨ Ord y ) ∧ y ’ = ( if y=v then u else y ) ) ( λu u ’ v v ’ w w ’ . u = q Eats v w ∧ u ’ = q Eats v ’ w ’ )
#40 abbreviation SeqConstP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` SeqConstP ≡ SeqCTermP False '' In this way , we can define the very similar predicates TermP and ConstP with a minimum of repeated material . Many other predicates must be defined . Abstraction and substitution must be defined separately for terms , atomic formulas and formulas . Here are the shadow definitions of abstraction and substitution for terms . They are similar enough ( both involve replacing a variable ) that a single function , SeqStTerm , can express both . BuildSeq2 is similar to BuildSeq above , but constructs a sequence of pairs . definition SeqStTerm : : `` hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool '' where `` SeqStTerm v u x x ’ s k ≡ is Var v ∧ BuildSeq2 ( λy y ’ . ( is Ind y ∨ Ord y ) ∧ y ’ = ( if y=v then u else y ) ) ( λu u ’ v v ’ w w ’ . u = q Eats v w ∧ u ’ = q Eats v ’ w ’ ) s k x x ’ '' definition AbstTerm : : `` hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool '' where `` AbstTerm v i x x ’ ≡ Ord i ∧ ( ∃ s k. SeqStTerm v ( q Ind i ) x x ’ s k ) '' definition SubstTerm : : `` hf ⇒ hf ⇒ hf ⇒ hf ⇒ bool '' where `` SubstTerm v u x x ’ ≡ Term u ∧ ( ∃ s k. SeqStTerm v u x x ’ s k ) '' Abstraction over formulas ( AbstForm/AbstFormP ) must be defined before formulas themselves , in order to formalise existential quantification . There is no circularity here : the abstraction operation can be defined independently of the notion of a well-formed formula , and is not restricted to them . The definition involves sequences of triples and is too complicated to present here . With abstraction over formulas defined , we can finally define the concept of a formula itself . An Atomic formula involves two terms , combined using the relations EQ or IN . Then MakeForm combines one or two existing formulas to build more complex ones . It constrains y to be the code of a formula constructed from existing formulas u and v by the disjunction u ∨ v , the negation ¬u or the existential formula ∃ ( u ’ ) , where u ’ has been obtained by abstracting u over some variable , v via the predicate AbstForm . definition MakeForm : : `` hf ⇒ hf ⇒ hf ⇒ bool '' where `` MakeForm y u w ≡ y = q Disj u w ∨ y = q Neg u ∨ ( ∃ v u ’ . AbstForm v 0 u u
#41 defined before formulas themselves , in order to formalise existential quantification . There is no circularity here : the abstraction operation can be defined independently of the notion of a well-formed formula , and is not restricted to them . The definition involves sequences of triples and is too complicated to present here . With abstraction over formulas defined , we can finally define the concept of a formula itself . An Atomic formula involves two terms , combined using the relations EQ or IN . Then MakeForm combines one or two existing formulas to build more complex ones . It constrains y to be the code of a formula constructed from existing formulas u and v by the disjunction u ∨ v , the negation ¬u or the existential formula ∃ ( u ’ ) , where u ’ has been obtained by abstracting u over some variable , v via the predicate AbstForm . definition MakeForm : : `` hf ⇒ hf ⇒ hf ⇒ bool '' where `` MakeForm y u w ≡ y = q Disj u w ∨ y = q Neg u ∨ ( ∃ v u ’ . AbstForm v 0 u u ’ ∧ y = q Ex u ’ ) '' nominal primrec MakeFormP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` [ [ atom v ♯ ( y , u , w , au ) ; atom au ♯ ( y , u , w ) ] ] =⇒ MakeFormP y u w = y EQ Q Disj u w OR y EQ Q Neg u OR Ex v ( Ex au ( AbstFormP ( Var v ) Zero u ( Var au ) AND y EQ Q Ex ( Var au ) ) ) '' Now , the sequence buildup of a formula can be defined with Atomic covering the base case and MakeForm expressing one level of the construction . Using similar methods to those illustrated above for constant terms , we arrive at the shadow predicate Form and the corresponding HF predicate FormP . 4.3 Verifying the Coding Predicates Most textbook presentations take the correctness of such definitions as obvious , and indeed many properties are not difficult to prove . To show that the predicate Term 20 accepts all coded terms , a necessary lemma is to show the analogous property for well-formed de Bruijn terms : lemma wf Term quot dbtm : assumes `` wf dbtm u '' shows `` Term [ [ quot dbtm u ] ] e '' The proof is by induction on the construction of u ( in other words , on the inductive definition of wf dbtm u ) , and is routine by the definitions of the predicates Term and SeqTerm . This implies the desired result for terms , by the ( overloaded ) definition of ⌈t⌉ . corollary Term quot tm : fixes t : :tm shows `` Term [ [ ⌈t⌉
#42 '' Now , the sequence buildup of a formula can be defined with Atomic covering the base case and MakeForm expressing one level of the construction . Using similar methods to those illustrated above for constant terms , we arrive at the shadow predicate Form and the corresponding HF predicate FormP . 4.3 Verifying the Coding Predicates Most textbook presentations take the correctness of such definitions as obvious , and indeed many properties are not difficult to prove . To show that the predicate Term 20 accepts all coded terms , a necessary lemma is to show the analogous property for well-formed de Bruijn terms : lemma wf Term quot dbtm : assumes `` wf dbtm u '' shows `` Term [ [ quot dbtm u ] ] e '' The proof is by induction on the construction of u ( in other words , on the inductive definition of wf dbtm u ) , and is routine by the definitions of the predicates Term and SeqTerm . This implies the desired result for terms , by the ( overloaded ) definition of ⌈t⌉ . corollary Term quot tm : fixes t : :tm shows `` Term [ [ ⌈t⌉ ] ] e '' Note that both results concern the shadow predicate Term , not the HF predicate TermP . The argument of Term is a set , denoted using the evaluation operator , [ [ ... ] ] e. Direct proofs about HF predicates are long and tiresome . Fortunately , many such questions can be reduced to the corresponding questions involving shadow predicates , because codes are ground terms ; then the theorem Sigma fm imp thm guarantees the existence of a proof , sparing us the need to construct one . The converse correctness property must also be proved , namely that everything accepted by Term actually is the code of some term . The proof requires a lemma about the predicate SeqTerm . The reasoning is simply that constants and variables are wellformed , and that combining two well-formed terms preserves this property . Such proofs are streamlined through the use of BuildSeq induct , a derived rule for reasoning about sequence construction by induction on the length of the sequence . lemma Term imp wf dbtm : assumes `` Term x '' obtains t : :dbtm where `` wf dbtm t '' `` x = [ [ quot dbtm t ] ] e '' By the meaning of obtains , we see that if Term x then there exists some well-formed de Bruijn term t whose code evaluates to x . Since for every well-formed de Bruijn term there exists an equivalent standard term of type tm , we can conclude that Term x implies that x is the code of some term . corollary Term imp is tm : assumes `` Term x '' obtains t : :tm where `` x = [ [ ⌈t⌉ ] ] e '' Similar theorems—with similar proofs—are necessary
#43 be proved , namely that everything accepted by Term actually is the code of some term . The proof requires a lemma about the predicate SeqTerm . The reasoning is simply that constants and variables are wellformed , and that combining two well-formed terms preserves this property . Such proofs are streamlined through the use of BuildSeq induct , a derived rule for reasoning about sequence construction by induction on the length of the sequence . lemma Term imp wf dbtm : assumes `` Term x '' obtains t : :dbtm where `` wf dbtm t '' `` x = [ [ quot dbtm t ] ] e '' By the meaning of obtains , we see that if Term x then there exists some well-formed de Bruijn term t whose code evaluates to x . Since for every well-formed de Bruijn term there exists an equivalent standard term of type tm , we can conclude that Term x implies that x is the code of some term . corollary Term imp is tm : assumes `` Term x '' obtains t : :tm where `` x = [ [ ⌈t⌉ ] ] e '' Similar theorems—with similar proofs—are necessary for each of the syntactic predicates . For example , the following result expresses that SubstForm correctly models the result A ( i : :=t ) of substituting t for i in the formula A. lemma SubstForm quot unique : '' SubstForm ( q Var i ) [ [ ⌈t⌉ ] ] e [ [ ⌈A⌉ ] ] e x ’ ←→ x ’ = [ [ ⌈A ( i : :=t ) ⌉ ] ] e '' 4.4 Predicates for the Coding of Deduction On the whole , the formalisation of deduction is quite different from the formalisation of syntactic operations , which mostly involve simulated recursion over terms or formulas . A proof step in the HF calculus is an axiom , an axiom scheme or an inference rule . Axioms and propositional inference rules are straightforward to recognise using the existing syntactic primitives . Simply x EQ ⌈refl ax⌉ tests whether x denotes the reflexivity axiom . More complicated are inference rules involving quantification , where several syntactic conditions including abstraction and substitution need to be checked in sequence . For example , consider specialisation axioms of the form φ ( t/x ) → ∃x φ . 21 nominal primrec Special axP : : `` tm ⇒ fm '' where '' [ [ atom v ♯ ( p , sx , y , ax , x ) ; atom x ♯ ( p , sx , y , ax ) ; atom ax ♯ ( p , sx , y ) ; atom y ♯ ( p , sx ) ; atom sx ♯ p ] ] =⇒ Special axP p = Ex v ( Ex x ( Ex ax ( Ex y ( Ex sx ( FormP ( Var x ) AND VarP ( Var v
#44 syntactic operations , which mostly involve simulated recursion over terms or formulas . A proof step in the HF calculus is an axiom , an axiom scheme or an inference rule . Axioms and propositional inference rules are straightforward to recognise using the existing syntactic primitives . Simply x EQ ⌈refl ax⌉ tests whether x denotes the reflexivity axiom . More complicated are inference rules involving quantification , where several syntactic conditions including abstraction and substitution need to be checked in sequence . For example , consider specialisation axioms of the form φ ( t/x ) → ∃x φ . 21 nominal primrec Special axP : : `` tm ⇒ fm '' where '' [ [ atom v ♯ ( p , sx , y , ax , x ) ; atom x ♯ ( p , sx , y , ax ) ; atom ax ♯ ( p , sx , y ) ; atom y ♯ ( p , sx ) ; atom sx ♯ p ] ] =⇒ Special axP p = Ex v ( Ex x ( Ex ax ( Ex y ( Ex sx ( FormP ( Var x ) AND VarP ( Var v ) AND TermP ( Var y ) AND AbstFormP ( Var v ) Zero ( Var x ) ( Var ax ) AND SubstFormP ( Var v ) ( Var y ) ( Var x ) ( Var sx ) AND p EQ Q Imp ( Var sx ) ( Q Ex ( Var ax ) ) ) ) ) ) ) '' This definition states that a specialisation axiom is created from a formula x , a variable v and a term y , combined by appropriate abstraction and substitution operations . Correctness means proving that this predicate exactly characterises the elements of the set special axioms , which was used to define the HF calculus . The most complicated such scheme is the induction axiom HF3 ( defined in Sect . 2.2 ) , with its three quantifiers . The treatment of the induction axiom requires nearly 180 lines , of which 120 are devoted to proving correctness with respect to the HF calculus . A proof of a theorem y is a sequence s of axioms and inference rules , ending with y : definition Prf : : `` hf ⇒ hf ⇒ hf ⇒ bool '' where `` Prf s k y ≡ BuildSeq ( λx . x ∈ Axiom ) ( λu v w. ModPon v w u ∨ Exists v u ∨ Subst v u ) s k Finally , y codes a theorem provided it has a proof : definition Pf : : `` hf ⇒ bool '' where `` Pf y ≡ ( ∃ s k. Prf s k y ) '' Having proved the correctness of the predicates formalising the axioms and rules , the correctness of Pf follows easily . ( Swierczkowski ’ s seven lines of proof start here
#45 characterises the elements of the set special axioms , which was used to define the HF calculus . The most complicated such scheme is the induction axiom HF3 ( defined in Sect . 2.2 ) , with its three quantifiers . The treatment of the induction axiom requires nearly 180 lines , of which 120 are devoted to proving correctness with respect to the HF calculus . A proof of a theorem y is a sequence s of axioms and inference rules , ending with y : definition Prf : : `` hf ⇒ hf ⇒ hf ⇒ bool '' where `` Prf s k y ≡ BuildSeq ( λx . x ∈ Axiom ) ( λu v w. ModPon v w u ∨ Exists v u ∨ Subst v u ) s k Finally , y codes a theorem provided it has a proof : definition Pf : : `` hf ⇒ bool '' where `` Pf y ≡ ( ∃ s k. Prf s k y ) '' Having proved the correctness of the predicates formalising the axioms and rules , the correctness of Pf follows easily . ( Swierczkowski ’ s seven lines of proof start here . ) ´ One direction is proved by induction on the proof of { } ⊢ α. lemma proved imp Pf : assumes `` H ⊢ α '' `` H= { } '' shows `` Pf [ [ ⌈α⌉ ] ] e '' Here , we use the shadow predicates and work directly in Isabelle/HOL . The corresponding HF predicate , PfP , is ( crucially ) a Σ formula . Moreover , codes are ground terms . Therefore PfP ⌈α⌉ is a Σ sentence and is formally provable . This is the main use of the theorem Sigma fm imp thm . corollary proved imp proved PfP : `` { } ⊢ α =⇒ { } ⊢ PfP ⌈α⌉ '' The reverse implication , despite its usefulness , is not always proved . Again using the rule BuildSeq induct , it holds by induction on the length of the coded proof of ⌈α⌉ . The groundwork for this result involves proving , for each coded axiom and inference rule , that there exists a corresponding proof step in the HF calculus . We continue to work at the level of shadow predicates . lemma Prf imp proved : assumes `` Prf s k x '' shows `` ∃ A. x = [ [ ⌈A⌉ ] ] e ∧ { } ⊢ A '' The corresponding result for Pf is immediate : corollary Pf quot imp is proved : `` Pf [ [ ⌈α⌉ ] ] e =⇒ { } ⊢ α '' Now { } ⊢ PfP ⌈α⌉ implies Pf [ [ ⌈α⌉ ] ] e simply by the soundness of the calculus . It is now easy to show that the predicate PfP corresponds exactly to deduction in the HF calculus . Swierczkowski calls this result the ´
#46 imp thm . corollary proved imp proved PfP : `` { } ⊢ α =⇒ { } ⊢ PfP ⌈α⌉ '' The reverse implication , despite its usefulness , is not always proved . Again using the rule BuildSeq induct , it holds by induction on the length of the coded proof of ⌈α⌉ . The groundwork for this result involves proving , for each coded axiom and inference rule , that there exists a corresponding proof step in the HF calculus . We continue to work at the level of shadow predicates . lemma Prf imp proved : assumes `` Prf s k x '' shows `` ∃ A. x = [ [ ⌈A⌉ ] ] e ∧ { } ⊢ A '' The corresponding result for Pf is immediate : corollary Pf quot imp is proved : `` Pf [ [ ⌈α⌉ ] ] e =⇒ { } ⊢ α '' Now { } ⊢ PfP ⌈α⌉ implies Pf [ [ ⌈α⌉ ] ] e simply by the soundness of the calculus . It is now easy to show that the predicate PfP corresponds exactly to deduction in the HF calculus . Swierczkowski calls this result the ´ proof formalisation condition . theorem proved iff proved PfP : `` { } ⊢ α ←→ { } ⊢ PfP ⌈α⌉ '' 22 Remark : PfP includes an additional primitive inference , substitution : H ⊢ α H ⊢ α ( t/x ) This inference is derivable in the HF calculus , but the second incompleteness theorem requires performing substitution inferences , and reconstructing the derivation of substitution within PfP would be infeasible . Including substitution in the definition of PfP makes such steps immediate without complicating other proofs . Swierczkowski avoids ´ this complication : his HF calculus [ 32 ] includes a substitution rule alongside a simpler specialisation axiom . 4.5 Pseudo-Functions The HF calculus contains no function symbols other than ⊳ . All other “ functions ” must be declared as predicates , which are mere abbreviations of formulas . This abuse of notation is understood in a standard way . The formula φ ( f ( x ) ) can be taken as an abbreviation for ∃y [ F ( x , y ) ∧ φ ( y ) ] where F is the relation representing the function f and provided that F can be proved to be single valued : F ( x , y ) , F ( x , y′ ) ⊢ y ′ = y . Then f is called a pseudo-function and something like f ( x ) is called a pseudo-term . Pseudo-terms do not actually exist , which will cause problems later . G¨odel formalised all syntactic operations as primitive recursive functions , while Boolos [ 2 ] used ∆ formulas . With both approaches , much effort is necessary to admit a function definition in the first place . But then , it is known to be a
#47 32 ] includes a substitution rule alongside a simpler specialisation axiom . 4.5 Pseudo-Functions The HF calculus contains no function symbols other than ⊳ . All other “ functions ” must be declared as predicates , which are mere abbreviations of formulas . This abuse of notation is understood in a standard way . The formula φ ( f ( x ) ) can be taken as an abbreviation for ∃y [ F ( x , y ) ∧ φ ( y ) ] where F is the relation representing the function f and provided that F can be proved to be single valued : F ( x , y ) , F ( x , y′ ) ⊢ y ′ = y . Then f is called a pseudo-function and something like f ( x ) is called a pseudo-term . Pseudo-terms do not actually exist , which will cause problems later . G¨odel formalised all syntactic operations as primitive recursive functions , while Boolos [ 2 ] used ∆ formulas . With both approaches , much effort is necessary to admit a function definition in the first place . But then , it is known to be a function . Here we see a drawback of Swierczkowski ’ s decision to base the formalisation on the n ´ otion of Σ formulas : they do not cover the property of being single valued . A predicate that corresponds to a function must be proved to be single valued within the HF calculus itself . G¨odel ’ s proof uses substitution as a function . The proof that substitution ( on terms and formulas ) is single valued requires nearly 500 lines in Isabelle/HOL , not counting considerable preparatory material ( such as the partial ordering properties of < ) mentioned in Sect . 3.2 above . Fortunately , these proofs are conceptually simple and highly repetitious , and again much of the proof development can be done by cut and paste . The first step is to prove an unfolding lemma about the sequence buildup : if the predicate holds , then either the base case holds , or else there exist values earlier in the sequence for which one of the recursive cases can be applied . The single valued theorem is proved by complete induction on the length of the sequence , with a fully quantified induction formula ( analogous to ∀xyy′ [ F ( x , y ) → F ( x , y′ ) → y ′ = y ] ) so that the induction hypothesis says that all shorter sequences are single valued for all possible arguments . All that is left is to apply the unfolding lemma to both instances of the relation F , and then to consider all combinations of cases . Most will be trivially contradictory , and in those few cases where the result has the same outer form , an appeal to the induction hypothesis for the
#48 ) mentioned in Sect . 3.2 above . Fortunately , these proofs are conceptually simple and highly repetitious , and again much of the proof development can be done by cut and paste . The first step is to prove an unfolding lemma about the sequence buildup : if the predicate holds , then either the base case holds , or else there exist values earlier in the sequence for which one of the recursive cases can be applied . The single valued theorem is proved by complete induction on the length of the sequence , with a fully quantified induction formula ( analogous to ∀xyy′ [ F ( x , y ) → F ( x , y′ ) → y ′ = y ] ) so that the induction hypothesis says that all shorter sequences are single valued for all possible arguments . All that is left is to apply the unfolding lemma to both instances of the relation F , and then to consider all combinations of cases . Most will be trivially contradictory , and in those few cases where the result has the same outer form , an appeal to the induction hypothesis for the operands will complete the proof . Overall , the G¨odel development proves single valued theorems for 12 predicates . Five of the theorems are proved by induction as sketched above . Here is an example : lemma SeqSubstFormP unique : '' { SeqSubstFormP v a x y s u , SeqSubstFormP v a x y ’ s ’ u ’ } ⊢ y ’ EQ y '' The remaining results are straightforward corollaries of those inductions : 23 theorem SubstFormP unique : '' { SubstFormP v tm x y , SubstFormP v tm x y ’ } ⊢ y ’ EQ y '' It is worth repeating that these proofs are formally conducted within the HF calculus , essentially by single-step inferences . Meta-theory is no help here . 5 G¨odel ’ s First Incompleteness Theorem Discussions involving encodings frequently need a way to refer to syntactic objects . We often see the convention where if x is a natural number , then a boldface x stands for the corresponding numeral . Then in expressions like x = y → Pf px = yq , we see that the boldface convention actually abbreviates the function x 7→ x , which needs to be formalisable in the HF calculus . Thus , we need to define a function Q such that Q ( x ) = pxq , in other words , Q ( x ) yields some term t whose denotation is x . This is trivial if x ranges over the natural numbers , by primitive recursion . It is problematical when x ranges over sets , because it requires a canonical ordering over the universe of sets . We don ’ t need to solve this problem just yet : the first incompleteness theorem needs only a function
#49 EQ y '' It is worth repeating that these proofs are formally conducted within the HF calculus , essentially by single-step inferences . Meta-theory is no help here . 5 G¨odel ’ s First Incompleteness Theorem Discussions involving encodings frequently need a way to refer to syntactic objects . We often see the convention where if x is a natural number , then a boldface x stands for the corresponding numeral . Then in expressions like x = y → Pf px = yq , we see that the boldface convention actually abbreviates the function x 7→ x , which needs to be formalisable in the HF calculus . Thus , we need to define a function Q such that Q ( x ) = pxq , in other words , Q ( x ) yields some term t whose denotation is x . This is trivial if x ranges over the natural numbers , by primitive recursion . It is problematical when x ranges over sets , because it requires a canonical ordering over the universe of sets . We don ’ t need to solve this problem just yet : the first incompleteness theorem needs only a function H such that H ( pAq ) = ppAqq for all A . Possible arguments of H are not arbitrary sets , but only nested tuples of ordinals ; these have a canonical form , so a functional relationship is easy to define [ 32 ] . A certain amount of effort establishes the required property:6 lemma prove HRP : fixes A : :fm shows `` { } ⊢ HRP ⌈A⌉ ⌈⌈A⌉⌉ '' Note that the function H has been formalised as the relation HRP ; it is defined using sequence operators , LstSeqP , etc. , as we have seen already . In order to prove G¨odel ’ s diagonal lemma , we need a function Ki to substitute the code of a formula into itself , replacing the variable xi . This function , again , is realised as a relation , combining HRP with SubstFormP . nominal primrec KRP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` atom y ♯ ( v , x , x ’ ) =⇒ KRP v x x ’ = Ex y ( HRP x ( Var y ) AND SubstFormP v ( Var y ) x x ’ ) '' We easily obtain a key result : Ki ( pαq ) = pα ( i : = pαq ) q. lemma prove KRP : `` { } ⊢ KRP ⌈Var i⌉ ⌈α⌉ ⌈α ( i : :=⌈α⌉ ) ⌉ '' However , it is essential to prove that KRP behaves like a function . The predicates KRP and HRP can be proved to be single valued using the techniques discussed in the previous section . Then an appeal to prove KRP uniquely characterises Ki as a function : lemma KRP subst fm : `` { KRP
#50 seen already . In order to prove G¨odel ’ s diagonal lemma , we need a function Ki to substitute the code of a formula into itself , replacing the variable xi . This function , again , is realised as a relation , combining HRP with SubstFormP . nominal primrec KRP : : `` tm ⇒ tm ⇒ tm ⇒ fm '' where `` atom y ♯ ( v , x , x ’ ) =⇒ KRP v x x ’ = Ex y ( HRP x ( Var y ) AND SubstFormP v ( Var y ) x x ’ ) '' We easily obtain a key result : Ki ( pαq ) = pα ( i : = pαq ) q. lemma prove KRP : `` { } ⊢ KRP ⌈Var i⌉ ⌈α⌉ ⌈α ( i : :=⌈α⌉ ) ⌉ '' However , it is essential to prove that KRP behaves like a function . The predicates KRP and HRP can be proved to be single valued using the techniques discussed in the previous section . Then an appeal to prove KRP uniquely characterises Ki as a function : lemma KRP subst fm : `` { KRP ⌈Var i⌉ ⌈α⌉ ( Var j ) } ⊢ Var j EQ ⌈α ( i : :=⌈α⌉ ) ⌉ '' Twenty five lines of tricky reasoning are needed to reach the next milestone : the diagonal lemma . Swierczkowski writes ´ We replace the variable xi in α by the [ pseudo-term Ki ( xi ) ] , and we denote by β the resulting formula . [ 32 , p. 22 ] The elimination of the pseudo-function Ki in favour of an existential quantifier involving KRP yields the following not-entirely-obvious Isabelle definition : 6 Here fixes A : :fm declares A to be a formula in the overloaded notation ⌈A⌉ . Swierczkowski ´ uses α , β , . . . to denote formulas , but I ’ ve frequently used the traditional A , B , . . . . 24 theorem Goedel I : assumes `` ¬ { } ⊢ Fls '' obtains δ where `` { } ⊢ δ IFF Neg ( PfP ⌈δ⌉ ) '' `` ¬ { } ⊢ δ '' `` ¬ { } ⊢ Neg δ '' '' eval fm e δ '' `` ground fm δ '' proof - fix i : :name obtain δ where `` { } ⊢ δ IFF Neg ( ( PfP ( Var i ) ) ( i : :=⌈δ⌉ ) ) '' and suppd : `` supp δ = supp ( Neg ( PfP ( Var i ) ) ) - { atom i } '' by ( metis SyntaxN.Neg diagonal ) then have diag : `` { } ⊢ δ IFF Neg ( PfP ⌈δ⌉ ) '' by simp then have np : `` ¬ { } ⊢ δ ∧ ¬ { } ⊢ Neg δ '' by ( metis Iff MP same NegNeg
#51 declares A to be a formula in the overloaded notation ⌈A⌉ . Swierczkowski ´ uses α , β , . . . to denote formulas , but I ’ ve frequently used the traditional A , B , . . . . 24 theorem Goedel I : assumes `` ¬ { } ⊢ Fls '' obtains δ where `` { } ⊢ δ IFF Neg ( PfP ⌈δ⌉ ) '' `` ¬ { } ⊢ δ '' `` ¬ { } ⊢ Neg δ '' '' eval fm e δ '' `` ground fm δ '' proof - fix i : :name obtain δ where `` { } ⊢ δ IFF Neg ( ( PfP ( Var i ) ) ( i : :=⌈δ⌉ ) ) '' and suppd : `` supp δ = supp ( Neg ( PfP ( Var i ) ) ) - { atom i } '' by ( metis SyntaxN.Neg diagonal ) then have diag : `` { } ⊢ δ IFF Neg ( PfP ⌈δ⌉ ) '' by simp then have np : `` ¬ { } ⊢ δ ∧ ¬ { } ⊢ Neg δ '' by ( metis Iff MP same NegNeg D Neg D Neg cong assms proved iff proved PfP ) then have `` eval fm e δ '' using hfthm sound [ where e=e , OF diag ] by simp ( metis Pf quot imp is proved ) moreover have `` ground fm δ '' using suppd by ( simp add : supp conv fresh ground fm aux def subset eq ) ( metis fresh ineq at base ) ultimately show ? thesis by ( metis diag np that ) qed Fig . 1 G¨odel ’ s First Incompleteness Theorem def β ≡ `` Ex j ( KRP ⌈Var i⌉ ( Var i ) ( Var j ) AND α ( i : := Var j ) ) '' Note that one occurrence of Var i is quoted and the other is not . The development is full of pitfalls such as these . The statement of the diagonal lemma is as follows . The second assertion states that the free variables of δ , the diagonal formula , are those of α , the original formula , minus i. lemma diagonal : obtains δ where `` { } ⊢ δ IFF α ( i : :=⌈δ⌉ ) '' `` supp δ = supp α - { atom i } '' Figure 1 presents the proof of the first incompleteness theorem itself . The top level argument is quite simple , given the diagonal lemma . The key steps of the proof should be visible even to somebody who is not an Isabelle expert , thanks to the structured Isar language . Note that if { } ⊢ Neg δ , then { } ⊢ PfP ⌈δ⌉ and therefore { } ⊢ δ by the proof formalisation condition , violating the assumption of consistency . 6 Towards the Second
#52 i⌉ ( Var i ) ( Var j ) AND α ( i : := Var j ) ) '' Note that one occurrence of Var i is quoted and the other is not . The development is full of pitfalls such as these . The statement of the diagonal lemma is as follows . The second assertion states that the free variables of δ , the diagonal formula , are those of α , the original formula , minus i. lemma diagonal : obtains δ where `` { } ⊢ δ IFF α ( i : :=⌈δ⌉ ) '' `` supp δ = supp α - { atom i } '' Figure 1 presents the proof of the first incompleteness theorem itself . The top level argument is quite simple , given the diagonal lemma . The key steps of the proof should be visible even to somebody who is not an Isabelle expert , thanks to the structured Isar language . Note that if { } ⊢ Neg δ , then { } ⊢ PfP ⌈δ⌉ and therefore { } ⊢ δ by the proof formalisation condition , violating the assumption of consistency . 6 Towards the Second Theorem : Pseudo-Coding and Quotations The second incompleteness theorem [ 1 ] has always been more mysterious than the first . G¨odel ’ s original paper [ 8 ] was designated “ Part I ” in anticipation of a subsequent “ Part II ” proving the second theorem , but no second paper appeared . Logicians recognised that the second theorem followed from the first , assuming that the first could itself be formalised in the internal calculus . While this assumption seems to be widely accepted , conducting such a formalisation explicitly remains difficult , even given today ’ s theoremproving technology . 25 A simpler route to the theorem involves the Hilbert-Bernays derivability conditions [ 2 , p. 15 ] [ 9 , p. 73 ] . If ⊢ α , then ⊢ Pf ( pαq ) ( D1 ) If ⊢ Pf ( pα → βq ) and ⊢ Pf ( pαq ) , then ⊢ Pf ( pβq ) ( D2 ) If α is a strict Σ sentence , then ⊢ α → Pf ( pαq ) ( D3 ) ( Where there is no ambiguity , we identify Pf with the formalised predicate PfP ; the latter is the actual HF predicate , but the notation Pf is widely used in the literature , along with G¨odel ’ s original Bew . ) Condition ( D1 ) is none other than the theorem proved iff proved PfP mentioned in Sect . 4.4 above . Condition ( D2 ) seems clear by the definition of the predicate Pf , although all details of the workings of this predicate must be proved using low-level inferences in the HF calculus . Condition ( D3 ) can be regarded as a version of the theorem Sigma fm imp
#53 s theoremproving technology . 25 A simpler route to the theorem involves the Hilbert-Bernays derivability conditions [ 2 , p. 15 ] [ 9 , p. 73 ] . If ⊢ α , then ⊢ Pf ( pαq ) ( D1 ) If ⊢ Pf ( pα → βq ) and ⊢ Pf ( pαq ) , then ⊢ Pf ( pβq ) ( D2 ) If α is a strict Σ sentence , then ⊢ α → Pf ( pαq ) ( D3 ) ( Where there is no ambiguity , we identify Pf with the formalised predicate PfP ; the latter is the actual HF predicate , but the notation Pf is widely used in the literature , along with G¨odel ’ s original Bew . ) Condition ( D1 ) is none other than the theorem proved iff proved PfP mentioned in Sect . 4.4 above . Condition ( D2 ) seems clear by the definition of the predicate Pf , although all details of the workings of this predicate must be proved using low-level inferences in the HF calculus . Condition ( D3 ) can be regarded as a version of the theorem Sigma fm imp thm ( “ true Σ sentences are theorems ” ) internalised as a theorem of the internal calculus . So while we avoid having to formalise the whole of G¨odel ’ s theorem within the calculus , we end up formalising a key part of it . Condition ( D3 ) is stated in a general form , but we only need one specific instance : ⊢ Pf ( pαq ) → Pf ( pPf ( pαq ) q ) . Despite a superficial resemblance , ( D3 ) does not follow from ( D1 ) , which holds by induction on the proof of ⊢ α . As Swierczkowski explains [ 32 , p. 23 ] , condition ( D3 ) is ´ not general enough to prove by induction . In the sequel , we generalise and prove it . 6.1 Pseudo-Coding Condition ( D3 ) can be proved by induction on α if the assertion is generalised so that α can have free variables , say x1 , . . . , xn : ⊢ α ( x1 , . . . , xn ) → Pf ( pα ( x1 , . . . , xn ) q ) The syntactic constructions used in this formula have to be formalised , and the necessary transformations have to be justified within the HF calculus . As mentioned above ( Sect . 5 ) , the boldface convention needs to be made rigorous . In particular , codings are always ground HF terms , and yet pα ( x1 , . . . , xn ) q has a functional dependence ( as an HF term ) on x1 , . . . , xn . The first step in this process is to generalise coding to allow
#54 induction on the proof of ⊢ α . As Swierczkowski explains [ 32 , p. 23 ] , condition ( D3 ) is ´ not general enough to prove by induction . In the sequel , we generalise and prove it . 6.1 Pseudo-Coding Condition ( D3 ) can be proved by induction on α if the assertion is generalised so that α can have free variables , say x1 , . . . , xn : ⊢ α ( x1 , . . . , xn ) → Pf ( pα ( x1 , . . . , xn ) q ) The syntactic constructions used in this formula have to be formalised , and the necessary transformations have to be justified within the HF calculus . As mentioned above ( Sect . 5 ) , the boldface convention needs to be made rigorous . In particular , codings are always ground HF terms , and yet pα ( x1 , . . . , xn ) q has a functional dependence ( as an HF term ) on x1 , . . . , xn . The first step in this process is to generalise coding to allow certain variables to be preserved as variables in the coded term . Recall that with normal quotations , every occurrence of a variable is replaced by the code of the variable name , ultimately a positive integer:7 function quot dbtm : : `` dbtm ⇒ tm '' where '' quot dbtm DBZero = Zero '' | `` quot dbtm ( DBVar name ) = ORD OF ( Suc ( nat of name name ) ) '' | ... Now let us define the V -code of a term or formula , where V is a set of variables to be preserved in the code : 7 ORD OF ( Suc n ) denotes an HF term that denotes a positive integer , even if n is a variable . 26 function vquot dbtm : : `` name set ⇒ dbtm ⇒ tm '' where '' vquot dbtm V DBZero = Zero '' | `` vquot dbtm V ( DBVar name ) = ( if name ∈ V then Var name else ORD OF ( Suc ( nat of name name ) ) ) '' | ... V -coding is otherwise identical to standard coding , with the overloaded syntax ⌊A⌋V . The parameter V is necessary because not all variables should be preserved ; it will be necessary to consider a series of V -codes for V = ∅ , { x1 } . . . , { x1 , . . . , xn } . 6.2 Simultaneous Substitution In order to formalise the notation pα ( x1 , . . . , xn ) q , it is convenient to introduce a function for simultaneous substitution . Here Swierczkowski ’ s presentation is a little ´ hard to follow : Suppose β is a theorem , i.e. ,
#55 preserved in the code : 7 ORD OF ( Suc n ) denotes an HF term that denotes a positive integer , even if n is a variable . 26 function vquot dbtm : : `` name set ⇒ dbtm ⇒ tm '' where '' vquot dbtm V DBZero = Zero '' | `` vquot dbtm V ( DBVar name ) = ( if name ∈ V then Var name else ORD OF ( Suc ( nat of name name ) ) ) '' | ... V -coding is otherwise identical to standard coding , with the overloaded syntax ⌊A⌋V . The parameter V is necessary because not all variables should be preserved ; it will be necessary to consider a series of V -codes for V = ∅ , { x1 } . . . , { x1 , . . . , xn } . 6.2 Simultaneous Substitution In order to formalise the notation pα ( x1 , . . . , xn ) q , it is convenient to introduce a function for simultaneous substitution . Here Swierczkowski ’ s presentation is a little ´ hard to follow : Suppose β is a theorem , i.e. , ⊢ β . If we replace each of the variables at each of its free occurrences in β by some constant term then the formula so obtained is also a theorem ( by the Substitution Rule . . . ) . This just described situation in the meta-theory admits description in HF . [ 32 , p. 24 ] It took me weeks of failed attempts to grasp the meaning of the phrase “ constant term ” . It does not mean a term containing no variables , but a term satisfying the predicate ConstP and thus denoting the code of a constant . Formalising this process seems to require replacing each variable xi by a new variable , x ′ i , intended to denote xi . Later , it will be constrained to do so by a suitable HF predicate . And so we need a function to perform simultaneous substitutions in a term for all variables in a set V . Using a “ fold ” operator over finite sets [ 19 ] eliminates the need to consider the variables in any particular order . definition ssubst : : `` tm ⇒ name set ⇒ ( name ⇒ tm ) ⇒ tm '' where `` ssubst t V F = Finite Set.fold ( λi . subst i ( F i ) ) t V '' The renaming of xi to x ′ i could be done using arithmetic on variable subscripts , but the formalisation instead follows an abstract approach , using nominal primitives . An Isabelle locale defines a proof context containing a permutation p ( mapping all variable names to new ones ) , a finite set Vs of variable names and finally the actual renaming function F , which simply applies the permutation to
#56 of a constant . Formalising this process seems to require replacing each variable xi by a new variable , x ′ i , intended to denote xi . Later , it will be constrained to do so by a suitable HF predicate . And so we need a function to perform simultaneous substitutions in a term for all variables in a set V . Using a “ fold ” operator over finite sets [ 19 ] eliminates the need to consider the variables in any particular order . definition ssubst : : `` tm ⇒ name set ⇒ ( name ⇒ tm ) ⇒ tm '' where `` ssubst t V F = Finite Set.fold ( λi . subst i ( F i ) ) t V '' The renaming of xi to x ′ i could be done using arithmetic on variable subscripts , but the formalisation instead follows an abstract approach , using nominal primitives . An Isabelle locale defines a proof context containing a permutation p ( mapping all variable names to new ones ) , a finite set Vs of variable names and finally the actual renaming function F , which simply applies the permutation to any variable in Vs. 8 locale quote perm = fixes p : : perm and Vs : : `` name set '' and F : : `` name ⇒ tm '' assumes p : `` atom ‘ ( p · Vs ) ♯ * Vs '' and pinv : `` -p = p '' and Vs : `` finite Vs '' defines `` F ≡ make F Vs p '' Most proofs about ssubst are done within the context of this locale , because it provides sufficient conditions for the simultaneous substitution to be meaningful . The first condition states that p maps all the variables in Vs to variables outside of that set , while second condition states that p is its own inverse . This abstract approach is a little unwieldy at times , but its benefits can be seen in the simple fact below , which states the effect of the simultaneous substitution on a single variable . 8 make F Vs p i = Var ( p · i ) provided i ∈ Vs. 27 lemma ssubst Var if : assumes `` finite V '' shows `` ssubst ( Var i ) V F = ( if i ∈ V then F i else Var i ) '' We need to show that the variables in the set Vs can be renamed , one at a time , in a pseudo-coded de Bruijn term . Let V ⊆ Vs and suppose that the variables in V have already been renamed , and choose one of the remaining variables , w. It will be replaced by a new variable , computed by F w. And something very subtle is happening : the variable w is represented in the term by its code , ⌈Var w⌉ . Its
#57 that p maps all the variables in Vs to variables outside of that set , while second condition states that p is its own inverse . This abstract approach is a little unwieldy at times , but its benefits can be seen in the simple fact below , which states the effect of the simultaneous substitution on a single variable . 8 make F Vs p i = Var ( p · i ) provided i ∈ Vs. 27 lemma ssubst Var if : assumes `` finite V '' shows `` ssubst ( Var i ) V F = ( if i ∈ V then F i else Var i ) '' We need to show that the variables in the set Vs can be renamed , one at a time , in a pseudo-coded de Bruijn term . Let V ⊆ Vs and suppose that the variables in V have already been renamed , and choose one of the remaining variables , w. It will be replaced by a new variable , computed by F w. And something very subtle is happening : the variable w is represented in the term by its code , ⌈Var w⌉ . Its replacement , F w , is Var ( p · w ) and a variable . lemma SubstTermP vquot dbtm : assumes w : `` w ∈ Vs - V '' and V : `` V ⊆ Vs '' `` V ’ = p · V '' and s : `` supp dbtm ⊆ atom ‘ Vs '' shows '' insert ( ConstP ( F w ) ) { ConstP ( F i ) | i. i ∈ V } ⊢ SubstTermP ⌈Var w⌉ ( F w ) ( ssubst ( vquot dbtm V dbtm ) V F ) ( subst w ( F w ) ( ssubst ( vquot dbtm ( insert w V ) dbtm ) V F ) ) '' This theorem is proved by structural induction on dbtm , the de Bruijn term . The condition supp dbtm ⊆ atom ‘ Vs states that the free variables of dbtm all belong to Vs . The variable case of the induction is tricky ( and is the crux of the entire proof ) . We are working with a coded term that contains both coded variables and real ones ( of the form F i ) ; it is necessary to show that the real variables are preserved by the substitution , because they are the xi that we are trying to introduce . The F i are preserved under the assumption that they denote constants , which is the point of including the formulas ConstP ( F i ) for all i ∈ V on the left side of the turnstile . These assumptions will have to be justified later . Under virtually the same assumptions ( omitted ) , the analogous result holds for pseudo-coded de Bruijn formulas . lemma SubstFormP vquot dbfm : ''
#58 subst w ( F w ) ( ssubst ( vquot dbtm ( insert w V ) dbtm ) V F ) ) '' This theorem is proved by structural induction on dbtm , the de Bruijn term . The condition supp dbtm ⊆ atom ‘ Vs states that the free variables of dbtm all belong to Vs . The variable case of the induction is tricky ( and is the crux of the entire proof ) . We are working with a coded term that contains both coded variables and real ones ( of the form F i ) ; it is necessary to show that the real variables are preserved by the substitution , because they are the xi that we are trying to introduce . The F i are preserved under the assumption that they denote constants , which is the point of including the formulas ConstP ( F i ) for all i ∈ V on the left side of the turnstile . These assumptions will have to be justified later . Under virtually the same assumptions ( omitted ) , the analogous result holds for pseudo-coded de Bruijn formulas . lemma SubstFormP vquot dbfm : '' insert ( ConstP ( F w ) ) { ConstP ( F i ) | i. i ∈ V } ⊢ SubstFormP ⌈Var w⌉ ( F w ) ( ssubst ( vquot dbfm V dbfm ) V F ) ( subst w ( F w ) ( ssubst ( vquot dbfm ( insert w V ) dbfm ) V F ) ) '' The proof is an easy structural induction on dbfm . Every case holds immediately by properties of substitution and the induction hypotheses or by the previous theorem , for terms . The only difficult case in these two proofs is the variable case discussed above . Using the notation for V -coding , we can see that the substitution predicate SubstFormP can transform the term ssubst ⌊A⌋V V F into ssubst ⌊A⌋ ( insert w V ) ( insert w V ) F. Repeating this step , we can replace any finite set of variables in a coded formula by real ones , realising Swierczkowski ’ s remark quoted at the top of this section , an ´ d in particular his last sentence . That is , if β is a theorem in HF ( if ⊢ Pf β holds ) then the result of substituting constants for its variables is also an HF theorem . More precisely still , we are replacing some subset V of the variables by fresh variables ( the F i ) , constrained by the predicate ConstP . theorem PfP implies PfP ssubst : fixes β : :fm assumes β : `` { } ⊢ PfP ⌈β⌉ '' and V : `` V ⊆ Vs '' and s : `` supp β ⊆ atom ‘ Vs '' shows `` { ConstP ( F i ) | i. i ∈ V
#59 two proofs is the variable case discussed above . Using the notation for V -coding , we can see that the substitution predicate SubstFormP can transform the term ssubst ⌊A⌋V V F into ssubst ⌊A⌋ ( insert w V ) ( insert w V ) F. Repeating this step , we can replace any finite set of variables in a coded formula by real ones , realising Swierczkowski ’ s remark quoted at the top of this section , an ´ d in particular his last sentence . That is , if β is a theorem in HF ( if ⊢ Pf β holds ) then the result of substituting constants for its variables is also an HF theorem . More precisely still , we are replacing some subset V of the variables by fresh variables ( the F i ) , constrained by the predicate ConstP . theorem PfP implies PfP ssubst : fixes β : :fm assumes β : `` { } ⊢ PfP ⌈β⌉ '' and V : `` V ⊆ Vs '' and s : `` supp β ⊆ atom ‘ Vs '' shows `` { ConstP ( F i ) | i. i ∈ V } ⊢ PfP ( ssubst ⌊β⌋V V F ) '' 28 The effort needed to formalise the results outlined above is relatively modest , at 330 lines of Isabelle/HOL , but this excludes the effort needed to prove some essential lemmas , which state that the various syntactic predicates work correctly . Because these proofs concern non-ground HF formulas , theorem Sigma fm imp thm does not help . Required is an HF formalisation of operations on sequences , such as concatenation . That in turn requires formalising further operations such as addition and set union . These proofs ( which are conducted largely in the HF calculus ) total over 2,800 lines . This total includes a library of results for truncating and concatenating sequences . Here is a selection of the results proved . Substitution preserves the value Zero : theorem SubstTermP Zero : `` { TermP t } ⊢ SubstTermP ⌈Var v⌉ t Zero Zero '' On terms constructed using Eats ( recall that Q Eats constructs the code of an Eats term ) , substitution performs the natural recursion . theorem SubstTermP Eats : '' { SubstTermP v i t1 u1 , SubstTermP v i t2 u2 } ⊢ SubstTermP v i ( Q Eats t1 t2 ) ( Q Eats u1 u2 ) '' This seemingly obvious result takes nearly 150 lines to prove . The sequences for both substitution computations are combined to form a new sequence , which must be extended to yield the claimed result and shown to be properly constructed . Substitution preserves constants . This fact is proved by induction on the sequence buildup of the constant c , using the previous two facts about SubstTermP . theorem SubstTermP Const : `` { ConstP c , TermP t } ⊢
#60 which are conducted largely in the HF calculus ) total over 2,800 lines . This total includes a library of results for truncating and concatenating sequences . Here is a selection of the results proved . Substitution preserves the value Zero : theorem SubstTermP Zero : `` { TermP t } ⊢ SubstTermP ⌈Var v⌉ t Zero Zero '' On terms constructed using Eats ( recall that Q Eats constructs the code of an Eats term ) , substitution performs the natural recursion . theorem SubstTermP Eats : '' { SubstTermP v i t1 u1 , SubstTermP v i t2 u2 } ⊢ SubstTermP v i ( Q Eats t1 t2 ) ( Q Eats u1 u2 ) '' This seemingly obvious result takes nearly 150 lines to prove . The sequences for both substitution computations are combined to form a new sequence , which must be extended to yield the claimed result and shown to be properly constructed . Substitution preserves constants . This fact is proved by induction on the sequence buildup of the constant c , using the previous two facts about SubstTermP . theorem SubstTermP Const : `` { ConstP c , TermP t } ⊢ SubstTermP ⌈Var w⌉ t c c '' Each recursive case of a syntactic predicate must be verified using the techniques outlined above for SubstTermP Eats . Even when there is only a single operand , as in the following case for negation , the proof is around 100 lines . theorem SubstFormP Neg : `` { SubstFormP v i x y } ⊢ SubstFormP v i ( Q Neg x ) ( Q Neg y ) '' A complication is that LstSeqP accepts sequences that are longer than necessary , and these must be truncated to a given length before they can be extended . These lengthy arguments must be repeated for each similar proof . So , for the third time , one of our chief tools is cut and paste . Exactly the same sort of reasoning can be used to show that proofs can be combined as expected in order to apply inference rules . The following theorem expresses the Hilbert-Bernays derivability condition ( D2 ) : theorem PfP implies ModPon PfP : `` [ [ H ⊢ PfP ( Q Imp x y ) ; H ⊢ PfP x ] ] =⇒ H ⊢ PfP y '' Now only one task remains : to show condition ( D3 ) . 6.3 Making Sense of Quoted Values As mentioned in Sect . 5 , making sense of expressions like x = y → Pf px = yq requires a function Q such that Q ( x ) = pxq : Q ( 0 ) = p0q = 0 Q ( x ⊳ y ) = hp⊳q , Q ( x ) , Q ( y ) i 29 Trying to make this definition unambiguous , Swierczkowski [ 32 ] sketches a total order- ´ ing on sets
#61 they can be extended . These lengthy arguments must be repeated for each similar proof . So , for the third time , one of our chief tools is cut and paste . Exactly the same sort of reasoning can be used to show that proofs can be combined as expected in order to apply inference rules . The following theorem expresses the Hilbert-Bernays derivability condition ( D2 ) : theorem PfP implies ModPon PfP : `` [ [ H ⊢ PfP ( Q Imp x y ) ; H ⊢ PfP x ] ] =⇒ H ⊢ PfP y '' Now only one task remains : to show condition ( D3 ) . 6.3 Making Sense of Quoted Values As mentioned in Sect . 5 , making sense of expressions like x = y → Pf px = yq requires a function Q such that Q ( x ) = pxq : Q ( 0 ) = p0q = 0 Q ( x ⊳ y ) = hp⊳q , Q ( x ) , Q ( y ) i 29 Trying to make this definition unambiguous , Swierczkowski [ 32 ] sketches a total order- ´ ing on sets , but the technical details are complicated and incomplete . The same ordering can be defined via the function f : HF → N such that f ( x ) = P { 2 f ( y ) | y ∈ x } . It is intuitively clear , but formalising the required theory in HF would be laborious . It turns out that we do not need a canonical term x or a function Q . We only need a relation : QuoteP relates a set x to ( the codes of ) the terms that denote x . The relation QuoteP can be defined using precisely the same methods as we have seen above for recursive functions , via a sequence buildup . The following facts can be proved using the methods described in the previous sections . lemma QuoteP Zero : `` { } ⊢ QuoteP Zero Zero '' lemma QuoteP Eats : '' { QuoteP t1 u1 , QuoteP t2 u2 } ⊢ QuoteP ( Eats t1 t2 ) ( Q Eats u1 u2 ) '' It is also necessary to prove ( by induction within the HF calculus ) that for every x there exists some term x. lemma exists QuoteP : assumes j : `` atom j ♯ x '' shows `` { } ⊢ Ex j ( QuoteP x ( Var j ) ) '' We need similar results for all of the predicates involved in concatenating two sequences . They essentially prove that the corresponding pseudo-functions are total . Now we need to start connecting these results with those of the previous section , which ( following Swierczkowski ) are proved for constants in general , althou ´ gh they are needed only for the outputs of QuoteP . An induction in
#62 The relation QuoteP can be defined using precisely the same methods as we have seen above for recursive functions , via a sequence buildup . The following facts can be proved using the methods described in the previous sections . lemma QuoteP Zero : `` { } ⊢ QuoteP Zero Zero '' lemma QuoteP Eats : '' { QuoteP t1 u1 , QuoteP t2 u2 } ⊢ QuoteP ( Eats t1 t2 ) ( Q Eats u1 u2 ) '' It is also necessary to prove ( by induction within the HF calculus ) that for every x there exists some term x. lemma exists QuoteP : assumes j : `` atom j ♯ x '' shows `` { } ⊢ Ex j ( QuoteP x ( Var j ) ) '' We need similar results for all of the predicates involved in concatenating two sequences . They essentially prove that the corresponding pseudo-functions are total . Now we need to start connecting these results with those of the previous section , which ( following Swierczkowski ) are proved for constants in general , althou ´ gh they are needed only for the outputs of QuoteP . An induction in HF on the sequence buildup proves that these outputs satisfy ConstP . lemma QuoteP imp ConstP : `` { QuoteP x y } ⊢ ConstP y '' This is obvious , because QuoteP involves only Zero and Q Eats , which construct quoted sets . Unfortunately , the proof requires the usual reasoning about sequences in order to show basic facts about ConstP , which takes hundreds of lines . The main theorem from the previous section included the set of formulas { ConstP ( F i ) | i. i ∈ V } on the left of the turnstile , representing the assumption that all introduced variables denoted constants . Now we can replace this assumption by one expressing that the relation QuoteP holds between each pair of old and new variables . definition quote all : : `` [ perm , name set ] ⇒ fm set '' where `` quote all p V = { QuoteP ( Var i ) ( Var ( p · i ) ) | i. i ∈ V } The relation QuoteP ( Var i ) ( Var ( p · i ) holds between the variable i and the renamed variable p · i , for all i ∈ V. Recall that p is a permutation on variable names . By virtue of the theorem QuoteP imp ConstP , we obtain a key result , which will be used heavily in subsequent proofs for reasoning about coded formulas and the Pf predicate . theorem quote all PfP ssubst : assumes β : `` { } ⊢ β '' and V : `` V ⊆ Vs '' and s : `` supp β ⊆ atom ‘ Vs '' shows `` quote all p V ⊢ PfP ( ssubst ⌊β⌋V V F )
#63 , representing the assumption that all introduced variables denoted constants . Now we can replace this assumption by one expressing that the relation QuoteP holds between each pair of old and new variables . definition quote all : : `` [ perm , name set ] ⇒ fm set '' where `` quote all p V = { QuoteP ( Var i ) ( Var ( p · i ) ) | i. i ∈ V } The relation QuoteP ( Var i ) ( Var ( p · i ) holds between the variable i and the renamed variable p · i , for all i ∈ V. Recall that p is a permutation on variable names . By virtue of the theorem QuoteP imp ConstP , we obtain a key result , which will be used heavily in subsequent proofs for reasoning about coded formulas and the Pf predicate . theorem quote all PfP ssubst : assumes β : `` { } ⊢ β '' and V : `` V ⊆ Vs '' and s : `` supp β ⊆ atom ‘ Vs '' shows `` quote all p V ⊢ PfP ( ssubst ⌊β⌋V V F ) '' In English : Let ⊢ β be a theorem of HF whose free variables belong to the set Vs. Take the code of this theorem , ⌊β⌋ , and replace some subset V ⊆ Vs of its free variables by 30 new variables constrained by the QuoteP relation . The result , ssubst ⌊β⌋V V F , satisfies the provability predicate . The reader of even a very careful presentation of G¨odel ’ s second incompleteness theorem , such as Grandy [ 9 ] , will look in vain for a clear and rigorous treatment of the x ( or x ) convention . Boolos [ 2 ] comes very close with his Bew [ F ] notation , but he is quite wrong to state “ notice that Bew [ F ] has the same variables free as [ the formula ] F ” [ 2 , p. 45 ] when in fact they have no variables in common . Even Swierczkowski ’ s highly ´ detailed account is at best ambiguous . He consistently uses function notation , but his carefully-stated guidelines for replacing occurrences of pseudo-functions by quantified formulas [ 32 , Sect . 5 ] are not relevant here . ( This problem only became clear after a time-consuming attempt at a formalisation on that basis . ) My companion paper [ 27 ] , which is aimed at logicians , provides a more detailed discussion of these points . It concludes that these various notations obscure not only the formal details of the proof but also the very intuitions they are intended to highlight . 6.4 Proving ⊢ α → Pf ( pαq ) We now have everything necessary to prove condition ( D3 ) : If α is a strict Σ sentence ,
#64 or x ) convention . Boolos [ 2 ] comes very close with his Bew [ F ] notation , but he is quite wrong to state “ notice that Bew [ F ] has the same variables free as [ the formula ] F ” [ 2 , p. 45 ] when in fact they have no variables in common . Even Swierczkowski ’ s highly ´ detailed account is at best ambiguous . He consistently uses function notation , but his carefully-stated guidelines for replacing occurrences of pseudo-functions by quantified formulas [ 32 , Sect . 5 ] are not relevant here . ( This problem only became clear after a time-consuming attempt at a formalisation on that basis . ) My companion paper [ 27 ] , which is aimed at logicians , provides a more detailed discussion of these points . It concludes that these various notations obscure not only the formal details of the proof but also the very intuitions they are intended to highlight . 6.4 Proving ⊢ α → Pf ( pαq ) We now have everything necessary to prove condition ( D3 ) : If α is a strict Σ sentence , then ⊢ α → Pf ( pαq ) The proof will be by induction on the structure of α . As stated in Sect . 3.3 above , a strict Σ formula has the form x ∈ y , α ∨ β , α ∧ β , ∃x α or ( ∀x ∈ y ) α . Therefore , the induction will include one single base case , x ∈ y → Pf px ∈ yq , ( 3 ) along with inductive steps for disjunction , conjunction , etc . 6.4.1 The Propositional Cases The propositional cases are not difficult , but are worth examining as a warmup exercise . From the induction hypotheses ⊢ α → Pf ( pαq ) and ⊢ β → Pf ( pβq ) , we must show ⊢ α ∨ β → Pf ( pα ∨ βq ) and ⊢ α ∧ β → Pf ( pα ∧ βq ) . Both of these cases are trivial by propositional logic , given the lemmas ⊢ Pf ( pαq ) → Pf ( pα ∨ βq ) , ⊢ Pf ( pβq ) → Pf ( pα ∨ βq ) and ⊢ Pf ( pαq ) → Pf ( pβq ) → Pf ( pα ∧ βq ) ( 4 ) Proving ( 4 ) directly from the definitions would need colossal efforts , but there is a quick proof . The automation of the HF calculus is good enough to prove tautologies , and from ⊢ α → β → α ∧ β , the proof formalisation condition9 yields ⊢ Pf ( pα → β → α ∧ βq ) Finally , the Hilbert-Bernays derivability condition ( D2 ) yields the desired lemma , ( 4 ) . This trick is needed whenever
#65 difficult , but are worth examining as a warmup exercise . From the induction hypotheses ⊢ α → Pf ( pαq ) and ⊢ β → Pf ( pβq ) , we must show ⊢ α ∨ β → Pf ( pα ∨ βq ) and ⊢ α ∧ β → Pf ( pα ∧ βq ) . Both of these cases are trivial by propositional logic , given the lemmas ⊢ Pf ( pαq ) → Pf ( pα ∨ βq ) , ⊢ Pf ( pβq ) → Pf ( pα ∨ βq ) and ⊢ Pf ( pαq ) → Pf ( pβq ) → Pf ( pα ∧ βq ) ( 4 ) Proving ( 4 ) directly from the definitions would need colossal efforts , but there is a quick proof . The automation of the HF calculus is good enough to prove tautologies , and from ⊢ α → β → α ∧ β , the proof formalisation condition9 yields ⊢ Pf ( pα → β → α ∧ βq ) Finally , the Hilbert-Bernays derivability condition ( D2 ) yields the desired lemma , ( 4 ) . This trick is needed whenever we need to do propositional reasoning with Pf . 9 Of Sect . 4.4 , but via the substitution theorem quote all PfP ssubst proved above . The induction concerns generalised formulas involving pseudo-coding : PfP ( ssubst ⌊α⌋V V F ) . 31 6.4.2 The Equality and Membership Cases Now comes one of the most critical parts of the formalisation . Many published proofs [ 2 , 32 ] of the second completeness theorem use the following lemma : x = y → Pf px = yq ( 5 ) This in turn is proved using a lemma stating that x = y implies x = y , which is false here : we have defined QuoteP only as a relation , and even { 0 , 1 } can be written in two different ways . Nevertheless , the statement ( 5 ) is clearly true : if x and y are constant terms denoting x and y , respectively , where x = y , then Pf px = yq holds . The equivalence of two different ways of writing a finite set should obviously be provable . This problem recalls the situation described in 3.3 above , and the induction used to prove Subset Mem sf lemma . The solution , once again , is to prove the conjunction ( x ∈ y → Pf px ∈ yq ) ∧ ( x ⊆ y → Pf px ⊆ yq ) by induction ( in HF ) on the sum of the sizes of x and y . The proof is huge ( nearly 340 lines ) , with eight universal quantifiers in the induction formula , each of which must be individually instantiated in order to apply an induction hypothesis . ⊢ All i ( All
#66 that x = y implies x = y , which is false here : we have defined QuoteP only as a relation , and even { 0 , 1 } can be written in two different ways . Nevertheless , the statement ( 5 ) is clearly true : if x and y are constant terms denoting x and y , respectively , where x = y , then Pf px = yq holds . The equivalence of two different ways of writing a finite set should obviously be provable . This problem recalls the situation described in 3.3 above , and the induction used to prove Subset Mem sf lemma . The solution , once again , is to prove the conjunction ( x ∈ y → Pf px ∈ yq ) ∧ ( x ⊆ y → Pf px ⊆ yq ) by induction ( in HF ) on the sum of the sizes of x and y . The proof is huge ( nearly 340 lines ) , with eight universal quantifiers in the induction formula , each of which must be individually instantiated in order to apply an induction hypothesis . ⊢ All i ( All i ’ ( All si ( All li ( All j ( All j ’ ( All sj ( All lj ( SeqQuoteP ( Var i ) ( Var i ’ ) ( Var si ) ( Var li ) IMP SeqQuoteP ( Var j ) ( Var j ’ ) ( Var sj ) ( Var lj ) IMP HaddP ( Var li ) ( Var lj ) ( Var k ) IMP ( ( Var i IN Var j IMP PfP ( Q Mem ( Var i ’ ) ( Var j ’ ) ) ) AND ( Var i SUBS Var j IMP PfP ( Q Subset ( Var i ’ ) ( Var j ’ ) ) ) ) ) ) ) ) ) ) ) ) '' Using SeqQuoteP ( which describes the sequence computation of QuoteP ) gives access to a size measure for the two terms , which are here designated i and j . Their sizes , li and lj , are added using HaddP , which is simply addition as defined in the HF calculus . ( This formalisation of addition is also needed for reasoning about sequences . ) Their sum , k , is used as the induction variable . Although the second half of the conjunction suffices to prove ( 5 ) , it is never needed outside of the induction , and neither is ( 5 ) itself . All we need is ( 3 ) . And so we reach the next milestone . lemma assumes `` atom i ♯ ( j , j ’ , i ’ ) '' `` atom i ’ ♯ ( j , j ’ ) '' `` atom j ♯ ( j ’ ) '' shows QuoteP Mem imp QMem
#67 Var i SUBS Var j IMP PfP ( Q Subset ( Var i ’ ) ( Var j ’ ) ) ) ) ) ) ) ) ) ) ) ) '' Using SeqQuoteP ( which describes the sequence computation of QuoteP ) gives access to a size measure for the two terms , which are here designated i and j . Their sizes , li and lj , are added using HaddP , which is simply addition as defined in the HF calculus . ( This formalisation of addition is also needed for reasoning about sequences . ) Their sum , k , is used as the induction variable . Although the second half of the conjunction suffices to prove ( 5 ) , it is never needed outside of the induction , and neither is ( 5 ) itself . All we need is ( 3 ) . And so we reach the next milestone . lemma assumes `` atom i ♯ ( j , j ’ , i ’ ) '' `` atom i ’ ♯ ( j , j ’ ) '' `` atom j ♯ ( j ’ ) '' shows QuoteP Mem imp QMem : '' { QuoteP ( Var i ) ( Var i ’ ) , QuoteP ( Var j ) ( Var j ’ ) , Var i IN Var j } ⊢ PfP ( Q Mem ( Var i ’ ) ( Var j ’ ) ) '' and QuoteP Mem imp QSubset : '' { QuoteP ( Var i ) ( Var i ’ ) , QuoteP ( Var j ) ( Var j ’ ) , Var i SUBS Var j } ⊢ PfP ( Q Subset ( Var i ’ ) ( Var j ’ ) ) '' Turning to the main induction on α , the notoriously “ delicate ” [ 2 , p. 48 ] case is bounded universal quantification . Many of the delicate points here are connected with the way the nominal approach is used . We need to maintain and extend a permutation relating old and new variable names . Such complexities are evident in mathematical texts , in their treatment of variable names [ 32 , Lemma 9.7 ] . lemma ( in quote perm ) quote all Mem imp All2 : assumes IH : `` insert ( QuoteP ( Var i ) ( Var i ’ ) ) ( quote all p Vs ) ⊢ α IMP PfP ( ssubst ⌊α⌋ ( insert i Vs ) ( insert i Vs ) Fi ) '' and `` supp ( All2 i ( Var j ) α ) ⊆ atom ‘ Vs '' 32 and j : `` atom j ♯ ( i , α ) '' and i : `` atom i ♯ p '' and i ’ : `` atom i ’ ♯ ( i , p , α ) '' shows `` insert ( All2 i ( Var j
#68 '' Turning to the main induction on α , the notoriously “ delicate ” [ 2 , p. 48 ] case is bounded universal quantification . Many of the delicate points here are connected with the way the nominal approach is used . We need to maintain and extend a permutation relating old and new variable names . Such complexities are evident in mathematical texts , in their treatment of variable names [ 32 , Lemma 9.7 ] . lemma ( in quote perm ) quote all Mem imp All2 : assumes IH : `` insert ( QuoteP ( Var i ) ( Var i ’ ) ) ( quote all p Vs ) ⊢ α IMP PfP ( ssubst ⌊α⌋ ( insert i Vs ) ( insert i Vs ) Fi ) '' and `` supp ( All2 i ( Var j ) α ) ⊆ atom ‘ Vs '' 32 and j : `` atom j ♯ ( i , α ) '' and i : `` atom i ♯ p '' and i ’ : `` atom i ’ ♯ ( i , p , α ) '' shows `` insert ( All2 i ( Var j ) α ) ( quote all p Vs ) ⊢ PfP ( ssubst ⌊All2 i ( Var j ) α⌋Vs Vs F ) '' The final case , for the existential quantifier , is also somewhat complicated to formalise . The details are again mostly connected with managing free and bound variable names using nominal methods , and are therefore omitted . We can conclude our discussion of the inductive argument by viewing the final result : lemma star : assumes `` ss fm α '' `` finite V '' `` supp α ⊆ atom ‘ V '' shows `` insert α ( quote all p V ) ⊢ PfP ( ssubst ⌊α⌋V V F ) '' Condition ( D3 ) now follows easily , since the formula α is then a sentence . Although some technical conditions ( involving variable names and permutations ) have been omitted from the previous two theorems , our main result below appears exactly as it was proved . Of course , α ⊢ Pf pαq is equivalent to ⊢ α → Pf pαq . theorem Provability : assumes `` Sigma fm α '' `` ground fm α '' shows `` { α } ⊢ PfP ⌈α⌉ '' 7 G¨odel ’ s Second Incompleteness Theorem The final steps of the second incompleteness theorem can be seen in Fig . 2 . The diagonal formula , δ , is obtained via the first incompleteness theorem . Then we can quickly establish both Pf pδq ⊢ Pf ( pPf pδqq ) and Pf pδq ⊢ Pf ( p¬Pf pδqq ) . These together imply Pf pδq ⊢ Pf ( p⊥q ) using a variant of condition ( D2 ) . It follows that if the system proves its own consistency , then it also proves ⊢
#69 insert α ( quote all p V ) ⊢ PfP ( ssubst ⌊α⌋V V F ) '' Condition ( D3 ) now follows easily , since the formula α is then a sentence . Although some technical conditions ( involving variable names and permutations ) have been omitted from the previous two theorems , our main result below appears exactly as it was proved . Of course , α ⊢ Pf pαq is equivalent to ⊢ α → Pf pαq . theorem Provability : assumes `` Sigma fm α '' `` ground fm α '' shows `` { α } ⊢ PfP ⌈α⌉ '' 7 G¨odel ’ s Second Incompleteness Theorem The final steps of the second incompleteness theorem can be seen in Fig . 2 . The diagonal formula , δ , is obtained via the first incompleteness theorem . Then we can quickly establish both Pf pδq ⊢ Pf ( pPf pδqq ) and Pf pδq ⊢ Pf ( p¬Pf pδqq ) . These together imply Pf pδq ⊢ Pf ( p⊥q ) using a variant of condition ( D2 ) . It follows that if the system proves its own consistency , then it also proves ⊢ ¬Pf pδq and therefore ⊢ δ , a contradiction . Swierczkowski [ 32 ] presents a few other results which have n ´ ot been formalised here . These include a refinement of the incompleteness theorem ( credited to Reinhardt ) and a theory of a linear order on the HF sets , but recall that claim ( 5 ) can be proved without using any such ordering . The approach adopted here undoubtedly involves less effort than formalising the ordering in the HF calculus . The total proof length of nearly 12,400 lines comprises around 4,600 lines for the second theorem and 7,700 lines for the first.10 ( One could also include 2,700 lines for HF set theory itself , but we would not count the standard libraries of natural numbers if they were used as the basis of the proof . ) O ’ Connor ’ s proof comprises 47,000 lines of Coq , while Shankar ’ s takes 20,000 lines [ 30 , p. 139 ] and Harrison ’ s [ 10 ] is a miniscule 4,400 lines of HOL Light . Recall that none of these other proofs include the second incompleteness theorem . But comparisons are almost meaningless because of the enormous differences among the formalisations . Shankar wrote ( and proved to be representable ) a LISP interpreter for coding up the metatheory [ 30 ] ; this was a huge effort , but then the various coding functions could then be written in LISP without further justification . He also used HF for coding , presumably because of its similarity to LISP S-expressions . O ’ Connor formalised a very general syntax for first-order logic [ 22 ] . He introduced a general inductive definition of the primitive recursive functions , but proving
#70 second theorem and 7,700 lines for the first.10 ( One could also include 2,700 lines for HF set theory itself , but we would not count the standard libraries of natural numbers if they were used as the basis of the proof . ) O ’ Connor ’ s proof comprises 47,000 lines of Coq , while Shankar ’ s takes 20,000 lines [ 30 , p. 139 ] and Harrison ’ s [ 10 ] is a miniscule 4,400 lines of HOL Light . Recall that none of these other proofs include the second incompleteness theorem . But comparisons are almost meaningless because of the enormous differences among the formalisations . Shankar wrote ( and proved to be representable ) a LISP interpreter for coding up the metatheory [ 30 ] ; this was a huge effort , but then the various coding functions could then be written in LISP without further justification . He also used HF for coding , presumably because of its similarity to LISP S-expressions . O ’ Connor formalised a very general syntax for first-order logic [ 22 ] . He introduced a general inductive definition of the primitive recursive functions , but proving specific functions to be primitive recursive turned out to be extremely difficult [ 23 , Sect . 5.3 ] . Harrison has 10 Prior to polishing and removing unused material , the proof totalled 17,000 lines . 33 theorem Goedel II : assumes `` ¬ { } ⊢ Fls '' shows `` ¬ { } ⊢ Neg ( PfP ⌈Fls⌉ ) '' proof - from assms Goedel I obtain δ where diag : `` { } ⊢ δ IFF Neg ( PfP ⌈δ⌉ ) '' `` ¬ { } ⊢ δ '' and gnd : `` ground fm δ '' by metis have `` { PfP ⌈δ⌉ } ⊢ PfP ⌈PfP ⌈δ⌉⌉ '' by ( auto simp : Provability ground fm aux def supp conv fresh ) moreover have `` { PfP ⌈δ⌉ } ⊢ PfP ⌈Neg ( PfP ⌈δ⌉ ) ⌉ '' apply ( rule MonPon PfP implies PfP [ OF gnd ] ) apply ( metis Conj E2 Iff def Iff sym diag ( 1 ) ) apply ( auto simp : ground fm aux def supp conv fresh ) done moreover have `` ground fm ( PfP ⌈δ⌉ ) '' by ( auto simp : ground fm aux def supp conv fresh ) ultimately have `` { PfP ⌈δ⌉ } ⊢ PfP ⌈Fls⌉ '' using PfP quot contra by ( metis ( no types ) anti deduction cut2 ) thus `` ¬ { } ⊢ Neg ( PfP ⌈Fls⌉ ) '' by ( metis Iff MP2 same Neg mono cut1 diag ) qed Fig . 2 G¨odel ’ s Second Incompleteness Theorem not published a paper describing his formalisation , but devotes a few pages to G¨odel ’ s theorems in his Handbook of Practical Logic [ 12 , p. 546–555 ] , including extracts of HOL
#71 by metis have `` { PfP ⌈δ⌉ } ⊢ PfP ⌈PfP ⌈δ⌉⌉ '' by ( auto simp : Provability ground fm aux def supp conv fresh ) moreover have `` { PfP ⌈δ⌉ } ⊢ PfP ⌈Neg ( PfP ⌈δ⌉ ) ⌉ '' apply ( rule MonPon PfP implies PfP [ OF gnd ] ) apply ( metis Conj E2 Iff def Iff sym diag ( 1 ) ) apply ( auto simp : ground fm aux def supp conv fresh ) done moreover have `` ground fm ( PfP ⌈δ⌉ ) '' by ( auto simp : ground fm aux def supp conv fresh ) ultimately have `` { PfP ⌈δ⌉ } ⊢ PfP ⌈Fls⌉ '' using PfP quot contra by ( metis ( no types ) anti deduction cut2 ) thus `` ¬ { } ⊢ Neg ( PfP ⌈Fls⌉ ) '' by ( metis Iff MP2 same Neg mono cut1 diag ) qed Fig . 2 G¨odel ’ s Second Incompleteness Theorem not published a paper describing his formalisation , but devotes a few pages to G¨odel ’ s theorems in his Handbook of Practical Logic [ 12 , p. 546–555 ] , including extracts of HOL Light proofs . He defines Σ1 and Π1 formulas and quotes some meta-theoretical results relating truth and provability . This project took approximately one year , in time left available after fulfilling teaching and administrative duties . The underlying set theory took only two weeks to formalise . The G¨odel development up to the proof formalisation condition took another five months . From there to the first incompleteness theorem took a further two months , mostly devoted to proving single valued properties . Then the second incompleteness theorem took a further four months , including much time wasted due to misunderstanding this perplexing material . Some material has since been consolidated or streamlined . The final version is available online [ 26 ] . 7.1 The Lengths of Proofs Figure 3 depicts the sizes of the Isabelle/HOL theories making up various sections of the proof development . The first theorem takes up the bulk of the effort . Apart from the massive HF proofs about predicates , which are mostly of obvious properties , the second theorem appears to be a fairly easy step given the first . Why then has it not been formalised until now ? A reasonable guess is that previous researchers were not aware of Swierczkowski ’ s [ 32 ] elaborate development . The most deta ´ iled of the previous proofs [ 2 , 9 ] left too much to the imagination , and even Swierczkowski makes some errors . He ´ devotes much of his Sect . 7 to proofs concerning substitution for ( non-existent ) pseudoterms analogous to x . Recall that pseudo-terms are merely a notational shorthand to allow function syntax , and are not actual terms . Finally , there was the critical issue of the ordering on the HF
#72 misunderstanding this perplexing material . Some material has since been consolidated or streamlined . The final version is available online [ 26 ] . 7.1 The Lengths of Proofs Figure 3 depicts the sizes of the Isabelle/HOL theories making up various sections of the proof development . The first theorem takes up the bulk of the effort . Apart from the massive HF proofs about predicates , which are mostly of obvious properties , the second theorem appears to be a fairly easy step given the first . Why then has it not been formalised until now ? A reasonable guess is that previous researchers were not aware of Swierczkowski ’ s [ 32 ] elaborate development . The most deta ´ iled of the previous proofs [ 2 , 9 ] left too much to the imagination , and even Swierczkowski makes some errors . He ´ devotes much of his Sect . 7 to proofs concerning substitution for ( non-existent ) pseudoterms analogous to x . Recall that pseudo-terms are merely a notational shorthand to allow function syntax , and are not actual terms . Finally , there was the critical issue of the ordering on the HF sets . Solving these mysteries required much thought , and the 34 first completed formalisation included thousands of lines of proofs belonging to aborted attempts . A discussion of the de Bruijn coefficient ( the expansion in size entailed by the process of formalisation ) is always interesting , but difficult to do rigorously . In this case , the formalisation required proving a great many theorems that were not even hinted at in the source text , for example , setting up a usable sequent calculus ( Swierczkowski ´ merely gives the rudiments of a Hilbert system ) , or proving that the various codings of syntax actually work ( virtually all authors take this for granted ) , or proving that “ functions ” are functions . The hundreds of lines of single-step HF calculus proofs are the single largest contributor to the size of this development , and such things never appear in standard presentations of the incompleteness theorems . A crude calculation yields 30 pages at 35 lines per page or 1050 lines for Swier- ´ czkowski ’ s proof , compared with 12,400 lines of Isabelle , for a de Bruijn factor of 12 . Focusing on just the proof of the first incompleteness theorem ( after the preliminary developments ) , we have about 80 lines of informal text and 671 lines of Isabelle , giving a factor of 8.4 ; that includes 150 lines in the Isabelle script to prove that functions are single valued . A further issue is the heavy use of cut and paste in the HF calculus proofs . Better automation for HF could help , but spending time to develop a tactic that will only be called a few times is hard to justify . An alternative idea
#73 or proving that the various codings of syntax actually work ( virtually all authors take this for granted ) , or proving that “ functions ” are functions . The hundreds of lines of single-step HF calculus proofs are the single largest contributor to the size of this development , and such things never appear in standard presentations of the incompleteness theorems . A crude calculation yields 30 pages at 35 lines per page or 1050 lines for Swier- ´ czkowski ’ s proof , compared with 12,400 lines of Isabelle , for a de Bruijn factor of 12 . Focusing on just the proof of the first incompleteness theorem ( after the preliminary developments ) , we have about 80 lines of informal text and 671 lines of Isabelle , giving a factor of 8.4 ; that includes 150 lines in the Isabelle script to prove that functions are single valued . A further issue is the heavy use of cut and paste in the HF calculus proofs . Better automation for HF could help , but spending time to develop a tactic that will only be called a few times is hard to justify . An alternative idea is to define higher-order operators for the sequence constructions , which could be proved to be functional once and for all . However , higher-order operators are difficult to define using nominal syntax . Perhaps it could be attempted using naive variables . Fig . 3 Sizes of Constituent Theories 7.2 The Formalisation of Variable Binding The role of bound variable syntax remains unclear . Shankar [ 30 , 31 ] used de Bruijn variables to formalise the Church-Rosser theorem but not the incompleteness theorem . Harrison did not use them either . O ’ Connor also used traditional syntactic bound variables , but complained about huge complications concerning substitution ( recall Sect . 2.3 ) . The present development uses the nominal package , easing many proofs , but at a price : over 900 lines involve freshness specifications , and around 70 lemmas involving freshness are proved . Moreover , many proof steps are slow . While the project was 35 underway , proof times taking minutes were not unusual . Even after recent improvements to the nominal package , they can take tens of seconds . Additional performance improvements would be welcome , as well as a more concise notation for freshness conditions when many new names are needed . In fairness to the nominal approach , explicit variable names would also have to be fresh and analogous assertions would be necessary , along with some procedure for calculating new names numerically and proving them to be fresh . The effort may be similar either way , but the nominal approach is more abstract and natural : who after all refers to specific , calculated variable names in textbook proofs ? My first attempt to formalise the incompleteness theorems used explicit names . Then , substitution on
#74 bound variables , but complained about huge complications concerning substitution ( recall Sect . 2.3 ) . The present development uses the nominal package , easing many proofs , but at a price : over 900 lines involve freshness specifications , and around 70 lemmas involving freshness are proved . Moreover , many proof steps are slow . While the project was 35 underway , proof times taking minutes were not unusual . Even after recent improvements to the nominal package , they can take tens of seconds . Additional performance improvements would be welcome , as well as a more concise notation for freshness conditions when many new names are needed . In fairness to the nominal approach , explicit variable names would also have to be fresh and analogous assertions would be necessary , along with some procedure for calculating new names numerically and proving them to be fresh . The effort may be similar either way , but the nominal approach is more abstract and natural : who after all refers to specific , calculated variable names in textbook proofs ? My first attempt to formalise the incompleteness theorems used explicit names . Then , substitution on formulas was only available as a relation , and many proofs required numerical operations on variable names . This effort would have multiplied considerably for the second incompleteness theorem . Using de Bruijn indices for HF syntax was not attractive : I had previously formalised G¨odel ’ s definition of the constructible sets and his proof of the relative consistency of the axiom of choice [ 25 ] . Here it was also necessary to define a great many predicates within an encoding of first-order logic . This work was done in Isabelle/ZF , a version of Isabelle for axiomatic set theory . I used de Bruijn indices in these definitions , but the loss of readability was a severe impediment to progress . It is worth investigating how this formalisation would be affected by the change to another treatment of variable binding . As regards the G¨odel numbering of formulas , the use of de Bruijn variables can be called an unqualified success . It was easy to set up and all necessary properties were proved without great difficulties . 7.3 On Verifying Proof Assistants In a paper entitled “ Towards Self-verification of HOL Light ” , Harrison says , G¨odel ’ s second incompleteness theorem tells us that [ a logical system ] can not prove its own consistency in any way at all . . . . So , regardless of implementation details , if we want to prove the consistency of a proof checker , we need to use a logic that in at least some respects goes beyond the logic the checker itself supports . [ 11 , p. 179 ] This statement is potentially misleading , and has given rise to the mistaken view that it is impossible to verify a proof checker in
#75 set theory . I used de Bruijn indices in these definitions , but the loss of readability was a severe impediment to progress . It is worth investigating how this formalisation would be affected by the change to another treatment of variable binding . As regards the G¨odel numbering of formulas , the use of de Bruijn variables can be called an unqualified success . It was easy to set up and all necessary properties were proved without great difficulties . 7.3 On Verifying Proof Assistants In a paper entitled “ Towards Self-verification of HOL Light ” , Harrison says , G¨odel ’ s second incompleteness theorem tells us that [ a logical system ] can not prove its own consistency in any way at all . . . . So , regardless of implementation details , if we want to prove the consistency of a proof checker , we need to use a logic that in at least some respects goes beyond the logic the checker itself supports . [ 11 , p. 179 ] This statement is potentially misleading , and has given rise to the mistaken view that it is impossible to verify a proof checker in its own logic . Harrison ’ s aim is to prove that HOL Light can not prove the theorem FALSE , and this indeed requires proving the consistency of higher-order logic itself . Unfortunately , most consistency proofs are unsatisfactory because they more or less assume the desired conclusion : they are thinly disguised versions of the tautology Con ( L ) ∧ L → Con ( L ) . This is a consequence of the second incompleteness theorem , since the consistency of L can only be proved in a strictly stronger formal system . Mathematicians accept strong formal systems , such as ZF set theory , with little justification other than intuition and experience . Moreover , they examine very strong further axioms . The axiom of constructibility is an instructive case : it is known to be relatively consistent with respect to the axioms of set theory , but it is not generally accepted as true [ 16 , p. 170 ] . The standard ZF axioms are generally regarded as true , although they can not even be proved to be consistent . Thus we have no good way of proving consistency , and yet consistency does not guarantee truth . 36 This situation calls for a separation of concerns . The builders of verification tools should be concerned with the correctness of their code , but the correctness of the underlying formal calculus is the concern of logicians . Harrison notes that “ almost all implementation bugs in HOL Light and other versions of HOL have involved variable renaming ” [ 11 , p. 179 ] , and this type of issue should be our focus . Verifying a proof assistant involves verifying that it implements a data structure for the assertions of the formal
#76 systems , such as ZF set theory , with little justification other than intuition and experience . Moreover , they examine very strong further axioms . The axiom of constructibility is an instructive case : it is known to be relatively consistent with respect to the axioms of set theory , but it is not generally accepted as true [ 16 , p. 170 ] . The standard ZF axioms are generally regarded as true , although they can not even be proved to be consistent . Thus we have no good way of proving consistency , and yet consistency does not guarantee truth . 36 This situation calls for a separation of concerns . The builders of verification tools should be concerned with the correctness of their code , but the correctness of the underlying formal calculus is the concern of logicians . Harrison notes that “ almost all implementation bugs in HOL Light and other versions of HOL have involved variable renaming ” [ 11 , p. 179 ] , and this type of issue should be our focus . Verifying a proof assistant involves verifying that it implements a data structure for the assertions of the formal calculus and that it satisfies a commuting diagram relating deductions on the implemented assertions with the corresponding deductions in the calculus . G¨odel ’ s theorems have no relevance here . 8 Conclusions The main finding is simply that G¨odel ’ s second incompleteness theorem can be proved with a relatively modest effort , in only a few months starting with a proof of the first incompleteness theorem . While the nominal approach to syntax is clearly not indispensable , it copes convincingly with a development of this size and complexity . The use of HF set theory as an alternative to Peano arithmetic is clearly justified , eliminating the need to formalise basic number theory within the embedded calculus ; the necessary effort to do that would greatly exceed the difficulties ( mentioned in Sect . 6.4 above ) caused by the lack of a simple canonical ordering on HF sets . Many published proofs of the incompleteness theorems replace technical proofs by vague appeals to Church ’ s thesis . Boolos [ 2 ] presents a more detailed and careful exposition , but still leaves substantial gaps . Even the source text [ 32 ] for this project , although written with great care , had problems : a significant gap ( concerning the canonical ordering of HF sets ) , a few minor ones ( concerning Σ formulas , for example ) , and pages of material that are , at the very least , misleading . These remarks are not intended as criticism but as objective observations of the complexity of this material , with its codings of codings . A complete formal proof , written in a fairly readable notation , should greatly clarify the issues involved in these crucially important theorems . Acknowledgment Jesse
#77 alternative to Peano arithmetic is clearly justified , eliminating the need to formalise basic number theory within the embedded calculus ; the necessary effort to do that would greatly exceed the difficulties ( mentioned in Sect . 6.4 above ) caused by the lack of a simple canonical ordering on HF sets . Many published proofs of the incompleteness theorems replace technical proofs by vague appeals to Church ’ s thesis . Boolos [ 2 ] presents a more detailed and careful exposition , but still leaves substantial gaps . Even the source text [ 32 ] for this project , although written with great care , had problems : a significant gap ( concerning the canonical ordering of HF sets ) , a few minor ones ( concerning Σ formulas , for example ) , and pages of material that are , at the very least , misleading . These remarks are not intended as criticism but as objective observations of the complexity of this material , with its codings of codings . A complete formal proof , written in a fairly readable notation , should greatly clarify the issues involved in these crucially important theorems . Acknowledgment Jesse Alama drew my attention to Swierczkowski [ 32 ] , the source material for this ´ project . Christian Urban assisted with nominal aspects of some of the proofs , even writing code . Brian Huffman provided the core formalisation of type hf . Dana Scott offered advice and drew my attention to Kirby [ 15 ] . Matt Kaufmann and the referees made many insightful comments . References [ 1 ] Joan Bagaria . A short guide to G¨odel ’ s second incompleteness theorem . Teorema , 22 ( 3 ) :5–15 , 2003 . [ 2 ] George Stephen Boolos . The Logic of Provability . Cambridge University Press , 1993 . [ 3 ] N. G. de Bruijn . Lambda calculus notation with nameless dummies , a tool for automatic formula manipulation , with application to the Church-Rosser Theorem . Indagationes Mathematicae , 34:381–392 , 1972 . [ 4 ] S. Feferman , editor . Kurt G¨odel : Collected Works , volume I. Oxford University Press , 1986 . 37 [ 5 ] Torkel Franz´en . G¨odel ’ s Theorem : An Incomplete Guide to Its Use and Abuse . A K Peters , 2005 . [ 6 ] M. J. Gabbay and A. M. Pitts . A new approach to abstract syntax with variable binding . Formal Aspects of Computing , 13:341–363 , 2001 . [ 7 ] Kurt G¨odel . On completeness and consistency . In Feferman [ 4 ] , pages 234–236 . [ 8 ] Kurt G¨odel . On formally undecidable propositions of Principia Mathematica and related systems . In Feferman [ 4 ] , pages 144–195 . First published in 1931 in the Monatshefte f¨ur Mathematik und Physik . [ 9 ] Richard E Grandy . Advanced Logic for Applications . Reidel
#78 Stephen Boolos . The Logic of Provability . Cambridge University Press , 1993 . [ 3 ] N. G. de Bruijn . Lambda calculus notation with nameless dummies , a tool for automatic formula manipulation , with application to the Church-Rosser Theorem . Indagationes Mathematicae , 34:381–392 , 1972 . [ 4 ] S. Feferman , editor . Kurt G¨odel : Collected Works , volume I. Oxford University Press , 1986 . 37 [ 5 ] Torkel Franz´en . G¨odel ’ s Theorem : An Incomplete Guide to Its Use and Abuse . A K Peters , 2005 . [ 6 ] M. J. Gabbay and A. M. Pitts . A new approach to abstract syntax with variable binding . Formal Aspects of Computing , 13:341–363 , 2001 . [ 7 ] Kurt G¨odel . On completeness and consistency . In Feferman [ 4 ] , pages 234–236 . [ 8 ] Kurt G¨odel . On formally undecidable propositions of Principia Mathematica and related systems . In Feferman [ 4 ] , pages 144–195 . First published in 1931 in the Monatshefte f¨ur Mathematik und Physik . [ 9 ] Richard E Grandy . Advanced Logic for Applications . Reidel , 1977 . [ 10 ] John Harrison . Re : Re : G¨odel ’ s incompleteness theorem . Email dated 15 January 2014 . [ 11 ] John Harrison . Towards self-verification of HOL Light . In Ulrich Furbach and Natarajan Shankar , editors , Automated Reasoning — Third International Joint Conference , IJCAR 2006 , LNAI 4130 , pages 177–191 . Springer , 2006 . [ 12 ] John Harrison . Handbook of Practical Logic and Automated Reasoning . Cambridge University Press , 2009 . [ 13 ] Richard E Hodel . An Introduction to Mathematical Logic . PWS Publishing Company , 1995 . [ 14 ] Joe Hurd and Tom Melham , editors . Theorem Proving in Higher Order Logics : TPHOLs 2005 , LNCS 3603 . Springer , 2005 . [ 15 ] Laurence Kirby . Addition and multiplication of sets . Mathematical Logic Quarterly , 53 ( 1 ) :52–65 , 2007 . [ 16 ] Kenneth Kunen . Set Theory : An Introduction to Independence Proofs . North-Holland , 1980 . [ 17 ] Andreas Lochbihler . Formalising finfuns — generating code for functions as data from Isabelle/HOL . In Stefan Berghofer , Tobias Nipkow , Christian Urban , and Makarius Wenzel , editors , TPHOLs , volume 5674 of Lecture Notes in Computer Science , pages 310–326 . Springer , 2009 . [ 18 ] Tobias Nipkow . More Church-Rosser proofs ( in Isabelle/HOL ) . Journal of Automated Reasoning , 26:51–66 , 2001 . [ 19 ] Tobias Nipkow and Lawrence C. Paulson . Proof pearl : Defining functions over finite sets . In Hurd and Melham [ 14 ] , pages 385–396 . [ 20 ] Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . Isabelle/HOL : A Proof
#79 PWS Publishing Company , 1995 . [ 14 ] Joe Hurd and Tom Melham , editors . Theorem Proving in Higher Order Logics : TPHOLs 2005 , LNCS 3603 . Springer , 2005 . [ 15 ] Laurence Kirby . Addition and multiplication of sets . Mathematical Logic Quarterly , 53 ( 1 ) :52–65 , 2007 . [ 16 ] Kenneth Kunen . Set Theory : An Introduction to Independence Proofs . North-Holland , 1980 . [ 17 ] Andreas Lochbihler . Formalising finfuns — generating code for functions as data from Isabelle/HOL . In Stefan Berghofer , Tobias Nipkow , Christian Urban , and Makarius Wenzel , editors , TPHOLs , volume 5674 of Lecture Notes in Computer Science , pages 310–326 . Springer , 2009 . [ 18 ] Tobias Nipkow . More Church-Rosser proofs ( in Isabelle/HOL ) . Journal of Automated Reasoning , 26:51–66 , 2001 . [ 19 ] Tobias Nipkow and Lawrence C. Paulson . Proof pearl : Defining functions over finite sets . In Hurd and Melham [ 14 ] , pages 385–396 . [ 20 ] Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . Isabelle/HOL : A Proof Assistant for Higher-Order Logic . Springer , 2002 . An up-to-date version is distributed with Isabelle . [ 21 ] Michael Norrish and Ren´e Vestergaard . Proof pearl : de Bruijn terms really do work . In Klaus Schneider and Jens Brandt , editors , Theorem Proving in Higher Order Logics : TPHOLs 2007 , LNCS 4732 , pages 207–222 . Springer , 2007 . [ 22 ] Russell O ’ Connor . Essential incompleteness of arithmetic verified by Coq . In Hurd and Melham [ 14 ] , pages 245–260 . [ 23 ] Russell S. S. O ’ Connor . Incompleteness & Completeness : Formalizing Logic and Analysis in Type Theory . PhD thesis , Radboud University Nijmegen , 2009 . [ 24 ] Lawrence C. Paulson . Set theory for verification : I . From foundations to functions . Journal of Automated Reasoning , 11 ( 3 ) :353–389 , 1993 . [ 25 ] Lawrence C. Paulson . The relative consistency of the axiom of choice — mechanized using Isabelle/ZF . LMS Journal of Computation and Mathematics , 6:198–248 , 2003. http : //www.lms.ac.uk/jcm/6/lms2003-001/ . [ 26 ] Lawrence C. Paulson . G¨odel ’ s incompleteness theorems . Archive of Formal Proofs , November 2013. http : //afp.sf.net/entries/Incompleteness.shtml , Formal proof development . [ 27 ] Lawrence C. Paulson . A machine-assisted proof of G¨odel ’ s incompleteness theorems for the theory of hereditarily finite sets . Review of Symbolic Logic , 7 ( 3 ) :484–498 , September 2014 . [ 28 ] Andrew M. Pitts . Nominal Sets : Names and Symmetry in Computer Science . Cambridge University Press , 2013 . [ 29 ] Natarajan Shankar . Proof-checking Metamathematics . PhD thesis , University of Texas at Austin , 1986 . [ 30
#80 Connor . Incompleteness & Completeness : Formalizing Logic and Analysis in Type Theory . PhD thesis , Radboud University Nijmegen , 2009 . [ 24 ] Lawrence C. Paulson . Set theory for verification : I . From foundations to functions . Journal of Automated Reasoning , 11 ( 3 ) :353–389 , 1993 . [ 25 ] Lawrence C. Paulson . The relative consistency of the axiom of choice — mechanized using Isabelle/ZF . LMS Journal of Computation and Mathematics , 6:198–248 , 2003. http : //www.lms.ac.uk/jcm/6/lms2003-001/ . [ 26 ] Lawrence C. Paulson . G¨odel ’ s incompleteness theorems . Archive of Formal Proofs , November 2013. http : //afp.sf.net/entries/Incompleteness.shtml , Formal proof development . [ 27 ] Lawrence C. Paulson . A machine-assisted proof of G¨odel ’ s incompleteness theorems for the theory of hereditarily finite sets . Review of Symbolic Logic , 7 ( 3 ) :484–498 , September 2014 . [ 28 ] Andrew M. Pitts . Nominal Sets : Names and Symmetry in Computer Science . Cambridge University Press , 2013 . [ 29 ] Natarajan Shankar . Proof-checking Metamathematics . PhD thesis , University of Texas at Austin , 1986 . [ 30 ] Natarajan Shankar . Metamathematics , Machines , and G¨odel ’ s Proof . Cambridge University Press , 1994 . [ 31 ] Natarajan Shankar . Shankar , Boyer , Church-Rosser and de Bruijn indices . E-mail , 2013 . 38 [ 32 ] S. Swierczkowski . Finite sets and G¨odel ’ s incompleteness th ´ eorems . Dissertationes Mathematicae , 422:1–58 , 2003. http : //journals.impan.gov.pl/dm/Inf/422-0-1.html . [ 33 ] Christian Urban . Nominal techniques in Isabelle/HOL . Journal of Automated Reasoning , 40 ( 4 ) :327–356 , 2008 . [ 34 ] Christian Urban and Cezary Kaliszyk . General bindings and alpha-equivalence in Nominal Isabelle . Logical Methods in Computer Science , 8 ( 2:14 ) :1–35 , 2012 .
#81 . General bindings and alpha-equivalence in Nominal Isabelle . Logical Methods in Computer Science , 8 ( 2:14 ) :1–35 , 2012 .