Quellcode-Bibliothek propositions.c Sprache: C

//-------------------------------------------
//      The following functions
//      have been derived from
//      Goedels 46+ propositions.
//
//  "On Formally Undecidable Propositions of
//   Principa Mathematics and Related Systems"
//      by Kurt Goedel, Vienna
//
//      Translated by B. Meltzer
//      Dover Publications 1962, 1992
//
//-------------------------------------------
//   EXISTS(v,low,high,cond,res)
//   := find first v>=low and v<=high
//      which satisfies cond andreturn res
//
//   FORALL(v,low,high,cond)
//   := do next check for all v>=low and v<=high
//
//-------------------------------------------
// (c) Context IT GmbH, Ahrensburg, Germany
//     Web: http://www.cococo.de
//
//   Version: 0.8 July, 7th 2012
//   Modified: NN
//
//   Please send bug reports and feature
//   requests to info@cococo.de
//-------------------------------------------
#include "defs.nat.h"
#include "propositions.h"
//--------------------------------------
//  1. Proposition
// x is divisible by y
//--------------------------------------
BOOLFUN2(divisible,x,y)
  EXISTS(z,ONE,x,Eq(x,Mul(y,z)),TRUE);
RET(FALSE)

//--------------------------------------
//  2. Proposition
// x is a prime number
//--------------------------------------
BOOLFUN1(Prim,x)
  if (Eq(x,ONE)) RESULT(TRUE);
  EXISTS(z,TWO,x,And(Ne(z,x),divisible(x,z)),FALSE);
RET(TRUE)
//--------------------------------------
//  3. Function (2 parameters)
// the n-th prime number contained in x
//--------------------------------------
NATFUN2(Pr2,n,x)
  if (Ne(n,ZERO)) {
    EXISTS(y,Add(Pr2(Sub(n,ONE),x),ONE),x,And(Prim(y),divisible(x,y)),y);}
RET(ZERO)

//--------------------------------------
//  4. Function
// faculty of n
// *** bug: Fac(0) undefiniert
//--------------------------------------
NATFUN1(Fac,n)
if (Eq(n,ZERO)) RESULT(ZERO)
else if (Eq(n,ONE)) RESULT(ONE)
RET(Mul(n,Fac(Sub(n,ONE))))

//--------------------------------------
//  5. Function (1 parameter)
// n-th prime number
// optimization: NAT n_1
//--------------------------------------
NATFUN1(Pr1,n)
if (Ne(n,ZERO)) {
   NAT n_1=Pr1(Sub(n,ONE));
   EXISTS(y,Add(n_1,ONE),Add(Fac(n_1),ONE),Prim(y),y);}
RET(ZERO)

//--------------------------------------
//  6. Function
// n-th term of a series of numbers
// assigned to x
//--------------------------------------
NATFUN2(Gl,n,x)
  NAT pp=Pr2(n,x);
  EXISTS(y,ONE,x,And(divisible(x,Pow(pp,y)),Not(divisible(x,Pow(pp,Add(y,ONE))))),y);
RET(ZERO)

//--------------------------------------
//  7. Function
// length a series of numbers  of
// assigned to x
//--------------------------------------
NATFUN1(l,x)
  EXISTS(y,ONE,x,And(Gt(Pr2(y,x),ZERO),Eq(Pr2(Add(y,ONE),x),ZERO)),y);
RET(ZERO)

//--------------------------------------
//  8. Function
// join together two finite series of numbers
//--------------------------------------
//  8.1
BOOLFUN2(Join1,x,z)
  EXISTS(n,ONE,l(x),Ne(Gl(n,z),Gl(n,x)),FALSE);
RET(TRUE)
//  8.2
BOOLFUN3(Join2,x,y,z)
  EXISTS(n,ZERO,l(y),Ne(Gl(Add(n,l(x)),z),Gl(n,y)),FALSE);
RET(TRUE)
//  8.
NATFUN2(Join,x,y)
  EXISTS(z,ONE,Pow(Pr1(Add(l(x),l(y))),Add(x,y)),And(Join1(x,z),Join2(x,y,z)),z);
