Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Tính đồng nhất của các chứng minh cho tính đồng nhất tuyến tính
Tóm tắt
Bài báo này bàn về tính đồng nhất của các chứng minh trong đó xuất hiện một toán tử nhị phân xác định các thuộc tính của tính đồng nhất, bên cạnh phép giao và mệnh đề true hằng số. Các thuộc tính của tính đồng nhất được đề cập là những thuộc tính của quan hệ sắp xếp trước, thuộc tính của quan hệ tương đương và một số thuộc tính khác phù hợp với quan hệ đồng nhất trong logic tuyến tính. Ý tưởng chính là tính đồng nhất của các chứng minh được phát sinh từ sự nhất quán, hiểu như sự tồn tại của một hàm đồng nhất trung thành từ một thể loại ngữ pháp vào một thể loại có các mũi tên tương ứng với các sơ đồ. Các cạnh trong những sơ đồ này nối các xuất hiện của các biến mà phải giữ nguyên trong mọi tổng quát của chứng minh. Người ta nhận thấy rằng các giả định về tính đồng nhất của các chứng minh cho tính đồng nhất là song song với các giả định tiêu chuẩn về tính đồng nhất của các mũi tên trong các thể loại. Chúng tái hiện các giả định thể loại tiêu chuẩn ở một cấp độ khác. Ngoài ra, còn nhận thấy rằng các giả định cho một quan hệ sắp xếp trước liên quan đến một tình huống bổ trợ.
Từ khóa
#tính đồng nhất #chứng minh #quan hệ sắp xếp #logic tuyến tính #thể loạiTài liệu tham khảo
Došen, K.: Equality in substructural logics, in [13], pp. 71–85
Došen, K.: Substructural predicates, in [13], pp. 87–101
Došen K.: Cut Elimination in Categories. Kluwer, Dordrecht (1999)
Došen, K.: Simplicial Endomorphisms, Communications in Algebra, vol. 36, pp. 2681–2709 (2008). Available at http://arXiv.org/math.GT/0301302
Došen, K., Petrić, Z.: Bicartesian Coherence, Studia Logica, vol. 71, pp. 331–353 (2002). Version with some corrections in the proof of maximality available at http://arXiv.org/math.CT/0006052
Došen, K., Petrić, Z.: Generality of proofs and its Brauerian representation. J. Symb. Log. 68, 740–750 (2003). Available at http://arXiv.org/math.LO/0211090
Došen, K., Petrić, Z.: A Brauerian representation of split preorders. Math. Log. Q. 49, 579–586 (2003). Misprints corrected in text available at http://arXiv.org/math.LO/0211277
Došen, K., Petrić, Z.: Proof-Theoretical Coherence. KCL Publications (College Publications), London (2004). Revised version available at http://www.mi.sanu.ac.yu/~kosta/coh.pdf
Došen, K., Petrić, Z.: Proof-Net Categories. Polimetrica, Monza (2007). Preprint available at http://www.mi.sanu.ac.yu/~kosta/pn.pdf
Došen, K., Petrić, Z.: Coherence and confluence. In: Béziau, J.-Y., Costa-Leite, A. (eds.) Perspectives on Universal Logic, pp. 205–215. Polimetrica, Monza (2007). Available at http://arXiv.org/math.CT/0506310
Jacobs B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)
Helman G.: On the equivalence of proofs involving identity. Notre Dame J. Form. Log. 28, 297–321 (1987)
Hodges W. et al.: (eds). Logic, from Foundations to Applications: European Logic Colloquium. Oxford University Press, Oxford (1996)
Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) Applications of Categorical Algebra, pp. 1–14. American Mathematical Society, Providence (1970)
Mac Lane, S.: Natural associativity and commutativity. Rice University Studies, Papers in Mathematics, vol. 49, pp. 28–46 (1963)
Mac Lane, S.: Categories for the Working Mathematician. Springer, Berlin (1971) (expanded 2nd edn, 1998)