James Martin
4a85719853

4 months ago  

conjectures  7 months ago  
dumps  4 months ago  
facts  6 months ago  
proofs  7 months ago  
.gitignore  7 months ago  
README.md  7 months ago  
TODO  5 months ago  
proofs.agdalib  7 months ago 
README.md
desertofthesurreal
Paracomplete_and_Paraconsistent_Co_and_Dual_and_codual_MetaSystem_Type_Theory_Project
Primary references for research:
Fuzzy Paraconsistent Systems
 https://arxiv.org/abs/1003.5976 (Lq, L2q, Lnq, Quantum metalanguage, qubits, paraconsistency, and paracompleteness)
 https://math.ucr.edu/home/baez/quantum/node3.html (category theory and Hilbert Spaces; related paper to find: the category of Hilbert spaces is selfdual)
 http://www.inf.ed.ac.uk/teaching/courses/cqi/5dualobjects.pdf (Finite Hilbert Space SelfDuality)
 http://library.utia.cas.cz/separaty/2016/MTR/noguera0469166.pdf (fuzzy logics, paraconsistency, degreepreserving entailment, definition of Boldly Paraconsistent, LFI)
Definitions of the Properties of Paraconsistent or Paracomplete Systems
 https://www.sciencedirect.com/science/article/pii/S1571066120300827 (Definition of Genuine Paraconsistency and Genuine Paracompleteness)
 https://projecteuclid.org/journals/notredamejournalofformallogic/volume43/issue3/ParaconsistencyEverywhere/10.1305/ndjfl/1074290713.pdf (Inconsistency Tolerant Logics)
 https://grahampriest.net/?ddownload=865 (Paraconsistent metalanguage and semantics)
 https://www.irishmathsoc.org/bull23/bull23_821.pdf (Paraconsistency, Classical Completeness as Dilemma)
 http://lna.unb.br/lna_n01_01_gpriest.pdf (Paraconsistency, Classical Completeneess as Dilemma)
 https://hal.archivesouvertes.fr/hal02383109/document (fire triangle of dependent type theories)
 http://tsinghualogic.net/JRC/wpcontent/uploads/2016/06/China_MT2_2016.pdf (Hintikka Sets, classical model theory, and consistency)
 https://arxiv.org/abs/quantph/0610097 (Nonlocality as a special case of contextuality)
 http://philsciarchive.pitt.edu/17240/1/CRPT.pdf (Counterfactual Reasoning, Contextuality)
 https://arxiv.org/abs/1705.07918 (Contextuality, Measure of Contextuality, Linear Programming, Resource Theories)
Type Theories
 https://www.math.unipd.it/~sambin/txt/MaiettiSambinrev2.pdf (minimal type theory, extensionality incompatibility with MLTT w/ axiom of choice, powerset compatibility with extensionality and incompatibility with axiom of choice, degeneracy of intuitionism to classical logic)
Specific System Definitions in Sambin's Cube
LK
 https://www.lix.polytechnique.fr/~lutz/papers/medialkurz.pdf (LK, Category of LK, Systemic collapses to Boolean Algebra)
Biintuitionism
Proof systems and refutation cosystem
 http://users.cecs.anu.edu.au/~linda/thesis.pdf (Simultaneous systems of paracomplete proof and paraconsistent refutation)
 https://research.uca.ac.uk/2985/1/SCCL(Final).pdf (Simultaneous systems of paracomplete proof and paraconsistent refutation, The system LJ and coLJ)
LJ
 TBD
LDJ
 https://projecteuclid.org/journalArticle/Download?urlId=10.1305%2Fndjfl%2F1039886520 (The system LDJ)
 https://link.springer.com/article/10.1007/s1122500584747 (LDJ and its relations to Nelson's logics)
BvN
 TBD
CLL
 https://www.irif.fr/~mellies/mpri/mpriens/biblio/categoricalsemanticsoflinearlogic.pdf (Linear Logic, Intuitionistic Linear Logic, Sequent Logic Review)
ILL
 https://www.irif.fr/~mellies/mpri/mpriens/biblio/categoricalsemanticsoflinearlogic.pdf (Linear Logic, Intuitionistic Linear Logic, Sequent Logic Review)
DILL
 TBD
B/B'
 https://www.math.unipd.it/~sambin/txt/SBF.pdf (Sambin et al, Basic Sequent Logic, paraconsistency and paracompleteness)
 https://arxiv.org/abs/1910.05120 (Refinement on the connectives for Basic Sequent Logic, reflection = derivability of identicals)
