Warum die Peano-Arithmetik allein ausreicht: PA kann Berechnungen kodieren

 (math.stackexchange.com)
1 Punkte von GN⁺ 2025-06-15 | 1 Kommentare | Auf WhatsApp teilen
  • PA kann den gesamten Goodstein-Satz ∀n G(n) nicht beweisen, aber für jede standardmäßige natürliche Zahl n lässt sich die Existenz eines PA-Beweises für G(n) innerhalb von PA zeigen
  • Der Kern ist eine Konstruktion, die nur bis zu dem für n benötigten Turm aus ω-Potenzen endlicher Höhe geht und für diesen Bereich einen transfiniten Induktionsbeweis mechanisch erzeugt
  • Die benötigte Höhe m entspricht der Höhe der hereditary base notation von n und ist O(log*(n)); mit der Kurzschreibweise ω^[m] sinkt die Beweislänge auf O(m log m)
  • Dieses Resultat bedeutet, dass man „für jeden Einzelfall einen Beweis konstruieren kann“, nicht dass PA den gesamten Goodstein-Satz beweist
  • PA kann Zahlen, Paare, Listen, Programmzustände und formale logische Beweise jeweils in einer einzelnen natürlichen Zahl kodieren, sodass innerhalb von PA auch überprüfbar ist, ob ein erzeugter Beweis tatsächlich ein PA-Beweis ist

Die mathematische Form der Frage

  • Gegenstand des Interesses ist die Aussage G(n), dass die Goodstein-Folge schließlich 0 erreicht

  • Die bekannte Unterscheidung ist die folgende

    • PA kann für jeden konkreten Standardfall Aussagen wie G(15) oder G(268) beweisen
    • PA kann die Gesamtaussage ∀n ∈ N: G(n) nicht beweisen

  • Die Frage ist, ob PA eine Aussage der folgenden Form beweisen kann

    ∀n ∈ N: ∃p ∈ N: P_PA(p, ⌜G(n)⌝)

  • P_PA(p, ⌜φ⌝) bedeutet, dass p ein Beweiscode für φ in PA ist

  • Die Schlussfolgerung lautet, dass auf dieser Ebene PA allein ausreicht

Was PA beweisen muss

  • Was PA für jedes n zeigen muss, umfasst die folgenden drei Punkte
    • Man kann die Beweislänge berechnen, die zum Beweis von G(n) nötig ist
    • Das Verfahren zum Konstruieren dieses Beweises terminiert
    • Der letzte Satz des konstruierten Beweises besagt die Terminierung von G(n)
  • Für jedes G(n) lässt sich ein PA-Beweis der Länge O(log*(n) log(log*(n))) konstruieren
  • log* ist der iterierte Logarithmus (iterated logarithm) und wächst extrem langsam
  • Da die benötigten Beweise mit wachsendem n länger werden, folgt daraus nicht, dass PA den gesamten Goodstein-Satz beweisen kann

Goodstein-Folgen und Ordinalschreibweisen

  • Goodstein-Folgen verwenden die hereditary base notation, die mit Ordinaldarstellungen in Cantor-Normalform verbunden ist

  • In der Konstruktion nach John von Neumann werden Ordinalzahlen als Mengen aufgebaut

    • 0 ist die leere Menge
    • Ist ord eine Ordinalzahl, dann ist auch ord ∪ {ord} eine Ordinalzahl
    • Ist X eine Menge von Ordinalzahlen, dann ist auch die Vereinigung von X eine Ordinalzahl

  • Die Cantor-Normalform stellt Ordinalzahlen in der folgenden Form dar

    ((n1, ord1), (n2, ord2), ..., (nk, ordk))
    • jedes ni ist eine positive natürliche Zahl
    • jedes ordi ist eine Ordinalzahl
    • ord1 > ord2 > ... > ordk

  • Diese Schreibweise bezeichnet die folgende Ordinalzahl

    n1·ω^ord1 + n2·ω^ord2 + ... + nk·ω^ordk

  • Der Vergleich erfolgt als lexikographischer Vergleich in der Reihenfolge ord1, n1, ord2, n2; endet eine Seite früher, dann ist die kürzere kleiner