RET(ZERO)

//--------------------------------------
//  9. Function
// a series of numbers
// with a single element x
//--------------------------------------
NATFUN1(R,x)
  RET(Pow(TWO,x))

//--------------------------------------
//  10. Function
// bracketing of a a series of numbers
//--------------------------------------
NATFUN1(E,x)
  RET(Join(R(ELEVEN),Join(x,R(THIRTEEN))))

//--------------------------------------
//  11. Function  (2 parameters)
// x is a variable of n-th type
//--------------------------------------
BOOLFUN2(Var2,n,x)
  if (Ne(n,ZERO)) EXISTS(z,Add(THIRTEEN,ONE),x,And(Prim(z),Eq(x,Pow(z,n))),TRUE);
RET(FALSE)

//--------------------------------------
//  12. Proposition  (1 parameter)
// x is a variable
//--------------------------------------
BOOLFUN1(Var1,x)
  EXISTS(n,ONE,x,Var2(n,x),TRUE);
RET(FALSE)

//--------------------------------------
//  13. Function
// negation of x
//--------------------------------------
NATFUN1(Neg,x)
  RET(Join(R(FIVE),E(x)))

//--------------------------------------
//  14. Function
// disjunction of x, y
//--------------------------------------
NATFUN2(Dis,x,y)
  RET(Join(E(x),Join(R(SEVEN),E(y))))

//--------------------------------------
//  15. Function
// generalization of y
// by means of variable x
//--------------------------------------
NATFUN2(Gen,x,y)
  RET(Join(R(x),Join(R(NINE),E(y))))

//--------------------------------------
//  16. Function
// n-fold prefixing of the sign f before x
//--------------------------------------
NATFUN2(N,n,x)
  if (Eq(n,ZERO)) RESULT(x)
RET(Join(R(THREE),N(Sub(n,ONE),x)))

//--------------------------------------
//  17. Function
// number sign for number n
//--------------------------------------
NATFUN1(Z,n)
  RET(N(n,R(ONE)))

//--------------------------------------
//  18. Proposition  (1 parameter)
// x is a sign of first type
//--------------------------------------
BOOLFUN1(Typ1,x)
  FORALL(n,ONE,x)
    EXISTS(m,ONE,x,Or(Eq(m,ONE),And(Var2(ONE,m),Eq(x,N(n,R(m))))),TRUE);
  ENDFOR
RET(FALSE)

//--------------------------------------
//  19. Proposition  (2 parameters)
// x is a sign of n-th type
//--------------------------------------
BOOLFUN2(Typ2,n,x)
  if    (Eq(n,ONE)) RESULT(Typ1(x))
  else  EXISTS(v,ONE,x,And(Var2(n,v),Eq(x,R(v))),TRUE);
RET(FALSE)

//--------------------------------------
//  20. Proposition
// x is an elementary type
//--------------------------------------
BOOLFUN1(Elf,x)
  FORALL(y,ONE,x)
    FORALL(z,ONE,x)
      EXISTS(n,ONE,x,And(Typ2(n,y),And(Typ2(Add(n,ONE),z),Eq(x,Join(z,E(y))))),TRUE)
    ENDFOR
  ENDFOR
RET(FALSE)

//--------------------------------------
//  21. Proposition
// nn
//--------------------------------------
BOOLFUN3(Op,x,y,z)
  if      (Eq(x,Neg(y))) RESULT(TRUE)
  else if (Eq(x,Dis(y,z))) RESULT(TRUE)
  else EXISTS(v,ONE,x,And(Var1(v),Eq(x,Gen(v,y))),TRUE);
RET(FALSE)

//--------------------------------------
//  22. Proposition
// x is a series of formula
// where each formula is either elementary
//  or it arises from negation, disjunction,
//  and generalization
//--------------------------------------
BOOLFUN1(FR,x)
  FORALL(n,ONE,x)
    if (And(Lt(ZERO,n),Le(n,l(x)))) RESULT(Elf(Gl(n,x)))
    else
      FORALL(p,ONE,n)
        EXISTS(q,ONE,n,Op(Gl(n,x),Gl(p,x),Gl(q,x)),TRUE);
      ENDFOR
  ENDFOR
