Documentation

LeanPool.PointwiseComposition.FailureOfComposition.PiOneDefinitions

Supporting results for pointwise provable equality.

Definitions for the Pi-one completeness characterization.

source
def PointwiseComposition.FailureOfComposition.PiOneCharacterization.PiOneComplete (T : FFL.FirstOrder.ArithmeticTheory) :
Prop

Every true arithmetical Pi-one sentence is provable in T.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def PointwiseComposition.FailureOfComposition.PiOneCharacterization.Extensional (F G : ProofSearch.Graph) :
    Prop

    Equality of the graphs on standard natural-number inputs and outputs.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.PiOneCharacterization.RightCompatible (T : FFL.FirstOrder.ArithmeticTheory) :
      Prop

      Right composition replaces the outer graph and fixes the inner graph.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def PointwiseComposition.FailureOfComposition.PiOneCharacterization.CompositionCongruence (T : FFL.FirstOrder.ArithmeticTheory) :
        Prop

        The pointwise equivalence is preserved by composition in both arguments.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def PointwiseComposition.FailureOfComposition.PiOneCharacterization.AgreesWithExtensional (T : FFL.FirstOrder.ArithmeticTheory) :
          Prop

          Pointwise provability agrees with standard equality on functional graphs.

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