U
 https://www.researchgate.net/publication/266988362_A_unification_of_the_basic_logics_of_Sambin_and_Visser
 https://www.researchgate.net/profile/KiarashRahmani/publication/266560337_A_Proof_of_CutElimination_Theorem_for_U_Logic/links/54c3514e0cf256ed5a9117dc/AProofofCutEliminationTheoremforULogic.pdf (B', U, and subintuitionistic cube of extensions)
Misc
 https://www.pauldownen.com/publications/downen_phd.pdf (the substructural system L which appears to be a combination of Sambin's Basic Logic as a Type Theory and its dual/co?)
 https://prooftheory.blog/2021/09/23/confluenceinthesequentcalculus/ (Cut elimination, nonconfluence of proof, proof irrelevance)
 https://sites.pitt.edu/~belnap/87displaylogic.pdf (Display Logic, Structural Proof Theory, semantically exposed sequent calculi)
Semantic Specifications
Truth and Satisfiability Semantics
 https://www.impan.pl/~kz/truthseminar/Kripke_Outline.pdf (Kripke Theory of Truth)
 https://scholarworks.uno.edu/cgi/viewcontent.cgi?article=1057&context=honors_theses (Definability of Truth)
 http://people.cs.uchicago.edu/~kaharris/phil525/week_1/paradox.html (Tarski TSchema, definability of truth, classical logic)
 https://macsphere.mcmaster.ca/bitstream/11375/13863/1/fulltext.pdf (Tarski's Hierachy of Languages and Metalanguages)
 https://arxiv.org/abs/quantph/0701171 (Metatheorem for the Liar's Paradox and TSchema in nonstructural systems like Lq)
 http://www.mbph.de/Logic/Para/SemanticClosure.pdf (Paraconsistency and semantic closure)
 http://people.cs.uchicago.edu/~kaharris/phil525/week_1/consistent.html (Semantically Closed Classical System)
Falsity and Unsatisfiability Semantics
 https://philosophy.stackexchange.com/questions/11448/whyisintuitionisticnegationnonconstructive
 https://link.springer.com/article/10.1007/s1122500584747
 http://people.cs.uchicago.edu/~kaharris/phil525/negation.pdf (Semantics of Classical Negation)
Theses:
 (Thesis) There is a trichotomy between equational theory, computation, and polarity.
 (Thesis) There is a dilemma between dependent types, the fire triangle of dependent types, and an interpretation of quantum computation as a hiddenvariable theory.
 (Thesis) There is a paraconsistent alternative to the metalinguistic hierarchy based on the problems of definability of truth and definability of falsity in paraconsistent systems.
Preliminaries of Systems Theory
 A system is a formal language or grammar or automata together with a formal semantic.
 A metasystem is a formal language or grammar or automata together with a formal semantic that maps the language to the semantic or the semantic to the language of the object system where the metasystem is generally higher order than the object system.
Definitions of Paraquality Systems
A system is called a syntactically paraconsistent system to some degree if it invalidates (or invalidatesbyepsilondegrees) any of the following:
 Law of Duns Scotus in the object system
 Non Contradiction on the right hand side of the turnstile in the object system
 Non Contradiction on the left hand side of the turnstile in the object system
A system is called a semantically paraconsistent system to some degree if it invalidates (or invalidatesbyepsilondegrees) any of the following:
 Law of Duns Scotus in the metasystem or in its formal semantics
 Bivalence on the right hand side of the turnstile in the metasystem or in its formal semantics
 Bivalence on the left hand side of the turnstile in the metasystem or in its formal semantics
A system is called a syntactically paracomplete system to some degree if it invalidates (or invalidatesbyepsilondegrees) any of the following:
 Law of Clavius in the object system
 Excluded Middle on the right hand side of the turnstile in the object system
 Excluded Middle on the left hand side of the turnstile in the object system
A system is called a semantically paracomplete system to some degree if it invalidates (or invalidatesbyepsilondegrees) any of the following:
 Law of Clavius in the metasystem or in its formal semantics
 Bivalence on the right hand side of the turnstile in the metasystem or in its formal semantics
 Bivalence on the left hand side of the turnstile in the metasystem or in its formal semantics
