Quelle 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 goedels@cococo.de
//-------------------------------------------
#include "defs.nat.h"
#include "propositions.h"
//--------------------------------------
//  I.1 Axiom
//--------------------------------------
NATFUN1(AxiomI1,n,"there is no predecessor for ZERO","Es gibt keinen Vorgaenger fuer NULL")
  EXISTS(z,ONE,Add(n,ONE),Eq(n,Add(z,ONE)),FALSE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  I.2 Axiom
//--------------------------------------
NATFUN2(AxiomI2,n,m,"if fx = fy then x = y","wenn fx = fy dann ist x = y")
  EXISTS(z,ONE,Add(n,ONE),Eq(n,Add(z,ONE)),FALSE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  I.3 Axiom
//--------------------------------------
NATFUN1(AxiomI3,n,"Ex x2(0) && Forall(x1,x2(x1)>x2(f x1)) \n"
                  " => Forall(x1,x2(x1))",
                  "Ex x2(0) && Forall(x1,x2(x1)>x2(f x1)) \n"
                  " => Forall(x1,x2(x1))")
  EXISTS(z,ONE,Add(n,ONE),Eq(n,Add(z,ONE)),FALSE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  II.1 Axiom
//--------------------------------------
NATFUN2(AxiomII1,p,q,"p or q => p", "p or q => p")
  CASE(Dis(p,q),Neg(p))
  RESULT(FALSE)
FIN

//--------------------------------------
//  II.2 Axiom
//--------------------------------------
NATFUN2(AxiomII2,p,q,"p => p or q","p => p or q")
  CASE(p,Dis(p,q))
  RESULT(FALSE)
FIN

//--------------------------------------
//  II.3 Axiom
//--------------------------------------
NATFUN2(AxiomII3,p,q,"p or q => p","p or q => p")
  CASE(Dis(p,q),Dis(q,p));
  RESULT(FALSE)
FIN

//--------------------------------------
//  II.1 Axiom
//--------------------------------------
NATFUN3(AxiomII4,p,q,r,"(p => q) => (r or p => r or q)","(p => q) => (r or p => r or q)")
  CASE(Dis(p,q),p)
  RESULT(FALSE)
FIN

//--------------------------------------
//  III.1 Axiom
//--------------------------------------
NATFUN2(AxiomIII1,a,c,"Forall(v,a) => Subst(a v c)","Forall(v,a) => Subst(a v c)")
  CASE(Dis(a,c),a)
  RESULT(FALSE)
FIN

//--------------------------------------
//  III.2 Axiom
//--------------------------------------
NATFUN2(AxiomIII2,a,c,"Forall(v,b or a) => b or Forall(v,a)","Forall(v,b or a) => b or Forall(v,a)")
  CASE(Dis(a,c),a)
  RESULT(FALSE)
FIN

//--------------------------------------
//  IV.1 Axiom
//--------------------------------------
NATFUN2(AxiomIV1,a,c,"Ex u Forall(v,u(v)=a)","Ex u Forall(v,u(v)=a)")
  CASE(Dis(a,c),a)
  RESULT(FALSE)
FIN

//--------------------------------------
//  V.1 Axiom
//--------------------------------------
NATFUN2(AxiomV1,a,c,"Forall(x1,(x2(x1) = y2(x1) => x2 = y2))","Forall(x1,(x2(x1) = y2(x1) => x2 = y2))")
  CASE(Dis(a,c),a)
  RESULT(FALSE)
FIN

//--------------------------------------
//  1. Proposition
//--------------------------------------
BOOLFUN2(divisible,x,y,"x is divisible by y","x ist durch y teilbar")
  EXISTS(z,TWO,x,Eq(x,Mul(y,z)),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  2. Proposition
//--------------------------------------
BOOLFUN1(Prim,x,"x is a prime number","x ist eine Primzahl")
  CASE(Eq(x,ONE),TRUE)
  EXISTS(z,TWO,x,And(Ne(z,x),divisible(x,z)),FALSE);
  RESULT(TRUE)
FIN

//--------------------------------------
//  3. Function (2 parameters)
//--------------------------------------
NATFUN2(Pr2,n,x,"the n-th prime number contained in x\n (also see Pr1, Pr2)"
,"die n'te Primzahl die in x enthalten ist\n (siehe auch Pr1, Pr2)")

  CASE(Eq(n,ZERO),ZERO)
  EXISTS(y,Add(Pr2(Sub(n,ONE),x),ONE),x,And(Prim(y),divisible(x,y)),y);
  RESULT(ZERO)
FIN

//--------------------------------------
//  4. Function
//--------------------------------------
NATFUN1(Fac,n,"faculty of n","Fakultaet von n")
CASE(Eq(n,ZERO),ZERO)
CASE(Eq(n,ONE),ONE)
RESULT(Mul(n,Fac(Sub(n,ONE))))
FIN

//--------------------------------------
//  5. Function (1 parameter)
//--------------------------------------
NATFUN1(Pr1,n,"n-th prime number\n(also see Pr1, Pr2)",
              "die n'te Primzahl\n(siehe auch Pr1, Pr2)")
CASE(Eq(n,ZERO),ZERO)
EXISTS(y,Add(Pr1(Sub(n,ONE)),ONE),Add(Fac(Pr1(Sub(n,ONE))),ONE),Prim(y),y);
RESULT(ZERO)
FIN

//--------------------------------------
//  6. Function
//--------------------------------------
NATFUN2(Gl,n,x,"n-th term of a series of numbers assigned to x",
               "der n'te Term einer Folge von Zahlen die x zugewiesen sind")
  NAT pp=Pr2(n,x);
  EXISTS(y,ONE,x,And(divisible(x,Pow(pp,y)),Not(divisible(x,Pow(pp,Add(y,ONE))))),y);
  RESULT(ZERO)
FIN

//--------------------------------------
//  7. Function
//--------------------------------------
NATFUN1(l,x,"length a series of numbers of assigned to x",
            "Laenge einer Folge von Zahlen die x zugewiésen sind")
  EXISTS(y,ONE,x,And(Gt(Pr2(y,x),ZERO),Eq(Pr2(Add(y,ONE),x),ZERO)),y);
  RESULT(ZERO)
FIN

//--------------------------------------
//  8. Function
//--------------------------------------
//  8.1
BOOLFUN2(Join1,x,z,"auxiliary","hilfsweise")
  EXISTS(n,ONE,l(x),Ne(Gl(n,z),Gl(n,x)),FALSE);
  RESULT(TRUE)
FIN

//  8.2
BOOLFUN3(Join2,x,y,z,"auxiliary","hilfsweise")
  EXISTS(n,ZERO,l(y),Ne(Gl(Add(n,l(x)),z),Gl(n,y)),FALSE);
  RESULT(TRUE)
FIN
//  8.
NATFUN2(Join,x,y,"join together two finite series of numbers",
                 "verkette zwei endliche Folgen von Zahlen")
  EXISTS(z,ONE,Pow(Pr1(Add(l(x),l(y))),Add(x,y)),And(Join1(x,z),Join2(x,y,z)),z);
  RESULT(ZERO)
FIN

//--------------------------------------
//  9. Function
//--------------------------------------
NATFUN1(R,x,"a series of numbers with a single element x",
            "eine Zahlenfolge mit nur einem Element x")
  RESULT(Pow(TWO,x))
FIN

//--------------------------------------
//  10. Function
//--------------------------------------
NATFUN1(E,x,"bracketing of a a series of numbers",
            "Klammerung eier Zahlenfolge")
  RESULT(Join(R(ELEVEN),Join(x,R(THIRTEEN))))
FIN

//--------------------------------------
//  11. Function  (2 parameters)
//--------------------------------------
BOOLFUN2(Var2,n,x,"x is a variable of n-th type\n (also see Var1, Var2)",
                  "x ist eine Variable vom n'ten Typ\n (siehe auch Var1, Var2)")
  CASE(Eq(n,ZERO),FALSE)
  EXISTS(z,Add(THIRTEEN,ONE),x,And(Prim(z),Eq(x,Pow(z,n))),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  12. Proposition  (1 parameter)
//--------------------------------------
BOOLFUN1(Var1,x,"x is a variable","x ist eine Variable")
  EXISTS(n,ONE,x,Var2(n,x),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  13. Function
//--------------------------------------
NATFUN1(Neg,x,"negation of x","Negation von x")
  RESULT(Join(R(FIVE),E(x)))
FIN

//--------------------------------------
//  14. Function
//--------------------------------------
NATFUN2(Dis,x,y,"disjunction of x, y","Disjunktion von x, y")
  RESULT(Join(E(x),Join(R(SEVEN),E(y))))
FIN

//--------------------------------------
//  15. Function
//--------------------------------------
NATFUN2(Gen,x,y,"generalization of y by means of variable x",
                "Generalisierung von y durch die Variable x")
  RESULT(Join(R(x),Join(R(NINE),E(y))))
FIN

//--------------------------------------
//  16. Function
//--------------------------------------
NATFUN2(N,n,x,"n-fold prefixing of the sign f(succ) before x",
              "n-facher Praefix des Zeichens f(succ) vor x")
  CASE(Eq(n,ZERO),x)
  RESULT(Join(R(THREE),N(Sub(n,ONE),x)))
FIN

//--------------------------------------
//  17. Function
//--------------------------------------
NATFUN1(Z,n,"number sign for number n","Zahlenzeichen fuer n")
  RESULT(N(n,R(ONE)))
FIN

//--------------------------------------
//  18. Proposition  (1 parameter)
//--------------------------------------
BOOLFUN1(Typ1,x,"x is a sign of first type\n (also see Typ1, Typ2)",
                "x ist ein Zeichen ersten Typs\n (siehe auch Typ1, Typ2)")
  FORALL(n,ONE,x)
    EXISTS(m,ONE,x,Or(Eq(m,ONE),And(Var2(ONE,m),Eq(x,N(n,R(m))))),TRUE);
  ENDFOR
  RESULT(FALSE)
FIN

//--------------------------------------
//  19. Proposition  (2 parameters)
//--------------------------------------
BOOLFUN2(Typ2,n,x,"x is a sign of n-th type\n (also see Typ1, Typ2)",
                  "x ist ein ZEichen n-ten Typs\n (siehe auch Typ1, Typ2)")
  CASE(Eq(n,ONE),Typ1(x))
  EXISTS(v,ONE,x,And(Var2(n,v),Eq(x,R(v))),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  20. Proposition
//--------------------------------------
BOOLFUN1(Elf,x,"x is an elementary type",
               "x ist ein elementaarer Typ")
  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
  RESULT(FALSE)
FIN

//--------------------------------------
//  21. Proposition
//--------------------------------------
BOOLFUN3(Op,x,y,z,"nn","NN")
  CASE(Eq(x,Neg(y)),TRUE)
  CASE(Eq(x,Dis(y,z)),TRUE)
  EXISTS(v,ONE,x,And(Var1(v),Eq(x,Gen(v,y))),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  22. Proposition
//--------------------------------------
BOOLFUN1(FR,x,"x is a series of formula \n"
              " where each formula is either elementary\n"
              " or it arises from negation, disjunction,\n"
              " and generalization",
              "x is eine Folge von Formeln \n"
              " in der jede Formel entweder elementar ist\n"
              " oder aus Negation, Disjunktion,\n"
              " und Generalisierung besteht")
  FORALL(n,ONE,x)
    CASE(And(Lt(ZERO,n),Le(n,l(x))),Elf(Gl(n,x)))
      FORALL(p,ONE,n)
        EXISTS(q,ONE,n,Op(Gl(n,x),Gl(p,x),Gl(q,x)),TRUE);
      ENDFOR
  ENDFOR
  RESULT(FALSE)
FIN

//--------------------------------------
//  23. Proposition
//--------------------------------------
BOOLFUN1(Form,x,"x is a formula","x ist eine Formel")
  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);
  RESULT(FALSE)
FIN

//--------------------------------------
//  24. Proposition
//--------------------------------------
BOOLFUN3(Geb,v,n,x,"variable v is bound at n-th place in x",
"Variable v ist an n-ter Stelle in x gebunden")
  CASE(Not(And(Var1(v),Form(x))),FALSE)
  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
FIN

//--------------------------------------
//  25. Proposition  (3 parameters)
//--------------------------------------
BOOLFUN3(Fr3,v,n,x,"variable v is free at n-th place in x\n (also see Fr2, Fr3)",
                   "Variable v ist an n-ter Stelle frei in x\n (siehe auch Fr2, Fr3)")
  RESULT(And(Var1(v),And(Form(x),And(Eq(v,Gl(n,x)),And(Le(n,l(x)),Geb(v,n,x))))))
FIN

//--------------------------------------
//  26. Proposition   (2 parameters)
//--------------------------------------
BOOLFUN2(Fr2,v,x,"v occurs in x as a free variable\n (also see Fr2, Fr3)",
                 "v ist eine freie Variable aus x\n (siehe auch Fr2, Fr3)")
  EXISTS(n,ONE,l(x),Fr3(v,n,x),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  27. Proposition
//--------------------------------------
NATFUN3(Su,x,n,y,"substitute y in place of the n-th term of x",
                 "ersetze y an der Stelle des n-ten Terms in x")
  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
  RESULT(ZERO)
FIN

//--------------------------------------
//  28. Function
//--------------------------------------
NATFUN3(St,k,v,x,"(k+1)-th place in x at which v is free in x, 0 else",
                 "die (k+1)-te Stelle in x an der v frei ist, 0 sonst")
  FORALL(n,ONE,l(x))
    EXISTS(p,Add(n,ONE),l(x),And(Eq(k,ZERO),And(Fr3(v,n,x),Fr3(v,p,x))),n);
  ENDFOR
  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
  RESULT(ZERO)
FIN

//--------------------------------------
//  29. Function
//--------------------------------------
NATFUN2(A,v,x,"number of places at which v is free in x",
              "Anzahl der Stellen an denen v frei in x ist")
  EXISTS(n,ONE,l(x),Eq(St(n,v,x),ZERO),n);
  RESULT(ZERO)
FIN

//--------------------------------------
//  30. Function
//--------------------------------------
NATFUN4(Sb4,k,x,v,y,"substitute ...\n (also see Sb3, Sb4)",
                    "ersetze ...\n (siehe auch Sb3, Sb4)")
  CASE(Eq(k,ZERO),x)
  RESULT(Su(Sb4(Sub(k,ONE),x,v,y),St(k,v,x),y))
FIN

//--------------------------------------
//  31. Function
//--------------------------------------
NATFUN3(Sb3,x,v,y,"substitute x by v in y\n (also see Sb3, Sb4)",
                  "ersetze x durch v in y\n (siehe auch Sb3, Sb4)")
  RESULT(Sb4(A(v,x),x,v,y))
FIN

//--------------------------------------
//  32a. Function
//--------------------------------------
NATFUN2(Imp,x,y,"implication",
                 "Implikation")
  RESULT(Dis(Neg(x),y))
FIN

//--------------------------------------
//  32b. Function
//--------------------------------------
NATFUN2(Con,x,y,"conjunction",
                "Konjunktion")
  RESULT(Neg(Dis(Neg(x),Neg(y))))
FIN

//--------------------------------------
//  32c. Function
//--------------------------------------
NATFUN2(Aeq,x,y,"equivalence",
                "Aequivalenz")
  RESULT(Con(Imp(x,y),Imp(y,x)))
FIN

//--------------------------------------
//  32d. Function
//--------------------------------------
NATFUN2(Ex,v,y,"exists","Es gibt")
  RESULT(Neg(Gen(v,Neg(y))))
FIN

//--------------------------------------
//  33. Function
//--------------------------------------
NATFUN2(Th,n,x,"n-th type lift of x",
               "n-ter Typ von 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
  RESULT(ZERO)
FIN

//--------------------------------------
//  34. Proposition
//--------------------------------------
BOOLFUN1(Z_Ax,x,"axioms I(1) to I(3)",
                "Axiome I(1) bis I(3)")
  CASE(Eq(x,z1),TRUE)
  CASE(Eq(x,z2),TRUE)
  CASE(Eq(x,z3),TRUE)
  RESULT(FALSE)
FIN

//--------------------------------------
//  35. Proposition
//--------------------------------------
BOOLFUN2(A1_Ax,n,x,"formula derived by substituton",
                   "Formel die durch Substitution abgeleitet wurde")
  EXISTS(y,ONE,x,And(Form(y),Eq(x,Imp(Dis(y,y),y))),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  36. Proposition
//--------------------------------------
BOOLFUN1(A_Ax,x,"formula derived by substituton",
"Formel die durch Substitution abgeleitet wurde")
  CASE(A1_Ax(ONE,x),TRUE)
  CASE(A1_Ax(TWO,x),TRUE)
  CASE(A1_Ax(THREE,x),TRUE)
  CASE(A1_Ax(FOUR,x),TRUE)
  RESULT(FALSE)
FIN

//--------------------------------------
//  37. Proposition
//--------------------------------------
BOOLFUN3(Q,z,y,v,"z contains no variable bound in y at position where v is free",
                 "z enthaelt keine Variable in y an der Position wo v frei ist")
  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
  RESULT(FALSE)
FIN

//--------------------------------------
//  38. Proposition
//--------------------------------------
BOOLFUN1(L1_Ax,x,"--> bug in paper Sb(v z)??\n"
                 " x is a formula derived from the axiom schema III,1 by substitution",
                 "--> Fehler in Papier Sb(v z) ??\n"
                 "x ist eine aus dem Axiomem III,1 durch Substitution abgeleitete Formel")
  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
  RESULT(FALSE)
FIN

//--------------------------------------
//  39. Proposition
//--------------------------------------
BOOLFUN1(L2_Ax,x,"x is a formula derived from the axiom schema III,2 by substitution",
                  "x ist eine aus dem Axiomem III,2 durch Substitution abgeleitete Formel")
  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
  RESULT(FALSE)
FIN

//--------------------------------------
//  40. Proposition
//--------------------------------------
BOOLFUN1(R_Ax,x,"x is a formula derived from the axiom schema IV,1 by substitution",
                "x ist eine aus dem Axiomem IV,1 durch Substitution abgeleitete Formel")
  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
  RESULT(FALSE)
FIN

//--------------------------------------
//  41. Proposition
//--------------------------------------
BOOLFUN1(M_Ax,x,"tbd","offen")
  EXISTS(n,ONE,x,(Eq(x,Th(n,z4))),TRUE);
  RESULT(FALSE)
FIN

//--------------------------------------
//  42. Proposition
//--------------------------------------
BOOLFUN1(Ax,x,"x is an axiom","x ist ein Axiom")
  CASE(Z_Ax(x),TRUE)
  CASE(A1_Ax(ONE,x),TRUE)
  CASE(L1_Ax(x),TRUE)
  CASE(L2_Ax(x),TRUE)
  CASE(R_Ax(x),TRUE)
  CASE(M_Ax(x),TRUE)
  RESULT(FALSE)
FIN

//--------------------------------------
//  43. Proposition
//--------------------------------------
BOOLFUN3(Fl,x,y,z,"x is an immediate consequence of y and z",
                  "x ist unmittelbare Folgerung von y und z")
  CASE(Imp(z,x),TRUE)
  EXISTS(v,ONE,x,And(Var1(v),Eq(x,Gen(v,y))),TRUE);
FIN

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

//--------------------------------------
//  45. Proposition
//--------------------------------------
BOOLFUN2(B,x,y,"x is a proof of the formula y",
                "x beweist Formal y")
    RESULT(And(Bw(x),Eq(Gl(l(x),x),y)))
FIN

//--------------------------------------
//  46. Proposition
//--------------------------------------
BOOLFUN1(Bew,x,"x is a provable formula\n"
               " (cannot be asserted that it is recursive)",
               "x ist eine beweisbare Formel\n"
               " (es kann nicht gesagt werden ob diese Funktion rekursiv ist)")
  EXISTS(y,ZERO,Add(y,ONE),B(y,x),TRUE);  //y+1==TRUE, INFINITE
  RESULT(FALSE)
FIN
//--------------------------------------
//
//  Additional Functions
//
//
//--------------------------------------
//  Primetwin
//--------------------------------------
NATFUN1(Primetwin,n,"p, p+2 are primes, p>n\n"
                    " (unknown if there are infinitely many)",
                    "p, p+2 sind Primzahlen, p>n\n"
                    " (unbekannt ob es fuer alle n terminiert)")
  EXISTS(p,n,Mul(n,ELEVEN),And(Prim(p),Prim(Add(p,TWO))),Pair(p,Add(p,TWO)));
  RESULT(ZERO)
FIN

//--------------------------------------
//  Goldbach
//--------------------------------------
NATFUN1(Goldbach,n," p+q=n where p,q are primes\n"
                   " (Goldbach's conjecture)",
                   " p+q=n wobei p,q Primzahlen sind"
                   " (Goldbachs Behauptung)")
  CASE(Ne(Mod(n,TWO),ZERO),ZERO)
  FORALL(q,ONE,Sub(n,ONE))
    EXISTS(p,ONE,Sub(n,ONE),And(Eq(Add(p,q),n),And(Prim(q),Prim(p))),Pair(p,q))
  ENDFOR
  CASE(TRUE,ZERO)
FIN

//--------------------------------------
//  Collatz
//--------------------------------------
NATFUN1(Collatz,n,"sequence of either n/2 or 3*n+1\n"
                  " (a proof of convergence is unknown)",
                  "eine Zahlenfolge mit n/2 oder 3*n+1 als Nachfolger"
                  " (ein Beweis fuer die Konvergenz existiert nicht)")
  CASE(Le(n,ONE),n)
  CASE(Eq(Mod(n,TWO),ZERO),Collatz(Div(n,TWO)))
  RESULT(Collatz(Add(Mul(n,THREE),ONE)))
FIN

//--------------------------------------
//  Fermat
//--------------------------------------
NATFUN1(Fermat,n,"Forall n, n mod 4 = 1\n"
                 " ex x,y x*x+y*y = n",
                 "Forall n, n mod 4 = 1\n"
                 " ex x,y x*x+y*y = n")
  CASE(Ne(Mod(n,FOUR),ONE),ZERO)
  FORALL(x,TWO,Sub(n,ONE))
    EXISTS(y,TWO,Sub(x,ONE),Eq(Add(Mul(x,x),Mul(y,y)),n),y)
  ENDFOR
FIN
//--------------------------------------
//  End of this Source
//--------------------------------------

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

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.