Von Induktion zu transfiniten Induktion

  • Das fünfte Axiom von PA liefert Induktion über natürliche Zahlen
    • S(0) ist wahr
    • aus S(n) folgt auch S(s n)
    • dann ist S für alle natürlichen Zahlen wahr
  • Daraus kann PA < rekursiv definieren und auch starke Induktion beweisen
    • Wenn man für jedes n zeigt, dass aus der Wahrheit von S für alle kleineren Zahlen auch S(n) folgt, dann ist S für alle natürlichen Zahlen wahr
  • In ZFC lässt sich transfinite Induktion als starke Induktion über alle Ordinalzahlen beweisen
  • Für Objekte in Cantor-Normalform werden dabei zwei Eigenschaften verwendet
    • jede streng fallende Folge von Objekten in Cantor-Normalform ist notwendig endlich
    • auf Objekte in Cantor-Normalform kann transfinite Induktion angewendet werden

Der Umfang transfiniten Induktion innerhalb von PA

  • PA kann transfinite Induktion nicht für alle Ordinalzahlen beweisen
  • Stattdessen kann PA bestimmte Ordinalbereiche endlicher Höhe behandeln
    • Da PA starke Induktion beweisen kann, kann es transfinite Induktion bis ω behandeln
    • Mit derselben Logik ist auch transfinite Induktion über ω^ω beweisbar
    • Auf dieselbe Weise kann man dies auf ω^(ω^ω), ω^(ω^(ω^ω)) und weitere Türme endlicher Höhe iterieren
  • In jedem Schritt ändert sich im Beweis nur die Höhe des Turms; die Erzeugung ist mechanisch
  • Schreibt man den m-ten Turm vollständig aus, hat der Gesamtbeweis Länge O(m^2)
  • Verwendet man eine Kurzschreibweise wie ω^[m], dann braucht man nur O(log m) Länge, um m zu schreiben, sodass der Gesamtbeweis O(m log m) hat
  • Für jede einzelne Ordinalzahl unterhalb von ε₀ existiert ein Beweis transfiniten Induktion in PA, aber um all diese Beweise zusammenzufassen, wäre ein unendlich langer Beweis nötig
  • Würde PA transfinite Induktion bis ε₀ beweisen, könnte es damit seine eigene Konsistenz beweisen, was mit Gödels zweitem Unvollständigkeitssatz kollidieren würde

Verfahren zur Erzeugung eines Beweises für jedes G(n)

  • Für ein bestimmtes n braucht man nur bis zur Turmhöhe der hereditary base notation zu gehen
  • Diese Höhe ist O(log*(n)) und kann in PA als leicht berechenbare Funktion behandelt werden
  • Ein Programm kann für Eingabe n Folgendes ausgeben
    • Beweise gemeinsamer Tatsachen über PA
    • einen Beweis dafür, dass G(n) für ein bestimmtes m eine fallende Folge innerhalb von ω^[m] verfolgt
    • den Rechengang zur Bestimmung dieses m und einen Beweis über den Wert von m
    • einen Beweis transfiniten Induktion für ω^[0]
    • einen Beweis dafür, dass transfinite Induktion über ω^[i] transfinite Induktion über ω^[i+1] impliziert
    • für jedes i = 0 bis m-2 den jeweiligen Beweis transfiniten Induktion dieses Schritts
    • einen Beweis dafür, dass transfinite Induktion über ω^[m-1] impliziert, dass alle fallenden Folgen in ω^[m] endlich sind
    • die Schlussfolgerung, dass G(n) terminiert
  • PA kann über dieses Verfahren Folgendes beweisen
    • das Verfahren terminiert
    • das Verfahren erzeugt eine Liste von Sätzen
    • die Liste beginnt mit Peano-Axiomen
    • jeder Satz folgt logisch aus früheren Sätzen
    • per Induktion sind alle Sätze bewiesen
    • der letzte Satz lautet: „G(n) terminiert“
  • Daher kann PA für jede beliebige natürliche Zahl n beweisen, dass PA die Terminierung von G(n) beweist

Wie PA Berechnungen kodiert

  • „Kodierung“ bedeutet, festzulegen, dass eine bestimmte natürliche Zahl für eine bestimmte Struktur steht
  • Die Grundbausteine von PA sind die folgenden
    • 0
    • die Nachfolgerfunktion (s n)
    • Gleichheit
    • der Vorgänger (p n) für von 0 verschiedene Zahlen
    • rekursive Definitionen, gerechtfertigt durch Induktion
    • bedingte Verzweigungen anhand von 0 oder 1
  • Innerhalb von PA lassen sich die folgenden grundlegenden arithmetischen Funktionen rekursiv definieren
    • <
    • min, max
    • +
    • *
    • Potenzierung
    • Rest %
    • ganzzahlige Division //
  • Die grundlegenden Eigenschaften dieser Funktionen sind in PA mittels Induktion beweisbar

