Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

More precise definition of derivations in natural deduction

Đang mở
  • Có gì không ổn?
#300 4 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó
3/5
Thời gian dự kiến
1-2 ngày
Mức phù hợp với người mới
38/100
Loại issue
Tài liệu
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Đình trệ
Công nghệ
tex
Lĩnh vực
documentation

Hướng nghiên cứu

Bắt đầu với content/first-order-logic/natural-deduction/derivations.tex và đọc định nghĩa hiện tại về các suy diễn cũng như chứng minh tính compact. Kiểm tra xem tính hữu hạn được sử dụng ở đâu, bao gồm cả phần thảo luận về số học hóa. Được xem là hoàn thành khi định nghĩa đảm bảo một cách rõ ràng rằng các suy diễn là hữu hạn, đồng thời vẫn giữ cách trình bày dễ tiếp cận, và các chỗ sử dụng bị ảnh hưởng vẫn đúng.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
TeX
Star
1.4k
Fork
289
Không có pull request nào được merge trong 30 ngày

Chuẩn bị môi trường

Dự án này không cung cấp dev container, Dockerfile hay hướng dẫn đóng góp, nên bạn cần tự thiết lập môi trường: hãy bắt đầu từ README và xem hướng dẫn đóng góp lần đầu của chúng tôi để biết các bước chung.

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của OpenLogicProject/OpenLogic

Tất cả issue của OpenLogicProject/OpenLogic

Issue tương tự

Thêm issue về Documentation

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.