RET(FALSE)

//--------------------------------------
//  23. Proposition
// x is a formula
//--------------------------------------
BOOLFUN1(Form,x)
  EXISTS(n,ONE,Pow(Pr1(Pow(l(x),TWO)),Mul(x,Pow(l(x),TWO))),And(FR(n),Eq(x,Gl(l(n),n))),TRUE);
RET(FALSE)

//--------------------------------------
//  24. Proposition
// variable v is bound at n-th place in x
//--------------------------------------
BOOLFUN3(Geb,v,n,x)
  if (And(Var1(v),Form(x)))
    FORALL(a,ONE,x)
      FORALL(b,ONE,x)
        EXISTS(c,ONE,x,And(Eq(x,Join(a,Join(Gen(v,b),c))),And(Form(b),And(Le(Add(l(a),ONE),n),Le(n,Add(l(a),l(Gen(v,b))))))),TRUE);
      ENDFOR
    ENDFOR
RET(FALSE)

//--------------------------------------
//  25. Proposition  (3 parameters)
//  variable v is free at n-th place in x
//--------------------------------------
BOOLFUN3(Fr3,v,n,x)
  RET(And(Var1(v),And(Form(x),And(Eq(v,Gl(n,x)),And(Le(n,l(x)),Geb(v,n,x))))))

//--------------------------------------
//  26. Proposition   (2 parameters)
// v occurs in x as a free variable
//--------------------------------------
BOOLFUN2(Fr2,v,x)
  EXISTS(n,ONE,l(x),Fr3(v,n,x),TRUE);
RET(FALSE)

//--------------------------------------
//  27. Proposition
// substitute y in place of the n-th term of x
//--------------------------------------
NATFUN3(Su,x,n,y)
  FORALL(z,ONE,Pr1(Add(Pow(l(x),l(y)),Add(x,y))))
    FORALL(u,ONE,x)
      EXISTS(v,ONE,x,And(Eq(x,Join(u,Join(R(Gl(n,x)),v))),And(Eq(z,Join(u,Join(y,v))),Eq(n,Add(l(u),ONE)))),v)
    ENDFOR
  ENDFOR
RET(ZERO)

//--------------------------------------
//  28. Function
// (k+1)-th place in x at which v is free in x
// 0 else
//--------------------------------------
NATFUN3(St,k,v,x)
  if (Eq(k,ZERO)) {
    FORALL(n,ONE,l(x))
      EXISTS(p,Add(n,ONE),l(x),And(Fr3(v,n,x),Fr3(v,p,x)),n);
    ENDFOR}
  else {
    FORALL(n,ONE,St(k,v,x))
      EXISTS(p,Add(n,ONE),St(k,v,x),And(Fr3(v,n,x),Fr3(v,p,x)),n);
    ENDFOR}
RET(ZERO)

//--------------------------------------
//  29. Function
// number of places at which v is free in x
//--------------------------------------
NATFUN2(A,v,x)
  EXISTS(n,ONE,l(x),Eq(St(n,v,x),ZERO),n);
RET(ZERO)

//--------------------------------------
//  30. Function
// substitute ...
//--------------------------------------
NATFUN4(Sb4,k,x,v,y)
  if (Eq(k,ZERO)) RESULT(x)
RET(Su(Sb4(Sub(k,ONE),x,v,y),St(k,v,x),y))

//--------------------------------------
//  31. Function
// substitute
//--------------------------------------
NATFUN3(Sb3,x,v,y)
  RET(Sb4(A(v,x),x,v,y))

//--------------------------------------
//  32a. Function
// implication simulation
//--------------------------------------
NATFUN2(Imp,x,y)
  RET(Dis(Neg(x),y))

//--------------------------------------
//  32b. Function
// conjunction simulation
//--------------------------------------
NATFUN2(Con,x,y)
  RET(Neg(Dis(Neg(x),Neg(y))))

