Type Theory exploration

 Type Theory

My understanding of Type theory.

Defining natural numbers:

zero:Nat

succ(n:Nat):Nat

So for example defining the number 2:

succ(succ(zero)):Nat

same as???

isNat(zero)

ForAll(n) :  isNat(n)=>isNat(succ(n))

We can define operations like plus and times and equals

//define proofs that  n==n

equals(zero,zero):Equals<zero,zero>

equals(succ(n:Nat),succ(n:Nat)):Equals<succ(n:Nat),succ(n:Nat)>


Proofs and Dependent types

Define a dependent type Even<n:Nat> which is a proof that n is even. 

{a:Nat, p:Equals<times(2,a),n>}:Even<n:Nat>

So that for example the following is a proof that 6 is even:

{3, equals(times(2,3),6)}:Even<6>

which becomes {3:Nat,equals(6,6):Equals<6,6>} :Even<6>


{a:Nat , p:Equals<times(2,a),n>}:Even<n:Nat>

isEven(n) = n =>    (a => (isNat(a) & equals(times(2,a),n)))

isEven(6) (3) 


In C syntax

typedef Even<Nat n> { Nat a, Equals<times(2,a),n> p };


Why not (?):

{a:Nat, p:IsTrue<equals(times(2,a),n)>}:Even<n:Nat>

{3,proof}:Even<6>


isEven( isNat(a) , equals(times(2,a),n)  , n)


larger(0,1):LargerThan<0,1>

larger(n,succ(n)):LargerThan<n,succ(n)>

larger(succ(n),succ(n)):LargerThan<succ(n),succ(n)>


{a:Nat, b:Nat, p1:LargerThan<1,a>,p2:LargerThan<1,b>, p3:Equals<times(a,b),n>}:  Composite<n:Nat>




Proof:

{2,3,larger(1,2),larger(1,3),equals(times(2,3),6)}:Composite<6>

isComposite = n->(a->b->  a & b & isLarger(1,a) & isLarger(1,b) & a*b=n)


f(x:Nat, p1:isComposite<n> ):G


(isNat(x) && isComposite(x)(a)(b) ==> isG(x))








proof:IsTrue<true>


{a:Nat, b:Nat, p1:IsTrue<larger(1,a)>,p2:IsTrue<larger(1,b)>, p3:IsTrue<equals(times(a,b),n)>}:  Composite<n:Nat>


Proof 1+1=2


sum(a:Nat,b:Nat):Sum<a,b>

zero_plus(n:Nat):Equals<Sum<zero,n>,n>

:Equals<x:Sum<a,b>,c:Nat>

Equals



isNat(a) & isNat(b) & larger(1,a) & larger(1,b) & equals(a*b,n)  =>  isComposite(c)


{a:Nat-> b:Nat -> c: Nat -> n:Nat -> a^n+b^n=c^n }:FermatLastTheorem


FermatLastTheorem = (a,b,c,n)=>(a^n+b^n=c^n)


Comments

Post a Comment

Popular posts from this blog

Vortex Solution to Navier Stokes Equations

Image
This is a solution I found to the Navier Stokes equations . It uses the flow lines of the Hopf Fibration (which is basically just a way of covering the entire 3D space in circles). The flow lines can be seen in this image below: You can see my paper here. Solution to Navier-Stokes equation . Unfortunately I won't get a million pounds for winning the Clay Millennium prize because this is a compressible not incompressible solution. :( Oh, well. Nice try! I think it's pretty nice anyway. :) Also it uses the nice identity: which paramaterizes the Pythagorean quadruples!
Read more

Distance Geometry in Superspace

We can define a distance invariant under superspace transformations: \[ R^2 = |x-y|^2 + \theta \gamma_\mu(x-y)^\mu \zeta \] For D space-time dimensions and E Grassman dimensions, does this satisfy a Cayley-Menger type equation? In 2 dimensions we know the volume of a tetrahedron is zero. Or: \[ \det \begin{bmatrix} 0 & R_{12} & R_{13} & R_{14} & 1\\ R_{12} & 0 & R_{23} & R_{24} & 1\\ R_{13} & R_{23} & 0 & R_{34} &1\\ R_{14} & R_{24} & R_{34} & 0 &1 \\ 1&1&1&1&0 \end{bmatrix} =0 \] What about when D=11 and E=32 ? Simplest is D=1, E=2 with (?): \[ R^2 = (x-y)^2 + (x-y)(\theta \zeta + \zeta^* \theta^* ) \] with for example: \[ R^4 = (x-y)^4 + 2 (x-y)^3(\theta \zeta + \zeta^* \theta^* ) + 2(x-y)^2( \theta \theta^* \zeta \zeta^* ) \] \[ R^6 = (x-y)^6 + 3 (x-y)^5(\theta \zeta + \zeta^* \theta^* ) + 6(x-y)^4( \theta \theta^* \zeta \zeta^* ) \] Then the area of the triangle is 0 (or an
Read more