Documentation

LeanPool.PointwiseComposition.FailureOfComposition.SigmaOneSemidecisionCore

Supporting results for pointwise provable equality.

Concrete zero-valued semidecision programs. The defining equivalences hold for every input vector in every model of PA.

source
def PointwiseComposition.FailureOfComposition.SigmaOneRealization.Semidecides {n : ℕ} (φ : FFL.FirstOrder.ArithmeticSemisentence n) (c : Nat.Partrec.Code) :
Prop

A program accepts exactly the satisfying input vectors and returns zero.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.verum_semidecides (n : ℕ) :
    Semidecides ⊤ Nat.Partrec.Code.zero

    The zero program accepts every vector.

    source
    theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.falsum_semidecides (n : ℕ) :
    Semidecides ⊥ Nat.Partrec.Code.succ.rfind'

    Searching for a zero of successor accepts no vector.

    source
    def PointwiseComposition.FailureOfComposition.SigmaOneRealization.andProgram (c d : Nat.Partrec.Code) :
    Nat.Partrec.Code

    Evaluate both children and discard their outputs.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.SigmaOneRealization.and_semidecides {n : ℕ} {φ ψ : FFL.FirstOrder.ArithmeticSemisentence n} {c d : Nat.Partrec.Code} (hφ : Semidecides φ c) (hψ : Semidecides ψ d) :
      Semidecides (φ ⋏ ψ) (andProgram c d)

      Pairing the two computations gives conjunction semidecision.