//--------------------------------------
//  32c. Function
// equivalence  simulation
//--------------------------------------
NATFUN2(Aeq,x,y)
  RET(Con(Imp(x,y),Imp(y,x)))

//--------------------------------------
//  32d. Function
// existence
//--------------------------------------
NATFUN2(Ex,v,y)
  RET(Neg(Gen(v,Neg(y))))

//--------------------------------------
//  33. Function
// n-th type lift of x
//--------------------------------------
NATFUN2(Th,n,x)
  FORALL(y,ONE,Pow(x,Pow(x,n)))
    EXISTS(k,ONE,l(x),And(Le(Gl(k,x),THIRTEEN),Eq(Gl(k,y),Gl(k,x))),y);
    EXISTS(k,ONE,l(x),And(Gt(Gl(k,x),THIRTEEN),Eq(Gl(k,y),Join(Gl(k,x),Pow(Pr2(ONE,Gl(k,x)),n)))),y);
  ENDFOR
RET(ZERO)

//--------------------------------------
//  34. Proposition
// axioms I(1) to I(3)
//--------------------------------------
BOOLFUN1(Z_Ax,x)
  if      (Eq(x,z1)) RESULT(TRUE)
  else if (Eq(x,z2)) RESULT(TRUE)
  else if (Eq(x,z3)) RESULT(TRUE)
RET(FALSE)

//--------------------------------------
//  35. Proposition
// formula derived by substituton
//--------------------------------------
BOOLFUN2(A1_Ax,n,x)
  EXISTS(y,ONE,x,And(Form(y),Eq(x,Imp(Dis(y,y),y))),TRUE);
RET(FALSE)

//--------------------------------------
//  36. Proposition
// formula derived by substituton
//--------------------------------------
BOOLFUN1(A_Ax,x)
  if      (A1_Ax(ONE,x)) RESULT(TRUE)
  else if (A1_Ax(TWO,x)) RESULT(TRUE)
  else if (A1_Ax(THREE,x)) RESULT(TRUE)
  else if (A1_Ax(FOUR,x)) RESULT(TRUE)
RET(FALSE)

//--------------------------------------
//  37. Proposition
// z contains no variable bound in y
// at position where v is free
//--------------------------------------
BOOLFUN3(Q,z,y,v)
  FORALL(n,ONE,l(y))
    FORALL(m,ONE,l(z))
      EXISTS(w,ONE,z,And(Eq(w,Gl(m,y)),And(Geb(w,n,y),Fr3(v,n,y))),TRUE);
    ENDFOR
  ENDFOR
RET(FALSE)

//--------------------------------------
//  38. Proposition
//  --> bug in paper Sb(v z)
// x is a formula derived from the axiom
// schema III,1 by substitution
//--------------------------------------
BOOLFUN1(L1_Ax,x)
  FORALL(v,ONE,x)
    FORALL(y,ONE,x)
      FORALL(z,ONE,x)
        EXISTS(n,ONE,x,And(Var2(n,v),And(Typ2(n,z),And(Form(y),
        And(Q(z,y,v),Eq(x,Imp(Gen(v,y),Sb3(n,v,z))))))),TRUE);
      ENDFOR
    ENDFOR
  ENDFOR
RET(FALSE)

//--------------------------------------
//  39. Proposition
// x is a formula derived from the axiom
// schema III,2 by substitution
//--------------------------------------
BOOLFUN1(L2_Ax,x)
  FORALL(v,ONE,x)
    FORALL(q,ONE,x)
      EXISTS(p,ONE,x,And(Var1(v),And(Form(p),And(Fr2(v,p),And(Form(q),
        Eq(x,Gen(v,Imp(Dis(p,q),Dis(p,Gen(v,q))))))))),TRUE);
    ENDFOR
  ENDFOR
RET(FALSE)

