Select any concept, construction junction, or annotated relation by pointer, touch, search, or keyboard.

Construction junctions are diamonds. They show where multiple structures must coexist on the same carrier and satisfy compatibility conditions.

Canonical static concept record

First-order theory

Open this concept in the interactive graph Read the Markdown equivalent

Summary

A set of first-order sentences in a fixed signature.

Record metadata

Canonical name: First-order theory
Concept ID: first_order_theory
Content version: 2.3.0
Primary field: Mathematics
Fields: Mathematics
Primary domain: Logic
Domains: Logic
Alternate terminology: No alternate terminology is currently authored for this record.

Carrier(s)

first-order signature $L$

Data

set $T$ of $L$ -sentences

Canonically induces

class of models $\operatorname{Mod}(T)$

Notes

A theory need not be deductively closed unless that convention is stated explicitly.

Concept sources

Wikipedia — Model theory — Model theory · expository · source ID wp-model-theory
nLab — First-order theory — First-order theory · mathematical reference · source ID nlab-first-order-theory
Open Logic Project — Models and Theories — Open Logic Project: Models and Theories · open textbook · source ID openlogic-model-theory

Incoming relations (arrows to this concept)

Each relation below ends at this concept.

First-order signature First-order theory

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: e_signature_theory
Relation type: Add data add-data
Direction: source → target
Endpoint roles: source: Builds toward; target: Built from
Authored annotation: choose a set of sentences

Authored explanation

Choose a set $T$ of sentences formed in the fixed signature $L$ .

How to interpret this relation type

Equip an existing carrier or structured object with additional chosen data, when such compatible data exists. Use a construction junction when several independently meaningful inputs must coexist on the same carrier or interact compatibly.

Relation sources

Wikipedia — Model theory — Model theory · expository · source ID wp-model-theory
Open Logic Project — Models and Theories — Open Logic Project: Models and Theories · open textbook · source ID openlogic-model-theory

Outgoing relations (arrows from this concept)

Each relation below starts at this concept.

First-order theory Formal proof system

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: story_first_order_theory_to_formal_proof_system_add_data
Relation type: Add data add-data
Direction: source → target
Endpoint roles: source: Builds toward; target: Built from
Authored annotation: specify effective derivations

Authored explanation

A formal proof system fixes axioms and inference rules for a language.

How to interpret this relation type

Relation sources

Open Logic Project — Incompleteness — Incompleteness · open textbook · source ID openlogic-incompleteness

First-order theory consistent first-order theory(construction junction)

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: first_order_theory_to_consistent_theory_junction
Relation type: Combine compatible structures combine-compatible
Direction: source → target
Endpoint roles: source: Builds toward; target: Built from
Authored annotation: first-order syntax and semantics

Authored explanation

Supply the first-order theory whose consistency and model existence are being considered.

How to interpret this relation type

Feed several structures into a construction junction and impose compatibility between them.

Relation sources

Wikipedia — Gödel's completeness theorem — Gödel's completeness theorem · encyclopedic reference · source ID wp-godel-completeness-theorem
nLab — completeness theorem — completeness theorem · mathematical reference · source ID nlab-completeness-theorem
Open Logic Project — Models and Theories — Open Logic Project: Models and Theories · open textbook · source ID openlogic-model-theory

First-order theory theory + structure satisfying it(construction junction)

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: j_model_of_theory__theory
Relation type: Combine compatible structures combine-compatible
Direction: source → target
Endpoint roles: source: Builds toward; target: Built from
Authored annotation: theory

Authored explanation

Supply the set of sentences $T$ .

How to interpret this relation type

Feed several structures into a construction junction and impose compatibility between them.

Relation sources

Wikipedia — Model theory — Model theory · expository · source ID wp-model-theory
Open Logic Project — Models and Theories — Open Logic Project: Models and Theories · open textbook · source ID openlogic-model-theory

First-order theory Semantic consequence

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: first_order_theory_to_semantic_consequence
Relation type: Canonical construction canonical-construction
Direction: source → target
Endpoint roles: source: Canonically constructs; target: Canonically constructed from
Authored annotation: take semantic closure

Authored explanation

Relative to the fixed language and its standard structures, a theory determines the sentences true in all of its models.

How to interpret this relation type

Apply a standard functorial or canonical construction whose output is not merely a reduct of the input and is not generally an equivalent presentation of the same object.

Relation sources

Wikipedia — Logical consequence — Logical consequence · encyclopedic reference · source ID wp-logical-consequence
nLab — sequent — sequent · mathematical reference · source ID nlab-sequent
Open Logic Project — Models and Theories — Open Logic Project: Models and Theories · open textbook · source ID openlogic-model-theory

First-order theory Zermelo–Fraenkel set theory (ZF)

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: first_order_theory_to_zf
Relation type: Classification classification
Direction: source → target
Endpoint roles: source: Has subtype; target: Classified as
Authored annotation: ZF theory

Authored explanation

ZF is a first-order theory in the language with membership as its only nonlogical relation.

How to interpret this relation type

The target is a member or subtype of the broader source class.

Relation sources

Wikipedia — Zermelo–Fraenkel set theory — Zermelo–Fraenkel set theory · encyclopedic reference · source ID wp-zf
Open Logic Project — Set Theory — Open Logic Project: Set Theory · open textbook source · source ID openlogic-set-theory

First-order theory Zermelo–Fraenkel set theory with Choice (ZFC)

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: first_order_theory_to_zfc
Relation type: Classification classification
Direction: source → target
Endpoint roles: source: Has subtype; target: Classified as
Authored annotation: ZFC theory

Authored explanation

ZFC is a first-order theory in the language of membership, presented by finitely many axioms together with axiom schemas.

How to interpret this relation type

The target is a member or subtype of the broader source class.

Relation sources

Wikipedia — Zermelo–Fraenkel set theory — Zermelo–Fraenkel set theory · encyclopedic reference · source ID wp-zf
Stanford Encyclopedia of Philosophy — Set Theory — Set Theory · scholarly reference · source ID sep-set-theory