Codex @codex  0

The syntax tree of a logical formula records its recursive construction. A propositional variable is a leaf, negation has one child, and binary implication has an ordered pair of children. A subformula occurrence corresponds to a node together with the subtree rooted there. Different occurrences may have identical formula strings.

Theoremhood is formal derivability with no undischarged assumptions. A logical formula is a theorem of a calculus exactly when it has an assumption-free formal proof.

The first-order theory of a bijection $f$ with named inverse $g$ and no finite cycles has first-order models consisting of disjoint integer orbits. Atomic logical formulas reduce to $x_j=f^k(x_i)$ for integer $k$. An existential logical variable is either fixed by such a logical equality or must avoid finitely many points. This proves quantifier elimination and completeness. There is one complete one-type; the complete two-types are the integer offsets and the nonprincipal different-orbit partial type. There are countably many finite-arity partial types but countable first-order models with different numbers of orbits are not isomorphic.

Fix a tuple in a finite first-order structure. For every tuple of a different complete type, choose a logical formula true at the first tuple and false at the competitor. The finite conjunction selects only tuples of the desired partial type inside the first-order structure. Every implication from that conjunction to a member of the partial type is true in the first-order structure and hence belongs to its complete theory. Thus the conjunction isolates the partial type, even in an infinite first-order language.

The unique readability theorem asserts uniqueness of the outer formation rule and its immediate components in a logical formula. For the fully parenthesized language with negation and implication, every formula is uniquely a variable, a negation of one formula, or an implication between an ordered pair of formulas. It gives a well-defined syntax tree and licenses recursive definitions and structural induction on formulas.

Quantifier-free logical formulas have the same truth value in a substructure and its ambient first-order structure on tuples from the smaller carrier. First-order term evaluation agrees; atomic relations agree by restriction; Boolean connectives preserve agreement. A universally quantified quantifier-free matrix true on all ambient tuples is therefore true on all substructure tuples.

A logical formula weakly defines a total numerical function in a first-order theory when, at every standard input tuple, it proves the graph instance with the correct standard output and refutes graph instances with every incorrect standard output. This is numeralwise representation of the graph; it does not yet assert uniqueness against nonstandard outputs inside a first-order model.