Czym jest „sprzeczność” w logice konstruktywnej?

W praktycznych podstaw dla języków programowania , Robert Harper mówi

Jeśli twierdzenie, które jest prawdziwe, oznacza posiadanie dowodu, co to znaczy, że twierdzenie jest fałszywe? Oznacza to, że mamy obalenie go, pokazując, że nie można tego udowodnić. Oznacza to, że twierdzenie jest fałszywe, jeśli możemy wykazać, że założenie, że jest prawdziwe (ma dowód), przeczy znanym faktom.

Ale to nasuwa pytanie: czym jest sprzeczność w logice konstruktywnej / intuicyjnej?

Czy oznacza to, że w jakiś sposób wywodzi się ? Jak miałoby to nastąpić w rozsądny sposób? Czy należałoby wprowadzić ocenę formy ?$(\bot\text{ true})$$(A \supset \bot \text{ true})$

Alternatywnie, czy może oznacza to, że czytelnik używa swojej dyskrecji, aby nieformalnie oznaczyć coś jako sprzeczne? Na przykład interpretowanie i jako sprzecznych zdań.a ≠ $a = b$$a \neq b$

Nie ma znaczenia, czy mówimy o logice konstruktywnej, czy klasycznej w tej sytuacji. Jeśli ponownie przeczytasz swoje pytania, zobaczysz, że dotyczą one obu rodzajów. Jedyną różnicą, że musimy zwracać uwagę na to prezentacja negacji . Można to przedstawić klasycznie na kilka sposobów, ale intuicyjnie najlepiej jest użyć go jako skrótu A ⇒ ⊥ (dokładnie o tym wspomina Bob Harper w cytowanym akapicie). Ale nie mylmy negacji i sprzeczności.$\lnot A$$A \Rightarrow \bot$

W obu przypadkach sprzeczność to sytuacja, w której udało nam się udowodnić fałsz $\bot$ . Jak moglibyśmy uzyskać w rozsądny sposób? Cóż, z niespójnego zestawu hipotez, byłoby to rozsądnym sposobem na zrobienie tego.$\bot$

Nie masz żadnych uprawnień do „deklarowania” sprzeczności. Musisz udowodnić, że dany zestaw hipotez jest sprzeczny, wyprowadzając . Na przykład, jeśli a = b i ¬ ( a = b ), to możemy użyć faktu, że ¬ ( a = b ) jest skrótem dla ( a = b ) ⇒ ⊥ i wnioskujemy ⊥ przez modus ponens.$\bot$$a = b$$\lnot (a = b)$$\lnot (a = b)$$(a = b) \Rightarrow \bot$$\bot$

$A \land \lnot A$ $\lnot A$$A \Rightarrow \bot$$\bot$$A \land \lnot A$$\bot$$\lnot$

$\bot$

$\bot$$A$$A \Rightarrow \bot$$A$$\lnot A \Rightarrow \bot$$\lnot \lnot A$$\lnot \lnot (\lnot \lnot A \lor \lnot A)$$\lnot \lnot \lnot A \Rightarrow \lnot A$