Justify intuitionistic logic through the BHK interpretation could be problematic
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 25/100
- Tipo di issue
- Documentazione
- Chiarezza
- Da chiarire
- Stato di attività
- Ferma
- Stack tecnologico
- tex
- Ambito
- documentation
Direzione di ricerca
La issue non indica alcun file, test o punto di ingresso. Inizia individuando la giustificazione BHK dell'OLT e confrontandola con la discussione citata di van Dalen e Troelstra. Il lavoro sarà completato quando sarà stata aggiunta una spiegazione chiara e condivisa di cosa significano le funzioni o trasformazioni costruttive e del perché la lettura classica sia insufficiente.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Using the BHK interpretation to justify intuitionistic logic requires a discussion on what we mean by a "function" that transforms a construction of A to a construction of B. van Dalen and Troelstra writes (in Constructivism in Mathematics):
This exercise shows that the BHK-interpretation in itself has no "explanatory power": the possibility of recognizing a classically valid logical schema as being constructively unacceptable depends entirely on our interpretation of "construction", "function", "operation".
The OLT is justifying the ND-rules for intuitionistic logic using the BHK-construction, but a similar BHK based argument justifies the RAA rules as well (interpreting "function" as a classical set theoretic object).
I think this should be commented on in the text together with a discussion on what a constructive transformation could mean. I'm afraid I won't be able to do it good enough.
- Lingua principale
- TeX
- Stelle
- 1.4k
- Fork
- 289
- Metriche di merge delle PR
- Nessuna PR unita negli ultimi 30g
Preparare l'ambiente
Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di OpenLogicProject/OpenLogic
-
Russel's Paradox typoAperta
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 65/100
OpenLogicProject/OpenLogic#339 · 1 commento ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 50/100
OpenLogicProject/OpenLogic#436 ·
-
Difficoltà 3/5 1-2 giorni Idoneità per principianti 68/100
OpenLogicProject/OpenLogic#435 · 1 commento ·
-
Order-type of models of PAAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100
OpenLogicProject/OpenLogic#425 · 1 commento ·
-
Improve docsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
OpenLogicProject/OpenLogic#390 ·
Tutte le issue di OpenLogicProject/OpenLogic
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
Juniper/ansible-junos-stdlib#904 ·
-
Antigravity-cli-hands-on]Aperta
Difficoltà 2/5 Meno di un'ora Idoneità per principianti 75/100
googlecodelabs/feedback#2364 ·
-
area:http-gateway good first issue priority:low type:docs
Difficoltà 2/5 1-3 ore Idoneità per principianti 88/100
crazy-goat/php-fpm-ng#828 ·
I maintainer di solito rispondono entro 1 giorno
-
documentation
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
danjdewhurst/story-skills#538 ·
I maintainer di solito rispondono entro 1 giorno
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
wimpysworld/sidra#290 ·
I maintainer di solito rispondono entro 1 giorno