Datenstrukturen aus einer einzigen natürlichen Zahl

  • Um zwei natürliche Zahlen in einer einzigen zu kodieren, kann man die Binärbits abwechselnd anordnen
    • Bits an ungeraden Positionen sind head
    • Bits an geraden Positionen sind tail
  • Aus dem so gebildeten Paar lassen sich head und tail wieder extrahieren
  • Kann man Paare bilden, dann lassen sich auch verkettete Listen darstellen
    • 0 als nil
    • leere Liste
    • ein Element vorn anfügen
    • Kopf und Schwanz auslesen
    • Länge berechnen
    • Zugriff auf beliebige Positionen
    • Einfügen und Löschen
  • Mit Zahlen, Paaren und Listen lassen sich auch Strukturen wie Stacks, Queues, Bäume, Textdokumente oder eine virtuelle Maschine jeweils als einzelne natürliche Zahl darstellen

Lisp und die Kodierung von Berechnungsverfahren

  • Lisp eignet sich wegen seiner Klammerstruktur und der Form command and arguments gut dazu, Parsing und Interpretation zu erläutern
  • Natürliche Zahlen in PA können als Paare (type, value) interpretiert werden
    • Zahlen
    • Boolesche Werte
    • Paare
    • Listen
    • Text usw.
  • Manche natürliche Zahlen sind möglicherweise keine gültigen Werte eines bestimmten Typs, aber gültige Werte können jeweils eindeutig eine bestimmte Struktur darstellen
  • Auf dieser Kodierung lassen sich Lisp-Datenstrukturen, eine Lisp-virtuelle Maschine und ein Lisp-Interpreter aufbauen
  • Da Lisp Turing-vollständig ist, können auf diesem Weg beliebige berechenbare Verfahren und ihre Zustände innerhalb von PA kodiert werden
  • Auch der Berechnungszustand nach einer bestimmten Zahl von Schritten kann innerhalb von PA dargestellt und verfolgt werden

