goed gevormde objectsEdit

als een verzameling objecten (symbolen en symboolsequenties) als “goed gevormde” moet worden beschouwd, moet er een algoritme bestaan om, door met een “ja” of “nee” antwoord te stoppen, te bepalen of het object al dan niet goed gevormde is (in de wiskunde verkort een wff goed gevormde formule). Dit algoritme, in het uiterste, kan een Turing machine of Turing-equivalent machine die “ontleedt” de symbool-string zoals gepresenteerd als “data” op de tape nodig hebben (of zijn) ; voordat een universele Turing machine een instructie op zijn tape kan uitvoeren, moet hij de symbolen ontleden om de exacte aard van de instructie en/of het gegeven dat daar gecodeerd is te bepalen. In eenvoudigere gevallen kan een eindige staat machine of een pushdown automaton het werk doen. Enderton beschrijft het gebruik van” bomen ” om te bepalen of een logische formule (in het bijzonder een reeks symbolen met haakjes) goed gevormd is. Alonzo Kerk 1934 beschrijft de constructie van” formules ” (opnieuw: sequenties van symbolen) zoals geschreven in Zijn λ-calculus door gebruik te maken van een recursieve beschrijving van hoe een formule te starten en vervolgens voort te bouwen op het Start-symbool met behulp van concatenatie en substitutie.

voorbeeld: Church specificeerde Zijn λ-calculus als volgt (de volgende is een vereenvoudigde versie zonder noties van vrij – en gebonden-variabele). Dit voorbeeld laat zien hoe een objecttheorie begint met een specificatie van een objectsysteem van symbolen en relaties (in het bijzonder door het gebruik van concatenatie van symbolen):

(1) verklaar de symbolen: {,}, (,), λ, plus een oneindig aantal variabelen a, b, c, …, x,… (2) definieer formule: een reeks symbolen (3) Definieer de notie van “goed gevormde formule” (wff) recursief beginnend met de “basis” (3.i):

• (3.1) (basis) een variabele x is een wff
• (3.2) als F en X WFF ‘ s zijn, dan is {F}(X) een wff; als x voorkomt in F of X dan wordt gezegd dat het een variabele is in {F}(X).
• (3.3) als M goed gevormd is en x in M voorkomt, is λx een wff.

(4) definieer verschillende afkortingen:

• {F} staat voor F(X) als F een enkel symbool is
• F {\displaystyle {{f}}}
  

  staat voor {F} (X,Y) of F (X,Y) als F een enkel symbool

• λx1λx2 is…] staat voor λx1x2…xn * M
• λab * a (b) wordt afgekort tot 1
• λab * a (a (b)) wordt afgekort tot 2, enz.

(5) Definieer de notie van “substitutie” van formule N voor variabele x in M (Kerk 1936)

ongedefinieerde (primitieve) objectsEdit

bepaalde objecten kunnen “ongedefinieerd” of “primitief” zijn en een definitie krijgen (in de termen van hun gedrag) door de introductie van de axioma ‘ s.

in het volgende voorbeeld zijn de ongedefinieerde symbolen { ※ ,ↀ,∫}. De axioma ‘ s beschrijven hun gedrag.

AxiomsEdit

Kleene merkt op dat de axioma ‘ s bestaan uit twee reeksen symbolen: (i) de ongedefinieerde of primitieve objecten en die welke eerder bekend zijn. In het volgende voorbeeld, het is eerder bekend in het volgende systeem ( O, ※, ↀ, ∫ ) dat O vormt een set van objecten (de “domeinnaam”), ※ is een object in het domein, ↀ en ∫ zijn symbolen voor de relaties tussen de objecten, => geeft het “ALS … DAN’ logische operator, ε is het symbool dat aangeeft “is een element van de verzameling O”, en “n” zal worden gebruikt om aan te geven een willekeurig element van set-van-objecten O.

Na (i) een definitie van “string S”—een object dat is een symbool ※ of samengevoegd symbolen ※, ↀ of ∫, en (ii) een definitie van “well-formed” strings — (basis) ※ en ↀS, ∫S waar S is een string, komen de axioma ‘ s:

• ↀ※ => ※, in woorden: “ALS ↀ wordt toegepast op het object ※ DAN object ※ resultaten.”
• ∫n ε o, in woorden “als ∫ wordt toegepast op willekeurig object” n “in O dan is dit object ∫n een element van O”.
• εn ε O, “als ↀ wordt toegepast op willekeurig object” n “in O dan is dit object ↀn een element van O”.
• ↀ ∫ n = > n, “als ↀ wordt toegepast op object ∫ n dan resulteert object n.”
• ∫ ↀn = > n, “als ∫ wordt toegepast op object ↀn dan resulteert object n.”

dus wat zou de (beoogde) interpretatie van deze symbolen, definities en axioma ‘ s kunnen zijn?

Als we stellen ※ als “0”, ∫ als “opvolger”, en ↀ als “voorganger” dan ↀ ※ => ※ geeft “goede aftrekken” (soms aangeduid door het symbool ∸, waar de “voorganger” trekt een eenheid van een nummer, dus 0 ∸1 = 0). De string ” ↀ ∫ n = > n ” geeft aan dat als eerst de opvolger wordt toegepast op een willekeurig object n en vervolgens de voorganger ↀ wordt toegepast op ∫n, de oorspronkelijke n resulteert.”

Is deze verzameling axioma ‘ s “adequaat”? Het juiste antwoord zou een vraag zijn: “adequaat om te beschrijven wat, in het bijzonder? De axioma ‘ s bepalen op welke systemen, gedefinieerd van buiten de theorie, de theorie van toepassing is.”(Kleene 1952: 27). Met andere woorden, de axioma ‘ s kunnen voldoende zijn voor het ene systeem, maar niet voor het andere.

in feite is het gemakkelijk om te zien dat deze axioma—verzameling niet erg goed is-in feite is het inconsistent (dat wil zeggen dat het inconsistente uitkomsten oplevert, ongeacht de interpretatie ervan):

voorbeeld: definieer ※ als 0, ∫ ※ als 1, en ↀ1 = 0. Vanaf het eerste axioma, ↀ ※ = 0, dus ∫ ↀ ※ = 0 0 = 1. Maar het laatste axioma specificeert dat voor elke willekeurige n inclusief ※ = 0, ∫ ↀn = > n, dus dit axioma bepaalt dat ∫ ↀ0 = > 0, niet 1.

merk ook op dat de axioma-verzameling niet specificeert dat ∫n ≠ n. Of, met uitzondering van het geval n=※, ↀn ≠ n. als we deze twee axioma ‘ s zouden opnemen, zouden we de intuïtieve noties “gelijken” moeten beschrijven, gesymboliseerd door = en niet-gelijken gesymboliseerd door ≠.