desert-of-the-surreal

Paracomplete_and_Paraconsistent_Co_and_Dual_and_codual_MetaSystem_Type_Theory_Project

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 hidden-variable 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 invalidates-by-epsilon-degrees) 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 invalidates-by-epsilon-degrees) 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 invalidates-by-epsilon-degrees) 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 invalidates-by-epsilon-degrees) 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 invalidates-by-epsilon-degrees) 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 inter-related 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 non-structural or degree-preserving-substructural 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"

Lambek Calculi

• Lambek calclus is a typeological grammar or a category grammar and underlies type-forming operations.
• Non-structural logic with liberated left context; multiplicative intuitionistic linear logic is an extension by the exchange rule.
• Lambek calculus enjoys at most three of the following four properties (https://arxiv.org/abs/1608.02254v1):
  • substitution
  • cut-free
  • the Lambek restriction
  • exponential operators

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 self-dual)
• http://www.inf.ed.ac.uk/teaching/courses/cqi/5-dualobjects.pdf (Finite Hilbert Space Self-Duality)
• http://library.utia.cas.cz/separaty/2016/MTR/noguera-0469166.pdf (fuzzy logics, paraconsistency, degree-preserving 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/notre-dame-journal-of-formal-logic/volume-43/issue-3/Paraconsistency-Everywhere/10.1305/ndjfl/1074290713.pdf (Inconsistency Tolerant Logics)
• https://grahampriest.net/?ddownload=865 (Paraconsistent metalanguage and semantics)
• https://www.irishmathsoc.org/bull23/bull23_8-21.pdf (Paraconsistency, Classical Completeness as Dilemma)
• http://lna.unb.br/lna_n01_01_gpriest.pdf (Paraconsistency, Classical Completeneess as Dilemma)
• https://hal.archives-ouvertes.fr/hal-02383109/document (fire triangle of dependent type theories)
• http://tsinghualogic.net/JRC/wp-content/uploads/2016/06/China_MT2_2016.pdf (Hintikka Sets, classical model theory, and consistency)
• https://arxiv.org/abs/quant-ph/0610097 (Nonlocality as a special case of contextuality)
• http://philsci-archive.pitt.edu/17240/1/CRPT.pdf (Counterfactual Reasoning, Contextuality)
• https://arxiv.org/abs/1705.07918 (Contextuality, Measure of Contextuality, Linear Programming, Resource Theories)
• https://arxiv.org/abs/2112.00357 (Negation-free Paraconsistency, Quasinegations, generalization towards operation-independent definitions of semi/non-classicality)
• http://www.jyb-logic.org/papers12-11/paraconsistent%20negations.pdf (Classical Negation, Paraconsistent negation, positive properties of classical negation)

Type Theories

• https://www.math.unipd.it/~sambin/txt/MaiettiSambin-rev2.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/medial-kurz.pdf (LK, Category of LK, Systemic collapses to Boolean Algebra)

Bi-intuitionism

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/s11225-005-8474-7 (LDJ and its relations to Nelson's logics)

BvN

• TBD

CLL

• https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/categorical-semantics-of-linear-logic.pdf (Linear Logic, Intuitionistic Linear Logic, Sequent Logic Review)

ILL

• https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/categorical-semantics-of-linear-logic.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/Kiarash-Rahmani/publication/266560337_A_Proof_of_Cut-Elimination_Theorem_for_U_Logic/links/54c3514e0cf256ed5a9117dc/A-Proof-of-Cut-Elimination-Theorem-for-U-Logic.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/confluence-in-the-sequent-calculus/ (Cut elimination, non-confluence of proof, proof irrelevance)
• https://sites.pitt.edu/~belnap/87displaylogic.pdf (Display Logic, Structural Proof Theory, semantically exposed sequent calculi)
• https://consequently.org/papers/subint.pdf (Subintuitionistic Logics, cube-like structure for relation between SJ and J)
• https://arxiv.org/abs/1606.08092 (Classifying Material Implication over Minimal Logic, Paracompleteness)

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 T-Schema, 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/quant-ph/0701171 (Metatheorem for the Liar's Paradox and T-Schema in non-structural 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/why-is-intuitionistic-negation-nonconstructive
• https://link.springer.com/article/10.1007/s11225-005-8474-7
• http://people.cs.uchicago.edu/~kaharris/phil525/negation.pdf (Semantics of Classical Negation)

Secondary References:

• https://www.cs.cmu.edu/~fp/courses/atp/handouts/ch3-seqcalc.pdf (Sequent calculi basics)
• https://faculty.sites.iastate.edu/dpigozzi/files/inline-files/aaldedth.pdf (Algebraization of logics, deduction theorem, equational theories)
• http://alessio.guglielmi.name/res/cos/ (Deep inference, intuitionistic logic, bi-intuitionism, 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/quant-ph/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/s10516-021-09561-8.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/Vienna2011-FOLP.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/Ashu-Notes.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 heat-process efficiency Limit)
• https://arxiv.org/abs/0811.4542 (Logical Independence and Quantum Randomness)
• http://philsci-archive.pitt.edu/8660/1/master_theory_experiment.pdf (Physical Theories, Consistency)
• https://www.cs.yale.edu/homes/piskac/teaching/decpro-729/fol.pdf (First Order Logic, Substitution)

To be investigated but possibly relevant:

• https://logic.rwth-aachen.de/Research/AlMoTh/index.html.en (finite model theory and algorithmic theory is particular relevant for substructural or non-structural systems, polarity)