Logical Consequence¶
A logic-relative relation licensing a formula as following from premises under a specified semantic or derivational criterion.
Core Idea¶
Logical consequence is the formal, logic-relative relation in which a conclusion formula is licensed by premises. Write \(\Gamma\vDash_{L}\varphi\) when, under a specified language and semantics for logic \(L\), every admissible model satisfying all formulas in \(\Gamma\) also satisfies \(\varphi\). Write \(\Gamma\vdash_{D}\varphi\) when a specified deductive calculus \(D\) derives \(\varphi\) from \(\Gamma\). These are distinct ways of determining a premise-to-conclusion relation. They coincide only where soundness and completeness have been established for the particular pairing of calculus and semantics; no such bridge theorem is constitutive of every consequence relation.[1][2][3]
The relation is meta-level: it makes a judgment about formulas and a chosen logic. It is not automatically the object-language conditional \(A\to B\). Tarski's original semantic treatment distinguishes consequence from a finite stock of accepted derivation rules, defines model-based consequence relative to language, and highlights the open question of which terms count as logical rather than extra-logical. Gentzen's proof-theoretic treatment instead makes assumptions, sequents and derivations explicit. KLM exhibit a further class of preferential nonmonotonic consequence relations where a conclusion may be retracted when new exception information is added.[1][2][3]
Structural Signature¶
Sig role-phrases: specified formal language and logic — premise collection — candidate conclusion — licensing criterion — relation-specific behavior.
- Formal language and logic. The formulas and logical constants must be specified; a semantic interpretation class or a deductive calculus fixes what counts as following. Tarski explicitly notes that satisfaction is language-relative and the logical/extra-logical division is nontrivial.[1]
- Premise collection. \(\Gamma\) supplies formulas assumed or treated as information. Gentzen's sequents put formulas on an antecedent side; KLM treat a premise condition in a preferential model. An empty \(\Gamma\) is a special theoremhood/validity case, not the only case.[2][3]
- Candidate conclusion. \(\varphi\) is the formula whose consequence status is tested. Without a conclusion target, no membership judgment \(\Gamma\mathrel{\vdash/\vDash}\varphi\) is formed.[1][2]
- Licensing criterion. Semantic versions ask whether selected models preserving the premises also preserve the conclusion; proof-theoretic versions ask whether accepted rules yield a derivation. The criterion is part of the typed relation, not a vague feeling of inevitability.[1][2][3]
- Relation-specific behavior. Reflexivity, cut and monotonicity must be evaluated for the selected relation rather than silently made universal. KLM's preferential examples intentionally fail classical monotonicity while retaining a formal consequence-relation framework.[3]
The structural test is not “is the conclusion true?” A false premise set may entail a formula classically, and a true conclusion may fail to follow from particular premises. The question is whether the relation's rule licenses this ordered premise/conclusion pair.[1]
What It Is Not¶
Not material implication. \(A\to B\) is a formula inside a language; \(\Gamma\vDash B\) and \(\Gamma\vdash B\) are metalanguage judgments involving a premise collection and a chosen criterion. Some calculi encode a one-premise consequence with a conditional under specified assumptions, but that is a theorem or convention, not generic identity. KLM explicitly distinguish their meta-level relation from a conditional connective.[2][3]
Not an inference rule or reasoning episode. A rule such as conjunction elimination is a schema for one licensed step in a calculus; a derivation is a sequence/tree of such steps. Consequence is the relation determined by all relevant derivations—or by a model condition. Live Inference Rule and prime Deductive Reasoning are therefore neighbors, not exact coverage.[2]
Not universally classical truth preservation. Tarski-style all-model truth preservation is one semantic specification. KLM's preferential criterion checks favored premise-compatible worlds and can be nonmonotonic. Other systems select other proof or model standards. A bare \(\Gamma\vDash\varphi\) should be read with its logic and model class stated.[1][3]
Not guaranteed sound-and-complete correspondence. A proof relation and a semantic relation may be compared, but their equivalence needs a proof for that precise language, calculus, semantics and assumptions. Neither Tarski nor Gentzen makes an arbitrary proof calculus automatically coextensive with every model class.[1][2]
Scope of Application¶
In classical first-order semantics, a model of premises fixes an interpretation of nonlogical symbols. Consequence requires no admissible countermodel in which all premises are true and the conclusion false. For example, \(\{\forall x(P(x)\to Q(x)),P(a)\}\vDash Q(a)\) under standard first-order semantics. The example depends on the logical meanings of \(\forall\) and \(\to\) and on \(a\) denoting an object in a nonempty domain; it is a source-grounded application of Tarski's model criterion, not a claim that he printed these exact formulas.[1]
In Gentzen-style proof systems, formulas appear as assumptions or antecedents and a conclusion is obtained by permitted proof figures. One can display a finite derivation of the same \(Q(a)\) using universal instantiation and detachment in a suitable calculus. That shows a syntactic consequence judgment; whether it matches the selected model relation requires its own soundness/completeness result.[2][1]
In preferential nonmonotonic logic, KLM model plausible consequence via preferred/normal worlds. From “Tweety is a bird,” one may defeasibly infer flight under a default-normality model; adding “Tweety is a penguin” can withdraw flight while preserving the earlier premise. The relation is still formally organized by premises, conclusion and criterion, but it fails ordinary monotonicity.[3]
Clarity¶
The symbols \(\vDash\) and \(\vdash\) clarify what must be supplied. For \(\vDash\), name the language, interpretations and model-selection standard. For \(\vdash\), name the calculus, assumptions and derivation rules. To ask whether they coincide, state a particular soundness direction (\(\vdash\) implies \(\vDash\)) and completeness direction (\(\vDash\) implies \(\vdash\)) rather than invoking an undifferentiated “bridge.”[1][2][3]
Tarski's logical/extra-logical boundary prevents an easy formalism shortcut. Holding \(\forall\) fixed while varying predicates gives a different range of admissible reinterpretations from treating more vocabulary as fixed. Thus “formal” does not mean the selection of logical vocabulary is settled by typography alone.[1]
Manages Complexity¶
Treating consequence as a relation lets one ask which premise/conclusion pairs satisfy a criterion without rehearsing a new informal argument each time. Model-based tests search for countermodels; proof-based tests seek derivations. The distinction also localizes disagreements: two logics may share syntax but disagree on admissible models or rules, so a formula's consequence status changes without changing the words of the premise and conclusion.[1][2][3]
The abstraction does not erase hard work. First-order consequence can involve complex proof search, and nonmonotonic reasoning requires specifying how preferred worlds change as premises grow. A soundness or representation theorem can connect accounts for a specified system; it cannot be borrowed from a different calculus solely because both use the word “consequence.”[2][3]
Abstract Reasoning¶
For a proposed judgment, first identify the formula language and chosen logic, then list the premise collection and candidate conclusion. State the criterion as a membership condition. If semantic, try to construct an admissible countermodel; if one exists, consequence fails. If proof-theoretic, exhibit a derivation or establish that the rules cannot produce one. The latter failure by itself says nothing about semantic consequence absent a completeness result.[1][2]
Properties belong to the relation, not to the label. Under classical model consequence, enlarging \(\Gamma\) cannot create a countermodel that was not already a model of \(\Gamma\), so monotonicity follows. In preferential consequence, adding information can alter the preferred subset of premise-compatible worlds and defeat a former conclusion. This contrast is why Monotonicity of Entailment is a separate live property, not an axiom imported into the generic identity.[1][3]
Knowledge Transfer¶
The premise–conclusion–criterion grammar transfers from Tarski's semantic account to Gentzen's proof calculi and KLM's preferential relation, but their extensions need not coincide. A model class, a proof calculus and a preference ordering are not interchangeable components; they are alternate or additional determinations of a consequence judgment.[1][2][3]
Live prime Relation is the proposed strict genus because each fixed logical consequence is a specified membership relation between premise collections and conclusions. Prime Deductive Reasoning and live Inference Rule concern processes or individual rules. Propositional Logic is one formal system where such a relation can be defined. The named identity remains domain-specific to formal logic despite the broad portability of its underlying relation skeleton.[4][2]
Examples¶
Classical model consequence. Let \(\Gamma=\{\forall x(P(x)\to Q(x)),P(a)\}\) and \(\varphi=Q(a)\). The language has \(P,Q,a\) and the ordinary first-order logical vocabulary; \(\Gamma\) is the premise collection and \(\varphi\) the conclusion. Every model satisfying both premises makes \(P(a)\) true and the universal conditional forces \(Q(a)\), so no countermodel exists. Mapped back: this is a premise-to-conclusion relation fixed by a classical all-model licensing criterion, and its monotonicity is a property of that criterion, not a universal definition.[1]
Preferential defeasible consequence. In KLM's bird/penguin example, the language represents bird, flight and penguin claims about Tweety; the premise first says bird and the target conclusion says flies. Preferred normal bird-worlds support the target. Adding the penguin premise changes the preferred premise-compatible worlds, and flight need no longer be licensed. Mapped back: the same typed premise/conclusion/criterion schema is present, but the selected-world criterion and nonmonotonic behavior differ from classical all-model consequence.[3]
Structural Tensions¶
Premise-expansion stability versus exception sensitivity. A monotone relation keeps a previously licensed conclusion after extra premises, making accumulation stable. A preferential relation can retract the conclusion when new exception information changes preferred worlds, gaining sensitivity at the cost of that stability. Both behaviors cannot be required of the same unrestricted premise expansion. Diagnostic: Should learning an exception be able to defeat an earlier conclusion while leaving the old premises intact?[3]
Inspectable derivation versus full chosen semantic reach. Restricting a calculus to a manageable stock of rules makes each derivation checkable but may leave some selected semantic consequences underivable; adding rules can improve reach only if their soundness is established against the intended models. The tension is not a theorem that completeness is impossible—some matched systems have it—but a design pressure until a particular bridge is proved. Diagnostic: For this exact calculus/model pairing, which soundness and completeness directions are established, and what consequence claims remain unmatched?[1][2][3]
Structural–Framed Character¶
Evaluative weight. “Consequence” is a formal licensing judgment, not by itself an evaluation that a conclusion is useful or morally acceptable. Choosing a logic for a task can be evaluative, but membership in its relation follows its declared criterion.[1][3]
Human-practice dependence. Humans select languages, rules, admissible models and sometimes preference orderings. Once fixed, those choices determine a relation that can be checked independently of an individual reasoner's thought process. This separates the formal structure from live prime Deductive Reasoning's cognitive aspect.[2][3]
Institutional origin. Tarski, Gentzen and KLM belong to distinct scholarly programs, not a single institutional rulebook. Their variants are source-supported mathematical-logical constructions, not policy-defined entitlements.[1][2][3]
Vocabulary travel. “Entails” and “follows from” travel into ordinary language, but a formal consequence claim must specify the language and criterion. The casual words are not automatically safe catalog aliases because they also have broader uses; “logical implication” may denote an object-language connective.[1][3]
Import versus recognition. In a new logical system one must specify premises, conclusions and a licensing rule, not merely recognize everyday persuasion. The portable relation skeleton is already live prime Relation; the contentful formula/model/proof apparatus stays in logic.[4][2]
Its character: structural within a formal-logical frame, with little intrinsic evaluative or institutional content; it is domain-specific because the exact premise–formula licensing identity depends on a declared logic even though the more general relation skeleton is prime.[4][1][3]
Structural Core vs. Domain Accent¶
The core is a typed relation between a collection of formal premises and a conclusion, with a logic-relative membership criterion. Classical all-model preservation, derivation in a named calculus and preferential normal-world selection are different ways to determine such a relation, not unqualified synonyms. Soundness/completeness theorems may connect specific determinations but do not constitute the generic relation.[1][2][3]
The cross-domain outer skeleton—relata plus a membership rule—is already live prime Relation, the proposed parent. The formula language, logical versus nonlogical vocabulary, assumptions, semantic models or proof rules and consequence status are constitutive logical structure, not detachable verbal accent. A future prime about licensed conclusions in nonlogical settings would need separate proof of transfer and identity; this entry does not assert one.[4][1]
Instantiates / Related Primes¶
This entry is a kind of Relation. Logical consequence is a formal relation between a premise collection and a conclusion.
Relationships to Other Abstractions¶
Current abstraction Logical Consequence Domain-specific
Parents (1) — more general patterns this builds on
-
Logical Consequence is a kind of Relation Prime
Logical consequence is a formal relation between a premise collection and a conclusion.Live Relation specifies relata and a rule for which tuples stand together. Logical consequence relates premise collections to conclusion formulas using an explicitly selected logic's semantic or derivational licensing criterion. Those formal-language and logical criteria strictly specialize Relation.
Hierarchy path (1) — routes to 1 parentless root
- Logical Consequence → Relation
Neighborhood in Abstraction Space¶
Logical Consequence sits in a moderately populated region (43rd percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Logical Semantics & Many-Valued Systems (11 abstractions)
Nearest neighbors
- Formal Theory — 0.87
- Peirce's Law — 0.87
- Sequent — 0.87
- Propositional logic — 0.87
- Lindström quantifier — 0.86
Computed from structural-signature embeddings · 2026-10-08
Not to Be Confused With¶
Model-theoretic consequence is the semantic determination using models and is a narrower redirected candidate sense, not automatic coverage of the whole identity. Logical implication can denote a connective \(A\to B\) inside the language. Consequence relation and entailment may be used broadly or technically and remain proposed lexical surfaces pending collision review. Follows from and logical conclusion are context-dependent phrases, not accepted aliases solely because Wikipedia redirected them. Monotonicity of entailment is a property some consequence relations have and KLM-style relations may lack.[1][2][3]
References¶
[1] A. Tarski, “On the Concept of Logical Consequence”, original 1936 essay in English translation, printed pp.410–420, especially pp.410–413 and 416–419. Scan inspected 2026-10-01; OCR is poor in its central pages and exact production quotations should be checked against the scan. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w ↩x ↩y
[2] G. Gentzen, “Investigations into Logical Deduction”, English translation/reprint, PDF pp.2–5, printed pp.290–293, §§2.3 and 3.1–3.2, inspected 2026-10-01. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u
[3] S. Kraus, D. Lehmann and M. Magidor, “Nonmonotonic Reasoning, Preferential Models and Cumulative Logics”, Artificial Intelligence 44 (1990), author-hosted copy, abstract and §§1.1–1.3, inspected 2026-10-01. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v ↩w
[4] Encyclopedia of Abstractions, live prime Relation, Core Idea and Structural Signature, inspected 2026-10-01. registry ↩a ↩b ↩c ↩d