Hacktoberfest 2026: die Issues, die Maintainer für den Oktober markiert haben – offen und einsteigerfreundlich. Hacktoberfest-Issues durchsuchen

More precise definition of derivations in natural deduction

Offen
  • Stimmt etwas nicht?
#300 4 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen

Dieses Issue hat noch niemand übernommen.

Bewertung

Schwierigkeit
3/5
Geschätzter Aufwand
1-2 Tage
Anfängerfreundlichkeit
38/100
Issue-Typ
Dokumentation
Klarheit
Größtenteils klar
Aktivitätsstatus
Veraltet
Tech-Stack
tex
Bereich
documentation

Rechercherichtung

Beginne mit content/first-order-logic/natural-deduction/derivations.tex und lies die aktuelle Definition von Ableitungen sowie den Beweis der Kompaktheit. Prüfe, wo Endlichkeit verwendet wird, einschließlich der Diskussion zur Arithmetisierung. Als abgeschlossen gilt die Aufgabe, wenn die Definition ausdrücklich endliche Ableitungen sicherstellt und dabei ihre zugängliche Darstellung beibehält, wobei die betroffenen Verwendungen weiterhin korrekt bleiben.

Vom Indexierungsmodell aus dem Issue-Text verfasst.

Beschreibung

The current definition of a derivation of a sentence !A from a set of assumptions \Gamma in natural deduction is a tree of sentences in which the bottommost sentence is !A, the topmost sentences are in \Gamma or are discharged by an application of a rule, and every sentence in the tree apart from the conclusion is a premise of a correct application of an inference whose conclusion stands immediately below that sentence in the tree.

Unless I'm missing something, this does not appear to rule out infinite derivations. Definitions of the set of derivations in other standard textbooks, e.g. van Dalen's Logic and Structure, use an inductive definition to ensure the finiteness of definitions. I propose that we do the same, and make explicit the fact that this implies that all derivations are finite. This would thereby fix a hole in the proof that the derivability relation is compact, which makes explicit and essential use of the fact that derivations are finite. It's also implicitly used when we arithmetize derivations.

If this sounds like a reasonable idea then I'm happy to put together a patch with a proposed solution. Obviously it's important to preserve the virtues of the current definition, namely its approachability and relative informality.

Any changes would (I think) be restricted to content/first-order-logic/natural-deduction/derivations.tex, although the effects of the correction would be felt in other places where the proposition that the derivability relation is compact is used.

Vorherrschende Sprache
TeX
Sterne
1.4k
Forks
289
Keine gemergten PRs in 30 T.

Entwicklungsumgebung

Dieses Projekt bietet weder Dev-Container noch Dockerfile noch Beitragsleitfaden – die Einrichtung liegt bei Ihnen. Beginnen Sie mit der README; die allgemeinen Schritte stehen in unserem Leitfaden für den ersten Beitrag.

Erste Schritte

  1. Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
  2. Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
  3. Forken Sie das Repository und arbeiten Sie in einem Branch.
  4. Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.

Mehr aus OpenLogicProject/OpenLogic

Alle Issues in OpenLogicProject/OpenLogic

Ähnliche Issues

Weitere Issues zu Documentation

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.