Supporting results for pointwise provable equality.

Arithmetic terms and atomic formulas compiled to arithmetic programs. Evaluation is proved in arbitrary arithmetic structures for terms and positive atoms, and in arbitrary models of PA⁻ for their Boolean complements.

def PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.termCode {n : ℕ} : FFL.FirstOrder.ArithmeticSemiterm Empty n → Nat.ArithPart₁.Code n

Compilation of arithmetic terms with no free variables.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.termCode (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar i) = PointwiseComposition.Nat.ArithPart₁.Code.proj i

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.termCode_eval {M : Type u_1} [FFL.ORingStructure M] {n : ℕ} (t : FFL.FirstOrder.ArithmeticSemiterm Empty n) (y : M) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code (termCode t)) ↔ y = FFL.FirstOrder.Semiterm.valb v t

The compiled term returns exactly its semantic value.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.termCode_total {M : Type u_1} [FFL.ORingStructure M] {n : ℕ} (t : FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code (termCode t))

Term programs terminate at every internal input tuple.

def PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.BoolValue {M : Type u_1} [FFL.ORingStructure M] (P : Prop) (y : M) : Prop

Boolean programs return 1 for truth and 0 for falsehood.

Equations

• PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.BoolValue P y = (P ∧ y = 1 ∨ ¬P ∧ y = 0)

def PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.atomCode {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) : (Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) → Nat.ArithPart₁.Code n

Boolean compilation of an equality or strict-order atom.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.negAtomCode {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) : Nat.ArithPart₁.Code n

Boolean compilation of the negation of an arithmetic atom.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.atomCode_eval {M : Type u_1} [FFL.ORingStructure M] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (y : M) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code (atomCode r ts)) ↔ BoolValue ((FFL.FirstOrder.Semiformula.Evalb v) (FFL.FirstOrder.Semiformula.rel r ts)) y

Positive atomic formulas have total Boolean programs with the exact internal semantics of the original formula.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.bool_total {M : Type u_1} [FFL.ORingStructure M] {n : ℕ} (c : Nat.ArithPart₁.Code n) (v : Fin n → M) (P : Prop) (hc : ∀ (y : M), (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code c) ↔ BoolValue P y) : ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code c)

An exact Boolean specification always supplies a value.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.atomCode_total {M : Type u_1} [FFL.ORingStructure M] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code (atomCode r ts))

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.bool_inverse_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n : ℕ} (c : Nat.ArithPart₁.Code n) (v : Fin n → M) (P : Prop) (hc : ∀ (y : M), (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code c) ↔ BoolValue P y) (z : M) : (FFL.FirstOrder.Semiformula.Evalb (z :> v)) (FFL.FirstOrder.Arithmetic.code (CategoricalRiceShapiro.ArithmeticCode.codeInv c)) ↔ BoolValue (¬P) z

Arithmetic inversion exchanges the two Boolean values.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.negAtomCode_eval {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (y : M) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code (negAtomCode r ts)) ↔ BoolValue ((FFL.FirstOrder.Semiformula.Evalb v) (FFL.FirstOrder.Semiformula.nrel r ts)) y

Negated atomic formulas have the exact complementary Boolean graph.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.negAtomCode_total {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : ∃ (y : M), (FFL.FirstOrder.Semiformula.Evalb (y :> v)) (FFL.FirstOrder.Arithmetic.code (negAtomCode r ts))

@[simp]

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.boolValue_one {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] (P : Prop) : BoolValue P 1 ↔ P

A Boolean graph returns 1 exactly when its proposition holds.

@[simp]

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.boolValue_zero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] (P : Prop) : BoolValue P 0 ↔ ¬P

A Boolean graph returns 0 exactly when its proposition fails.

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.atomCode_one_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (1 :> v)) (FFL.FirstOrder.Arithmetic.code (atomCode r ts)) ↔ (FFL.FirstOrder.Semiformula.Evalb v) (FFL.FirstOrder.Semiformula.rel r ts)

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.atomCode_zero_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (0 :> v)) (FFL.FirstOrder.Arithmetic.code (atomCode r ts)) ↔ ¬(FFL.FirstOrder.Semiformula.Evalb v) (FFL.FirstOrder.Semiformula.rel r ts)

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.negAtomCode_one_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (1 :> v)) (FFL.FirstOrder.Arithmetic.code (negAtomCode r ts)) ↔ (FFL.FirstOrder.Semiformula.Evalb v) (FFL.FirstOrder.Semiformula.nrel r ts)

theorem PointwiseComposition.FailureOfComposition.ArithmeticFormulaAtoms.negAtomCode_zero_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻] {n k : ℕ} (r : FFL.FirstOrder.Language.ORing.Rel k) (ts : Fin k → FFL.FirstOrder.ArithmeticSemiterm Empty n) (v : Fin n → M) : (FFL.FirstOrder.Semiformula.Evalb (0 :> v)) (FFL.FirstOrder.Arithmetic.code (negAtomCode r ts)) ↔ ¬(FFL.FirstOrder.Semiformula.Evalb v) (FFL.FirstOrder.Semiformula.nrel r ts)