PA kodiert auch PA-Beweise

  • Ein Beweis in der Prädikatenlogik erster Stufe kann als Liste von Sätzen aufgefasst werden
    • jeder Satz ist ein einzelner Inferenzschritt
    • man kann auch falsche Sätze oder ungültige Schlüsse hinschreiben, aber ein Verifikationsverfahren kann diese aussortieren
  • Innerhalb von PA kann man einen Typ wie type-proof einführen und Beweise als Satzlisten kodieren
  • Auch das folgende Verifikationsverfahren lässt sich in PA kodieren
    • prüfen, ob ein Beweis wohlgeformt ist
    • prüfen, ob jeder Beweisschritt gültig ist
    • prüfen, welche Axiome vorausgesetzt werden
    • prüfen, ob die letzte Schlussfolgerung der gewünschten Aussage entspricht
  • Wenn aus bestimmten Axiomen ein Beweis einer bestimmten Aussage existiert, dann existiert auch eine konkrete natürliche Zahl in PA, die diesen Beweis darstellt
  • PA kann die Berechnung ausdrücken, mit der geprüft wird, ob diese Zahl tatsächlich ein Beweiscode ist; daher kann PA einen „Beweis in PA“ selbst innerhalb von PA behandeln
  • Gödel kodierte die Logik in PA, ohne die gesamte Berechnung zu kodieren; aus Sicht von Programmierern ist der Zugang über die Kodierung von Berechnung jedoch ein natürlicherer Weg zum Verständnis

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2025-06-15
Hacker-News-Kommentare

  • Ein Stack-Overflow-Post, der zu einem Blogbeitrag ausgebaut wurde
    Es geht um die Grenzen dessen, was sich mit den Peano-Axiomen beweisen lässt, und darum, wie man beginnt, darin Lisp zu bootstrappen
    Alle schlechten Witze stehen im zweiten Abschnitt, und Korrekturen oder Nachfragen sind willkommen

    • Ich habe den ganzen Text gelesen und dabei bemerkt, dass im Abschnitt "Why Lisp?" im Beispiel (defun not (x) ...) an einer Stelle die Klammern nicht passen
      Das war im Zusammenspiel mit der späteren Aussage, dass es „wirklich einfach ist, den Computer ausgeglichene Klammern finden zu lassen“, ziemlich lustig, und auch der Kommentar im Abschnitt "Basic Number Theory", dass man „den Haufen schließender Klammern nicht mehr sieht“, war witzig
      Obwohl ich schon lange kein Lisp mehr gemacht habe, konnte ich dem Text wieder folgen und den Kern erfassen, daher hat mir der Beitrag gefallen
    • Ich habe noch nicht viel über die Einleitung hinaus gelesen, aber die Prämisse ist interessant, dass sich für jede konkrete Goodstein-Folge innerhalb von PA beweisen lässt, dass sie bei 0 endet, während sich die Aussage, dass alle Folgen enden, nicht beweisen lässt
      Dass sich Berechnung allein mit den Peano-Axiomen kodieren lässt, ist auch auf seltsame Weise faszinierend und wirkt wie eine weitere Ebene der Selbstreferenz
      Ich habe vor Kurzem angefangen, mich intensiver mit Mengenlehre zu beschäftigen und bin dabei auch auf Goodstein-Folgen gestoßen; mich würden Empfehlungen für weiterführende Lehrbücher zu fortgeschrittener Mengenlehre oder zu Peano-Arithmetik im Detail interessieren
    • Boot Sector Lisp bootstrapped sich ebenfalls selbst: https://justine.lol/sectorlisp2/
      Mehrere Lisps auf https://t3x.org implementieren Zahlen und den Rest ebenfalls über Cons-Zellen sowie apply/eval
      John McCarthys metazirkulärer Evaluator ist der Code, den Alan Kay die „Maxwell-Gleichungen der Software“ nannte, und in SectorLISP ist das in der Art ASSOC EVAL EVCON APPLY EVLIS PAIRLIS umgesetzt
      Manche Forths sind ähnlich, und T3Xs Zenlisp erklärt es rund um die Art, wie eval/apply sich gegenseitig rekursiv aufrufen: http://t3x.org/zsp/index.html
    • An zwei Stellen steht „omega“, dort sollte vermutlich \omega stehen

  • Aus Sicht von jemandem, der sowohl Mathematik als auch Programmierung gemacht hat, ist weniger die Kodierung von Berechnung selbst interessant als die Möglichkeit, die Unabhängigkeit des Goodstein-Theorems auf diese selbstreferenzielle Weise zu umgehen
    Es klingt so, als könne PA + „PA ist ω-konsistent“ das Goodstein-Theorem beweisen, und vielleicht wäre damit allgemein auch transfinite Induktion bis ε₀ möglich
    Korrektur: Vielleicht reicht auch schon PA + „PA ist konsistent“

    • Als Verfasser der ursprünglichen SO-Frage habe ich noch ein paar Links zu relevanten Antworten ergänzt
      Zentral ist, dass „PA ist konsistent“ allein nicht ausreicht, wohl aber das uniforme Reflexionsprinzip „wenn PA etwas beweist, dann ist es wahr“
      Ich bin mir nicht zu 100 % sicher, ob dieses Prinzip äquivalent zu ω-Konsistenz ist, aber das hier liest sich so: https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relation_to_other_consistency_principles
      Wikipedia beschreibt, dass T ω-konsistent ist, als „T + RFN_T + die Menge aller wahren Aussagen ist konsistent“, was für mich dasselbe zu bedeuten scheint wie „T + RFN_T ist wahr“
    • Diese rekursive Struktur gefällt mir
      Im Wesentlichen konstruiert man einen Metabeweis darüber, was PA beweist, und wenn man PA vertraut, vertraut man dann auch diesem Metabeweis
      Ich verstehe nur nicht genau, wie PA + „PA ist konsistent“ dafür ausreichen soll
      Dieses System würde in den Standard-Naturzahlen zwar zulassen, dass das Goodstein-Theorem wahr ist, aber auch Modelle, in denen es für irgendeine nichtstandardmäßige ganze Zahl N falsch ist, und genau diesen Fall scheint die stärkere ω-Konsistenz auszuschließen
    • Leider ist es wohl nicht so, und allein mit rein allquantifizierten Formeln geht es anscheinend auch sonst nicht
      Es ist also kein spezielles Problem von Con(PA), sondern ein allgemeineres Phänomen: https://math.stackexchange.com/questions/5003237/can-goodsteins-theorem-be-proven-in-mathrmpa-conpa
      Im Zusammenhang mit der ersten Frage würde mich interessieren, wie man ω-Konsistenz als Formel von PA kodiert
    • Im Math-Exchange-Beitrag heißt es, dass PA + transfinite Induktion über ε₀ die Konsistenz von PA beweist
      Deshalb wirkt es so, als sollte PA + „PA ist konsistent“ transfinite Induktion über ε₀ beweisen können
    • Inzwischen ist das etwas außerhalb des Bereichs, in dem ich selbstbewusst Details behaupten würde
      ChatGPT meinte, PA + „PA ist konsistent“ reiche nicht aus, und da es Logiklehrbücher wohl gründlich genug verarbeitet hat, kann man dieser Aussage vielleicht trauen

  • Als ich zum ersten Mal Peano-Arithmetik verwendet habe, war ich von ihrer Ausdrucksstärke ziemlich überrascht
    Anfangs wirkt sie wie ein grundlegendes System, aber sobald man erkennt, dass sich Berechnung selbst innerhalb von PA kodieren lässt und dass sich viele Arten von Berechnung nachahmen lassen, fügen sich die Dinge zusammen, die vorher komplex wirkten
    Mich würden Empfehlungen für Material interessieren, das diese Kodierungstechniken für Einsteiger verständlich erklärt

  • Das ist der Boyer-Moore-Theorie sehr ähnlich. Auch diese Theorie baut Mathematik auf dem Niveau der Peano-Axiome auf.
    Boyer und Moore entwickelten dafür sogar einen automatischen Theorembeweiser, und eine auf GNU Common Lisp laufende Kopie liegt unter https://github.com/John-Nagle/nqthm/tree/master.
    Ihrer Beschreibung zufolge ist es am einfachsten, wenn man das Programm wie einen ziemlich guten Mathematikstudenten betrachtet. Wenn man ihm nur die Peano-Axiome gibt, kann man kaum erwarten, dass es den Satz der Primfaktorzerlegung beweist oder entdeckt; gibt man ihm aber zusammen mit den Peano-Axiomen eine Liste von Sätzen wie „Beweise das Kommutativgesetz der Addition“, „Beweise, dass die Multiplikation distributiv über der Addition ist“ oder „Beweise, dass das Ergebnis der GCD-Funktion beide Argumente teilt“, dann kann es damit gut umgehen.
    Artikel: https://www.cs.utexas.edu/~boyer/acl.pdf

  • Der Kommentar auf Math StackExchange an JoJoModding war falsch.
    Die Erklärung „PA kann zwar beweisen, dass es selbst einen Beweis erzeugt, aber vielleicht nicht, dass dieser Beweis endliche Länge hat“ verfehlt den Kern.
    Wenn PA beweist, dass „PA X beweist“, dann kann PA X beweisen.
    Der wichtige Punkt ist nicht, dass es nichtstandardmäßige Modelle gibt, sondern dass das Standardmodell der natürlichen Zahlen ein Modell von PA ist.
    Wenn PA also beweist, dass „PA X beweist“, dann gibt es tatsächlich eine standardmäßige endliche natürliche Zahl, die einem kodierten Beweis von „PA beweist X“ entspricht, und mit dieser natürlichen Zahl kann man innerhalb von PA einen Beweis von X konstruieren.

    • Die angegebene natürlichsprachliche Version ist mehrdeutig, daher ist die Unterscheidung wichtig.
      Gezeigt wurde nicht, dass „PA Provable(forall n, G(n)) beweist“, sondern eher, dass „PA forall n, Provable(G(n)) beweist“.
      Im ersten Fall würde tatsächlich folgen, dass „PA forall n, G(n) beweist“, aber das zweite ist etwas anderes.
      Ohne auf Goodstein-Folgen zu verweisen, würde ich gern ein Argument dafür sehen, dass man für eine allgemeine Aussage P aus einem Beweis von forall n, Provable(P(n)) nicht auf einen Beweis von Provable(forall n, P(n)) schließen kann.
    • Die Aussage „Wenn PA beweist, dass ‚PA X beweist‘, dann kann PA X beweisen“ ist nicht wahr.
      Innerhalb von PA kann man eine Funktion konstruieren, die alle Beweise durchsucht, die PA erzeugen kann, und darauf aufbauend eine Funktion will-return, die analysiert, was eine bestimmte Funktion bei einer bestimmten Eingabe zurückgeben wird.
      Das ist ähnlich wie ein Versuch, das Halteproblem zu lösen, funktioniert also nicht immer, aber in vielen Fällen doch.
      Konstruiert man daraufhin opposite-return, kann man es so definieren, dass es genau dann zurückkehrt, wenn die gegebene Funktion bei der gegebenen Eingabe nicht zurückkehrt, und nicht zurückkehrt, wenn sie zurückkehrt.
      Betrachtet man dann wie im Standardbeweis des Halteproblems (opposite-return opposite-return opposite-return), kann PA beweisen: „Wenn PA beweisen kann, dass opposite-return zurückkehrt, dann kehrt es in Wirklichkeit nicht zurück“, „Wenn PA beweisen kann, dass es nicht zurückkehrt, dann kehrt es in Wirklichkeit zurück“, „Wenn PA alles tatsächlich beweisen kann, wovon es beweist, dass es es beweist, dann müsste es einen Beweis für eine dieser beiden Aussagen haben“ und „Daher wäre PA in diesem Fall inkonsistent“.
      Das ist eine Form von Gödels zweitem Unvollständigkeitssatz, und deshalb muss man zwischen „PA beweist“ und „PA beweist, dass es selbst beweist“ unterscheiden.
    • Dass das Standardmodell ein Modell von PA ist, gilt nur dann, wenn PA konsistent ist, und PA kann seine eigene Konsistenz nicht beweisen. Solange es nicht inkonsistent ist, ist das wegen des Gödel-Theorems unmöglich.
      Deshalb funktioniert der vorgeschlagene Beweis innerhalb von PA nicht, und genau das scheint der Punkt jenes Kommentars zu sein.

  • https://math.stackexchange.com/questions/4408124/what-does-the-kirby-paris-theorem-mean

  • Ich sprach mit jemandem über induktive Datentypen und zeigte eine zero/succ-Definition wie Nat in Lean oder Rocq.
    Die andere Person fragte: „Ist das alles? Was ist mit den Peano-Axiomen? Gibt es etwas noch Primitiveres als induktive Datentypen?“ – das fand ich interessant.
    Es erinnerte mich daran, dass es sinnvoll ist, die Peano-Axiome nicht als selbstverständlich eingebaut zu betrachten, sondern als eine von mehreren möglichen Konstruktionen.

    • Ich würde natürliche Zahlen für primitiver halten als induktive Datentypen.
      Denn jeder induktive Datentyp lässt sich aus natürlichen Zahlen und primitiven Typkonstruktoren für Summen zusammen mit z. B. Π, Σ, = und Ω aufbauen.

  • Schon der reine Lambda-Kalkül reicht aus, weil er Berechnung kodiert.

  • In Bezug auf die Konsistenz von PA: Das kann innerhalb von PA bewiesen werden: https://youtu.be/6pjLmmkZnIA

    • Für Nicht-Logiker ist hier Kontext unbedingt nötig.
      Gödels zweiter Unvollständigkeitssatz zeigt, dass PA inkonsistent wäre und daher alles beweisen könnte, einschließlich Falschem, wenn PA seine eigene Konsistenz beweisen könnte.
      Die verlinkte Arbeit hat nicht gezeigt, dass PA inkonsistent ist; vielmehr definiert sie eine neue, schwächere Bedeutung von „beweist seine eigene Konsistenz“ und zeigt dann, dass PA diese schwächere Aufgabe leisten kann.
      Das ist interessante Arbeit, aber ihr Sinn erschließt sich erst, wenn man bereits viel Logik kennt.

  • Dieser Beitrag erhielt 123 Punkte, der verlinkte SO-Beitrag aber nur 11 Upvotes.

    • Auf Stack Overflow braucht man 15 Reputationspunkte, um upvoten zu können.
      Dort kommt zur Reputationshürde, dass Beiträge leicht gelöscht werden; zusammen mit der 15-Punkte-Grenze scheint das viele Leute vom Upvoten abzuhalten.