Introduction:
Introduction:
Picture entering a world where ideas unfold like puzzles waiting to be solved. Our adventure starts with a curious look into a rule called double negation elimination and formalizing it using the Wolfram Axiom. It’s a fascinating concept that, when explored, reveals the core of logic itself.
Building Blocks:
Building Blocks:
Before we dive in, let’s understand the basics of propositional logic. It’s like a playground where we encounter statements of Binary nature either true or false—the starting point for logical thinking. Propositional logic is the examination of the meanings and inferential relationships among sentences, focusing on a specific class of logical operators called propositional connectives. These operators play a crucial role in determining the truth value of sentences. While the significance of propositional connectives was noted as early as Aristotle, it wasn’t until the nineteenth century that propositional logic as a distinct field emerged. This then emphasized studying the behavior of propositional connectives in isolation from other operators, marking a significant advancement in logical analysis.
Meet Lean:
Meet Lean:
Lean is an automatic and interactive theorem prover. It can be used to create specifications, build mathematical libraries, and solve constraints. Developed at Microsoft Research, Lean excels in providing a robust platform for expressing and validating mathematical truths using dependent type theory. What sets Lean apart is its ability to bridge the gap between logic and formalization. Its user-friendly interface and extensive libraries make it an accessible yet sophisticated tool, inviting novice and seasoned mathematicians and computer scientists to explore the connections between logic and programming.
Double Negation Elimination (DNE):
Double Negation Elimination (DNE):
Since we use DNE as an example it is significant to know a bit about what it goes over. DNE has been significant in logic because it underscores a fundamental aspect of logical equivalence and simplicity. The principle states that if you negate something twice, it is equivalent to the original statement. Symbolically, ¬¬P ≡ P, where P is any proposition. For example saying “It is not not raining.” is equivalent to saying “It is raining.” This helps us simplify and prove other logical propositions.
Formalizing Axioms:
Formalizing Axioms:
My project focuses on the formalization of double negation elimination using the Lean proof assistant and using this to maybe formalize Wolfram axiom. The goal is to use the precision of Lean in capturing and verifying the fundamental logical principle of double negation elimination. By translating this concept into Lean’s formal language, the project aims to contribute to the understanding of how advanced proof assistants can be utilized to express and validate logical properties in an efficient manner and then use it on our axiom. This deep dive emphasizes the bridge between logical reasoning and formalization, highlighting the significance of mathematical thinking within Lean.
The code for this is found below:
The code for this is found below:
import Mathlib . Logic . Basic
example (P : Prop) : ¬ ¬ P = P := by
--Introduce hypothesis
intro h
--Introduce the goal
apply by_contradiction
--Assume negation of proposition
intro
--Use the hypothesis and the assumed negation to derive a contradiction
apply h
--Conclude using LEM
rfl
example (P : Prop) : ¬ ¬ P = P := by
--Introduce hypothesis
intro h
--Introduce the goal
apply by_contradiction
--Assume negation of proposition
intro
--Use the hypothesis and the assumed negation to derive a contradiction
apply h
--Conclude using LEM
rfl
This Lean4 code presents a proof for the double negation elimination property, expressed as ¬¬P = P for any proposition P. First, a hypothesis h is introduced, representing the assumption of ¬¬P. The goal is then introduced, and the by_contradiction tactic is applied, setting the stage for a proof by contradiction. Subsequently, an assumption is made about the negation of the original proposition. Leveraging the introduced hypothesis and the assumed negation, a contradiction is derived using the apply h tactic. The proof concludes by invoking the Law of Excluded Middle (LEM), symbolized by rfl, establishing that ¬¬P indeed is equivalent to P.
Now using this way to formalize an axiom we can potentially try to formalize the Wolfram Axiom. The Wolfram axiom is as follows:
Now using this way to formalize an axiom we can potentially try to formalize the Wolfram Axiom. The Wolfram axiom is as follows:
axiom wolfram_axiom (a b c : A) : (((a * b) * c) * (a * ((a * c) * a))) = c
This axiom tells us that it is a mathematical relationship that describes a property of the binary operation represented by the dot operator which can be either NAND or NOR. Using this we can start formalizing the proof as follows:
--Declare type variables
variable {A : Type}
variable {a b c α : A}
--Declare binary operation dot with infix notation *
axiom dot : A -> A -> A
infix : 50 " * " = > dot
--Declare the Wolfram axiom
axiom wolfram_axiom (a b c : A) : a = (((b * c) * a) * (b * ((b * a) * b)))
--Double negation
theorem double_negation (a : A) : ((a * a) * (a * a)) = a := by
-- CriticalPairLemma1
-- a * ((a * b) * a) == b * ((a * c) * (((a * c) * (a * ((a * b) * a))) * (a * c)))
have sr1 := wolfram_axiom b a c
have cpl1 := wolfram_axiom (a * ((a * b) * a)) (a * c) b
--Apply the Wolfram axiom and rewrite at the specified occurrence
rewrite (config := {occs := . pos [1]}) [< -sr1] at cpl1
-- CriticalPairLemma2
-- a == (b * a) * (((c * α) * b) * ((((c * α) * b) * a) * ((c * α) * b)))
have sr2 := wolfram_axiom b c α
have cpl2 := wolfram_axiom a ((c * α) * b) (c * ((c * b) * c))
--Apply the Wolfram axiom and rewrite at the specified occurrence
rewrite (config := {occs := . pos [1]}) [< -sr2] at cpl2
-- Placeholder for rest of the proof
sorry
variable {A : Type}
variable {a b c α : A}
--Declare binary operation dot with infix notation *
axiom dot : A -> A -> A
infix : 50 " * " = > dot
--Declare the Wolfram axiom
axiom wolfram_axiom (a b c : A) : a = (((b * c) * a) * (b * ((b * a) * b)))
--Double negation
theorem double_negation (a : A) : ((a * a) * (a * a)) = a := by
-- CriticalPairLemma1
-- a * ((a * b) * a) == b * ((a * c) * (((a * c) * (a * ((a * b) * a))) * (a * c)))
have sr1 := wolfram_axiom b a c
have cpl1 := wolfram_axiom (a * ((a * b) * a)) (a * c) b
--Apply the Wolfram axiom and rewrite at the specified occurrence
rewrite (config := {occs := . pos [1]}) [< -sr1] at cpl1
-- CriticalPairLemma2
-- a == (b * a) * (((c * α) * b) * ((((c * α) * b) * a) * ((c * α) * b)))
have sr2 := wolfram_axiom b c α
have cpl2 := wolfram_axiom a ((c * α) * b) (c * ((c * b) * c))
--Apply the Wolfram axiom and rewrite at the specified occurrence
rewrite (config := {occs := . pos [1]}) [< -sr2] at cpl2
-- Placeholder for rest of the proof
sorry
The provided Lean code seeks to formally prove the “double negation” theorem by employing the Wolfram axiom, which specifies a particular relationship between elements in a given type. The code introduces Critical Pair Lemmas based on the Wolfram axiom, expressing specific connections between elements. The rewrite tactic is then employed to simplify expressions by applying the Wolfram axiom in specific occurrences. The goal is to demonstrate that the expression ((a * a) * (a * a)) is equal to a. However, the proof is currently incomplete, marked by the sorry placeholder, indicating the need for additional steps to conclude the formalization of the theorem.
Now we will go over a proof function, dataset, graph and notebook in the next few sections.
Now we will go over a proof function, dataset, graph and notebook in the next few sections.
ProofObjectToLean[po_]:=Module[{leanCode},(*ConvertproofobjectpotoLeansourcecode*)leanCode=StringJoin["theorem my_proof : ",ToString[po]," := by\n sorry\n"];(*ReturntheLeansourcecodeasastring*)leanCode]proofObject="variable {A : Type}variable {a b c α: A}axiom dot : A -> A -> Ainfix:50 \" * \" => dotaxiom wolfram_axiom (a b c : A) : a = (((b * c) * a) * (b * ((b * a) * b)))theorem double_negation (a : A) : ((a * a) * (a * a)) = a := by -- CriticalPairLemma1 -- a * ((a * b) * a) == b * ((a * c) * (((a * c) * (a * ((a * b) * a))) * (a * c))) have sr1 := wolfram_axiom b a c have cpl1 := wolfram_axiom (a * ((a * b) * a)) (a * c) b rewrite (config := {occs := .pos [1]}) [<-sr1] at cpl1 -- CriticalPairLemma2 -- a == (b * a) * (((c * α) * b) * ((((c * α) * b) * a) * ((c * α) * b))) have sr2 := wolfram_axiom b c α have cpl2 := wolfram_axiom a ((c * α) * b) (c * ((c * b) * c)) rewrite (config := {occs := .pos [1]}) [<-sr2] at cpl2 sorry";leanSourceCode=ProofObjectToLean[proofObject]
Out[]=
theorem my_proof : variable {A : Type}variable {a b c α: A}axiom dot : A -> A -> Ainfix:50 " * " => dotaxiom wolfram_axiom (a b c : A) : a = (((b * c) * a) * (b * ((b * a) * b)))theorem double_negation (a : A) : ((a * a) * (a * a)) = a := by -- CriticalPairLemma1 -- a * ((a * b) * a) == b * ((a * c) * (((a * c) * (a * ((a * b) * a))) * (a * c))) have sr1 := wolfram_axiom b a c have cpl1 := wolfram_axiom (a * ((a * b) * a)) (a * c) b rewrite (config := {occs := .pos [1]}) [<-sr1] at cpl1 -- CriticalPairLemma2 -- a == (b * a) * (((c * α) * b) * ((((c * α) * b) * a) * ((c * α) * b))) have sr2 := wolfram_axiom b c α have cpl2 := wolfram_axiom a ((c * α) * b) (c * ((c * b) * c)) rewrite (config := {occs := .pos [1]}) [<-sr2] at cpl2 sorry := by sorry
Out[]=
Out[]=
Success
Prove an elementary theorem like ours as follows
In[]:=
proof=FindEquationalProof["DoubleNegation","WolframAxioms"]["ProofObject"]
Out[]=
ProofObject[ProofObject]
Now we show the abstract proof network, with tooltips showing the intermediate expressions using the graph function:
In[]:=
proof=FindEquationalProof["DoubleNegation","WolframAxioms"]["ProofGraph"]
Out[]=
We then show the complete list of proof steps as a Dataset object:
In[]:=
proof=FindEquationalProof["DoubleNegation","WolframAxioms"]["ProofDataset"]
Now we typeset a natural language argument as follows:
Conclusion:
Conclusion:
In the realm of formalizing mathematical relationships, this project delved into the intricacies of the Wolfram axiom within Lean, aiming to prove the “double negation” theorem via the wolfram axiom. Leveraging the axiom’s expressiveness, Critical Pair Lemmas were introduced to mention specific connections between mathematical elements. The application of the rewrite tactic further demonstrated the power of the Wolfram axiom in simplifying complex expressions. While the full proof of the “double negation” theorem is a work in progress, the structured approach using the Wolfram axiom taken in this project lays the groundwork for future exploration and refinement.
Sources:
Sources:
1. Magnus, PD (2023), An Introduction to Formal Logic, DigiCat.
CITE THIS NOTEBOOK
CITE THIS NOTEBOOK
Lean Exploration: A Deep Dive into the Wolfram Axiom
by Shriya Thakur
Wolfram Community, STAFF PICKS, January 12, 2024
https://community.wolfram.com/groups/-/m/t/3100869
by Shriya Thakur
Wolfram Community, STAFF PICKS, January 12, 2024
https://community.wolfram.com/groups/-/m/t/3100869