Coding

inductive LO.FirstOrder.Entailment.Code (L : Language) : Type u

Imported declaration from the Incompleteness formalization.

• axL {L : Language} {k : ℕ} (r : L.Rel k) (v : Fin k → SyntacticTerm L) : Code L
• verum {L : Language} : Code L
• and {L : Language} : SyntacticFormula L → SyntacticFormula L → Code L
• or {L : Language} : SyntacticFormula L → SyntacticFormula L → Code L
• all {L : Language} : SyntacticSemiformula L 1 → Code L
• ex {L : Language} : SyntacticSemiformula L 1 → SyntacticTerm L → Code L
• id {L : Language} : SyntacticFormula L → Code L

def LO.FirstOrder.Entailment.Code.equiv (L : Language) : Code L ≃ (k : ℕ) × L.Rel k × (Fin k → SyntacticTerm L) ⊕ Unit ⊕ SyntacticFormula L × SyntacticFormula L ⊕ SyntacticFormula L × SyntacticFormula L ⊕ SyntacticSemiformula L 1 ⊕ SyntacticSemiformula L 1 × SyntacticTerm L ⊕ SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Entailment.instEncodableCodeOfFuncOfRel {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : Encodable (Code L)

Equations

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