A system is called a paracomplete and paraconsistent system to some degree if it satisfies at least one condition from each of the paraconsistent and paracomplete conditions and invalidates (or invalidatesbyepsilondegrees) any of the following.
 (conjectured) Law of indiscernibles in the object system
 (conjectured) Law of indiscernibles in the metasystem
There exists a complex relationship between paracomplete and paraconsistent systems in terms of their relative duality and polarity with respect to each other.
There exists a complex relationship between paracomplete and paraconsistent systems in terms of their relative (free?) contextuality on the RHS or LHS of sequents.
Contextuality, Duality, Polarity, and Structures
(Conjecture) Contextuality, duality, and polarity are interrelated to (co)varying degrees.
These complexes of relations are expressed in the squares of oppositions between the sequent systems: LJ (intuitionistic logic), LDJ (dual intuitionistic logic), coLJ (intuitionistic refutation), and coLDJ (dual intuitonistic refutation).
For each of the systems expressed in the cube of extensions of Sambin's Basic Logic, there exists these squares of oppositions.
 (Conjectured) there are generalized polytopes of opposition for each such square of oppositions under paraconsistent or degree preserving entailment systems.
 (Conjectured) there exists a kind of hybrid cut which is a combination of a part of cut of proofs and a part of cut of refutations.
 (Conjectured) the hybrid cut is related in nonstructural or degreepreservingsubstructural systems to the EPR cut in Lq.
"But in dependent types, equational inconsistency means that any two types will be equal, which further entails logical inconsistency. https://proofassistants.stackexchange.com/a/713"
Secondary References:
 http://alessio.guglielmi.name/res/cos/ (Deep inference, intuitionistic logic, biintuitionism, linear and local logics, structural proof theory, and a LOT more)
 https://core.ac.uk/download/pdf/162572056.pdf (Fuzzy multisets)
 https://www.researchgate.net/publication/221320313_Fuzzy_Multisets_and_Their_Generalizations
 https://www.researchgate.net/publication/230657496_On_Generalized_Fuzzy_Multisets_and_their_Use_in_Computation
 https://arxiv.org/abs/quantph/0607100 (A model of Paraconsistent Turing Machines)
 https://arxiv.org/abs/0802.0150 (Paraconsistent Turing Machines compared to Quantum Computers)
 https://link.springer.com/content/pdf/10.1007/s10516021095618.pdf (Type Theories, Limits of Computability)
 https://www.sciencedirect.com/science/article/pii/S0304397511008978 (Proof system of Nelson's logic N4)
 http://www.cle.unicamp.br/prof/coniglio/LETJ.pdf (paraconsistency and Nelson's logics, evidentiary interpretations)
 https://sartemov.ws.gc.cuny.edu/files/2013/01/Vienna2011FOLP.pdf (FOLP, Paracompleteness, LJ + predicates, Inconsistency Tolerance)
 https://www.youtube.com/watch?v=9ZqcTEX4v9E (Assertion and Denial)
 https://arxiv.org/abs/1103.4324v3 (Review of Paraconsistent Systems)
 https://sites.ualberta.ca/~francisp/Phil428/Phil428.11/PostPellMartin.pdf (Functional Completeness)
 https://people.math.wisc.edu/logic/quals/AshuNotes.pdf (Summary of Classical First Order Logic properties such as categoricity, completeness, and compactness)
 https://espace.library.uq.edu.au/view/UQ:4fcc5f0 (Inconsistent Truth Tables)
 https://arxiv.org/pdf/1811.03678v2.pdf (Reversible Computing, Quantum Computing)
 http://holtz.org/Library/Natural%20Science/Physics/Optimization%20Through%20Evolution%20and%20Recombination%20%20Bremermann%201962.htm (Bremermann Computing Limit)
 https://arxiv.org/pdf/1611.05821.pdf (Communication Limit)
 http://worrydream.com/refs/Landauer%20%20Irreversibility%20and%20Heat%20Generation%20in%20the%20Computing%20Process.pdf (Landauer heatprocess efficiency Limit)
 https://arxiv.org/abs/0811.4542 (Logical Independence and Quantum Randomness)
 http://philsciarchive.pitt.edu/8660/1/master_theory_experiment.pdf (Physical Theories, Consistency)
 https://www.cs.yale.edu/homes/piskac/teaching/decpro729/fol.pdf (First Order Logic, Substitution)
To be investigated but possibly relevant:
 https://logic.rwthaachen.de/Research/AlMoTh/index.html.en (finite model theory and algorithmic theory is particular relevant for substructural or nonstructural systems, polarity)