Skip to content

Instantly share code, notes, and snippets.

@lambduli

lambduli/Nat.dt Secret

Last active May 18, 2024 20:19
Show Gist options
  • Save lambduli/d99a935f00845b910402d73976fa41a5 to your computer and use it in GitHub Desktop.
Save lambduli/d99a935f00845b910402d73976fa41a5 to your computer and use it in GitHub Desktop.
Download ZIP
This is a proof of a totality of addition on natural numbers in peano arithmetics. Written in the Fitch-style notation.
Raw
Nat.dt
module ℕ
constants : Zero, Suc
axiom nat-zero : ℕ(Zero)
axiom nat-suc : ∀ n : ℕ(n) ==> ℕ(Suc(n))
axiom sum-zero : ∀ n : ℕ(n) ==> Sum(Zero , n , n)
axiom sum-suc : ∀ n₁ n₂ n₃ : ℕ(n₁) ==>
ℕ(n₂) ==>
ℕ(n₃) ==>
Sum( n₁ , n₂ , n₃ ) ==> Sum( Suc(n₁) , n₂ , Suc(n₃) )
-- Now I need some axiom of induction.
axiom ind-sum : -- The base case.
{ ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Zero , n₂ , n₃ ) } ==>
-- The inductive case.
[ ∀ n : ℕ(n) ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n , n₂ , n₃ ) } ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n) , n₂ , n₃ ) } ] ==>
{ ∀ n₁ : ℕ(n₁) ==> ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n₂ , n₃ ) }
theorem totality : ∀ n₁ : ℕ(n₁) ==> ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n₂ , n₃ )
|
|------------------------------------------------------------------
|
| -- Let's prove the base case: { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Zero , n₂ , n₃ ) }
|
| uni-n2 : | for all n2
| |------------------------------------------------------
| |
| | N2 : | p1 : ℕ(n2) -- the goal is: ∃ n₃ : ℕ(n₃) ∧ Sum( Zero , n₂ , n₃ )
| | |----------------------------------------------
| | |
| | | sum-z1 : ℕ(n2) ==> Sum( Zero , n2 , n3 ) by rule ∀-elim on sum-zero
| | | sum-z2 : Sum( Zero , n2 , n3 ) by rule ==>-elim on sum-z1, p1
| | | n3∧sum : ℕ(n3) ∧ Sum( Zero , n2 , n3 ) by rule ∧-intro on p1, sum-z2
| | | ∃ n₃ : ℕ(n₃) ∧ Sum( Zero , n2 , n₃ ) by rule ∃-intro on n3∧sum
| |
| | ℕ(n2) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Zero , n2 , n₃ ) by rule ==>-intro on N2
|
| base : { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Zero , n₂ , n₃ ) } by rule ∀-intro on uni-n2
|
|
|
| -- Let's prove the inductive case: [ ∀ n : ℕ(n) ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n , n₂ , n₃ ) } ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n) , n₂ , n₃ ) } ]
|
| uni-n : | for all n₁
| |--------------------------------------------------------
| |
| | N1 : | p2 : ℕ(n₁)
| | |--------------------------------------------------------------------
| | |
| | |
| | | impl : | p3 : ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n₂ , n₃ ) -- the goal is: ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n₂ , n₃ )
| | | |--------------------------------------------------------------------------------------------------------------------------------------------------
| | | |
| | | | -- ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n₂ , n₃ )
| | | |
| | | | uni-n2b : | for all n2b -- the goal is: ℕ(n2b) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n2b , n₃ )
| | | | |--------------------------------------------------------------------------
| | | | |
| | | | | N2b : | p4 : ℕ(n2b) -- the goal is: ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n2b , n₃ )
| | | | | |-------------------------------------------------------------
| | | | | |
| | | | | | d1 : ℕ(n2b) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n2b , n₃ ) by rule ∀-elim on p3
| | | | | | d2 : ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n2b , n₃ ) by rule ==>-elim on d1, p4
| | | | | |
| | | | | | exn3 : | p5 : ℕ(n3b) ∧ Sum( n₁ , n2b , n3b ) for some n3b
| | | | | | |--------------------------------------------------------
| | | | | | | -- the goal is: ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n2b , n₃ )
| | | | | | |
| | | | | | | d3 : ℕ(n3b) by rule ∧-elim on p5
| | | | | | | d4 : Sum( n₁ , n2b , n3b ) by rule ∧-elim on p5
| | | | | | |
| | | | | | | sum-s : ℕ(n₁) ==> ℕ(n2b) ==> ℕ(n3b) ==> Sum( n₁ , n2b , n3b ) ==> Sum( Suc(n₁) , n2b , Suc(n3b) ) by rule ∀-elim on sum-suc
| | | | | | | sum-n1+1 : Sum( Suc(n₁) , n2b , Suc(n3b) ) by rule ==>-elim on sum-s, p2, p4, d3, d4
| | | | | | |
| | | | | | | d5 : ℕ(n3b) ==> ℕ(Suc(n3b)) by rule ∀-elim on nat-suc
| | | | | | | d6 : ℕ(Suc(n3b)) by rule ==>-elim on d5, d3
| | | | | | | d7 : ℕ(Suc(n3b)) ∧ Sum( Suc(n₁) , n2b , Suc(n3b) ) by rule ∧-intro on d6, sum-n1+1
| | | | | | | ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n2b , n₃ ) by rule ∃-intro on d7
| | | | | |
| | | | | | ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n2b , n₃ ) by rule ∃-elim on d2, exn3
| | | | |
| | | | | ℕ(n2b) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n2b , n₃ ) by rule ==>-intro on N2b
| | | |
| | | | ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n₂ , n₃ ) by rule ∀-intro on uni-n2b
| | |
| | | { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n₂ , n₃ ) } ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n₂ , n₃ ) } by rule ==>-intro on impl
| |
| | ℕ(n₁) ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n₂ , n₃ ) } ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n₁) , n₂ , n₃ ) } by rule ==>-intro on N1
|
| step : [ ∀ n : ℕ(n) ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n , n₂ , n₃ ) } ==> { ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( Suc(n) , n₂ , n₃ ) } ] by rule ∀-intro on uni-n
|
|
| -- Let's use the induction now.
| ∀ n₁ : ℕ(n₁) ==> ∀ n₂ : ℕ(n₂) ==> ∃ n₃ : ℕ(n₃) ∧ Sum( n₁ , n₂ , n₃ ) by rule ==>-elim on ind-sum, base, step
Raw
ℕ.dt
-- This module uses custom syntax and judgments.
module ℕ
syntax ℕ = Zero -- Zero : ℕ
| Suc(ℕ) -- Suc : ℕ -> ℕ
judgment sum = Sum(ℕ, ℕ, ℕ)
rule schema sum-zero for all objects (n : ℕ) :
|
|-------------------------------------- sum-zero
| Sum(Zero, n, n)
rule schema sum-suc for all objects (m : ℕ), (n : ℕ), (o : ℕ) :
| Sum(m, n, o)
|-------------------------------------- sum-suc
| Sum(Suc(m), n, Suc(o))
theorem total : ∀ (n₁ : ℕ) (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( n₁ , n₂ , n₃ )
∀ (n₁ : ℕ) (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( n₁ , n₂ , n₃ ) by induction :
case Zero ->
|
|--------------------------------------------------------------------------------------------
| -- let's prove the base case
| -- ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( Zero , n₂ , n₃ )
|
| uni-n2 : | for all (n2 : ℕ)
| |--------------------------------------------------------------------------------
| |
| | sz : Sum( Zero , n2 , n3 ) by rule sum-zero
| | ∃ (n₃ : ℕ) : Sum( Zero , n2 , n₃ ) by rule ∃-intro on sz
|
| result : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( Zero , n₂ , n₃ ) by rule ∀-intro on uni-n2
case Suc(m) ->
| induction-hypothesis : ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( m , n₂ , n₃ )
|--------------------------------------------------------------------------------------------
| -- let's prove the inductive case
| -- { ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( m , n₂ , n₃ ) }
| -- ==> { ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( Suc(m) , n₂ , n₃ ) }
|
| uni-n2b : | for all (N2 : ℕ)
| |--------------------------------------------------------------------------------
| |
| | d1 : ∃ (n₃ : ℕ) : Sum( m , N2 , n₃ ) by rule ∀-elim on induction-hypothesis
| |
| | exn3 : | p5 : Sum( m , N2 , n3 ) for some (n3 : ℕ)
| | |----------------------------------------------------------------------
| | |
| | | sum-m+1 : Sum( Suc(m) , N2 , Suc(n3) ) by rule sum-suc on p5
| | | ∃ (n₃ : ℕ) : Sum( Suc(m) , N2 , n₃ ) by rule ∃-intro on sum-m+1
| |
| | ∃ (n₃ : ℕ) : Sum( Suc(m) , N2 , n₃ ) by rule ∃-elim on d1, exn3
|
| ∀ (n₂ : ℕ) : ∃ (n₃ : ℕ) : Sum( Suc(m) , n₂ , n₃ ) by rule ∀-intro on uni-n2b
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment