-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
5 changed files
with
766 additions
and
729 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
111 changes: 111 additions & 0 deletions
111
Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,111 @@ | ||
| import Arithmetization.ISigmaOne.Metamath.Formula.Basic | ||
| import Arithmetization.ISigmaOne.Metamath.Term.Functions | ||
|
|
||
| noncomputable section | ||
|
|
||
| namespace LO.Arith | ||
|
|
||
| open FirstOrder FirstOrder.Arith | ||
|
|
||
| variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] | ||
|
|
||
| variable {L : Arith.Language V} {pL : LDef} [Arith.Language.Defined L pL] | ||
|
|
||
| namespace Negation | ||
|
|
||
| def blueprint (pL : LDef) : Language.UformulaRec.Blueprint pL 0 where | ||
| rel := .mkSigma “y n k R v | !qqNRelDef y n k R v” (by simp) | ||
| nrel := .mkSigma “y n k R v | !qqRelDef y n k R v” (by simp) | ||
| verum := .mkSigma “y n | !qqFalsumDef y n” (by simp) | ||
| falsum := .mkSigma “y n | !qqVerumDef y n” (by simp) | ||
| and := .mkSigma “y n p₁ p₂ y₁ y₂ | !qqOrDef y n y₁ y₂” (by simp) | ||
| or := .mkSigma “y n p₁ p₂ y₁ y₂ | !qqAndDef y n y₁ y₂” (by simp) | ||
| all := .mkSigma “y n p₁ y₁ | !qqExDef y n y₁” (by simp) | ||
| ex := .mkSigma “y n p₁ y₁ | !qqAllDef y n y₁” (by simp) | ||
|
|
||
| variable (L) | ||
|
|
||
| def construction : Language.UformulaRec.Construction V L (blueprint pL) where | ||
| rel {_} := fun n k R v ↦ ^nrel n k R v | ||
| nrel {_} := fun n k R v ↦ ^rel n k R v | ||
| verum {_} := fun n ↦ ^⊥[n] | ||
| falsum {_} := fun n ↦ ^⊤[n] | ||
| and {_} := fun n _ _ y₁ y₂ ↦ y₁ ^⋎[n] y₂ | ||
| or {_} := fun n _ _ y₁ y₂ ↦ y₁ ^⋏[n] y₂ | ||
| all {_} := fun n _ y₁ ↦ ^∃[n] y₁ | ||
| ex {_} := fun n _ y₁ ↦ ^∀[n] y₁ | ||
| rel_defined := by intro v; simp [blueprint]; rfl | ||
| nrel_defined := by intro v; simp [blueprint]; rfl | ||
| verum_defined := by intro v; simp [blueprint] | ||
| falsum_defined := by intro v; simp [blueprint] | ||
| and_defined := by intro v; simp [blueprint]; rfl | ||
| or_defined := by intro v; simp [blueprint]; rfl | ||
| all_defined := by intro v; simp [blueprint]; rfl | ||
| ex_defined := by intro v; simp [blueprint]; rfl | ||
|
|
||
| end Negation | ||
|
|
||
| section negation | ||
|
|
||
| open Negation | ||
|
|
||
| variable (L) | ||
|
|
||
| def Language.neg (p : V) : V := (construction L).result ![] p | ||
|
|
||
| variable {L} | ||
|
|
||
| @[simp] lemma neg_rel {n k R v} (hR : L.Rel k R) (hv : L.TermSeq k n v) : | ||
| L.neg (^rel n k R v) = ^nrel n k R v := by simp [Language.neg, hR, hv, construction] | ||
|
|
||
| @[simp] lemma neg_nrel {n k R v} (hR : L.Rel k R) (hv : L.TermSeq k n v) : | ||
| L.neg (^nrel n k R v) = ^rel n k R v := by simp [Language.neg, hR, hv, construction] | ||
|
|
||
| @[simp] lemma neg_verum (n) : | ||
| L.neg ^⊤[n] = ^⊥[n] := by simp [Language.neg, construction] | ||
|
|
||
| @[simp] lemma neg_falsum (n) : | ||
| L.neg ^⊥[n] = ^⊤[n] := by simp [Language.neg, construction] | ||
|
|
||
| @[simp] lemma neg_and {n p q} (hp : L.Semiformula n p) (hq : L.Semiformula n q) : | ||
| L.neg (p ^⋏[n] q) = L.neg p ^⋎[n] L.neg q := by simp [Language.neg, hp, hq, construction] | ||
|
|
||
| @[simp] lemma neg_or {n p q} (hp : L.Semiformula n p) (hq : L.Semiformula n q) : | ||
| L.neg (p ^⋎[n] q) = L.neg p ^⋏[n] L.neg q := by simp [Language.neg, hp, hq, construction] | ||
|
|
||
| @[simp] lemma neg_all {n p} (hp : L.Semiformula (n + 1) p) : | ||
| L.neg (^∀[n] p) = ^∃[n] (L.neg p) := by simp [Language.neg, hp, construction] | ||
|
|
||
| @[simp] lemma neg_ex {n p} (hp : L.Semiformula (n + 1) p) : | ||
| L.neg (^∃[n] p) = ^∀[n] (L.neg p) := by simp [Language.neg, hp, construction] | ||
|
|
||
| section | ||
|
|
||
| def _root_.LO.FirstOrder.Arith.LDef.negDef (pL : LDef) : 𝚺₁-Semisentence 2 := (blueprint pL).result | ||
|
|
||
| variable (L) | ||
|
|
||
| lemma neg_defined : 𝚺₁-Function₁ L.neg via pL.negDef := (construction L).result_defined | ||
|
|
||
| @[simp] lemma neg_defined_iff (v : Fin 2 → V) : | ||
| Semiformula.Evalbm (L := ℒₒᵣ) V v pL.negDef ↔ v 0 = L.neg (v 1) := (neg_defined L).df.iff v | ||
|
|
||
| instance neg_definable : 𝚺₁-Function₁ L.neg := | ||
| Defined.to_definable _ (neg_defined L) | ||
|
|
||
| @[simp, definability] instance neg_definable' (Γ) : (Γ, m + 1)-Function₁ L.neg := | ||
| .of_sigmaOne (neg_definable L) _ _ | ||
|
|
||
| end | ||
|
|
||
| end negation | ||
|
|
||
| section substs | ||
|
|
||
|
|
||
|
|
||
| end substs | ||
|
|
||
| end LO.Arith | ||
|
|
||
| end |
Oops, something went wrong.