Concept coverage

How much of Logic’s own ontology (Ontology.toml) actually has a formalized declaration behind it: 45 of 74 concepts have at least one, so far. Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a concept to jump to it below. The same concepts are also listed as headings below the graph, in reading order, if that’s easier to browse.

thickmoderatethinuncoveredcoversprecedes

legend

popper (41)

(no declarations yet)

basis (16)

• Logic.Popper.Basis1
• Logic.Popper.Basis3

follows (8)

• Logic.Popper.Basis1.Follows
• Logic.Popper.Basis3.Follows

reflexivity (2)

• Logic.Popper.Basis1.follows_refl
• Logic.Popper.Basis3.refl

transitivity (2)

• Logic.Popper.Basis1.follows_trans
• Logic.Popper.Basis3.trans

mutual-deducibility (2)

• Logic.Popper.Basis1.Mutual

substitutivity (1)

• Logic.Popper.Basis1.substitutivity

deducibility (6)

• Logic.Popper.Basis1.Deduce

generalised-reflexivity (1)

• Logic.Popper.Basis1.rg

generalised-transitivity (1)

• Logic.Popper.Basis1.tg

exchange-of-premises (1)

• Logic.Popper.Basis1.exchange

weakening-of-premises (1)

• Logic.Popper.Basis1.weaken

contraction-of-premises (1)

• Logic.Popper.Basis1.contract

relative-demonstrability (6)

• Logic.Popper.Basis1.Demonstrate

demonstrable (1)

• Logic.Popper.Basis1.Demonstrable

complementarity (1)

• Logic.Popper.Basis1.Complementary

refutable (1)

• Logic.Popper.Basis1.Refutable

contradictory (1)

• Logic.Popper.Basis1.Contradictory

context (0)

(no declarations yet)

cut (1)

• Logic.Popper.Basis1.cut

connective (13)

(no declarations yet)

inferential-definition (5)

• Logic.Popper.Basis1.isClassicalNegation_congr
• Logic.Popper.Basis1.isConjunction_congr
• Logic.Popper.Basis1.isDisjunction_congr
• Logic.Popper.Basis1.isImplication_congr
• Logic.Popper.Basis1.isIntuitionisticNegation_congr

conjunction (1)

• Logic.Popper.Basis1.IsConjunction

disjunction (1)

• Logic.Popper.Basis1.IsDisjunction

classical-negation (2)

• Logic.Popper.Basis1.IsClassicalNegation
• Logic.Popper.Basis1.contradictory_of_isClassicalNegation

intuitionistic-negation (2)

• Logic.Popper.Basis1.IsIntuitionisticNegation
• Logic.Popper.Basis1.contradictory_of_isIntuitionisticNegation

implication (2)

• Logic.Popper.Basis1.IsImplication

deduction-theorem (1)

• Logic.Popper.Basis1.IsImplication

modus-ponens (1)

• Logic.Popper.Basis1.demonstrate_mp

substitution (4)

• Logic.Popper.HasSubstitution

name (1)

• Logic.Popper.HasSubstitution.DIST

non-dependence (1)

• Logic.Popper.NonDep

freshness (1)

• Logic.Popper.HasSubstitution.fresh

quantification (2)

• Logic.Popper.Basis1.IsUniversal

universal-quantifier (1)

• Logic.Popper.Basis1.IsUniversal

existential-quantifier (1)

• Logic.Popper.Basis1.IsExistential

proof-theory (11)

(no declarations yet)

proof-system (5)

• Logic.ProofTheory.ProofSystem

deduction (3)

• Logic.ProofTheory.Derivation

premise (1)

• Logic.ProofTheory.Application.premises

conclusion (1)

• Logic.ProofTheory.Application.conclusion

finitary (0)

(no declarations yet)

certificate (0)

(no declarations yet)

cut-elimination (1)

• Logic.ProofTheory.derivable_iff_derivableCutFree

proof-rule (6)

• Logic.ProofTheory.Application

axiom (1)

• Logic.ProofTheory.Schema.IsAxiom

simple-rule (1)

• Logic.ProofTheory.Schema.IsSimpleRule

complex-rule (1)

• Logic.ProofTheory.Schema.IsComplexRule

rule-schema (1)

• Logic.ProofTheory.Schema

assumption (1)

• Logic.ProofTheory.Derivation.assumption

rule-redundancy (0)

(no declarations yet)

provable-object (0)

(no declarations yet)

derivable-rule (0)

(no declarations yet)

admissible-rule (0)

(no declarations yet)

weakly-admissible-rule (0)

(no declarations yet)

syllogistic-logic (0)

(no declarations yet)

term (0)

(no declarations yet)

universal-statement (0)

(no declarations yet)

law-of-identity (0)

(no declarations yet)

barbara (0)

(no declarations yet)

particular-statement (0)

(no declarations yet)

conversion (0)

(no declarations yet)

existential-import (0)

(no declarations yet)

interpretation (0)

(no declarations yet)

soundness (0)

(no declarations yet)

completeness (0)

(no declarations yet)

term-model (0)

(no declarations yet)

propositional-logic (0)

(no declarations yet)

modal-logic (0)

(no declarations yet)

first-order-logic (0)

(no declarations yet)

separation-logic (0)

(no declarations yet)

second-order-logic (0)

(no declarations yet)

Other concepts

Not part of the lecture order or covered by anything else in the ontology.

uniqueness-of-definition (5)

• Logic.Popper.Basis1.isClassicalNegation_unique
• Logic.Popper.Basis1.isConjunction_unique
• Logic.Popper.Basis1.isDisjunction_unique
• Logic.Popper.Basis1.isImplication_unique
• Logic.Popper.Basis1.isIntuitionisticNegation_unique

derivation (0)

(no declarations yet)