Set_Operations_on_Primitive_Recursive_Relations

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilityprimitive-recursive-functionsproofwiki

Let $\RR_1 \subseteq N^k$ and $\RR_2 \subseteq N^k$ be $k$ -ary relations on $N^k$ . Let $\RR_1$ and $\RR_2$ be primitive recursive. Then the following are all primitive recursive relations $\TT = \neg \RR_1$ $\UU = \RR_1 \land \RR_2$ $\VV = \RR_1 \lor \RR_2$

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Set_Operations_on_Primitive_Recursive_Relations (R1 R2 : ℕ → ℕ → Prop) [DecidableRel R1] [DecidableRel R2] (hR1 : PrimrecRel R1) (hR2 : PrimrecRel R2) : PrimrecRel (fun a b => R1 a b ∧ R2 a b) ∧ PrimrecRel (fun a b => R1 a b ∨ R2 a b) ∧ PrimrecRel (fun a b => ¬R1 a b) := by sorry

Source

https://proofwiki.org/wiki/Set_Operations_on_Primitive_Recursive_Relations

View graph