A framework for co and dual logics, type theories, and programming languages.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
James Martin 4a85719853
Efficiency & complexity, and pulling taut (runtime)
6 days ago
conjectures Unified cobasic rules draft. 3 months ago
dumps Efficiency & complexity, and pulling taut (runtime) 6 days ago
facts Update TarskianHierarchies.md 3 months ago
proofs Basic identity axiom is *admissible*! 3 months ago
.gitignore Unified cobasic rules draft. 3 months ago
README.md Update README.md 3 months ago
TODO Update TODO 1 month ago
proofs.agda-lib Cut elimination for basic logic. 4 months ago

README.md

desert-of-the-surreal

Paracomplete_and_Paraconsistent_Co_and_Dual_and_codual_MetaSystem_Type_Theory_Project

Primary references for research:

Fuzzy Paraconsistent Systems

Definitions of the Properties of Paraconsistent or Paracomplete Systems

Type Theories

Specific System Definitions in Sambin's Cube

LK

Bi-intuitionism

Proof systems and refutation cosystem
LJ
  • TBD
LDJ

BvN

  • TBD

CLL

ILL

DILL

  • TBD

B/B'

U

Misc

Semantic Specifications

Truth and Satisfiability Semantics

Falsity and Unsatisfiability Semantics

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"

Secondary References:

To be investigated but possibly relevant: