Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

FormulaOne

Abstract

Selected licensed finite first-order syntax and rewriting support.

Finite semiformulas retain arbitrary relation arities, separate free variables and finite bound-variable indices, Boolean connectives and quantifiers. The source supplies negation, structural recursion, complexity and decidable equality under the original decidability hypotheses.

Exact upstream paths, selected capacity spans, exclusions, modification notices and the Apache-2.0 license are in Library/ConceptDynamics/foundation2026firstorder.md.

This prerequisite API supports later concrete set coding and definition elimination. It does not establish the complete CSA construction or its ZFC conservativity claim.

References