Definition·D096
Logical consequence
A theory entails a formula when every structure that models the theory also models the formula.
For a language
,
, and
:
logically entails
, written
, for every L-structure
:
In words
A set of formulas logically entails a formula exactly when, for every structure, modeling the set forces modeling the formula too.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).
Remarks
The semantic notion of consequence, using only modeling - no proof or deduction system yet enters. This is one side of what soundness and Gödel's completeness theorem will eventually show coincides with *provable* consequence, once a deduction system is defined: soundness will say every provable consequence is a logical consequence (nothing false is provable), and completeness the converse (everything true in every model is provable).
is vacuously true whenever
has no models at all (vacuous implication) - in particular an inconsistent theory (one with no models) entails everything, the semantic mirror of ex falso.