Logical Connectives & Formal Systems

← Back to Domain-Specific Families

Abstractions about logical connectives and formal proof systems, including propositional inference rules, satisfiability variants like planar SAT, grammar and sequent formalisms, and semantic conventions governing names and meaning.

13 abstractions in this family — domain-specific abstractions that sit near one another in structural-signature space (k-means over structural-signature embeddings). Each is shown with its short description.

• Classical Modal Logic — A propositional modal logic with necessity–possibility duality and replacement of provable equivalents, broader than the class of normal modal logics.
• Denying the Antecedent — The invalid conditional inference that concludes not-Q from if-P-then-Q and not-P, treating a sufficient condition as necessary.
• Destructive Dilemma — The valid propositional inference from P→Q, R→S, and ¬Q∨¬S to ¬P∨¬R, combining two modus-tollens branches under a disjunction.
• First-Order Arithmetic — Formal first-order theories of natural-number arithmetic defined by a signature, axioms, models, and a specified induction scheme.
• Linear Grammar — A context-free grammar whose productions contain at most one nonterminal on each right-hand side, maintaining one active derivational obligation while emitting terminals around it.
• Logical NOR — The Boolean connective that is true exactly when all its operands are false, equivalently the negation of disjunction; repeated NOR alone is functionally complete for propositional logic.
• Logical or — The inclusive disjunction connective: classically false only when every disjunct is false, and otherwise governed by the declared logic’s semantic and proof rules.
• Matrices of Concepts — A six-position semiotic model that arranges a concept, its inverse, and positive and negative variants into specified relations of duality, contrariety, complementarity, corollary, and association.
• Meaning Postulate — An object-language semantic axiom that restricts interpretations of lexical predicates, so a stipulated word relation supports analytic inferences beyond logical form alone.
• Planar SAT — A Boolean satisfiability restriction in which the bipartite incidence graph connecting variables to the clauses containing them is planar, while the decision question remains whether a satisfying truth assignment exists.
• Resolution Proof Compression by Splitting — A post-processing algorithm that splits a resolution refutation on a chosen variable into complementary branch proofs, recombines them by resolution, and retains the result when it reduces proof size.
• Sequent — Package antecedent and succedent formula contexts into a two-sided formal judgment whose interpretation and admissible transformations are fixed by a proof calculus.
• Unique Name Assumption — A semantic assumption that distinct individual names denote distinct entities, making the interpretation of names injective within the formal reasoning system.