Nếu hai điều không bằng nhau, chúng có bình đẳng không?

Question

Nếu hai giá trị trong Agda hoặc một số ngôn ngữ được nhập khác, bạn có thể chứng minh rằng v₁ không bằng v₂, bạn có thể chứng minh v₁ bằng v₂ không?

Giống như, có chức năng thuộc loại ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂ không?

Điều này có vẻ như một cái gì đó an toàn để thêm vào như tiên đề nếu nó không thể được chứng minh, vì có thể có nhiều nhất một giá trị v₁ ≡ v₂.

Lý do thú vị là việc phủ định kép ((a → ⊥) → ⊥) tạo thành một monad. Thông thường bạn không thể trích xuất các giá trị từ nó, nhưng bạn có thể có các giá trị nhất định, như ⊥ từ nó (nếu bạn nhận được một mâu thuẫn trong đơn nguyên logic cổ điển, bạn có mâu thuẫn). Tôi đã tự hỏi nếu bình đẳng là một điều có thể được trích xuất.

Answer 1

Tôi nghĩ rằng luật không thể được chứng minh trong Agda hoặc Coq.

đại khái, chúng ta chỉ có một giả thuyết

(v1 = v2 -> False) -> False 

và chúng tôi cần phải chứng minh luận án v1 = v2.

Hãy xem xét bằng chứng miễn phí về điều đó trong hệ thống chứng minh dựa trên trình tự. Quy tắc cuối cùng sẽ là gì?

Không thể giới thiệu v1 = v2, bởi vì Refl không phải loại đó (v1,v2 là các biến riêng biệt).

Vì vậy, nó phải là một loại bỏ các giả thuyết, tức là

H1: (v1 = v2 -> False) -> False |- v1 = v2 -> False 
H2: (v1 = v2 -> False) -> False , False |- v1 = v2 
--------------------------------------------------- (->E) 
(v1 = v2 -> False) -> False |- v1 = v2 

Tuy nhiên, nếu H1 là thực sự chứng minh, chúng ta cũng phải có

(v1 = v2 -> False) -> False |- False 

từ đó chúng ta lấy được

|- ((v1 = v2 -> False) -> False) -> False 

tương đương với

|- v1 = v2 -> False 

rõ ràng là không thể chứng minh được nếu không có bất kỳ giả định nào khác trên v1,v2. Thật vậy, nếu không, chúng tôi có thể khái quát hóa điều đó thành

|- forall v1 v2, v1 = v2 -> False 

rõ ràng là sai.

Mặt khác, tôi tin rằng Agda/Coq/... phù hợp với Luật bị loại trừ ở giữa, ngụ ý luật được đề xuất. Do đó, luật pháp không thể vi phạm tính nhất quán.

Answer 2

Loại trừ phủ định kép không thể giải thích được trong lý thuyết loại trực giác, như chi tiết được trình bày ở đây, nhưng phủ định của nó cũng không thể giải quyết được, vì vậy nó có thể được giả định nhất quán.

Tuy nhiên, trong khi tiên đề cổ điển không thể chứng minh được cho tất cả các loại, chúng có thể chứng minh được cho các loại có thể giải mã được.loại Decidable là những được provably nơi sinh sống hoặc không có người ở:

Decidable : Type -> Type 
Decidable A = Either A (A -> False) 

Với Decidable A, người ta có thể thực hiện loại bỏ phủ đúp vào A: chỉ cần mô hình phù hợp trên Either A (A -> False), và nếu chúng ta có được một A, sau đó chúng tôi đang thực hiện, nếu chúng tôi nhận được A -> False, sau đó chúng tôi áp dụng (A -> False) -> False và sử dụng ex falso.

Như trường hợp đặc biệt ((a = b -> False) -> False) -> a = b có thể chứng minh được nếu (a b : A) -> Decidable (a = b), i. e. A có sự bình đẳng đáng kể.

Với (A -> False) -> False đơn vị tiếp tục, khi chúng tôi làm việc bên trong đơn nguyên này, chúng tôi nhận được một số lý do cổ điển, vì monadic tham gia ở đây tương ứng với loại bỏ phủ định "bốn", vì vậy not (not (not (not A))) -> not (not A)). Chúng tôi cũng có thể sử dụng callCC, tương ứng với Peirce's law, một tuyên bố cổ điển khác. Có một quan sát thú vị về điều này: chúng tôi có thể lấy bất kỳ bằng chứng cổ điển nào, nâng tất cả mệnh đề lên Cont False (nói cách khác, nhân đôi chúng), và chúng tôi nhận được bằng chứng xây dựng tương ứng chứng minh sự phủ định kép của đề xuất ban đầu. Điều này có nghĩa là logic xây dựng có thể chứng minh tất cả mọi thứ logic cổ điển có thể, tương đương logic cổ điển modulo, vì một mệnh đề và phủ định kép của nó là tương đương về mặt cổ điển.