Keyboard graph navigation: press N for concepts or E for relations; use arrow keys, Home, and End to move; Enter selects; Shift plus Enter selects and centers; plus and minus zoom; zero fits; Escape clears the selection. Use the visible viewport buttons as alternatives to dragging, wheel, and pinch gestures.
Canonical static concept record
Open this concept in the interactive graphRead the Markdown equivalent
A finitary, syntactically specified collection of formulas, axioms, and inference rules defining formal derivability.
wp-formal-proof-systemopenlogic-incompletenessEach relation below ends at this concept.
This is an authored directed relation from the source endpoint to the target endpoint.
A formal proof system fixes axioms and inference rules for a language.
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.
openlogic-incompletenessThis is an authored directed relation from the source endpoint to the target endpoint.
Hilbert’s program motivated precise formal systems and metamathematical consistency proofs.
The source experiment, observation, anomaly, or problem materially motivated the development, revision, or acceptance of the target concept. Historical influence is not logical derivation; the edge detail states the documented role and avoids retrospective origin myths.
openlogic-incompletenessEach relation below starts at this concept.
This is an authored directed relation from the source endpoint to the target endpoint.
Consistency requires that contradiction is not derivable.
Keep the existing data and select the subclass satisfying an additional law, existence condition, finiteness condition, or other property.
openlogic-incompletenessThis is an authored directed relation from the source endpoint to the target endpoint.
For an effectively presented formal system, a Gödel numbering adds a computable encoding of symbols, formulas, and finite proofs by natural numbers.
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.
godel-incompleteness-paperThis is an authored directed relation from the source endpoint to the target endpoint.
Supply an effectively axiomatized proof system with mechanically checkable finite proofs.
Feed several structures into a construction junction and impose compatibility between them.
openlogic-incompletenessgodel-incompleteness-paperThis is an authored directed relation from the source endpoint to the target endpoint.
Supply an effectively axiomatized proof system with mechanically checkable finite proofs.
Feed several structures into a construction junction and impose compatibility between them.
openlogic-incompletenessgodel-incompleteness-paperThis is an authored directed relation from the source endpoint to the target endpoint.
For an effectively axiomatized proof system with mechanically checkable finite proofs, the Gödel numbers of its theorems form a computably enumerable set.
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.
openlogic-incompletenessturing-computable-numbersThis is an authored directed relation from the source endpoint to the target endpoint.
Syntactic completeness requires a proof of each sentence or its negation.
Keep the existing data and select the subclass satisfying an additional law, existence condition, finiteness condition, or other property.
openlogic-incompleteness