Se due cose non sono uguali, sono uguali?

Question

Se due valori in Agda o qualche altra lingua tipizzata in modo dipendente, è possibile dimostrare che v₁ non è uguale a v₂, è possibile provare v₁ uguale a v₂?

Come, c'è una funzione del tipo ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂?

Questo sembra qualcosa che è sicuro aggiungere come assioma se non può essere provato, dal momento che può esserci al massimo un valore di v₁ ≡ v₂.

Un motivo interessante è che la doppia negazione ((a → ⊥) → ⊥) costituisce un monad. Di solito non puoi estrarre i valori da esso, ma puoi usare certi valori, come ⊥ (se si ottiene una contraddizione nella monade della logica classica, si ha una contraddizione). Mi stavo chiedendo se l'uguaglianza fosse una cosa che poteva essere estratta.

Answer 1

Penso che la legge non sia dimostrabile in Agda o Coq.

Grosso modo, abbiamo un solo un'ipotesi

(v1 = v2 -> False) -> False 

e abbiamo bisogno di dimostrare la tesi v1 = v2.

Considerare una prova senza interruzione di ciò in un sistema di prova basato su sequenze. Quale sarebbe l'ultima regola?

Non può essere un'introduzione di v1 = v2, perché Refl non ha quel tipo (v1,v2 sono variabili distinte).

Quindi, deve essere l'eliminazione delle ipotesi, vale a dire

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

Tuttavia, se H1 è davvero dimostrabile, dobbiamo anche avere

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

da cui deriva

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

che è equivalente a

|- v1 = v2 -> False 

che non è chiaramente dimostrabile senza altre ipotesi su v1,v2. Infatti, in caso contrario si potrebbe generalizzare che a

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

che è chiaramente sbagliata.

D'altro canto, credo che Agda/Coq/... siano coerenti con la Legge del Centro Escluso, che implica la legge proposta. Quindi, la legge non può violare la coerenza.

Answer 2

La doppia eliminazione della negazione non è dimostrabile nella teoria del tipo intuizionista, come il chi presentato qui, ma anche la sua negazione è indimostrabile, quindi può essere assunta in modo coerente.

Tuttavia, mentre gli assiomi classici non sono dimostrabili per tutti i tipi, sono dimostrabili per i tipi decidibili.tipi decidibili sono quelli che sono dimostrabilmente abitate o disabitate:

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

Dato Decidable A, si può implementare doppia eliminazione negazione on A: appena partita modello su Either A (A -> False), e se otteniamo un A, allora abbiamo finito, se otteniamo A -> False, quindi applichiamo (A -> False) -> False e usiamo ex falso.

Come caso speciale ((a = b -> False) -> False) -> a = b è dimostrabile se (a b : A) -> Decidable (a = b), i. e. A ha uguaglianza decidibile.

quanto alla monade (A -> False) -> False seguito, quando si lavora all'interno di questa monade otteniamo qualche forma di ragionamento classica, poiché monadic join qui corrisponde all'eliminazione negazione "quadrupla", così not (not (not (not A))) -> not (not A)). Possiamo anche usare callCC, che corrisponde a Peirce's law, un'altra affermazione classica.

C'è un'osservazione interessante su questo: possiamo prendere qualsiasi prova classica, sollevare tutte le proposizioni su Cont False (in altre parole, negarle due volte), e otteniamo una prova costruttiva corrispondente che provi la doppia negazione della proposizione originale. Ciò significa che la logica costruttiva può dimostrare tutto ciò che la logica classica può, modulo classica equivalenza logica, poiché una proposizione e la sua doppia negazione sono classicamente equivalenti.