//--------------------------------------
//  40. Proposition
// x is a formula derived from the axiom
// schema IV,1 by substitution
//--------------------------------------
BOOLFUN1(R_Ax,x)
  FORALL(u,ONE,x)
    FORALL(v,ONE,x)
      FORALL(y,ONE,x)
        EXISTS(n,ONE,x,And(Var2(n,v),And(Var2(Add(n,ONE),u),And(Fr2(u,y),
          And(Form(y),Eq(x,Ex(u,Gen(v,Aeq(Join(R(u),E(R(v))),y)))))))),TRUE);
      ENDFOR
    ENDFOR
  ENDFOR
RET(FALSE)

//--------------------------------------
//  41. Proposition
// ...
//--------------------------------------
BOOLFUN1(M_Ax,x)
  EXISTS(n,ONE,x,(Eq(x,Th(n,z4))),TRUE);
RET(FALSE)

//--------------------------------------
//  42. Proposition
// x is an axiom
//--------------------------------------
BOOLFUN1(Ax,x)
  if      (Z_Ax(x)) RESULT(TRUE)
  else if (A1_Ax(ONE,x)) RESULT(TRUE)
  else if (L1_Ax(x)) RESULT(TRUE)
  else if (L2_Ax(x)) RESULT(TRUE)
  else if (R_Ax(x)) RESULT(TRUE)
  else if (M_Ax(x)) RESULT(TRUE)
RET(FALSE)

//--------------------------------------
//  43. Proposition
// x is an immediate consequence of y and z
//--------------------------------------
BOOLFUN3(Fl,x,y,z)
  if (Imp(z,x)) RESULT(TRUE)
  else EXISTS(v,ONE,x,And(Var1(v),Eq(x,Gen(v,y))),TRUE);
RET(FALSE)

//--------------------------------------
//  44. Proposition
// x is a proof schema
//--------------------------------------
BOOLFUN1(Bw,x)
  FORALL(n,ZERO,l(x))
    if (And(Not(Ax(Gl(n,x))),Gt(l(x),ZERO)))
      FORALL(p,ZERO,n)
        EXISTS(q,ZERO,n,Fl(Gl(n,x),Gl(p,x),Gl(q,x)),FALSE);
      ENDFOR
  ENDFOR
RET(TRUE)

//--------------------------------------
//  45. Proposition
// x is a proof of the formula y
//--------------------------------------
BOOLFUN2(B,x,y)
  RET(And(Bw(x),Eq(Gl(l(x),x),y)))

//--------------------------------------
//  46. Proposition
// x is a provable formula
// (cannot be asserted that it is recursive)
//--------------------------------------
BOOLFUN1(Bew,x)
  EXISTS(y,ZERO,Add(y,ONE),B(y,x),TRUE);  //y+1==TRUE, INFINITE
RET(FALSE)
//--------------------------------------
//
//  Additional Functions
//
//
//--------------------------------------
//  Primetwin
// p, p+2 are primes, p>n
// (unknown if there are infinitely many)
//--------------------------------------
NATFUN1(Primetwin,n)
  EXISTS(p,n,Mul(n,ELEVEN),And(Prim(p),Prim(Add(p,TWO))),p);  //p+1==TRUE, INFINITE
RET(ZERO)
//--------------------------------------
//  Goldbach
// p+q=n where p,q are primes
// (Goldbach's conjecture)
//--------------------------------------
NATFUN1(Goldbach,n)
  if (divisible(n,TWO))
    FORALL(q,ONE,Sub(n,ONE))
      EXISTS(p,ONE,Sub(n,ONE),And(Eq(Add(p,q),n),And(Prim(q),Prim(p))),p)
    ENDFOR
RET(ZERO)
//--------------------------------------
//  Collatz
// sequence of either n/2 or 3*n+1
// (a proof of convergence is unknown)
//--------------------------------------
NATFUN1(Collatz,n)
  if (Le(n,ONE)) RESULT(n)
  else if (divisible(n,TWO)) RESULT(Collatz(Div(n,TWO)))
  else RESULT(Collatz(Add(Mul(n,THREE),ONE)))
RET(ONE)
//--------------------------------------
//  End of this Source
//--------------------------------------

quality95%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.18Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.